adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

x64: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242) 

Apply "invert-fastpath" changes to x64 (ainvs, refine, partial crefine).
See main commit for arm for more context.
This commit is contained in:
Rafal Kolanski 2017-11-24 22:33:02 +11:00
parent 7b36283c70
commit 2f28bfeaec
19 changed files with 1418 additions and 759 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

61
proof/crefine/X64/Move.thy
View File

@ -117,5 +117,66 @@ lemma ksPSpace_update_eq_ExD:
\<Longrightarrow> \<exists>ps. s = t \<lparr> ksPSpace := ps \<rparr>"
by (erule exI)
lemma threadGet_wp'':
"\<lbrace>\<lambda>s. \<forall>v. obj_at' (\<lambda>tcb. f tcb = v) thread s \<longrightarrow> P v s\<rbrace> threadGet f thread \<lbrace>P\<rbrace>"
apply (rule hoare_pre)
apply (rule threadGet_wp)
apply (clarsimp simp: obj_at'_def)
done
lemma tcbSchedEnqueue_queued_queues_inv:
"\<lbrace>\<lambda>s. obj_at' tcbQueued t s \<and> P (ksReadyQueues s) \<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>"
unfolding tcbSchedEnqueue_def unless_def
apply (wpsimp simp: if_apply_def2 wp: threadGet_wp)
apply normalise_obj_at'
done
lemma addToBitmap_sets_L1Bitmap_same_dom:
"\<lbrace>\<lambda>s. p \<le> maxPriority \<and> d' = d \<rbrace> addToBitmap d' p
\<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrace>"
unfolding addToBitmap_def bitmap_fun_defs
apply wpsimp
apply (clarsimp simp: maxPriority_def numPriorities_def word_or_zero le_def
prioToL1Index_max[simplified wordRadix_def, simplified])
done
crunch ksReadyQueuesL1Bitmap[wp]: setQueue "\<lambda>s. P (ksReadyQueuesL1Bitmap s)"
lemma tcb_in_cur_domain'_def':
"tcb_in_cur_domain' t = (\<lambda>s. obj_at' (\<lambda>tcb. tcbDomain tcb = ksCurDomain s) t s)"
unfolding tcb_in_cur_domain'_def
by (auto simp: obj_at'_def)
lemma sts_running_ksReadyQueuesL1Bitmap[wp]:
"\<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
setThreadState Structures_H.thread_state.Running t
\<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace>"
unfolding setThreadState_def
apply wp
apply (rule hoare_pre_cont)
apply (wpsimp simp: if_apply_def2
wp: hoare_drop_imps hoare_vcg_disj_lift threadSet_tcbState_st_tcb_at')+
done
lemma sts_running_ksReadyQueuesL2Bitmap[wp]:
"\<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace>
setThreadState Structures_H.thread_state.Running t
\<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace>"
unfolding setThreadState_def
apply wp
apply (rule hoare_pre_cont)
apply (wpsimp simp: if_apply_def2
wp: hoare_drop_imps hoare_vcg_disj_lift threadSet_tcbState_st_tcb_at')+
done
lemma asUser_obj_at_not_queued[wp]:
"\<lbrace>obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) p\<rbrace> asUser t m \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) p\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp hoare_drop_imps | simp)+
done
lemma ko_at'_obj_at'_field:
"ko_at' ko (t s) s \<Longrightarrow> obj_at' (\<lambda>ko'. f ko' = f ko) (t s) s"
by (erule obj_at'_weakenE, simp)
end

5
proof/crefine/X64/SR_lemmas_C.thy
View File

@ -2427,6 +2427,11 @@ lemma capTCBPtr_eq:
apply clarsimp
done
lemma rf_sr_sched_action_relation:
"(s, s') \<in> rf_sr
\<Longrightarrow> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))"
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
end
end

4
proof/crefine/X64/StateRelation_C.thy
View File

@ -785,9 +785,9 @@ definition
\<Rightarrow> ((domain \<times> nat) \<Rightarrow> machine_word) \<Rightarrow> bool"
where
"cbitmap_L2_relation cbitmap2 abitmap2 \<equiv>
\<forall>d i. ((d \<le> maxDomain \<and> i \<le> numPriorities div wordBits)
\<forall>d i. ((d \<le> maxDomain \<and> i < l2BitmapSize)
\<longrightarrow> cbitmap2.[unat d].[i] = abitmap2 (d, i)) \<and>
((\<not> (d \<le> maxDomain \<and> i \<le> numPriorities div wordBits))
((\<not> (d \<le> maxDomain \<and> i < l2BitmapSize))
\<longrightarrow> abitmap2 (d, i) = 0)"
end (* interpretation Arch . (*FIXME: arch_split*) *)

2
proof/invariant-abstract/X64/ArchDetSchedAux_AI.thy
View File

@ -46,8 +46,6 @@ crunch idle_thread[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s. P (idl
wrap_ext_det_ext_ext_def mapM_x_defsym
ignore: freeMemory retype_region_ext)
crunch inv[wp]: get_tcb_queue, ethread_get "\<lambda>s. P s"
lemma tcb_sched_action_valid_idle_etcb:
"\<lbrace>valid_idle_etcb\<rbrace>
tcb_sched_action foo thread

3
proof/invariant-abstract/X64/ArchDetSchedSchedule_AI.thy
View File

@ -326,7 +326,8 @@ global_interpretation DetSchedSchedule_AI?: DetSchedSchedule_AI
context Arch begin global_naming X64
lemma handle_hyp_fault_valid_sched[wp, DetSchedSchedule_AI_assms]:
"\<lbrace>valid_sched and invs and st_tcb_at active t and not_queued t and scheduler_act_not t\<rbrace>
"\<lbrace>valid_sched and invs and st_tcb_at active t and not_queued t and scheduler_act_not t
and (ct_active or ct_idle)\<rbrace>
handle_hypervisor_fault t fault \<lbrace>\<lambda>_. valid_sched\<rbrace>"
by (cases fault; wpsimp wp: handle_fault_valid_sched simp: valid_fault_def)

17
proof/refine/X64/DomainTime_R.thy
View File

@ -94,7 +94,7 @@ crunch ksDomSchedule_inv[wp]: performInvocation "\<lambda>s. P (ksDomSchedule s)
simp: unless_def crunch_simps filterM_mapM)
crunch ksDomSchedule_inv[wp]: schedule "\<lambda>s. P (ksDomSchedule s)"
(ignore: setNextPC threadSet simp:crunch_simps wp:findM_inv)
(ignore: setNextPC threadSet simp:crunch_simps bitmap_fun_defs wp:findM_inv hoare_drop_imps)
crunch ksDomSchedule_inv[wp]: activateThread "\<lambda>s. P (ksDomSchedule s)"
@ -108,10 +108,15 @@ lemma handleRecv_ksDomSchedule_inv[wp]:
by (rule hoare_pre)
(wp hoare_drop_imps | simp add: crunch_simps | wpc)+
context
notes if_cong [cong]
begin
crunch ksDomSchedule_inv[wp]: handleEvent "\<lambda>s. P (ksDomSchedule s)"
(wp: hoare_drop_imps hv_inv' syscall_valid' throwError_wp withoutPreemption_lift
simp: runErrorT_def
ignore: setThreadState)
end
lemma callKernel_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> callKernel e \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>"
@ -127,7 +132,7 @@ crunch ksDomainTime[wp]: setExtraBadge, cteInsert "\<lambda>s. P (ksDomainTime s
crunch ksDomainTime[wp]: transferCapsToSlots "\<lambda>s. P (ksDomainTime s)"
crunch ksDomainTime[wp]: setupCallerCap, switchIfRequiredTo, doIPCTransfer, attemptSwitchTo "\<lambda>s. P (ksDomainTime s)"
crunch ksDomainTime[wp]: setupCallerCap, doIPCTransfer, possibleSwitchTo "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: zipWithM_x_mapM ignore: constOnFailure)
crunch ksDomainTime_inv[wp]: setEndpoint, setNotification, storePTE, storePDE, storePDPTE, storePML4E
@ -294,11 +299,11 @@ lemma schedule_domain_time_left':
(\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<rbrace>
ThreadDecls_H.schedule
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
unfolding schedule_def
unfolding schedule_def scheduleChooseNewThread_def
supply word_neq_0_conv[simp]
apply (wp | wpc)+
apply (rule_tac Q="\<lambda>_. valid_domain_list'" in hoare_post_imp, clarsimp)
apply (wp | clarsimp)+
apply (rule_tac Q="\<lambda>_. valid_domain_list'" in hoare_post_imp, clarsimp)
apply (wp | clarsimp | wp_once hoare_drop_imps)+
done
lemma handleEvent_ksDomainTime_inv:
@ -308,7 +313,7 @@ lemma handleEvent_ksDomainTime_inv:
apply (cases e, simp_all)
apply (rename_tac syscall)
apply (case_tac syscall, simp_all add: handle_send_def)
apply (wp hv_inv'|simp add: handleEvent_def |wpc)+
apply (wp hv_inv'|simp add: handleEvent_def cong: if_cong|wpc)+
done
lemma callKernel_domain_time_left:

12
proof/refine/X64/EmptyFail.thy
View File

@ -128,5 +128,17 @@ lemma empty_fail_getThreadState[iff]:
declare empty_fail_stateAssert [wp]
declare setRegister_empty_fail [intro!, simp]
lemma empty_fail_getSchedulerAction [intro!, wp, simp]:
"empty_fail getSchedulerAction"
by (simp add: getSchedulerAction_def getObject_def split_def)
lemma empty_fail_scheduleSwitchThreadFastfail [intro!, wp, simp]:
"empty_fail (scheduleSwitchThreadFastfail a b c d)"
by (simp add: scheduleSwitchThreadFastfail_def split: if_splits)
lemma empty_fail_curDomain [intro!, wp, simp]:
"empty_fail curDomain"
by (simp add: curDomain_def)
end
end

6
proof/refine/X64/EmptyFail_H.thy
View File

@ -181,7 +181,7 @@ lemma ignoreFailure_empty_fail[intro!, wp, simp]:
"empty_fail x \<Longrightarrow> empty_fail (ignoreFailure x)"
by (simp add: ignoreFailure_def empty_fail_catch)
crunch (empty_fail) empty_fail[intro!, wp, simp]: cancelIPC, setThreadState, tcbSchedDequeue, setupReplyMaster, isBlocked, switchIfRequiredTo
crunch (empty_fail) empty_fail[intro!, wp, simp]: cancelIPC, setThreadState, tcbSchedDequeue, setupReplyMaster, isBlocked, possibleSwitchTo, tcbSchedAppend
(simp: Let_def)
crunch (empty_fail) "_H_empty_fail": "ThreadDecls_H.suspend"
@ -289,12 +289,12 @@ crunch (empty_fail) empty_fail[intro!, wp, simp]: chooseThread
crunch (empty_fail) empty_fail[intro!, wp, simp]: getDomainTime
crunch (empty_fail) empty_fail[intro!, wp, simp]: nextDomain
crunch (empty_fail) empty_fail[intro!, wp, simp]: scheduleSwitchThreadFastfail, isHighestPrio
lemma ThreadDecls_H_schedule_empty_fail[intro!, wp, simp]:
"empty_fail schedule"
apply (simp add: schedule_def)
apply (simp | wp | wpc)+
apply (clarsimp simp: scheduleChooseNewThread_def split: if_split | wp | wpc)+
done
crunch (empty_fail) empty_fail[wp, simp]: setMRs, setMessageInfo

61
proof/refine/X64/Interrupt_R.thy
View File

@ -672,14 +672,6 @@ lemma tcbSchedAppend_valid_objs':
apply (clarsimp simp add:obj_at'_def typ_at'_def)
done
lemma tcbSchedAppend_sch_act_wf:
"\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> tcbSchedAppend thread
\<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add:tcbSchedAppend_def bitmap_fun_defs)
apply (wp hoare_unless_wp setQueue_sch_act threadGet_wp|simp)+
apply (fastforce simp:typ_at'_def obj_at'_def)
done
lemma valid_tcb_tcbTimeSlice_update[simp]:
"valid_tcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) s = valid_tcb' tcb s"
by (simp add:valid_tcb'_def tcb_cte_cases_def)
@ -1027,16 +1019,18 @@ lemma rescheduleRequired_valid_irq_node'[wp]:
apply simp
done
lemma rescheduleRequired_cur_tcb'[wp]:
"\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> rescheduleRequired
\<lbrace>\<lambda>rv s. cur_tcb' s \<rbrace>"
apply (simp add:rescheduleRequired_def)
apply wp
apply (simp add:cur_tcb'_def)
apply (wp|wpc)+
apply simp
done
(* catch up tcbSchedAppend to tcbSchedEnqueue, which has these from crunches on possibleSwitchTo *)
crunch ifunsafe[wp]: tcbSchedAppend if_unsafe_then_cap'
crunch irq_handlers'[wp]: tcbSchedAppend valid_irq_handlers'
(simp: unless_def tcb_cte_cases_def wp: crunch_wps)
crunch irq_states'[wp]: tcbSchedAppend valid_irq_states'
crunch irqs_masked'[wp]: tcbSchedAppend irqs_masked'
(simp: unless_def wp: crunch_wps)
crunch ct[wp]: tcbSchedAppend cur_tcb'
(wp: cur_tcb_lift crunch_wps)
crunch cur_tcb'[wp]: tcbSchedAppend cur_tcb'
(simp: unless_def wp: crunch_wps)
lemma timerTick_invs'[wp]:
"\<lbrace>invs'\<rbrace> timerTick \<lbrace>\<lambda>rv. invs'\<rbrace>"
@ -1046,26 +1040,23 @@ lemma timerTick_invs'[wp]:
tcbSchedAppend_invs_but_ct_not_inQ'
| simp add: tcb_cte_cases_def numDomains_def invs_ChooseNewThread
| wpc)+
apply (simp add:decDomainTime_def)
apply wp
apply simp
apply (rule_tac Q="\<lambda>rv. invs'"
in hoare_post_imp)
apply (simp add:decDomainTime_def)
apply wp
apply simp
apply (rule_tac Q="\<lambda>rv. invs'" in hoare_post_imp)
apply (clarsimp simp add:invs'_def valid_state'_def)
apply (wp threadGet_wp threadSet_cur threadSet_timeslice_invs
rescheduleRequired_all_invs_but_ct_not_inQ
hoare_vcg_imp_lift threadSet_ct_idle_or_in_cur_domain'
|wpc | simp)+
apply wpc
apply (wp add: threadGet_wp threadSet_cur threadSet_timeslice_invs
rescheduleRequired_all_invs_but_ct_not_inQ
hoare_vcg_imp_lift threadSet_ct_idle_or_in_cur_domain'
del: tcbSchedAppend_sch_act_wf)+
apply (rule hoare_strengthen_post[OF tcbSchedAppend_invs_but_ct_not_inQ'])
apply (clarsimp simp:valid_pspace'_def sch_act_wf_weak)
apply wp
apply (wp threadSet_pred_tcb_no_state threadSet_tcbDomain_triv
threadSet_valid_objs' threadSet_timeslice_invs
| simp)+
apply (wp threadGet_wp)
apply (wp gts_wp')+
apply (clarsimp simp:invs'_def st_tcb_at'_def obj_at'_def
valid_state'_def numDomains_def)
apply (wpsimp simp: valid_pspace'_def sch_act_wf_weak)+
apply (wpsimp wp: threadSet_pred_tcb_no_state threadSet_tcbDomain_triv
threadSet_valid_objs' threadSet_timeslice_invs)+
apply (wp threadGet_wp)
apply (wp gts_wp')+
apply (clarsimp simp: invs'_def st_tcb_at'_def obj_at'_def valid_state'_def numDomains_def)
done
lemma resetTimer_invs'[wp]:

112
proof/refine/X64/Invariants_H.thy
View File

@ -897,10 +897,12 @@ where
definition
(* for given domain and priority, the scheduler bitmap indicates a thread is in the queue *)
(* second level of the bitmap is stored in reverse for better cache locality in common case *)
bitmapQ :: "domain \<Rightarrow> priority \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"bitmapQ d p s \<equiv> ksReadyQueuesL1Bitmap s d !! prioToL1Index p
\<and> ksReadyQueuesL2Bitmap s (d, prioToL1Index p) !! unat (p && mask wordRadix)"
\<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p))
!! unat (p && mask wordRadix)"
definition
valid_queues_no_bitmap :: "kernel_state \<Rightarrow> bool"
@ -917,7 +919,8 @@ definition
bitmapQ_no_L2_orphans :: "kernel_state \<Rightarrow> bool"
where
"bitmapQ_no_L2_orphans \<equiv> \<lambda>s.
\<forall>d i j. ksReadyQueuesL2Bitmap s (d, i) !! j \<longrightarrow> (ksReadyQueuesL1Bitmap s d !! i)"
\<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize
\<longrightarrow> (ksReadyQueuesL1Bitmap s d !! i)"
definition
(* If the scheduler finds a set bit in L1 of the bitmap, it must find some bit set in L2
@ -929,8 +932,8 @@ definition
bitmapQ_no_L1_orphans :: "kernel_state \<Rightarrow> bool"
where
"bitmapQ_no_L1_orphans \<equiv> \<lambda>s.
\<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, i) \<noteq> 0 \<and>
i < numPriorities div wordBits"
\<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and>
i < l2BitmapSize"
definition
valid_bitmapQ :: "kernel_state \<Rightarrow> bool"
@ -1470,6 +1473,9 @@ lemma ntfn_splits[split]:
section "Lemmas"
schematic_goal wordBits_def': "wordBits = numeral ?n" (* arch-specific consequence *)
by (simp add: wordBits_def word_size)
lemma valid_bound_ntfn'_None[simp]:
"valid_bound_ntfn' None = \<top>"
by (auto simp: valid_bound_ntfn'_def)
@ -3447,6 +3453,43 @@ lemma obj_at'_and:
"obj_at' (P and P') t s = (obj_at' P t s \<and> obj_at' P' t s)"
by (rule iffI, (clarsimp simp: obj_at'_def)+)
lemma obj_at'_activatable_st_tcb_at':
"obj_at' (activatable' \<circ> tcbState) t = st_tcb_at' activatable' t"
by (rule ext, clarsimp simp: st_tcb_at'_def)
lemma st_tcb_at'_runnable_is_activatable:
"st_tcb_at' runnable' t s \<Longrightarrow> st_tcb_at' activatable' t s"
by (simp add: st_tcb_at'_def)
(fastforce elim: obj_at'_weakenE)
lemma tcb_at'_has_tcbPriority:
"tcb_at' t s \<Longrightarrow> \<exists>p. obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s"
by (clarsimp simp add: obj_at'_def)
lemma pred_tcb_at'_Not:
"pred_tcb_at' f (Not o P) t s = (tcb_at' t s \<and> \<not> pred_tcb_at' f P t s)"
by (auto simp: pred_tcb_at'_def obj_at'_def)
lemma obj_at'_conj_distrib:
"obj_at' (\<lambda>ko. P ko \<and> Q ko) p s \<Longrightarrow> obj_at' P p s \<and> obj_at' Q p s"
by (auto simp: obj_at'_def)
lemma not_obj_at'_strengthen:
"obj_at' (Not \<circ> P) p s \<Longrightarrow> \<not> obj_at' P p s"
by (clarsimp simp: obj_at'_def)
lemma not_pred_tcb_at'_strengthen:
"pred_tcb_at' f (Not \<circ> P) p s \<Longrightarrow> \<not> pred_tcb_at' f P p s"
by (clarsimp simp: pred_tcb_at'_def obj_at'_def)
lemma obj_at'_ko_at'_prop:
"ko_at' ko t s \<Longrightarrow> obj_at' P t s = P ko"
by (drule obj_at_ko_at', clarsimp simp: obj_at'_def)
lemma idle_tcb_at'_split:
"idle_tcb_at' (\<lambda>p. P (fst p) \<and> Q (snd p)) t s \<Longrightarrow> st_tcb_at' P t s \<and> bound_tcb_at' Q t s"
by (clarsimp simp: pred_tcb_at'_def dest!: obj_at'_conj_distrib)
lemma valid_queues_no_bitmap_def':
"valid_queues_no_bitmap =
(\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)).
@ -3554,10 +3597,38 @@ lemma invs_valid_global'[elim!]:
"invs' s \<Longrightarrow> valid_global_refs' s"
by (fastforce simp: invs'_def valid_state'_def)
lemma invs_invs_no_cicd':
"invs' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s"
by (simp add: invs'_to_invs_no_cicd'_def)
lemma valid_queues_valid_bitmapQ:
"valid_queues s \<Longrightarrow> valid_bitmapQ s"
by (simp add: valid_queues_def)
lemma valid_queues_valid_queues_no_bitmap:
"valid_queues s \<Longrightarrow> valid_queues_no_bitmap s"
by (simp add: valid_queues_def)
lemma valid_queues_bitmapQ_no_L1_orphans:
"valid_queues s \<Longrightarrow> bitmapQ_no_L1_orphans s"
by (simp add: valid_queues_def)
lemma invs'_bitmapQ_no_L1_orphans:
"invs' s \<Longrightarrow> bitmapQ_no_L1_orphans s"
by (drule invs_queues, simp add: valid_queues_def)
lemma invs_ksCurDomain_maxDomain' [elim!]:
"invs' s \<Longrightarrow> ksCurDomain s \<le> maxDomain"
by (simp add: invs'_def valid_state'_def)
lemma ksCurThread_active_not_idle':
"\<lbrakk> ct_active' s ; valid_idle' s \<rbrakk> \<Longrightarrow> ksCurThread s \<noteq> ksIdleThread s"
apply clarsimp
apply (clarsimp simp: ct_in_state'_def valid_idle'_def)
apply (drule idle_tcb_at'_split)
apply (clarsimp simp: pred_tcb_at'_def obj_at'_def)
done
lemma simple_st_tcb_at_state_refs_ofD':
"st_tcb_at' simple' t s \<Longrightarrow> bound_tcb_at' (\<lambda>x. tcb_bound_refs' x = state_refs_of' s t) t s"
by (fastforce simp: pred_tcb_at'_def obj_at'_def state_refs_of'_def
@ -3645,6 +3716,39 @@ lemma valid_bitmap_valid_bitmapQ_exceptI[intro]:
"valid_bitmapQ s \<Longrightarrow> valid_bitmapQ_except d p s"
unfolding valid_bitmapQ_except_def valid_bitmapQ_def
by simp
lemma mask_wordRadix_less_wordBits:
assumes sz: "wordRadix \<le> size w"
shows "unat ((w::'a::len word) && mask wordRadix) < wordBits"
proof -
note pow_num = semiring_numeral_class.power_numeral
{ assume "wordRadix = size w"
hence ?thesis
by (fastforce intro!: unat_lt2p[THEN order_less_le_trans]
simp: wordRadix_def wordBits_def' word_size)
} moreover {
assume "wordRadix < size w"
hence ?thesis unfolding wordRadix_def wordBits_def' mask_def
apply simp
apply (subst unat_less_helper, simp_all)
apply (rule word_and_le1[THEN order_le_less_trans])
apply (simp add: word_size bintrunc_mod2p)
apply (subst int_mod_eq', simp_all)
apply (rule order_le_less_trans[where y="2^wordRadix", simplified wordRadix_def], simp)
apply (simp del: pow_num)
apply (subst int_mod_eq', simp_all)
apply (rule order_le_less_trans[where y="2^wordRadix", simplified wordRadix_def], simp)
apply (simp del: pow_num)
done
}
ultimately show ?thesis using sz by fastforce
qed
lemma priority_mask_wordRadix_size:
"unat ((w::priority) && mask wordRadix) < wordBits"
by (rule mask_wordRadix_less_wordBits, simp add: wordRadix_def word_size)
end
(* The normalise_obj_at' tactic was designed to simplify situations similar to:
ko_at' ko p s \<Longrightarrow>

4
proof/refine/X64/IpcCancel_R.thy
View File

@ -1325,8 +1325,8 @@ definition
lemma removeFromBitmap_conceal_valid_inQ_queues[wp]:
"\<lbrace> valid_inQ_queues \<rbrace> removeFromBitmap_conceal d p q t \<lbrace> \<lambda>_. valid_inQ_queues \<rbrace>"
unfolding bitmap_fun_defs valid_inQ_queues_def removeFromBitmap_conceal_def
by wp clarsimp
unfolding valid_inQ_queues_def removeFromBitmap_conceal_def
by (wp|clarsimp simp: bitmap_fun_defs)+
lemma tcbSchedDequeue_valid_inQ_queues[wp]:
"\<lbrace>valid_inQ_queues\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>"

252
proof/refine/X64/Ipc_R.thy
View File

@ -2060,12 +2060,6 @@ crunch typ_at'[wp]: handleFaultReply "\<lambda>s. P (typ_at' T p s)"
lemmas hfr_typ_ats[wp] = typ_at_lifts [OF handleFaultReply_typ_at']
crunch tcb_at'[wp]: attemptSwitchTo "tcb_at' t"
(wp: crunch_wps)
crunch valid_pspace'[wp]: attemptSwitchTo valid_pspace'
(wp: crunch_wps)
crunch ct'[wp]: handleFaultReply "\<lambda>s. P (ksCurThread s)"
lemma doIPCTransfer_sch_act_simple [wp]:
@ -2075,17 +2069,14 @@ lemma doIPCTransfer_sch_act_simple [wp]:
lemma possibleSwitchTo_invs'[wp]:
"\<lbrace>invs' and st_tcb_at' runnable' t
and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
possibleSwitchTo t b \<lbrace>\<lambda>rv. invs'\<rbrace>"
possibleSwitchTo t \<lbrace>\<lambda>_. invs'\<rbrace>"
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (wp static_imp_wp ssa_invs' threadGet_wp | wpc | simp)+
apply (auto simp: obj_at'_def tcb_in_cur_domain'_def)
apply (wp tcbSchedEnqueue_invs' ssa_invs')
apply (rule hoare_post_imp[OF _ rescheduleRequired_sa_cnt])
apply (wpsimp wp: ssa_invs' threadGet_wp)+
apply (clarsimp dest!: obj_at_ko_at' simp: tcb_in_cur_domain'_def obj_at'_def)
done
crunch invs'[wp]: attemptSwitchTo "invs'"
crunch cte_wp_at'[wp]: attemptSwitchTo "cte_wp_at' P p"
(wp: crunch_wps)
crunch cur' [wp]: isFinalCapability "\<lambda>s. P (cur_tcb' s)"
(simp: crunch_simps unless_when
wp: crunch_wps getObject_inv loadObject_default_inv)
@ -2339,6 +2330,23 @@ crunch valid_objs'[wp]: handleFaultReply valid_objs'
lemma valid_tcb'_tcbFault_update[simp]: "\<And>tcb s. valid_tcb' tcb s \<Longrightarrow> valid_tcb' (tcbFault_update f tcb) s"
by (clarsimp simp: valid_tcb'_def tcb_cte_cases_def)
lemma restart_rewrite:
"(if rst then
do y \<leftarrow> setThreadState Structures_H.Restart receiver;
y \<leftarrow> possibleSwitchTo receiver;
return (Some receiver)
od
else
do y \<leftarrow> setThreadState Structures_H.Inactive receiver;
return None
od) =
do
setThreadState (if rst then Structures_H.Restart else Structures_H.Inactive) receiver;
when rst (possibleSwitchTo receiver);
return (if rst then Some receiver else None)
od"
by (simp add: when_def)
lemma do_reply_transfer_corres:
"corres dc
(einvs and tcb_at receiver and tcb_at sender
@ -2347,7 +2355,7 @@ lemma do_reply_transfer_corres:
and valid_pspace' and cte_at' (cte_map slot))
(do_reply_transfer sender receiver slot)
(doReplyTransfer sender receiver (cte_map slot))"
apply (simp add: do_reply_transfer_def doReplyTransfer_def)
apply (simp add: do_reply_transfer_def doReplyTransfer_def restart_rewrite cong: option.case_cong)
apply (rule corres_split' [OF _ _ gts_sp gts_sp'])
apply (rule corres_guard_imp)
apply (rule gts_corres, (clarsimp simp add: st_tcb_at_tcb_at)+)
@ -2381,9 +2389,10 @@ lemma do_reply_transfer_corres:
apply (rule corres_split [OF _ dit_corres])
apply (rule corres_split [OF _ cap_delete_one_corres])
apply (rule corres_split [OF _ sts_corres])
apply (rule attemptSwitchTo_corres)
apply (wp set_thread_state_runnable_valid_sched set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at' sts_st_tcb' sts_valid_queues sts_valid_objs' delete_one_tcbDomain_obj_at'
| simp add: valid_tcb_state'_def)+
apply (rule possibleSwitchTo_corres)
apply simp
apply (wp set_thread_state_runnable_valid_sched set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at' sts_st_tcb' sts_valid_queues sts_valid_objs' delete_one_tcbDomain_obj_at'
| simp add: valid_tcb_state'_def)+
apply (strengthen cte_wp_at_reply_cap_can_fast_finalise)
apply (wp hoare_vcg_conj_lift)
apply (rule hoare_strengthen_post [OF do_ipc_transfer_non_null_cte_wp_at])
@ -2408,6 +2417,7 @@ lemma do_reply_transfer_corres:
apply (clarsimp simp: invs_def valid_sched_def valid_sched_action_def)
apply (simp)
apply (auto simp: invs'_def valid_state'_def)[1]
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ cap_delete_one_corres])
apply (rule corres_split_mapr [OF _ get_mi_corres])
@ -2422,16 +2432,15 @@ lemma do_reply_transfer_corres:
and Invariants_H.valid_queues and valid_queues' and valid_objs'"
in corres_guard_imp)
apply (case_tac rvb, simp_all)[1]
apply (fold dc_def)
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ sts_corres])
apply (simp add: when_def)
apply (rule attemptSwitchTo_corres)
apply (wp static_imp_wp static_imp_conj_wp set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at'
sts_st_tcb' sts_valid_queues | simp | force simp: valid_sched_def valid_sched_action_def valid_tcb_state'_def)+
apply (fold dc_def, rule possibleSwitchTo_corres)
apply simp
apply (wp static_imp_wp static_imp_conj_wp set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at'
sts_st_tcb' sts_valid_queues | simp | force simp: valid_sched_def valid_sched_action_def valid_tcb_state'_def)+
apply (rule corres_guard_imp)
apply (rule sts_corres)
apply (simp_all)[20]
apply (rule sts_corres)
apply (simp_all)[20]
apply (clarsimp simp add: tcb_relation_def fault_rel_optionation_def
tcb_cap_cases_def tcb_cte_cases_def exst_same_def)+
apply (wp threadSet_cur weak_sch_act_wf_lift_linear threadSet_pred_tcb_no_state
@ -2582,11 +2591,11 @@ lemma setupCallerCap_weak_sch_act_from_sch_act:
apply (clarsimp simp: weak_sch_act_wf_def)
done
lemma attemptSwitchTo_weak_sch_act_wf[wp]:
lemma possibleSwitchTo_weak_sch_act_wf[wp]:
"\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s\<rbrace>
attemptSwitchTo t \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add: attemptSwitchTo_def possibleSwitchTo_def
setSchedulerAction_def threadGet_def curDomain_def)
possibleSwitchTo t \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add: possibleSwitchTo_def setSchedulerAction_def threadGet_def curDomain_def
bitmap_fun_defs)
apply (wp rescheduleRequired_weak_sch_act_wf
weak_sch_act_wf_lift_linear[where f="tcbSchedEnqueue t"]
getObject_tcb_wp static_imp_wp
@ -2597,7 +2606,7 @@ lemma attemptSwitchTo_weak_sch_act_wf[wp]:
lemmas transferCapsToSlots_pred_tcb_at' =
transferCapsToSlots_pres1 [OF cteInsert_pred_tcb_at']
crunch pred_tcb_at'[wp]: doIPCTransfer, attemptSwitchTo "pred_tcb_at' proj P t"
crunch pred_tcb_at'[wp]: doIPCTransfer, possibleSwitchTo "pred_tcb_at' proj P t"
(wp: mapM_wp' crunch_wps simp: zipWithM_x_mapM)
@ -2619,16 +2628,22 @@ lemma setSchedulerAction_ct_in_domain:
\<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>"
by (simp add:setSchedulerAction_def | wp)+
crunch ct_idle_or_in_cur_domain'[wp]: setupCallerCap, switchIfRequiredTo, doIPCTransfer, attemptSwitchTo ct_idle_or_in_cur_domain'
crunch ct_idle_or_in_cur_domain'[wp]: setupCallerCap, doIPCTransfer, possibleSwitchTo ct_idle_or_in_cur_domain'
(wp: crunch_wps setSchedulerAction_ct_in_domain simp: zipWithM_x_mapM)
crunch ksCurDomain[wp]: setupCallerCap, switchIfRequiredTo, doIPCTransfer, attemptSwitchTo "\<lambda>s. P (ksCurDomain s)"
crunch ksCurDomain[wp]: setupCallerCap, doIPCTransfer, possibleSwitchTo "\<lambda>s. P (ksCurDomain s)"
(wp: crunch_wps simp: zipWithM_x_mapM)
crunch ksDomSchedule[wp]: setupCallerCap, switchIfRequiredTo, doIPCTransfer, attemptSwitchTo "\<lambda>s. P (ksDomSchedule s)"
crunch ksDomSchedule[wp]: setupCallerCap, doIPCTransfer, possibleSwitchTo "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps simp: zipWithM_x_mapM)
crunch tcbDomain_obj_at'[wp]: doIPCTransfer "obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t"
(wp: crunch_wps constOnFailure_wp simp: crunch_simps)
crunch tcb_at'[wp]: possibleSwitchTo "tcb_at' t"
(wp: crunch_wps)
crunch valid_pspace'[wp]: possibleSwitchTo valid_pspace'
(wp: crunch_wps)
lemma send_ipc_corres:
(* call is only true if called in handleSyscall SysCall, which
is always blocking. *)
@ -2693,7 +2708,7 @@ proof -
simp del: dc_simp split del: if_split cong: if_cong)
apply (rule corres_split [OF _ dit_corres])
apply (rule corres_split [OF _ sts_corres])
apply (rule corres_split [OF _ attemptSwitchTo_corres])
apply (rule corres_split [OF _ possibleSwitchTo_corres])
apply (rule corres_split [OF _ threadget_fault_corres])
apply (fold when_def)[1]
apply (rename_tac fault fault')
@ -2774,7 +2789,7 @@ proof -
split del: if_split cong: if_cong)
apply (rule corres_split [OF _ dit_corres])
apply (rule corres_split [OF _ sts_corres])
apply (rule corres_split [OF _ attemptSwitchTo_corres])
apply (rule corres_split [OF _ possibleSwitchTo_corres])
apply (rule corres_split [OF _ threadget_fault_corres])
apply (rename_tac rv rv')
apply (case_tac rv)
@ -2887,7 +2902,7 @@ lemma send_signal_corres:
apply (rule corres_split[OF _ sts_corres])
apply (simp add: badgeRegister_def badge_register_def)
apply (rule corres_split[OF _ user_setreg_corres])
apply (rule switchIfRequiredTo_corres)
apply (rule possibleSwitchTo_corres)
apply wp
apply (clarsimp simp: thread_state_relation_def)
apply (wp set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at'
@ -2920,7 +2935,7 @@ lemma send_signal_corres:
apply (rule corres_split [OF _ sts_corres])
apply (simp add: badgeRegister_def badge_register_def)
apply (rule corres_split [OF _ user_setreg_corres])
apply (rule switchIfRequiredTo_corres)
apply (rule possibleSwitchTo_corres)
apply ((wp | simp)+)[1]
apply (rule_tac Q="\<lambda>_. Invariants_H.valid_queues and valid_queues' and
(\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and
@ -2951,7 +2966,7 @@ lemma send_signal_corres:
apply (rule corres_split [OF _ sts_corres])
apply (simp add: badgeRegister_def badge_register_def)
apply (rule corres_split [OF _ user_setreg_corres])
apply (rule switchIfRequiredTo_corres)
apply (rule possibleSwitchTo_corres)
apply (wp cur_tcb_lift | simp)+
apply (wp sts_st_tcb_at' set_thread_state_runnable_weak_valid_sched_action
| simp)+
@ -2994,22 +3009,19 @@ crunch typ'[wp]: setMRs "\<lambda>s. P (typ_at' T p s)"
lemma possibleSwitchTo_sch_act[wp]:
"\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s\<rbrace>
possibleSwitchTo t b
possibleSwitchTo t
\<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs)
apply (wp static_imp_wp threadSet_sch_act setQueue_sch_act threadGet_wp
| simp add: unless_def | wpc)+
apply (auto simp: obj_at'_def projectKOs tcb_in_cur_domain'_def)
done
lemmas attemptSwitchTo_sch_act[wp]
= possibleSwitchTo_sch_act[where b=True, folded attemptSwitchTo_def]
lemma possibleSwitchTo_valid_queues[wp]:
"\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t\<rbrace>
possibleSwitchTo t b
possibleSwitchTo t
\<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>"
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs)
apply (wp hoare_drop_imps | wpc | simp)+
apply (auto simp: valid_tcb'_def weak_sch_act_wf_def
dest: pred_tcb_at'
@ -3023,41 +3035,39 @@ lemma valid_queues'_ksSchedulerAction_update[simp]:
lemma possibleSwitchTo_ksQ':
"\<lbrace>(\<lambda>s. t' \<notin> set (ksReadyQueues s p) \<and> sch_act_not t' s) and K(t' \<noteq> t)\<rbrace>
possibleSwitchTo t same
possibleSwitchTo t
\<lbrace>\<lambda>_ s. t' \<notin> set (ksReadyQueues s p)\<rbrace>"
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs)
apply (wp static_imp_wp rescheduleRequired_ksQ' tcbSchedEnqueue_ksQ threadGet_wp
| wpc
| simp split del: if_split)+
apply (auto simp: obj_at'_def)
done
lemma attemptSwitchTo_ksQ:
"\<lbrace>(\<lambda>s. t' \<notin> set (ksReadyQueues s p) \<and> sch_act_not t' s) and K (t' \<noteq> t)\<rbrace>
attemptSwitchTo t \<lbrace>\<lambda>_ s. t' \<notin> set (ksReadyQueues s p)\<rbrace>"
by (simp add: attemptSwitchTo_def, wp possibleSwitchTo_ksQ', (fastforce)+)
lemma possibleSwitchTo_valid_queues'[wp]:
"\<lbrace>valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)
and st_tcb_at' runnable' t\<rbrace>
possibleSwitchTo t b
possibleSwitchTo t
\<lbrace>\<lambda>rv. valid_queues'\<rbrace>"
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs)
apply (wp static_imp_wp threadGet_wp | wpc | simp)+
apply (auto simp: obj_at'_def)
done
lemmas attemptSwitchTo_vq[wp]
= possibleSwitchTo_valid_queues[where b=True, folded attemptSwitchTo_def]
possibleSwitchTo_valid_queues'[where b=True, folded attemptSwitchTo_def]
crunch st_refs_of'[wp]: attemptSwitchTo "\<lambda>s. P (state_refs_of' s)"
crunch st_refs_of'[wp]: possibleSwitchTo "\<lambda>s. P (state_refs_of' s)"
(wp: crunch_wps)
crunch cap_to'[wp]: possibleSwitchTo "ex_nonz_cap_to' p"
(wp: crunch_wps)
crunch objs'[wp]: possibleSwitchTo valid_objs'
(wp: crunch_wps)
crunch ct[wp]: possibleSwitchTo cur_tcb'
(wp: cur_tcb_lift crunch_wps)
lemma possibleSwitchTo_iflive[wp]:
"\<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' t
and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace>
possibleSwitchTo t b
possibleSwitchTo t
\<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>"
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (wp | wpc | simp)+
@ -3066,24 +3076,21 @@ lemma possibleSwitchTo_iflive[wp]:
apply (auto simp: obj_at'_def projectKOs)
done
lemmas attemptSwitchTo_iflive[wp]
= possibleSwitchTo_iflive[where b=True, folded attemptSwitchTo_def]
crunch ifunsafe[wp]: attemptSwitchTo if_unsafe_then_cap'
crunch ifunsafe[wp]: possibleSwitchTo if_unsafe_then_cap'
(wp: crunch_wps)
crunch idle'[wp]: attemptSwitchTo valid_idle'
crunch idle'[wp]: possibleSwitchTo valid_idle'
(wp: crunch_wps)
crunch global_refs'[wp]: attemptSwitchTo valid_global_refs'
crunch global_refs'[wp]: possibleSwitchTo valid_global_refs'
(wp: crunch_wps)
crunch arch_state'[wp]: attemptSwitchTo valid_arch_state'
crunch arch_state'[wp]: possibleSwitchTo valid_arch_state'
(wp: crunch_wps)
crunch irq_node'[wp]: attemptSwitchTo "\<lambda>s. P (irq_node' s)"
crunch irq_node'[wp]: possibleSwitchTo "\<lambda>s. P (irq_node' s)"
(wp: crunch_wps)
crunch typ_at'[wp]: attemptSwitchTo "\<lambda>s. P (typ_at' T p s)"
crunch typ_at'[wp]: possibleSwitchTo "\<lambda>s. P (typ_at' T p s)"
(wp: crunch_wps)
crunch irq_handlers'[wp]: attemptSwitchTo valid_irq_handlers'
crunch irq_handlers'[wp]: possibleSwitchTo valid_irq_handlers'
(simp: unless_def tcb_cte_cases_def wp: crunch_wps)
crunch irq_states'[wp]: attemptSwitchTo valid_irq_states'
crunch irq_states'[wp]: possibleSwitchTo valid_irq_states'
(wp: crunch_wps)
(* Levity: added (20090713 10:04:33) *)
@ -3148,42 +3155,7 @@ lemma cteDeleteOne_reply_cap_to'[wp]:
apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps)
done
lemma switchIfRequiredTo_sch_act[wp]:
"\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s\<rbrace>
switchIfRequiredTo t
\<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add: switchIfRequiredTo_def tcbSchedEnqueue_def)
apply wp
done
lemmas switchIfRequiredTo_vq[wp]
= possibleSwitchTo_valid_queues[where b=True, folded switchIfRequiredTo_def]
possibleSwitchTo_valid_queues'[where b=True, folded switchIfRequiredTo_def]
crunch st_refs_of'[wp]: switchIfRequiredTo "\<lambda>s. P (state_refs_of' s)"
lemmas switchIfRequiredTo_iflive[wp]
= possibleSwitchTo_iflive[where b=False, folded switchIfRequiredTo_def]
crunch ifunsafe[wp]: switchIfRequiredTo if_unsafe_then_cap'
crunch idle'[wp]: switchIfRequiredTo valid_idle'
crunch global_refs'[wp]: switchIfRequiredTo valid_global_refs'
crunch arch_state'[wp]: switchIfRequiredTo valid_arch_state'
crunch irq_node'[wp]: switchIfRequiredTo "\<lambda>s. P (irq_node' s)"
crunch typ_at'[wp]: switchIfRequiredTo "\<lambda>s. P (typ_at' T p s)"
crunch irq_handlers'[wp]: switchIfRequiredTo valid_irq_handlers'
(simp: unless_def tcb_cte_cases_def)
crunch irq_states'[wp]: switchIfRequiredTo valid_irq_states'
crunch vp[wp]: switchIfRequiredTo valid_pspace'
crunch tcb_at'[wp]: switchIfRequiredTo "tcb_at' t"
crunch ct'[wp]: switchIfRequiredTo "\<lambda>s. P (ksCurThread s)"
(wp: crunch_wps)
crunch it'[wp]: switchIfRequiredTo "\<lambda>s. P (ksIdleThread s)"
(wp: crunch_wps)
crunch ct[wp]: switchIfRequiredTo cur_tcb'
(wp: cur_tcb_lift)
crunch vms'[wp]: setupCallerCap, switchIfRequiredTo, asUser,
crunch vms'[wp]: setupCallerCap, possibleSwitchTo, asUser,
doIPCTransfer "valid_machine_state'"
(wp: crunch_wps simp: zipWithM_x_mapM_x)
@ -3209,27 +3181,13 @@ crunch nosch[wp]: isFinalCapability "\<lambda>s. P (ksSchedulerAction s)"
(simp: Let_def)
crunch pspace_domain_valid[wp]:
setupCallerCap, switchIfRequiredTo, asUser, setMRs, doIPCTransfer
setupCallerCap, asUser, setMRs, doIPCTransfer, possibleSwitchTo
"pspace_domain_valid"
(wp: crunch_wps simp: zipWithM_x_mapM_x)
lemma switchIfRequiredTo_valid_queues:
"\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t\<rbrace>
switchIfRequiredTo t \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>"
apply (simp add: switchIfRequiredTo_def)
apply wp
done
lemma switchIfRequiredTo_valid_queues':
"\<lbrace>valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t\<rbrace>
switchIfRequiredTo t \<lbrace>\<lambda>_. valid_queues'\<rbrace>"
by (simp add: switchIfRequiredTo_def, wp)
crunch ksDomScheduleIdx[wp]: setupCallerCap, switchIfRequiredTo, doIPCTransfer, attemptSwitchTo "\<lambda>s. P (ksDomScheduleIdx s)"
crunch ksDomScheduleIdx[wp]: setupCallerCap, doIPCTransfer, possibleSwitchTo "\<lambda>s. P (ksDomScheduleIdx s)"
(wp: crunch_wps simp: zipWithM_x_mapM)
crunch invs'[wp]: switchIfRequiredTo "invs'"
lemma setThreadState_not_rct[wp]:
"\<lbrace>\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<rbrace>
setThreadState st t
@ -3605,7 +3563,7 @@ lemma receive_ipc_corres:
apply simp
apply simp
apply (rule corres_split [OF _ sts_corres])
apply (rule switchIfRequiredTo_corres)
apply (rule possibleSwitchTo_corres)
apply simp
apply (wp sts_st_tcb_at' set_thread_state_runnable_weak_valid_sched_action
| simp)+
@ -3813,7 +3771,7 @@ crunch tcb' [wp]: sendFaultIPC "tcb_at' t" (wp: crunch_wps)
lemma possibleSwitchTo_weak_sch_act[wp]:
"\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s\<rbrace>
possibleSwitchTo t b
possibleSwitchTo t
\<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add: possibleSwitchTo_def setSchedulerAction_def curDomain_def)
apply (wp static_imp_wp rescheduleRequired_weak_sch_act_wf threadGet_wp | wpc)+
@ -4148,10 +4106,10 @@ crunch urz[wp]: doIPCTransfer "untyped_ranges_zero'"
crunch gsUntypedZeroRanges[wp]: receiveIPC "\<lambda>s. P (gsUntypedZeroRanges s)"
(wp: crunch_wps transferCapsToSlots_pres1 simp: zipWithM_x_mapM ignore: constOnFailure)
crunch ctes_of[wp]: switchIfRequiredTo "\<lambda>s. P (ctes_of s)"
crunch ctes_of[wp]: possibleSwitchTo "\<lambda>s. P (ctes_of s)"
(wp: crunch_wps ignore: constOnFailure)
lemmas switchIfRequiredTo_cteCaps_of[wp]
= cteCaps_of_ctes_of_lift[OF switchIfRequiredTo_ctes_of]
lemmas possibleSwitchToTo_cteCaps_of[wp]
= cteCaps_of_ctes_of_lift[OF possibleSwitchTo_ctes_of]
(* t = ksCurThread s *)
lemma ri_invs' [wp]:
@ -4231,9 +4189,9 @@ lemma ri_invs' [wp]:
apply (rule hoare_pre)
apply (wp valid_irq_node_lift hoare_drop_imps setEndpoint_valid_mdb'
set_ep_valid_objs' sts_st_tcb' sts_sch_act' sts_valid_queues
setThreadState_ct_not_inQ switchIfRequiredTo_valid_queues
switchIfRequiredTo_valid_queues'
switchIfRequiredTo_ct_not_inQ hoare_vcg_all_lift
setThreadState_ct_not_inQ possibleSwitchTo_valid_queues
possibleSwitchTo_valid_queues'
possibleSwitchTo_ct_not_inQ hoare_vcg_all_lift
setEndpoint_ksQ setEndpoint_ct'
| simp add: valid_tcb_state'_def case_bool_If
case_option_If
@ -4424,13 +4382,6 @@ apply (wp sch_act_wf_lift valid_queues_lift
cur_tcb_lift tcb_in_cur_domain'_lift)+
done
crunch cap_to'[wp]: attemptSwitchTo "ex_nonz_cap_to' p"
(wp: crunch_wps)
crunch objs'[wp]: attemptSwitchTo valid_objs'
(wp: crunch_wps)
crunch ct[wp]: attemptSwitchTo cur_tcb'
(wp: cur_tcb_lift crunch_wps)
lemma setupCallerCap_cap_to' [wp]:
"\<lbrace>ex_nonz_cap_to' p\<rbrace> setupCallerCap a b \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>"
apply (simp add: setupCallerCap_def getThreadCallerSlot_def getThreadReplySlot_def)
@ -4452,22 +4403,19 @@ lemma setupCaller_pred_tcb_recv':
done
lemma possibleSwitchTo_sch_act_not:
"\<lbrace>sch_act_not t' and K (t \<noteq> t')\<rbrace> possibleSwitchTo t b \<lbrace>\<lambda>rv. sch_act_not t'\<rbrace>"
"\<lbrace>sch_act_not t' and K (t \<noteq> t')\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>rv. sch_act_not t'\<rbrace>"
apply (simp add: possibleSwitchTo_def setSchedulerAction_def curDomain_def)
apply (wp hoare_drop_imps | wpc | simp)+
done
lemmas attemptSwitchTo_sch_act_not
= possibleSwitchTo_sch_act_not[where b=True, folded attemptSwitchTo_def]
crunch vms'[wp]: possibleSwitchTo valid_machine_state'
crunch pspace_domain_valid[wp]: possibleSwitchTo pspace_domain_valid
crunch ct_idle_or_in_cur_domain'[wp]: possibleSwitchTo ct_idle_or_in_cur_domain'
crunch vms'[wp]: attemptSwitchTo valid_machine_state'
crunch pspace_domain_valid[wp]: attemptSwitchTo pspace_domain_valid
crunch ct_idle_or_in_cur_domain'[wp]: attemptSwitchTo ct_idle_or_in_cur_domain'
crunch ct'[wp]: attemptSwitchTo "\<lambda>s. P (ksCurThread s)"
crunch it[wp]: attemptSwitchTo "\<lambda>s. P (ksIdleThread s)"
crunch irqs_masked'[wp]: attemptSwitchTo "irqs_masked'"
crunch urz[wp]: attemptSwitchTo "untyped_ranges_zero'"
crunch ct'[wp]: possibleSwitchTo "\<lambda>s. P (ksCurThread s)"
crunch it[wp]: possibleSwitchTo "\<lambda>s. P (ksIdleThread s)"
crunch irqs_masked'[wp]: possibleSwitchTo "irqs_masked'"
crunch urz[wp]: possibleSwitchTo "untyped_ranges_zero'"
(simp: crunch_simps unless_def wp: crunch_wps)
lemma si_invs'[wp]:
@ -4490,8 +4438,8 @@ lemma si_invs'[wp]:
apply (rule_tac P="a\<noteq>t" in hoare_gen_asm)
apply (wp valid_irq_node_lift setupCaller_pred_tcb_recv'
sts_valid_objs' set_ep_valid_objs' setEndpoint_valid_mdb' sts_st_tcb' sts_sch_act'
attemptSwitchTo_sch_act_not sts_valid_queues setThreadState_ct_not_inQ
attemptSwitchTo_ksQ attemptSwitchTo_ct_not_inQ hoare_vcg_all_lift sts_ksQ'
possibleSwitchTo_sch_act_not sts_valid_queues setThreadState_ct_not_inQ
possibleSwitchTo_ksQ' possibleSwitchTo_ct_not_inQ hoare_vcg_all_lift sts_ksQ'
hoare_convert_imp [OF doIPCTransfer_nosch doIPCTransfer_ct']
hoare_convert_imp [OF getThreadState_nosch getThreadState_ct']
hoare_convert_imp [OF setEndpoint_nosch setEndpoint_ct']
@ -4793,7 +4741,7 @@ lemma hf_makes_runnable_simple':
| simp add: handleDoubleFault_def)+
done
crunch pred_tcb_at'[wp]: switchIfRequiredTo, completeSignal "pred_tcb_at' proj P t"
crunch pred_tcb_at'[wp]: possibleSwitchTo, completeSignal "pred_tcb_at' proj P t"
lemma ri_makes_runnable_simple':
"\<lbrace>st_tcb_at' P t' and K (t \<noteq> t') and K (P = runnable' \<or> P = simple')\<rbrace>

443
proof/refine/X64/Orphanage.thy
View File

@ -305,7 +305,7 @@ lemma setQueue_almost_no_orphans_enq_lift:
apply fastforce
done
lemma tcbSchedEnqueue_no_orphans:
lemma tcbSchedEnqueue_no_orphans[wp]:
"\<lbrace> \<lambda>s. no_orphans s \<rbrace>
tcbSchedEnqueue tcb_ptr
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
@ -316,6 +316,17 @@ lemma tcbSchedEnqueue_no_orphans:
apply auto
done
lemma tcbSchedAppend_no_orphans[wp]:
"\<lbrace> \<lambda>s. no_orphans s \<rbrace>
tcbSchedAppend tcb_ptr
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding tcbSchedAppend_def
apply (wp setQueue_no_orphans_enq threadSet_no_orphans | clarsimp simp: unless_def)+
apply (wp getObject_tcb_wp | clarsimp simp: threadGet_def)+
apply (drule obj_at_ko_at')
apply auto
done
lemma ko_at_obj_at':
"ko_at' ko p s \<and> P ko \<Longrightarrow> obj_at' P p s"
unfolding obj_at'_def
@ -407,6 +418,18 @@ lemma tcbSchedEnqueue_inQueue [wp]:
apply (fastforce simp: obj_at'_def valid_queues'_def inQ_def)
done
lemma tcbSchedAppend_inQueue [wp]:
"\<lbrace> \<lambda>s. valid_queues' s \<rbrace>
tcbSchedAppend tcb_ptr
\<lbrace> \<lambda>rv s. tcb_ptr \<in> all_queued_tcb_ptrs s \<rbrace>"
unfolding tcbSchedAppend_def all_queued_tcb_ptrs_def
apply (wp | clarsimp simp: unless_def)+
apply (rule_tac Q="\<lambda>rv. \<top>" in hoare_post_imp)
apply fastforce
apply (wp getObject_tcb_wp | clarsimp simp: threadGet_def)+
apply (fastforce simp: obj_at'_def valid_queues'_def inQ_def)
done
lemma rescheduleRequired_no_orphans [wp]:
"\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<rbrace>
rescheduleRequired
@ -698,6 +721,14 @@ lemma tcbSchedEnqueue_inQueue_eq:
apply wp
done
lemma tcbSchedAppend_inQueue_eq:
"\<lbrace> valid_queues' and K (tcb_ptr = tcb_ptr') \<rbrace>
tcbSchedAppend tcb_ptr
\<lbrace> \<lambda>rv s. tcb_ptr' \<in> all_queued_tcb_ptrs s \<rbrace>"
apply (rule hoare_gen_asm, simp)
apply wp
done
lemma findM_on_success:
"\<lbrakk> \<And>x. \<lbrace> P x \<rbrace> f x \<lbrace> \<lambda>rv s. rv \<rbrace>; \<And>x y. \<lbrace> P x \<rbrace> f y \<lbrace> \<lambda>rv. P x \<rbrace> \<rbrakk> \<Longrightarrow>
\<lbrace> \<lambda>s. \<exists>x \<in> set xs. P x s \<rbrace> findM f xs \<lbrace> \<lambda>rv s. \<exists> y. rv = Some y \<rbrace>"
@ -769,12 +800,46 @@ lemma chooseThread_no_orphans [wp]:
apply (wp assert_inv ThreadDecls_H_switchToThread_no_orphans)
apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def
valid_queues_def st_tcb_at'_def)
apply (fold lookupBitmapPriority_def)
apply (fastforce dest!: lookupBitmapPriority_obj_at' elim: obj_at'_weaken
simp: all_active_tcb_ptrs_def)
apply (simp add: bitmap_fun_defs | wp)+
done
lemma tcbSchedAppend_in_ksQ:
"\<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedAppend t
\<lbrace>\<lambda>r s. \<exists>domain priority. t \<in> set (ksReadyQueues s (domain, priority))\<rbrace>"
apply (rule_tac Q="\<lambda>s. \<exists>d p. valid_queues' s \<and>
obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and>
obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s"
in hoare_pre_imp)
apply (clarsimp simp: tcb_at'_has_tcbPriority tcb_at'_has_tcbDomain)
including no_pre
apply (wp hoare_vcg_ex_lift)
apply (simp add: tcbSchedAppend_def unless_def)
apply wp
apply clarsimp
apply wp+
apply (rule_tac Q="\<lambda>rv s. tdom = d \<and> rv = p \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s
\<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s"
in hoare_post_imp, clarsimp)
apply (wp, (wp threadGet_const)+)
apply (rule_tac Q="\<lambda>rv s.
obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and>
obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<and>
obj_at' (\<lambda>tcb. tcbQueued tcb = rv) t s \<and>
(rv \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)))" in hoare_post_imp)
apply (clarsimp simp: o_def elim!: obj_at'_weakenE)
apply (wp threadGet_obj_at' hoare_vcg_imp_lift threadGet_const)
apply (case_tac "obj_at' (Not \<circ> tcbQueued) t s")
apply (clarsimp)
apply (clarsimp simp: valid_queues'_def)
apply (drule_tac x=d in spec)
apply (drule_tac x=p in spec)
apply (drule_tac x=t in spec)
apply (subgoal_tac "obj_at' (inQ d p) t s", clarsimp)
apply (clarsimp simp: obj_at'_def inQ_def)+
done
lemma hoare_neg_imps:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda> rv s. \<not> R rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. R r s \<longrightarrow> Q r s\<rbrace>"
by (auto simp: valid_def)
@ -822,16 +887,225 @@ lemma all_invs_but_ct_idle_or_in_cur_domain'_strg:
"invs' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s"
by (clarsimp simp: invs'_to_invs_no_cicd'_def)
lemma schedule_no_orphans [wp]:
"\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_wf (ksSchedulerAction s) s \<rbrace>
lemma setSchedulerAction_cnt_sch_act_not[wp]:
"\<lbrace> \<top> \<rbrace> setSchedulerAction ChooseNewThread \<lbrace>\<lambda>rv s. sch_act_not x s\<rbrace>"
by (rule hoare_pre, rule hoare_strengthen_post[OF setSchedulerAction_direct]) auto
lemma obj_at'_static_fix:
"\<lbrakk> obj_at' (\<lambda>(ko::'a::pspace_storable). True) p s ; P \<rbrakk> \<Longrightarrow> obj_at' (\<lambda>(ko::'a::pspace_storable). P) p s"
by (erule obj_at'_weakenE, simp)
lemma tcbSchedEnqueue_in_ksQ_aqtp[wp]:
"\<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedEnqueue t
\<lbrace>\<lambda>r s. t \<in> all_queued_tcb_ptrs s\<rbrace>"
apply (clarsimp simp: all_queued_tcb_ptrs_def)
apply (rule tcbSchedEnqueue_in_ksQ)
done
crunch ksReadyQueues[wp]: threadGet "\<lambda>s. P (ksReadyQueues s)"
lemma tcbSchedEnqueue_in_ksQ_already_queued:
"\<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and>
(\<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))) \<rbrace>
tcbSchedEnqueue t
\<lbrace>\<lambda>r s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))\<rbrace>"
apply (case_tac "t'=t", wpsimp wp: tcbSchedEnqueue_in_ksQ)
apply (wpsimp simp: tcbSchedEnqueue_def unless_def)
apply (rule_tac Q="\<lambda>_ s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))"
in hoare_post_imp)
apply metis
apply wpsimp+
done
lemma tcbSchedAppend_in_ksQ_already_queued:
"\<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and>
(\<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))) \<rbrace>
tcbSchedAppend t
\<lbrace>\<lambda>r s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))\<rbrace>"
apply (case_tac "t'=t", wpsimp wp: tcbSchedAppend_in_ksQ)
apply (wpsimp simp: tcbSchedAppend_def unless_def)
apply (rule_tac Q="\<lambda>_ s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))"
in hoare_post_imp)
apply metis
apply wpsimp+
done
lemma tcbSchedEnqueue_in_ksQ'':
"\<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and>
(t' \<noteq> t \<longrightarrow> (\<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority)))) \<rbrace>
tcbSchedEnqueue t
\<lbrace>\<lambda>r s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))\<rbrace>"
apply (case_tac "t'=t", wpsimp wp: tcbSchedEnqueue_in_ksQ)
apply clarsimp
apply (wpsimp simp: tcbSchedEnqueue_def unless_def)
apply (rule_tac Q="\<lambda>_ s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))"
in hoare_post_imp)
apply metis
apply wpsimp+
done
lemma tcbSchedAppend_in_ksQ'':
"\<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and>
(t' \<noteq> t \<longrightarrow> (\<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority)))) \<rbrace>
tcbSchedAppend t
\<lbrace>\<lambda>r s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))\<rbrace>"
apply (case_tac "t'=t", wpsimp wp: tcbSchedAppend_in_ksQ)
apply clarsimp
apply (wpsimp simp: tcbSchedAppend_def unless_def)
apply (rule_tac Q="\<lambda>_ s. \<exists>domain priority. t' \<in> set (ksReadyQueues s (domain, priority))"
in hoare_post_imp)
apply metis
apply wpsimp+
done
crunch st_tcb_at': setSchedulerAction "\<lambda>s. P (st_tcb_at' Q t s)"
lemmas ssa_st_tcb_at'_ksCurThread[wp] =
hoare_lift_Pf2[where f=ksCurThread, OF setSchedulerAction_st_tcb_at' setSchedulerAction_ct']
lemma ct_active_st_tcb_at':
"ct_active' s = st_tcb_at' runnable' (ksCurThread s) s"
apply (rule iffI)
apply (drule ct_active_runnable')
apply (simp add: ct_in_state'_def)
apply (clarsimp simp: ct_in_state'_def)
apply (erule pred_tcb'_weakenE)
apply (case_tac st, auto)
done
lemma tcbSchedEnqueue_in_ksQ_already_queued_aqtp:
"\<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and>
t' \<in> all_queued_tcb_ptrs s \<rbrace> tcbSchedEnqueue t
\<lbrace>\<lambda>r s. t' \<in> all_queued_tcb_ptrs s \<rbrace>"
by (clarsimp simp: all_queued_tcb_ptrs_def tcbSchedEnqueue_in_ksQ_already_queued)
(* FIXME move *)
lemma invs_switchToThread_runnable':
"\<lbrakk> invs' s ; ksSchedulerAction s = SwitchToThread t \<rbrakk> \<Longrightarrow> st_tcb_at' runnable' t s"
by (simp add: invs'_def valid_state'_def)
(* for shoving pred_tcb_at' through hoare_vcg_imp_lift for tcbs we know are there *)
lemma not_pred_tcb_at'I:
"\<lbrakk> pred_tcb_at' f (Not \<circ> P) t s ; tcb_at' t s \<rbrakk> \<Longrightarrow> \<not> pred_tcb_at' f P t s"
by (subst (asm) pred_tcb_at'_Not, blast)
lemma in_all_active_tcb_ptrsD:
"t \<in> all_active_tcb_ptrs s \<Longrightarrow> st_tcb_at' runnable' t s"
unfolding all_active_tcb_ptrs_def is_active_tcb_ptr_def
is_active_thread_state_def isRunning_def isRestart_def
apply clarsimp
apply (erule pred_tcb'_weakenE)
apply (case_tac st; clarsimp)
done
lemma scheduleChooseNewThread_no_orphans:
"\<lbrace> invs' and no_orphans
and (\<lambda>s. ksSchedulerAction s = ChooseNewThread
\<and> (st_tcb_at' runnable' (ksCurThread s) s
\<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))) \<rbrace>
scheduleChooseNewThread
\<lbrace>\<lambda>_. no_orphans \<rbrace>"
unfolding scheduleChooseNewThread_def
apply (wp add: ssa_no_orphans hoare_vcg_all_lift)
apply (wp hoare_disjI1 chooseThread_nosch)+
apply (wp nextDomain_invs_no_cicd' hoare_vcg_imp_lift
hoare_lift_Pf2 [OF ksQ_all_queued_tcb_ptrs_lift[OF nextDomain_ksQ]
nextDomain_ct']
hoare_lift_Pf2 [OF st_tcb_at'_is_active_tcb_ptr_lift[OF nextDomain_st_tcb_at']
nextDomain_ct']
hoare_vcg_all_lift getDomainTime_wp)[2]
apply (wpsimp simp: if_apply_def2 invs_invs_no_cicd' all_queued_tcb_ptrs_def
is_active_tcb_ptr_runnable')+
done
lemma schedule_no_orphans[wp]:
notes ssa_lift[wp del]
shows
"\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
schedule
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
proof -
have do_switch_to:
"\<And>candidate.
\<lbrace>\<lambda>s. no_orphans s \<and> ksSchedulerAction s = SwitchToThread candidate
\<and> st_tcb_at' runnable' candidate s
\<and> (st_tcb_at' runnable' (ksCurThread s) s
\<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<rbrace>
do ThreadDecls_H.switchToThread candidate;
setSchedulerAction ResumeCurrentThread
od
\<lbrace>\<lambda>rv. no_orphans\<rbrace>"
apply (wpsimp wp: scheduleChooseNewThread_no_orphans ssa_no_orphans
hoare_vcg_all_lift ThreadDecls_H_switchToThread_no_orphans)+
apply (rule_tac Q="\<lambda>_ s. (t = candidate \<longrightarrow> ksCurThread s = candidate) \<and>
(t \<noteq> candidate \<longrightarrow> sch_act_not t s)"
in hoare_post_imp)
apply (wpsimp wp: stt_nosch static_imp_wp)+
apply (fastforce dest!: in_all_active_tcb_ptrsD simp: all_queued_tcb_ptrs_def comp_def)
done
have abort_switch_to_enq:
"\<And>candidate.
\<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_queues' s
\<and> ksSchedulerAction s = SwitchToThread candidate
\<and> (st_tcb_at' runnable' (ksCurThread s) s
\<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<rbrace>
do tcbSchedEnqueue candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od
\<lbrace>\<lambda>rv. no_orphans\<rbrace>"
apply (rule hoare_pre)
apply (wp scheduleChooseNewThread_no_orphans ssa_no_orphans setSchedulerAction_direct)
apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_ex_lift
simp: is_active_tcb_ptr_runnable' all_queued_tcb_ptrs_def
| rule hoare_lift_Pf2[where f=ksCurThread, OF setSchedulerAction_ksQ])+
apply (wp tcbSchedEnqueue_in_ksQ' tcbSchedEnqueue_no_orphans hoare_vcg_all_lift hoare_vcg_imp_lift' hoare_vcg_disj_lift)
apply (wp hoare_lift_Pf2[where f=ksCurThread, OF tcbSchedEnqueue_pred_tcb_at']
hoare_lift_Pf2[where f=ksCurThread, OF tcbSchedEnqueue_in_ksQ_already_queued]
tcbSchedEnqueue_no_orphans
| strengthen not_pred_tcb_at'_strengthen
| wp_once hoare_vcg_imp_lift')+
apply (clarsimp)
apply (frule invs_sch_act_wf', clarsimp simp: pred_tcb_at')
apply (simp add: st_tcb_at_neg' tcb_at_invs')
done
have abort_switch_to_app:
"\<And>candidate.
\<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_queues' s
\<and> ksSchedulerAction s = SwitchToThread candidate
\<and> (st_tcb_at' runnable' (ksCurThread s) s
\<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))) ) \<rbrace>
do tcbSchedAppend candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od
\<lbrace>\<lambda>rv. no_orphans\<rbrace>"
apply (rule hoare_pre)
apply (wp scheduleChooseNewThread_no_orphans ssa_no_orphans setSchedulerAction_direct)
apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_ex_lift
simp: is_active_tcb_ptr_runnable' all_queued_tcb_ptrs_def
| rule hoare_lift_Pf2[where f=ksCurThread, OF setSchedulerAction_ksQ])+
apply (wp tcbSchedAppend_in_ksQ'' tcbSchedAppend_no_orphans hoare_vcg_all_lift hoare_vcg_imp_lift' hoare_vcg_disj_lift)
apply (wp hoare_lift_Pf2[where f=ksCurThread, OF tcbSchedAppend_pred_tcb_at']
hoare_lift_Pf2[where f=ksCurThread, OF tcbSchedAppend_in_ksQ_already_queued]
tcbSchedAppend_no_orphans
| strengthen not_pred_tcb_at'_strengthen
| wp_once hoare_vcg_imp_lift')+
apply (clarsimp)
apply (frule invs_sch_act_wf', clarsimp simp: pred_tcb_at')
apply (simp add: st_tcb_at_neg' tcb_at_invs')
done
show ?thesis
unfolding schedule_def
apply (wp, wpc)
-- "action = ResumeCurrentThread"
apply (wp)[1]
-- "action = ChooseNewThread"
apply (clarsimp simp: when_def)
apply (clarsimp simp: when_def scheduleChooseNewThread_def)
apply (wp ssa_no_orphans hoare_vcg_all_lift)
apply (wp hoare_disjI1 chooseThread_nosch)
apply (wp nextDomain_invs_no_cicd' hoare_vcg_imp_lift
@ -846,42 +1120,32 @@ lemma schedule_no_orphans [wp]:
hoare_drop_imp
| clarsimp simp: all_queued_tcb_ptrs_def
| strengthen all_invs_but_ct_idle_or_in_cur_domain'_strg
| wps tcbSchedEnqueue_ct')+)[2]
| wps tcbSchedEnqueue_ct')+)[1]
apply ((wp tcbSchedEnqueue_no_orphans tcbSchedEnqueue_in_ksQ'
hoare_drop_imp
| clarsimp simp: all_queued_tcb_ptrs_def
| strengthen all_invs_but_ct_idle_or_in_cur_domain'_strg
| wps tcbSchedEnqueue_ct')+)[1]
apply wp[1]
-- "action = SwitchToThread word"
apply (rename_tac word)
apply (wp ssa_no_orphans hoare_vcg_all_lift
ThreadDecls_H_switchToThread_no_orphans)
apply (rule_tac Q="\<lambda>_ s. (t=word \<longrightarrow> ksCurThread s = word) \<and>
(t\<noteq>word \<longrightarrow> sch_act_not t s)"
in hoare_post_imp, clarsimp)
apply (wp stt_nosch static_imp_wp)
apply (wp tcbSchedEnqueue_no_orphans hoare_drop_imp)
apply (rule_tac Q="\<lambda>_ s. \<exists>p. curThread \<in> set (ksReadyQueues s p)
\<and> curThread = ksCurThread s"
in hoare_post_imp, clarsimp simp: all_queued_tcb_ptrs_def)
apply (wps tcbSchedEnqueue_ct')
apply clarsimp
apply (wp tcbSchedEnqueue_in_ksQ)[1]
apply (wp)+
apply (case_tac "ksSchedulerAction s")
apply (clarsimp)
apply (clarsimp simp: pred_tcb_at'_def is_active_tcb_ptr_def)
apply (rule conjI, clarsimp simp: invs'_def valid_state'_def cur_tcb'_def)
apply (clarsimp simp: is_active_thread_state_def comp_def
all_invs_but_ct_idle_or_in_cur_domain'_strg)
apply (drule(1) obj_at_not_obj_at_conj)
apply (subgoal_tac "obj_at' (\<lambda>_. False) (ksCurThread s) s", clarsimp)
apply (erule obj_at'_weakenE)
apply (case_tac "tcbState k", (clarsimp simp: isRunning_def isRestart_def is_active_thread_state_def)+)
apply (rule conjI, clarsimp simp: invs'_def valid_state'_def cur_tcb'_def)
apply (clarsimp simp: pred_tcb_at'_def all_active_tcb_ptrs_def comp_def
is_active_thread_state_def is_active_tcb_ptr_def)
apply (drule(1) obj_at_not_obj_at_conj)
apply (subgoal_tac "obj_at' (\<lambda>_. False) (ksCurThread s) s", clarsimp)
apply (erule obj_at'_weakenE)
apply (case_tac "tcbState k", (clarsimp simp: isRunning_def isRestart_def)+)
-- "action = SwitchToThread candidate"
apply (clarsimp)
apply (rename_tac candidate)
apply (wpsimp wp: do_switch_to abort_switch_to_enq abort_switch_to_app)
(* isHighestPrio *)
apply (wp hoare_drop_imps)
apply (wp add: tcbSchedEnqueue_no_orphans)+
apply (clarsimp simp: conj_ac cong: conj_cong imp_cong split del: if_split)
apply (wp hoare_lift_Pf2[where f=ksCurThread, OF tcbSchedEnqueue_pred_tcb_at']
hoare_lift_Pf2[where f=ksCurThread, OF tcbSchedEnqueue_in_ksQ']
hoare_vcg_imp_lift'
| strengthen not_pred_tcb_at'_strengthen)+
apply (clarsimp simp: comp_def)
apply (frule invs_queues)
apply (clarsimp simp: invs_valid_queues' tcb_at_invs' st_tcb_at_neg' is_active_tcb_ptr_runnable')
apply (fastforce simp: all_invs_but_ct_idle_or_in_cur_domain'_strg invs_switchToThread_runnable')
done
qed
lemma setNotification_no_orphans [wp]:
"\<lbrace> \<lambda>s. no_orphans s \<rbrace>
@ -900,37 +1164,22 @@ crunch no_orphans [wp]: completeSignal "no_orphans"
(simp: crunch_simps wp: crunch_wps)
lemma possibleSwitchTo_almost_no_orphans [wp]:
"\<lbrace> \<lambda>s. almost_no_orphans target s \<and> valid_queues' s \<and> st_tcb_at' runnable' target s \<rbrace>
possibleSwitchTo target onSamePriority
"\<lbrace> \<lambda>s. almost_no_orphans target s \<and> valid_queues' s \<and> st_tcb_at' runnable' target s
\<and> weak_sch_act_wf (ksSchedulerAction s) s \<rbrace>
possibleSwitchTo target
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding possibleSwitchTo_def
apply (wp tcbSchedEnqueue_almost_no_orphans ssa_almost_no_orphans static_imp_wp | wpc | clarsimp)+
apply (wp hoare_drop_imps | clarsimp)+
done
by (wp rescheduleRequired_valid_queues'_weak tcbSchedEnqueue_almost_no_orphans
ssa_almost_no_orphans static_imp_wp
| wpc | clarsimp
| wp_once hoare_drop_imp)+
lemma attemptSwitchTo_almost_no_orphans [wp]:
"\<lbrace> \<lambda>s. almost_no_orphans target s \<and> valid_queues' s \<and> st_tcb_at' runnable' target s \<rbrace>
attemptSwitchTo target
lemma possibleSwitchTo_almost_no_orphans':
"\<lbrace> \<lambda>s. almost_no_orphans target s \<and> valid_queues' s \<and> st_tcb_at' runnable' target s
\<and> sch_act_wf (ksSchedulerAction s) s \<rbrace>
possibleSwitchTo target
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding attemptSwitchTo_def
apply wp
done
lemma switchIfRequiredTo_schedule_no_orphans [wp]:
"\<lbrace> \<lambda>s. almost_no_orphans target s \<and> valid_queues' s \<and> st_tcb_at' runnable' target s \<rbrace>
switchIfRequiredTo target
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding switchIfRequiredTo_def by wp
lemma tcbSchedAppend_no_orphans:
"\<lbrace> \<lambda>s. no_orphans s \<rbrace>
tcbSchedAppend thread
\<lbrace> \<lambda>_ s. no_orphans s \<rbrace>"
unfolding tcbSchedAppend_def
apply (wp setQueue_no_orphans_enq threadSet_no_orphans weak_if_wp
| clarsimp simp: unless_def | simp only: subset_insertI)+
done
by wp (strengthen sch_act_wf_weak, assumption)
lemma tcbSchedAppend_almost_no_orphans:
"\<lbrace> \<lambda>s. almost_no_orphans thread s \<and> valid_queues' s \<rbrace>
@ -1037,8 +1286,11 @@ lemma sendIPC_no_orphans [wp]:
sendIPC blocking call badge canGrant thread epptr
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding sendIPC_def
apply (wp hoare_drop_imps setThreadState_not_active_no_orphans sts_st_tcb' | wpc
apply (wp hoare_drop_imps setThreadState_not_active_no_orphans sts_st_tcb'
possibleSwitchTo_almost_no_orphans'
| wpc
| clarsimp simp: is_active_thread_state_def isRestart_def isRunning_def)+
apply (rule_tac Q="\<lambda>rv. no_orphans and valid_queues' and valid_objs' and ko_at' rv epptr
and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp)
apply (fastforce simp: valid_objs'_def valid_obj'_def valid_ep'_def obj_at'_def projectKOs)
@ -1227,6 +1479,13 @@ lemma createObject_no_orphans:
projectKO_opt_tcb isRunning_def isRestart_def archObjSize_def
APIType_capBits_def objBits_simps
split: option.splits)+)[1]
apply ((wp createObjects'_wp_subst
createObjects_no_orphans[where sz = sz ] |
clarsimp simp: projectKO_opt_tcb cte_wp_at_ctes_of projectKO_opt_ep
is_active_thread_state_def makeObject_tcb pageBits_def ptBits_def
projectKO_opt_tcb isRunning_def isRestart_def archObjSize_def
APIType_capBits_def objBits_simps pteBits_def
split: option.splits)+)[1]
apply ((wp createObjects'_wp_subst
createObjects_no_orphans[where sz = sz] |
clarsimp simp: projectKO_opt_tcb cte_wp_at_ctes_of projectKO_opt_ep
@ -1466,7 +1725,9 @@ lemma sendSignal_no_orphans [wp]:
\<lbrace> \<lambda>_ s. no_orphans s \<rbrace>"
unfolding sendSignal_def
apply (rule hoare_pre)
apply (wp sts_st_tcb' gts_wp' getNotification_wp asUser_almost_no_orphans | wpc | clarsimp)+
apply (wp sts_st_tcb' gts_wp' getNotification_wp asUser_almost_no_orphans
cancelIPC_weak_sch_act_wf
| wpc | clarsimp simp: sch_act_wf_weak)+
done
lemma handleInterrupt_no_orphans [wp]:
@ -1695,12 +1956,11 @@ lemma doReplyTransfer_no_orphans[wp]:
doReplyTransfer sender receiver slot
\<lbrace>\<lambda>rv. no_orphans\<rbrace>"
unfolding doReplyTransfer_def
apply (rule hoare_pre)
apply (wp threadSet_valid_queues' threadSet_no_orphans
setThreadState_not_active_no_orphans sts_st_tcb'
| wpc | clarsimp simp: is_active_thread_state_def isRunning_def
isRestart_def
| strengthen invs_valid_queues')+
apply (wp sts_st_tcb' setThreadState_not_active_no_orphans threadSet_no_orphans
threadSet_valid_queues' threadSet_weak_sch_act_wf
| wpc | clarsimp simp: is_active_thread_state_def isRunning_def isRestart_def
| wp_once hoare_drop_imps
| strengthen sch_act_wf_weak invs_valid_queues')+
apply (rule_tac Q="\<lambda>rv. invs' and no_orphans" in hoare_post_imp)
apply (fastforce simp: inQ_def)
apply (wp hoare_drop_imps | clarsimp)+
@ -1725,7 +1985,7 @@ lemma restart_no_orphans [wp]:
restart t
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding restart_def isBlocked_def2 including no_pre
apply (wp tcbSchedEnqueue_almost_no_orphans sts_st_tcb' | clarsimp
apply (wp tcbSchedEnqueue_almost_no_orphans sts_st_tcb' cancelIPC_weak_sch_act_wf | clarsimp
| strengthen no_orphans_strg_almost
| strengthen invs_valid_queues')+
apply (rule hoare_strengthen_post, rule gts_sp')
@ -1767,7 +2027,7 @@ lemma setPriority_no_orphans [wp]:
setPriority tptr prio
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding setPriority_def
apply (wp hoare_drop_imps | clarsimp)+
apply (wp add: hoare_drop_imps del: tcbSchedEnqueue_no_orphans | clarsimp)+
apply (wp hoare_drop_imps tcbSchedEnqueue_almost_no_orphans)+
apply (rule_tac Q="\<lambda>rv s. almost_no_orphans tptr s \<and> valid_queues' s" in hoare_post_imp)
apply (fastforce simp: is_active_tcb_ptr_runnable' pred_tcb_at'_def obj_at'_def
@ -2081,7 +2341,8 @@ lemma receiveIPC_no_orphans [wp]:
hoare_vcg_all_lift sts_st_tcb'
| wpc
| clarsimp simp: is_active_thread_state_def isRunning_def isRestart_def
doNBRecvFailedTransfer_def)+
doNBRecvFailedTransfer_def invs_valid_queues'
| strengthen sch_act_wf_weak)+
done
crunch valid_objs' [wp]: getThreadCallerSlot "valid_objs'"
@ -2137,6 +2398,22 @@ lemma activatable_from_running':
"ct_running' s \<Longrightarrow> ct_in_state' activatable' s"
by (clarsimp simp: ct_in_state'_def elim!: pred_tcb'_weakenE)
(* FIXME move *)
lemma sts_tcb_at'_preserve:
"\<lbrace> st_tcb_at' P t and K (P st) \<rbrace> setThreadState st t' \<lbrace>\<lambda>_. st_tcb_at' P t \<rbrace>"
by (wpsimp wp: sts_st_tcb')
(* FIXME move *)
(* e.g. if you set a non-runnable thread to Inactive, all runnable threads are still runnable *)
lemma sts_tcb_at'_preserve':
"\<lbrace> st_tcb_at' P t and st_tcb_at' (\<lambda>st. \<not> P st) t' and K (\<not> P st) \<rbrace>
setThreadState st t'
\<lbrace>\<lambda>_. st_tcb_at' P t \<rbrace>"
by (wpsimp wp: sts_st_tcb' simp: st_tcb_at_neg')
(* FIXME move to where disj_imp lives *)
lemma disj_imp': "(P \<or> Q) = (\<not>Q \<longrightarrow> P)" by blast
lemma handleEvent_no_orphans [wp]:
"\<lbrace> \<lambda>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and>
(e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<and>
@ -2162,17 +2439,7 @@ theorem callKernel_no_orphans [wp]:
callKernel e
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding callKernel_def including no_pre
apply (wp | clarsimp)+
apply (rule_tac Q="\<lambda>rv s. invs' s" in hoare_post_imp)
apply (wp weak_if_wp schedule_invs' | clarsimp)+
apply (rule_tac Q="\<lambda>_. invs'" in hoare_post_imp, clarsimp)
apply (wp)
apply (rule_tac Q="\<lambda>_. invs' and no_orphans" in hoare_post_imp, clarsimp)
apply (wp | simp)+
apply (rule_tac Q="\<lambda>y s. invs' s \<and> no_orphans s" and
E="\<lambda>y s. invs' s \<and> no_orphans s" in hoare_post_impErr)
apply (wp hoare_vcg_conj_liftE | clarsimp)+
done
by (wpsimp wp: weak_if_wp schedule_invs' hoare_vcg_conj_liftE)
end

5
proof/refine/X64/Refine.thy
View File

@ -253,9 +253,8 @@ lemma activate_thread_sched_act:
lemma schedule_sched_act_rct[wp]:
"\<lbrace>\<top>\<rbrace> Schedule_A.schedule
\<lbrace>\<lambda>rs (s::det_state). scheduler_action s = resume_cur_thread\<rbrace>"
apply (simp add: Schedule_A.schedule_def)
apply (wp | wpc | simp add: set_scheduler_action_def)+
done
unfolding Schedule_A.schedule_def
by (wpsimp)
lemma call_kernel_sched_act_rct[wp]:
"\<lbrace>einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)

816
proof/refine/X64/Schedule_R.thy
View File

File diff suppressed because it is too large Load Diff

6
proof/refine/X64/StateRelation.thy
View File

@ -799,5 +799,11 @@ lemma ghost_relation_typ_at:
apply (intro conjI impI iffI allI,simp_all)
apply (auto elim!: allE)
done
lemma runnable_coerce_abstract:
"\<lbrakk> runnable' st'; thread_state_relation st st' \<rbrakk>
\<Longrightarrow> runnable st"
by (case_tac st, simp_all)
end
end

63
proof/refine/X64/Syscall_R.thy
View File

@ -889,14 +889,6 @@ lemma isReply_awaiting_reply':
"isReply st = awaiting_reply' st"
by (case_tac st, (clarsimp simp add: isReply_def)+)
lemma obj_at'_conj_distrib:
"obj_at' (\<lambda>ko. P ko \<and> Q ko) p s \<Longrightarrow> obj_at' P p s \<and> obj_at' Q p s"
by (auto simp: obj_at'_def)
lemma idle_tcb_at'_split:
"idle_tcb_at' (\<lambda>p. P (fst p) \<and> Q (snd p)) t s \<Longrightarrow> st_tcb_at' P t s \<and> bound_tcb_at' Q t s"
by (clarsimp simp: pred_tcb_at'_def dest!: obj_at'_conj_distrib)
lemma doReply_invs[wp]:
"\<lbrace>tcb_at' t and tcb_at' t' and
cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t False) slot and
@ -2041,15 +2033,13 @@ crunch sane [wp]: transferCaps "sch_act_sane"
ignore: transferCapsToSlots)
lemma possibleSwitchTo_sane:
"\<lbrace>\<lambda>s. sch_act_sane s \<and> t \<noteq> ksCurThread s\<rbrace> possibleSwitchTo t b \<lbrace>\<lambda>_. sch_act_sane\<rbrace>"
apply (simp add: possibleSwitchTo_def setSchedulerAction_def curDomain_def cong: if_cong)
"\<lbrace>\<lambda>s. sch_act_sane s \<and> t \<noteq> ksCurThread s\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>_. sch_act_sane\<rbrace>"
apply (simp add: possibleSwitchTo_def setSchedulerAction_def curDomain_def
cong: if_cong)
apply (wp hoare_drop_imps | wpc)+
apply (simp add: sch_act_sane_def)
done
lemmas attemptSwitchTo_sane
= possibleSwitchTo_sane[where b=True, folded attemptSwitchTo_def]
crunch sane [wp]: handleFaultReply sch_act_sane
( wp: threadGet_inv hoare_drop_imps crunch_wps
simp: crunch_simps
@ -2064,7 +2054,7 @@ lemma doReplyTransfer_sane:
"\<lbrace>\<lambda>s. sch_act_sane s \<and> t' \<noteq> ksCurThread s\<rbrace>
doReplyTransfer t t' callerSlot \<lbrace>\<lambda>rv. sch_act_sane\<rbrace>"
apply (simp add: doReplyTransfer_def liftM_def)
apply (wp attemptSwitchTo_sane hoare_drop_imps hoare_vcg_all_lift|wpc)+
apply (wp possibleSwitchTo_sane hoare_drop_imps hoare_vcg_all_lift|wpc)+
apply simp
done
@ -2100,10 +2090,10 @@ proof -
have astct: "\<And>t p.
\<lbrace>(\<lambda>s. ksCurThread s \<notin> set(ksReadyQueues s p) \<and> sch_act_sane s)
and (\<lambda>s. ksCurThread s \<noteq> t)\<rbrace>
attemptSwitchTo t \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set(ksReadyQueues s p)\<rbrace>"
possibleSwitchTo t \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set(ksReadyQueues s p)\<rbrace>"
apply (rule hoare_weaken_pre)
apply (wps attemptSwitchTo_ct')
apply (wp attemptSwitchTo_ksQ)
apply (wps possibleSwitchTo_ct')
apply (wp possibleSwitchTo_ksQ')
apply (clarsimp simp: sch_act_sane_def)
done
have stsct: "\<And>t st p.
@ -2156,6 +2146,10 @@ lemma handleReply_ct_not_ksQ:
apply (clarsimp)
done
crunch valid_etcbs[wp]: possible_switch_to "valid_etcbs"
crunch valid_etcbs[wp]: handle_recv "valid_etcbs"
(wp: crunch_wps simp: crunch_simps)
lemma hrw_corres:
"corres dc (einvs and ct_running)
(invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
@ -2343,6 +2337,41 @@ lemma ct_active_not_idle'[simp]:
elim: pred_tcb'_weakenE)+
done
lemma deleteCallerCap_st_tcb_at_runnable[wp]:
"\<lbrace>st_tcb_at' runnable' t\<rbrace> deleteCallerCap t' \<lbrace>\<lambda>rv. st_tcb_at' runnable' t\<rbrace>"
apply (simp add: deleteCallerCap_def getThreadCallerSlot_def
locateSlot_conv)
apply (wp cteDeleteOne_tcb_at_runnable' hoare_drop_imps | simp)+
done
lemma handleRecv_st_tcb_at':
"\<lbrace>invs' and st_tcb_at' runnable' t and (\<lambda>s. ksCurThread s \<noteq> t)\<rbrace>
handleRecv True
\<lbrace>\<lambda>rv. st_tcb_at' runnable' t\<rbrace>"
unfolding handleRecv_def
apply (wp hf_makes_runnable_simple' rai_makes_runnable_simple')
apply simp
apply (wp hf_makes_runnable_simple' rai_makes_runnable_simple')
apply (wpc ; clarsimp)
apply (wp rai_makes_runnable_simple' | wpc | simp)+
apply (wp hoare_drop_imps)[1]
apply (wp rai_makes_runnable_simple' ri_makes_runnable_simple' | wpc | simp)+
apply (wp hoare_drop_imps)[1]
apply clarsimp
apply wp+
apply simp
done
crunch ksCurThread[wp]:
handleFault,receiveSignal,receiveIPC,asUser "\<lambda>s. P (ksCurThread s)"
(wp: hoare_drop_imps crunch_wps simp: crunch_simps)
lemma handleRecv_ksCurThread[wp]:
"\<lbrace>\<lambda>s. P (ksCurThread s) \<rbrace> handleRecv b \<lbrace>\<lambda>rv s. P (ksCurThread s) \<rbrace>"
unfolding handleRecv_def
by ((simp, wp hoare_drop_imps) | wpc | wpsimp wp: hoare_drop_imps)+
lemma he_invs'[wp]:
"\<lbrace>invs' and
(\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and

301
proof/refine/X64/TcbAcc_R.thy
View File

@ -36,10 +36,84 @@ declare complement_def[simp]
(* Auxiliaries and basic properties of priority bitmap functions *)
lemma countLeadingZeros_word_clz[simp]:
"countLeadingZeros w = word_clz w"
unfolding countLeadingZeros_def word_clz_def
by (simp add: to_bl_upt)
lemma wordLog2_word_log2[simp]:
"wordLog2 = word_log2"
apply (rule ext)
unfolding wordLog2_def word_log2_def
by (simp add: word_size wordBits_def)
lemmas bitmap_fun_defs = addToBitmap_def removeFromBitmap_def
modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def
(* lookupBitmapPriority is a cleaner version of getHighestPrio *)
definition
"lookupBitmapPriority d \<equiv> \<lambda>s.
l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) ||
of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d,
invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))"
lemma getHighestPrio_def'[simp]:
"getHighestPrio d = gets (lookupBitmapPriority d)"
unfolding getHighestPrio_def gets_def
by (fastforce simp: gets_def get_bind_apply lookupBitmapPriority_def bitmap_fun_defs)
(* isHighestPrio_def' is a cleaner version of isHighestPrio_def *)
lemma isHighestPrio_def':
"isHighestPrio d p = gets (\<lambda>s. ksReadyQueuesL1Bitmap s d = 0 \<or> lookupBitmapPriority d s \<le> p)"
unfolding isHighestPrio_def bitmap_fun_defs getHighestPrio_def'
apply (rule ext)
apply (clarsimp simp: gets_def bind_assoc return_def NonDetMonad.bind_def get_def
split: if_splits)
done
lemma getHighestPrio_inv[wp]:
"\<lbrace> P \<rbrace> getHighestPrio d \<lbrace>\<lambda>_. P \<rbrace>"
unfolding bitmap_fun_defs by simp
lemma valid_bitmapQ_bitmapQ_simp:
"\<lbrakk> valid_bitmapQ s \<rbrakk> \<Longrightarrow>
bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> [])"
unfolding valid_bitmapQ_def
by simp
lemma invs_bitmapQ_tcb_at_cur_domain'_hd:
"\<lbrakk> invs' s; bitmapQ (ksCurDomain s) p s;
st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, p))) s\<rbrakk>
\<Longrightarrow> tcb_in_cur_domain' (hd (ksReadyQueues s (ksCurDomain s, p))) s"
apply (rule_tac xs="tl (ksReadyQueues s (ksCurDomain s, p))"
in invs_queues_tcb_in_cur_domain'[rotated], assumption, rule refl)
apply (drule invs_queues)
apply (clarsimp simp: valid_queues_def)
apply (simp add: valid_bitmapQ_bitmapQ_simp)
done
lemma prioToL1Index_l1IndexToPrio_or_id:
"\<lbrakk> unat (w'::priority) < 2 ^ wordRadix ; w < 2^(size w' - wordRadix) \<rbrakk>
\<Longrightarrow> prioToL1Index ((l1IndexToPrio w) || w') = w"
unfolding l1IndexToPrio_def prioToL1Index_def
apply (simp add: shiftr_over_or_dist shiftr_le_0 wordRadix_def')
apply (subst shiftl_shiftr_id, simp, simp add: word_size)
apply (rule word_of_nat_less)
apply simp
apply (subst unat_of_nat_eq, simp_all add: word_size)
done
lemma bitmapQ_no_L1_orphansD:
"\<lbrakk> bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d !! i \<rbrakk>
\<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize"
unfolding bitmapQ_no_L1_orphans_def by simp
lemma l1IndexToPrio_wordRadix_mask[simp]:
"l1IndexToPrio i && mask wordRadix = 0"
unfolding l1IndexToPrio_def
by (simp add: wordRadix_def')
definition
(* when in the middle of updates, a particular queue might not be entirely valid *)
valid_queues_no_bitmap_except :: "machine_word \<Rightarrow> kernel_state \<Rightarrow> bool"
@ -61,14 +135,50 @@ lemma valid_queues_no_bitmap_exceptE:
unfolding valid_queues_no_bitmap_except_def valid_queues_no_bitmap_def
by fastforce
lemma st_tcb_at_coerce_abstract:
assumes t: "st_tcb_at' P t c"
assumes sr: "(a, c) \<in> state_relation"
shows "st_tcb_at (\<lambda>st. \<exists>st'. thread_state_relation st st' \<and> P st') t a"
using assms
apply (clarsimp simp: state_relation_def pred_tcb_at'_def obj_at'_def
projectKOs objBits_simps)
apply (erule(1) pspace_dom_relatedE)
apply (erule(1) obj_relation_cutsE, simp_all)
apply (clarsimp simp: st_tcb_at_def obj_at_def other_obj_relation_def
tcb_relation_def
split: Structures_A.kernel_object.split_asm if_split_asm
X64_A.arch_kernel_obj.split_asm)+
apply fastforce
done
lemma st_tcb_at_runnable_coerce_concrete:
assumes t: "st_tcb_at runnable t a"
assumes sr: "(a, c) \<in> state_relation"
assumes tcb: "tcb_at' t c"
shows "st_tcb_at' runnable' t c"
using t
apply -
apply (rule ccontr)
apply (drule pred_tcb_at'_Not[THEN iffD2, OF conjI, OF tcb])
apply (drule st_tcb_at_coerce_abstract[OF _ sr])
apply (clarsimp simp: st_tcb_def2)
apply (case_tac "tcb_state tcb"; simp)
done
lemma bitmapL2_L1_limitD:
"\<lbrakk> ksReadyQueuesL2Bitmap s (d, i) !! j ; bitmapQ_no_L1_orphans s ; bitmapQ_no_L2_orphans s \<rbrakk>
\<Longrightarrow> i < numPriorities div wordBits"
unfolding bitmapQ_no_L1_orphans_def bitmapQ_no_L2_orphans_def
by blast
lemma pspace_relation_tcb_at':
assumes p: "pspace_relation (kheap a) (ksPSpace c)"
assumes t: "tcb_at t a"
assumes aligned: "pspace_aligned' c"
assumes distinct: "pspace_distinct' c"
shows "tcb_at' t c" using assms
apply (clarsimp simp: obj_at_def projectKOs)
apply (drule(1) pspace_relation_absD)
apply (clarsimp simp: is_tcb other_obj_relation_def)
apply (simp split: kernel_object.split_asm)
apply (drule(2) aligned_distinct_obj_atI'[where 'a=tcb], simp)
apply (erule obj_at'_weakenE)
apply simp
done
lemma valid_objs_valid_tcbE: "\<And>s t.\<lbrakk> valid_objs' s; tcb_at' t s; \<And>tcb. valid_tcb' tcb s \<Longrightarrow> R s tcb \<rbrakk> \<Longrightarrow> obj_at' (R s) t s"
apply (clarsimp simp add: projectKOs valid_objs'_def ran_def typ_at'_def
@ -1902,10 +2012,9 @@ lemma addToBitmap_if_null_corres_noop: (* used this way in Haskell code *)
lemma removeFromBitmap_corres_noop:
"corres dc \<top> \<top> (return ()) (removeFromBitmap tdom prioa)"
unfolding removeFromBitmap_def modifyReadyQueuesL1Bitmap_def getReadyQueuesL1Bitmap_def
modifyReadyQueuesL2Bitmap_def getReadyQueuesL2Bitmap_def
unfolding removeFromBitmap_def
by (rule corres_noop)
(wp | simp add: state_relation_def | rule no_fail_pre)+
(wp | simp add: bitmap_fun_defs state_relation_def | rule no_fail_pre)+
crunch typ_at'[wp]: addToBitmap "\<lambda>s. P (typ_at' T p s)"
(wp: hoare_drop_imps setCTE_typ_at')
@ -2055,15 +2164,13 @@ lemmas threadSet_weak_sch_act_wf
lemma removeFromBitmap_nosch[wp]:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
unfolding removeFromBitmap_def getReadyQueuesL1Bitmap_def modifyReadyQueuesL1Bitmap_def
getReadyQueuesL2Bitmap_def modifyReadyQueuesL2Bitmap_def
by (simp|wp setObject_nosch)+
unfolding removeFromBitmap_def
by (simp add: bitmap_fun_defs|wp setObject_nosch)+
lemma addToBitmap_nosch[wp]:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> addToBitmap d p \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
unfolding addToBitmap_def getReadyQueuesL1Bitmap_def modifyReadyQueuesL1Bitmap_def
getReadyQueuesL2Bitmap_def modifyReadyQueuesL2Bitmap_def
by (simp|wp setObject_nosch)+
unfolding addToBitmap_def
by (simp add: bitmap_fun_defs|wp setObject_nosch)+
lemmas removeFromBitmap_weak_sch_act_wf[wp]
= weak_sch_act_wf_lift[OF removeFromBitmap_nosch]
@ -2090,19 +2197,15 @@ crunch obj_at'[wp]: addToBitmap "obj_at' P t"
lemma removeFromBitmap_tcb_in_cur_domain'[wp]:
"\<lbrace>tcb_in_cur_domain' t\<rbrace> removeFromBitmap tdom prio \<lbrace>\<lambda>ya. tcb_in_cur_domain' t\<rbrace>"
unfolding tcb_in_cur_domain'_def removeFromBitmap_def
modifyReadyQueuesL2Bitmap_def getReadyQueuesL2Bitmap_def
modifyReadyQueuesL1Bitmap_def getReadyQueuesL1Bitmap_def
apply (rule_tac f="\<lambda>s. ksCurDomain s" in hoare_lift_Pf)
apply (wp setObject_cte_obj_at_tcb' | simp)+
apply (wp setObject_cte_obj_at_tcb' | simp add: bitmap_fun_defs)+
done
lemma addToBitmap_tcb_in_cur_domain'[wp]:
"\<lbrace>tcb_in_cur_domain' t\<rbrace> addToBitmap tdom prio \<lbrace>\<lambda>ya. tcb_in_cur_domain' t\<rbrace>"
unfolding tcb_in_cur_domain'_def addToBitmap_def
modifyReadyQueuesL2Bitmap_def getReadyQueuesL2Bitmap_def
modifyReadyQueuesL1Bitmap_def getReadyQueuesL1Bitmap_def
apply (rule_tac f="\<lambda>s. ksCurDomain s" in hoare_lift_Pf)
apply (wp setObject_cte_obj_at_tcb' | simp)+
apply (wp setObject_cte_obj_at_tcb' | simp add: bitmap_fun_defs)+
done
lemma tcbSchedDequeue_weak_sch_act_wf[wp]:
@ -2709,6 +2812,16 @@ lemma threadGet_const:
apply (clarsimp simp: obj_at'_def)
done
schematic_goal l2BitmapSize_def': (* arch specific consequence *)
"l2BitmapSize = numeral ?X"
by (simp add: l2BitmapSize_def wordBits_def word_size numPriorities_def)
lemma prioToL1Index_size [simp]:
"prioToL1Index w < l2BitmapSize"
unfolding prioToL1Index_def wordRadix_def l2BitmapSize_def'
by (fastforce simp: shiftr_div_2n' nat_divide_less_eq
intro: order_less_le_trans[OF unat_lt2p])
lemma prioToL1Index_max:
"prioToL1Index p < 2 ^ wordRadix"
unfolding prioToL1Index_def wordRadix_def
@ -2716,8 +2829,8 @@ lemma prioToL1Index_max:
lemma prioToL1Index_bit_set:
"((2 :: machine_word) ^ prioToL1Index p) !! prioToL1Index p"
using prioToL1Index_max[simplified wordRadix_def]
by (fastforce simp: nth_w2p_same)
using l2BitmapSize_def'
by (fastforce simp: nth_w2p_same intro: order_less_le_trans[OF prioToL1Index_size])
lemma prioL2Index_bit_set:
fixes p :: priority
@ -2732,7 +2845,7 @@ lemma addToBitmap_bitmapQ:
unfolding addToBitmap_def
modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def
by (wp, clarsimp simp: bitmapQ_def prioToL1Index_bit_set prioL2Index_bit_set)
by (wp, clarsimp simp: bitmap_fun_defs bitmapQ_def prioToL1Index_bit_set prioL2Index_bit_set)
lemma addToBitmap_valid_queues_no_bitmap_except:
" \<lbrace> valid_queues_no_bitmap_except t \<rbrace>
@ -2795,15 +2908,15 @@ lemma valid_queues_no_bitmap_except_objD:
lemma bitmapQ_no_L1_orphansE:
"\<lbrakk> bitmapQ_no_L1_orphans s ;
ksReadyQueuesL1Bitmap s d !! i \<rbrakk>
\<Longrightarrow> ksReadyQueuesL2Bitmap s (d, i) \<noteq> 0"
\<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0"
unfolding bitmapQ_no_L1_orphans_def
by clarsimp
lemma bitmapQ_no_L2_orphansE:
"\<lbrakk> bitmapQ_no_L2_orphans s ;
ksReadyQueuesL2Bitmap s (d, prioToL1Index p) !! unat (p && mask wordRadix) \<rbrakk>
ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix) \<rbrakk>
\<Longrightarrow> ksReadyQueuesL1Bitmap s d !! prioToL1Index p"
unfolding bitmapQ_no_L2_orphans_def
unfolding bitmapQ_no_L2_orphans_def using prioToL1Index_size
by blast
lemma valid_bitmapQ_exceptE:
@ -2812,25 +2925,34 @@ lemma valid_bitmapQ_exceptE:
unfolding valid_bitmapQ_except_def
by blast
lemma invertL1Index_eq_cancelD:
"\<lbrakk> invertL1Index i = invertL1Index j ; i < l2BitmapSize ; j < l2BitmapSize \<rbrakk>
\<Longrightarrow> i = j"
by (simp add: invertL1Index_def l2BitmapSize_def')
lemma invertL1Index_eq_cancel:
"\<lbrakk> i < l2BitmapSize ; j < l2BitmapSize \<rbrakk>
\<Longrightarrow> (invertL1Index i = invertL1Index j) = (i = j)"
by (rule iffI, simp_all add: invertL1Index_eq_cancelD)
lemma removeFromBitmap_bitmapQ_no_L1_orphans[wp]:
"\<lbrace> bitmapQ_no_L1_orphans \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans \<rbrace>"
unfolding bitmap_fun_defs
by (wp)
(fastforce simp: prioToL1Index_complement_nth_w2p bitmapQ_no_L1_orphans_def)
apply (wp | simp add: bitmap_fun_defs bitmapQ_no_L1_orphans_def)+
apply (fastforce simp: invertL1Index_eq_cancel prioToL1Index_bit_not_set
prioToL1Index_complement_nth_w2p)
done
lemma removeFromBitmap_bitmapQ_no_L2_orphans[wp]:
"\<lbrace> bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans \<rbrace>
removeFromBitmap d p
\<lbrace>\<lambda>_. bitmapQ_no_L2_orphans \<rbrace>"
unfolding bitmap_fun_defs
apply (wp, clarsimp)
apply (rule conjI)
apply (clarsimp simp: bitmapQ_no_L2_orphans_def prioToL1Index_complement_nth_w2p)
apply (subst prioToL1Index_complement_nth_w2p')
apply (rule order_less_le_trans[OF bitmapL2_L1_limitD], simp_all add: bitmapQ_no_L2_orphans_def)[1]
apply (simp add: word_size numPriorities_def wordBits_def)
apply simp
apply (clarsimp simp: bitmapQ_no_L2_orphans_def)
apply (wp, clarsimp simp: bitmap_fun_defs bitmapQ_no_L2_orphans_def)+
apply (rule conjI, clarsimp)
apply (rule conjI, clarsimp)
apply (clarsimp simp: complement_nth_w2p l2BitmapSize_def')
apply clarsimp
apply metis
done
@ -2862,7 +2984,7 @@ proof -
apply (clarsimp simp: bitmapQ_def)
apply (rule conjI; clarsimp)
apply (rename_tac p')
apply (rule conjI; clarsimp)
apply (rule conjI; clarsimp simp: invertL1Index_eq_cancel)
apply (drule_tac p=p' in valid_bitmapQ_exceptE[where d=d], clarsimp)
apply (clarsimp simp: bitmapQ_def)
apply (drule_tac n'="unat (p' && mask wordRadix)" in no_other_bits_set)
@ -2878,7 +3000,7 @@ proof -
(* after clearing bit in L2, some bits in L2 field are still set *)
apply clarsimp
apply (subst valid_bitmapQ_except_def, clarsimp)+
apply (clarsimp simp: bitmapQ_def)
apply (clarsimp simp: bitmapQ_def invertL1Index_eq_cancel)
apply (rule conjI; clarsimp)
apply (frule (1) prioToL1Index_bits_low_high_eq)
apply (drule_tac d=d and p=pa in valid_bitmapQ_exceptE, simp)
@ -2898,11 +3020,6 @@ lemma addToBitmap_bitmapQ_no_L1_orphans[wp]:
apply (clarsimp simp: word_or_zero prioToL1Index_bit_set ucast_and_mask[symmetric]
unat_ucast_upcast is_up wordRadix_def' word_size nth_w2p
wordBits_def numPriorities_def)
apply (clarsimp simp: prioToL1Index_def wordRadix_def')
apply (rule order_less_le_trans[OF unat_shiftr_less_t2n[where m="size p - wordRadix"]])
apply (simp add: wordRadix_def wordBits_def word_size)
apply (fastforce intro: order_less_le_trans[OF unat_lt2p] simp: word_size)
apply (simp add: wordRadix_def wordBits_def word_size)
done
lemma addToBitmap_bitmapQ_no_L2_orphans[wp]:
@ -2910,7 +3027,7 @@ lemma addToBitmap_bitmapQ_no_L2_orphans[wp]:
unfolding bitmap_fun_defs bitmapQ_defs
apply wp
apply clarsimp
apply (metis prioToL1Index_bit_set)
apply (fastforce simp: invertL1Index_eq_cancel prioToL1Index_bit_set)
done
lemma addToBitmap_valid_bitmapQ_except:
@ -2919,17 +3036,10 @@ lemma addToBitmap_valid_bitmapQ_except:
\<lbrace>\<lambda>_. valid_bitmapQ_except d p \<rbrace>"
unfolding bitmap_fun_defs bitmapQ_defs
apply wp
apply (clarsimp simp: bitmapQ_def prioToL1Index_bit_set prioToL1Index_nth_w2p)
apply (case_tac "ksReadyQueuesL2Bitmap s (d, prioToL1Index p) !! unat (pa && mask wordRadix)")
apply (subgoal_tac "ksReadyQueuesL1Bitmap s d !! prioToL1Index p")
prefer 2
apply fastforce
apply force
apply (case_tac "ksReadyQueuesL1Bitmap s d !! prioToL1Index p")
apply (clarsimp simp: ucast_and_mask[symmetric] unat_ucast_upcast is_up nth_w2p)
apply (fastforce dest: prioToL1Index_bits_low_high_eq)
apply (clarsimp simp: ucast_and_mask[symmetric] unat_ucast_upcast is_up nth_w2p)
apply (fastforce dest: prioToL1Index_bits_low_high_eq)
apply (clarsimp simp: bitmapQ_def prioToL1Index_nth_w2p invertL1Index_eq_cancel
ucast_and_mask[symmetric] unat_ucast_upcast is_up nth_w2p)
apply (fastforce simp: priority_mask_wordRadix_size[simplified wordBits_def']
dest: prioToL1Index_bits_low_high_eq)
done
lemma addToBitmap_valid_bitmapQ:
@ -3294,6 +3404,16 @@ lemma rescheduleRequired_valid_queues'[wp]:
apply (wp | wpc | simp | fastforce simp: valid_queues'_def)+
done
(* weaker precondition than rescheduleRequired_valid_queues', which is sometimes too strong *)
lemma rescheduleRequired_valid_queues'_weak:
"\<lbrace>\<lambda>s. valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
rescheduleRequired
\<lbrace>\<lambda>_. valid_queues'\<rbrace>"
apply (simp add: rescheduleRequired_def)
apply (wp | wpc | simp | fastforce simp: valid_queues'_def)+
apply (clarsimp simp: weak_sch_act_wf_def)
done
lemma rescheduleRequired_valid_queues'_sch_act_simple:
"\<lbrace>valid_queues' and sch_act_simple\<rbrace>
rescheduleRequired
@ -4310,7 +4430,7 @@ lemma addToBitmap_ksMachine[wp]:
lemma removeFromBitmap_ksMachine[wp]:
"\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>"
unfolding bitmap_fun_defs
by (wp, simp)
by (wp|simp add: bitmap_fun_defs)+
lemma tcbSchedEnqueue_ksMachine[wp]:
"\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> tcbSchedEnqueue x \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>"
@ -4330,14 +4450,13 @@ lemma setThreadState_vms'[wp]:
lemma ct_not_inQ_addToBitmap[wp]:
"\<lbrace> ct_not_inQ \<rbrace> addToBitmap d p \<lbrace>\<lambda>_. ct_not_inQ \<rbrace>"
unfolding addToBitmap_def modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def
unfolding bitmap_fun_defs
by (wp, clarsimp simp: ct_not_inQ_def)
lemma ct_not_inQ_removeFromBitmap[wp]:
"\<lbrace> ct_not_inQ \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. ct_not_inQ \<rbrace>"
unfolding removeFromBitmap_def modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def
by (wp, clarsimp simp: ct_not_inQ_def)
unfolding bitmap_fun_defs
by (wp|simp add: bitmap_fun_defs ct_not_inQ_def comp_def)+
lemma setBoundNotification_vms'[wp]:
"\<lbrace>valid_machine_state'\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace>"
@ -4377,6 +4496,38 @@ lemma tcbSchedEnqueue_ct_not_inQ:
done
qed
lemma tcbSchedAppend_ct_not_inQ:
"\<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
tcbSchedAppend t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
(is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>")
proof -
have ts: "\<lbrace>?PRE\<rbrace> threadSet (tcbQueued_update (\<lambda>_. True)) t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
apply (simp add: ct_not_inQ_def)
apply (rule_tac Q="\<lambda>s. ksSchedulerAction s = ResumeCurrentThread
\<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ksCurThread s \<noteq> t"
in hoare_pre_imp, clarsimp)
apply (rule hoare_convert_imp [OF threadSet_no_sa])
apply (rule hoare_weaken_pre)
apply (wps setObject_ct_inv)
apply (rule threadSet_obj_at'_strongish)
apply (clarsimp simp: comp_def)
done
have sq: "\<And>d p q. \<lbrace>ct_not_inQ\<rbrace> setQueue d p q \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
apply (simp add: ct_not_inQ_def setQueue_def)
apply (wp)
apply (clarsimp)
done
show ?thesis
apply (simp add: tcbSchedAppend_def unless_def null_def)
apply (wp ts sq hoare_convert_imp [OF addToBitmap_nosch addToBitmap_ct'])+
apply (rule_tac Q="\<lambda>_. ?PRE" in hoare_post_imp, clarsimp)
apply (wp sq hoare_convert_imp [OF setQueue_no_sa setQueue_ct'])+
apply (rule_tac Q="\<lambda>_. ?PRE" in hoare_post_imp, clarsimp)
apply wp
apply assumption
done
qed
lemma ct_not_inQ_update_cnt:
"ct_not_inQ s \<Longrightarrow> ct_not_inQ (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)"
by (simp add: ct_not_inQ_def)
@ -4418,27 +4569,29 @@ lemma rescheduleRequired_ct_not_inQ:
apply (wp setSchedulerAction_direct)
done
crunch nosch[wp]: tcbSchedEnqueue "\<lambda>s. P (ksSchedulerAction s)"
(simp: unless_def)
crunch nosch[wp]: tcbSchedAppend "\<lambda>s. P (ksSchedulerAction s)"
(simp: unless_def)
crunch nosch[wp]: tcbSchedDequeue "\<lambda>s. P (ksSchedulerAction s)"
lemma rescheduleRequired_sa_cnt[wp]:
"\<lbrace>\<lambda>s. True \<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. ksSchedulerAction s = ChooseNewThread \<rbrace>"
unfolding rescheduleRequired_def setSchedulerAction_def
by wpsimp
lemma possibleSwitchTo_ct_not_inQ:
"\<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
possibleSwitchTo t same \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
possibleSwitchTo t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
(is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>")
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (wp static_imp_wp rescheduleRequired_ct_not_inQ tcbSchedEnqueue_ct_not_inQ threadGet_wp
| wpc
| clarsimp simp: ct_not_inQ_update_stt)+
| (rule hoare_post_imp[OF _ rescheduleRequired_sa_cnt], fastforce)
| clarsimp simp: ct_not_inQ_update_stt bitmap_fun_defs)+
apply (fastforce simp: obj_at'_def)
done
lemma attemptSwitchTo_ct_not_inQ:
"\<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
attemptSwitchTo t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
by (simp add: attemptSwitchTo_def, wp possibleSwitchTo_ct_not_inQ)
lemma switchIfRequiredTo_ct_not_inQ:
"\<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
switchIfRequiredTo t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
by (simp add: switchIfRequiredTo_def, wp possibleSwitchTo_ct_not_inQ)
lemma threadSet_tcbState_update_ct_not_inQ[wp]:
"\<lbrace>ct_not_inQ\<rbrace> threadSet (tcbState_update f) t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
apply (simp add: ct_not_inQ_def)

4
proof/refine/X64/Tcb_R.thy
View File

@ -221,7 +221,7 @@ lemma restart_corres:
apply (rule corres_split_nor [OF _ cancel_ipc_corres])
apply (rule corres_split_nor [OF _ setup_reply_master_corres])
apply (rule corres_split_nor [OF _ sts_corres])
apply (rule corres_split [OF switchIfRequiredTo_corres tcbSchedEnqueue_corres])
apply (rule corres_split [OF possibleSwitchTo_corres tcbSchedEnqueue_corres])
apply (wp_trace set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at' sts_valid_queues sts_st_tcb' | clarsimp simp: valid_tcb_state'_def)+
apply (rule_tac Q="\<lambda>rv. valid_sched and cur_tcb" in hoare_strengthen_post)
apply wp
@ -247,7 +247,7 @@ lemma setupReplyMaster_sch_act_simple[wp]:
lemma restart_invs':
"\<lbrace>invs' and ex_nonz_cap_to' t and (\<lambda>s. t \<noteq> ksIdleThread s)\<rbrace>
ThreadDecls_H.restart t \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (simp add: restart_def isBlocked_def2 switchIfRequiredTo_def)
apply (simp add: restart_def isBlocked_def2)
apply (wp setThreadState_nonqueued_state_update
cancelIPC_simple setThreadState_st_tcb
| wp_once sch_act_simple_lift)+