diff --git a/proof/crefine/Move_C.thy b/proof/crefine/Move_C.thy index 3300eb4861..ca190281b6 100644 --- a/proof/crefine/Move_C.thy +++ b/proof/crefine/Move_C.thy @@ -936,7 +936,7 @@ lemma sts_running_ksReadyQueuesL1Bitmap[wp]: unfolding setThreadState_def scheduleTCB_def rescheduleRequired_def apply wpsimp apply (rule hoare_pre_cont) - by (wpsimp wp: hoare_drop_imps isSchedulable_wp)+ + by (wpsimp wp: hoare_drop_imps getSchedulable_wp)+ lemma asUser_obj_at_not_queued[wp]: "\obj_at' (\tcb. \ tcbQueued tcb) p\ asUser t m \\rv. obj_at' (\tcb. \ tcbQueued tcb) p\" diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy index 8bf5d48256..9d88bd4600 100644 --- a/proof/crefine/RISCV64/Finalise_C.thy +++ b/proof/crefine/RISCV64/Finalise_C.thy @@ -1304,7 +1304,8 @@ lemma threadSet_tcbInReleaseQueue_ccorres[corres]: lemma tcbReleaseRemove_ccorres: "ccorres dc xfdc valid_objs' \\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\ [] (tcbReleaseRemove tcbPtr) (Call tcbReleaseRemove_'proc)" - apply (cinit lift: tcb_' simp: inReleaseQueue_def when_def) + apply (cinit lift: tcb_' + simp: inReleaseQueue_def when_def readInReleaseQueue_def threadGet_def[symmetric]) apply (rule ccorres_stateAssert)+ apply (rule_tac r'="\rv rv'. rv = to_bool rv'" and xf'="ret__unsigned_longlong_'" in ccorres_split_nothrow) @@ -1461,15 +1462,6 @@ lemma schedContext_cancelYieldTo_ccorres: apply (fastforce dest: typ_heap_simps' split: if_splits) done -lemma threadSet_isSchedulable_bool: - "\\tcb. tcbState tcb = tcbState (f tcb); \tcb. tcbInReleaseQueue tcb = tcbInReleaseQueue (f tcb); - \tcb. tcbSchedContext tcb = tcbSchedContext (f tcb)\ - \ threadSet f t \\s. P (isSchedulable_bool t s)\" - apply (wpsimp wp: threadSet_wp) - apply (erule_tac P=P in back_subst) - by (fastforce simp: pred_map_simps isSchedulable_bool_def isScActive_def opt_map_def obj_at_simps - split: if_splits option.splits) - lemma active_runnable': "active' state \ runnable' state" by fastforce diff --git a/proof/crefine/RISCV64/Invoke_C.thy b/proof/crefine/RISCV64/Invoke_C.thy index 6eb2c54a5c..2c238b1f7a 100644 --- a/proof/crefine/RISCV64/Invoke_C.thy +++ b/proof/crefine/RISCV64/Invoke_C.thy @@ -81,17 +81,17 @@ lemma setDomain_ccorres: apply (rule_tac Q'="\rv'. invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and tcb_at' t and (\s. curThread = ksCurThread s)" in hoare_strengthen_post) - apply (wpsimp wp: isSchedulable_wp) + apply (wpsimp wp: getSchedulable_wp) apply (fastforce simp: valid_pspace_valid_objs' weak_sch_act_wf_def split: if_splits) apply (rule_tac Q'="\_. invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and tcb_at' t and (\s. curThread = ksCurThread s)" in hoare_strengthen_post) apply (wpsimp wp: threadSet_tcbDomain_update_invs' hoare_vcg_imp_lift' - threadSet_isSchedulable_bool)+ + threadSet_schedulable')+ apply (simp add: guard_is_UNIV_def) apply (wpsimp wp: tcbSchedDequeue_not_queued hoare_vcg_all_lift hoare_vcg_imp_lift') - apply (fastforce simp: isSchedulable_bool_def pred_map_simps opt_map_def obj_at_simps) + apply fastforce done lemma decodeDomainInvocation_ccorres: diff --git a/proof/crefine/RISCV64/IpcCancel_C.thy b/proof/crefine/RISCV64/IpcCancel_C.thy index dfe7e847f8..835b43e549 100644 --- a/proof/crefine/RISCV64/IpcCancel_C.thy +++ b/proof/crefine/RISCV64/IpcCancel_C.thy @@ -420,29 +420,25 @@ lemma isStopped_ccorres [corres]: apply (simp add: ThreadState_defs)+ done -lemma isRunnable_ccorres [corres]: +lemma isRunnable_ccorres[corres]: "ccorres (\r r'. r = to_bool r') ret__unsigned_long_' - (tcb_at' thread) (UNIV \ {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) [] - (isRunnable thread) (Call isRunnable_'proc)" - apply (cinit lift: thread_' simp: getThreadState_def) + (tcb_at' thread) {s. thread_' s = tcb_ptr_to_ctcb_ptr thread} hs + (isRunnable thread) (Call isRunnable_'proc)" + apply (cinit lift: thread_' simp: readRunnable_def threadGet_def[symmetric] getThreadState_def) apply (rule ccorres_move_c_guard_tcb) apply (rule ccorres_pre_threadGet) apply (rule ccorres_symb_exec_r) apply (rule ccorres_cond_weak) + apply (fastforce intro: ccorres_return_C) apply (rule ccorres_return_C) - apply (simp) - apply (simp) - apply (simp) - apply (simp add: ccorres_cond_iffs) - apply (rule ccorres_return_C) - apply (simp) - apply (simp) - apply (simp) - apply (vcg) + apply simp + apply simp + apply simp + apply vcg apply (rule conseqPre) - apply (vcg) - apply (clarsimp) - apply (clarsimp) + apply vcg + apply clarsimp + apply clarsimp apply (clarsimp simp: typ_heap_simps ctcb_relation_thread_state_to_tsType split: thread_state.splits) apply (simp add: ThreadState_defs)+ @@ -1777,25 +1773,29 @@ lemma tcb_at_1: apply (clarsimp simp add: is_aligned_def ctcb_size_bits_def) done -crunch inReleaseQueue, isSchedulable +crunch inReleaseQueue, getSchedulable for (empty_fail) empty_fail[wp] lemma isSchedulable_ccorres [corres]: "ccorres (\r r'. r = to_bool r') ret__unsigned_long_' (tcb_at' tcbPtr and no_0_obj') \\thread = tcb_ptr_to_ctcb_ptr tcbPtr\ [] - (isSchedulable tcbPtr) (Call isSchedulable_'proc)" + (getSchedulable tcbPtr) (Call isSchedulable_'proc)" supply Collect_const[simp del] if_split[split del] - apply (cinit lift: thread_') + apply (cinit lift: thread_' + simp: readSchedulable_def isRunnable_def[symmetric] threadGet_def[symmetric] + gets_the_if_distrib ohaskell_state_assert_def gets_the_ostate_assert) + apply (subst gets_the_obind scActive_def[symmetric] inReleaseQueue_def[symmetric] + fun_app_def Nondet_Reader_Option.gets_the_return)+ apply (ctac add: isRunnable_ccorres) apply (rename_tac runnable) apply csymbr - apply (rule ccorres_pre_threadGet) + apply (rule ccorres_pre_threadGet, rename_tac scPtrOpt) apply clarsimp apply (rule_tac P="to_bool runnable" in ccorres_cases; clarsimp simp: to_bool_def) apply ccorres_rewrite apply (rule ccorres_move_c_guard_tcb) - apply (rule ccorres_stateAssert) + apply (rule ccorres_stateAssert[simplified HaskellLib_H.stateAssert_def]) apply (rule_tac xf'=ret__int_' and val="from_bool (scPtrOpt \ None)" and R="\s. obj_at' (\tcb. tcbSchedContext tcb = scPtrOpt) tcbPtr s @@ -1832,7 +1832,7 @@ lemma isSchedulable_ccorres [corres]: apply (rule ccorres_cond_true) apply (rule ccorres_rhs_assoc) apply (rule ccorres_move_c_guard_tcb) - apply (clarsimp simp: inReleaseQueue_def) + apply (clarsimp simp: inReleaseQueue_def readInReleaseQueue_def simp flip: threadGet_def) apply (rule_tac r'="\rv rv'. rv = to_bool rv'" and xf'="ret__unsigned_longlong_'" in ccorres_split_nothrow) apply (rule threadGet_vcg_corres) @@ -1860,7 +1860,7 @@ lemma isSchedulable_ccorres [corres]: apply (rule ccorres_cond_seq) apply (rule ccorres_cond_false) apply ccorres_rewrite - apply (rule ccorres_stateAssert) + apply (rule ccorres_stateAssert[simplified HaskellLib_H.stateAssert_def]) apply (rule ccorres_if_lhs) apply (fastforce intro: ccorres_return_C) apply clarsimp @@ -1913,7 +1913,7 @@ lemma rescheduleRequired_ccorres: apply (clarsimp simp: to_bool_def split: if_split) apply (ctac add: tcbSchedEnqueue_ccorres) apply (rule ccorres_return_Skip) - apply (wpsimp wp: isSchedulable_wp) + apply (wpsimp wp: getSchedulable_wp) apply (vcg exspec=isSchedulable_modifies) apply (clarsimp simp: to_bool_def) apply (rule ccorres_cond_false) @@ -2239,7 +2239,7 @@ lemma possibleSwitchTo_ccorres: and xf'=ret__int_' and P'="\\ret__int = from_bool (\scPtr. scOpt = Some scPtr)\" in ccorres_split_nothrow) - apply (clarsimp simp: inReleaseQueue_def) + apply (clarsimp simp: inReleaseQueue_def readInReleaseQueue_def simp flip: threadGet_def) apply (rule threadGet_vcg_corres_P_P') apply (rule allI, rule conseqPre, vcg) apply clarsimp @@ -2327,7 +2327,7 @@ lemma scheduleTCB_ccorres: apply (fastforce simp: to_bool_def) apply (ctac (no_vcg) add: rescheduleRequired_ccorres) apply (rule ccorres_return_Skip) - apply (wpsimp wp: isSchedulable_wp) + apply (wpsimp wp: getSchedulable_wp) apply ccorres_rewrite apply (rule ccorres_cond_false) apply (rule ccorres_symb_exec_l') @@ -2423,7 +2423,7 @@ lemma scheduleTCB_ccorres_simple: apply (fastforce simp: to_bool_def) apply (ctac (no_vcg) add: rescheduleRequired_ccorres_simple) apply (rule ccorres_return_Skip) - apply (wpsimp wp: isSchedulable_wp) + apply (wpsimp wp: getSchedulable_wp) apply ccorres_rewrite apply (rule ccorres_cond_false) apply (rule ccorres_symb_exec_l') diff --git a/proof/crefine/RISCV64/IsolatedThreadAction.thy b/proof/crefine/RISCV64/IsolatedThreadAction.thy index 8cf5825d06..542b725ee4 100644 --- a/proof/crefine/RISCV64/IsolatedThreadAction.thy +++ b/proof/crefine/RISCV64/IsolatedThreadAction.thy @@ -854,7 +854,8 @@ lemma oblivious_switchToThread_schact: getCurThread_def setCurThread_def liftM_def threadSet_def tcbSchedEnqueue_def unless_when asUser_def getQueue_def setQueue_def storeWordUser_def setRegister_def - pointerInUserData_def isRunnable_def isStopped_def threadGet_getObject + pointerInUserData_def isRunnable_def readRunnable_def threadGet_def[symmetric] + isStopped_def threadGet_getObject getThreadState_def tcbSchedDequeue_def bitmap_fun_defs ready_qs_runnable_def ready_or_release'_asrt_def ksReadyQueues_asrt_def) by (safe intro!: oblivious_bind oblivious_tcbQueueRemove @@ -1482,13 +1483,14 @@ lemma lookupIPCBuffer_isolatable: apply (simp add: assert_isolatable thread_actions_isolatable_return | wp)+ done -crunch isSchedulable +crunch getSchedulable for (empty_fail) empty_fail[wp] lemma setThreadState_rewrite_simple: "monadic_rewrite True True - (\s. ((runnable' st \ pred_map (\tcb. \ tcbInReleaseQueue tcb) (tcbs_of' s) (ksCurThread s) - \ pred_map (\scPtr. isScActive scPtr s) (tcbSCs_of s) (ksCurThread s)) + (\s. ((runnable' st + \ ((\sc. 0 < scRefillMax sc) |< (tcbs_of' s |> tcbSchedContext |> scs_of' s)) (ksCurThread s) + \ (Not \ tcbInReleaseQueue |< tcbs_of' s) (ksCurThread s)) \ ksSchedulerAction s \ ResumeCurrentThread \ t \ ksCurThread s) \ tcb_at' t s) (setThreadState st t) @@ -1497,18 +1499,17 @@ lemma setThreadState_rewrite_simple: apply (simp add: setThreadState_def scheduleTCB_def when_def) apply (monadic_rewrite_l monadic_rewrite_if_l_False \wpsimp wp: hoare_vcg_disj_lift hoare_vcg_imp_lift' threadSet_tcbState_st_tcb_at' - isSchedulable_wp threadSet_wp\) + getSchedulable_wp threadSet_wp\) (* take the threadSet, drop everything until return () *) apply (rule monadic_rewrite_trans[OF monadic_rewrite_bind_tail]) apply (rule monadic_rewrite_symb_exec_l_drop)+ apply (rule monadic_rewrite_refl) apply (wpsimp simp: getCurThread_def - wp: hoare_vcg_disj_lift hoare_vcg_imp_lift' threadSet_tcbState_st_tcb_at')+ + wp: hoare_vcg_disj_lift hoare_vcg_imp_lift' threadSet_tcbState_st_tcb_at')+ apply (rule monadic_rewrite_refl) - apply (clarsimp simp: isSchedulable_bool_def pred_map_simps obj_at_simps vs_all_heap_simps - opt_map_def isScActive_def - split: option.splits if_splits) - by (metis Structures_H.kernel_object.distinct(75) map_upd_eqD1) + apply (fastforce simp: schedulable'_def obj_at_simps opt_map_def opt_pred_def + split: option.splits if_splits) + done end diff --git a/proof/crefine/RISCV64/Refine_C.thy b/proof/crefine/RISCV64/Refine_C.thy index 4ba4f0efae..6b3968736d 100644 --- a/proof/crefine/RISCV64/Refine_C.thy +++ b/proof/crefine/RISCV64/Refine_C.thy @@ -1048,36 +1048,22 @@ lemma refinement2_both: simp add: sch_act_simple_def) apply (clarsimp simp: ex_abs_def full_invs_def) apply (intro conjI) - apply (frule_tac s=abstract_state in invs_sym_refs) - apply (frule_tac s'=haskell_state in state_refs_of_cross_eq) - apply fastforce - apply fastforce - apply force - apply clarsimp - apply (erule (1) ct_running_cross) - apply fastforce - apply fastforce - apply (rule ct_running_or_idle_cross; simp?; fastforce) - apply (prop_tac "cur_sc abstract_state = ksCurSc haskell_state", - fastforce dest!: state_relationD) - apply (prop_tac "sc_at (cur_sc abstract_state) abstract_state") - apply (rule cur_sc_tcb_sc_at_cur_sc[OF invs_valid_objs invs_cur_sc_tcb]; simp) - apply (prop_tac "sc_at' (ksCurSc haskell_state) haskell_state") - apply (rule sc_at_cross[OF state_relation_pspace_relation invs_psp_aligned invs_distinct]; simp) - apply (prop_tac "is_active_sc' (ksCurSc haskell_state) haskell_state") - apply (rule is_active_sc'2_cross[OF _ invs_psp_aligned invs_distinct], simp+) - apply (clarsimp simp: invs'_def valid_pspace'_def) - apply (rule sym_refs_tcbSCs; simp?) - apply (clarsimp simp: invs_def valid_state_def valid_pspace_def state_refs_of_cross_eq) - apply (fastforce dest!: cur_sc_tcb_cross[simplified schact_is_rct_def] - simp: invs_def valid_state_def valid_pspace_def) - apply (prop_tac "cur_tcb' haskell_state") - apply (rule cur_tcb_cross[OF invs_cur invs_psp_aligned invs_distinct]; simp?) - apply (frule_tac s=abstract_state and s'=haskell_state in ct_not_in_release_q_cross) + apply (frule_tac s=abstract_state in invs_sym_refs) + apply (frule_tac s'=haskell_state in state_refs_of_cross_eq) + apply fastforce apply fastforce - apply (clarsimp simp: cur_tcb'_def dest!: state_relationD) - apply fastforce - apply fastforce + apply clarsimp + apply (erule (1) ct_running_cross) + apply fastforce + apply fastforce + apply (rule ct_running_or_idle_cross; simp?; fastforce) + apply (frule curthread_relation) + apply clarsimp + apply (erule schedulable_schedulable'_eq[THEN iffD1], fastforce+) + apply (clarsimp simp: schedulable_def2) + apply (rule conjI) + apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def) + apply (force elim!: schact_is_rct_ct_active_sc) apply (frule_tac a=abstract_state in resume_cur_thread_cross; fastforce) apply (clarsimp simp: state_relation_def) apply (fastforce simp: ct_running'_C) diff --git a/proof/crefine/RISCV64/Schedule_C.thy b/proof/crefine/RISCV64/Schedule_C.thy index 39d500c4f6..7deec0662d 100644 --- a/proof/crefine/RISCV64/Schedule_C.thy +++ b/proof/crefine/RISCV64/Schedule_C.thy @@ -105,7 +105,7 @@ lemma threadGet_exs_valid[wp]: lemma isRunnable_exs_valid[wp]: "tcb_at' t s \ \(=) s\ isRunnable t \\\r. (=) s\" - unfolding isRunnable_def getThreadState_def + apply (clarsimp simp: isRunnable_def readRunnable_def simp flip: threadGet_def) by (wpsimp wp: exs_getObject) (* FIXME: move *) @@ -313,7 +313,7 @@ proof - apply assumption apply (rule conseqPre, vcg) apply clarsimp - apply (wpsimp wp: isSchedulable_wp)+ + apply (wpsimp wp: getSchedulable_wp)+ apply (clarsimp simp: Let_def guard_is_UNIV_def ctcb_queue_relation_def option_to_ctcb_ptr_def cready_queues_index_to_C_def numPriorities_def le_maxDomain_eq_less_numDomains unat_trans_ucast_helper queue_in_range diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy index 2967444e25..26e2e8870b 100644 --- a/proof/crefine/RISCV64/Tcb_C.thy +++ b/proof/crefine/RISCV64/Tcb_C.thy @@ -1210,7 +1210,7 @@ crunch schedContextResume crunch schedContextResume for tcbDomain[wp]: "obj_at' (\tcb. P (tcbDomain tcb)) t" - (wp: isSchedulable_wp simp: crunch_simps) + (wp: getSchedulable_wp simp: crunch_simps) lemma schedContextResume_sch_act_wf[wp]: "schedContextResume scPtr \\s. sch_act_wf (ksSchedulerAction s) s\" diff --git a/proof/invariant-abstract/AInvs.thy b/proof/invariant-abstract/AInvs.thy index 0a413a00cb..6345a77971 100644 --- a/proof/invariant-abstract/AInvs.thy +++ b/proof/invariant-abstract/AInvs.thy @@ -29,13 +29,12 @@ lemma pred_tcb_at_upd_apply: lemma thread_set_tcb_arch_ct_schedulable[wp]: "thread_set (\tcb. tcb\tcb_arch := arch_tcb_context_set us (tcb_arch tcb)\) t \ct_schedulable\" + apply (clarsimp simp: schedulable_def) apply (simp add: thread_set_def) apply (rule bind_wp[OF _ assert_get_tcb_ko']) apply (wpsimp wp: set_object_wp) - apply (fastforce simp: schedulable_def is_sc_active_def get_tcb_def ko_atD - in_release_queue_def - split: option.splits ) - done + by (fastforce simp: obj_at_def opt_pred_def opt_map_def tcbs_of_kh_def scs_of_kh_def + split: option.splits) lemma thread_set_tcb_arch_ct_not_running[wp]: "thread_set (\tcb. tcb\tcb_arch := arch_tcb_context_set us (tcb_arch tcb)\) t \\s. \ ct_running s\" @@ -53,7 +52,7 @@ lemma akernel_invs: (call_kernel e) :: (unit, unit) s_monad \\_ s. invs s \ (ct_running s \ ct_idle s)\" unfolding call_kernel_def preemption_path_def - apply (wpsimp wp: activate_invs check_budget_invs charge_budget_invs is_schedulable_wp + apply (wpsimp wp: activate_invs check_budget_invs charge_budget_invs update_time_stamp_invs hoare_drop_imps hoare_vcg_all_lift hoare_vcg_if_lift2) apply (fastforce intro: schact_is_rct_ct_active_sc simp: schedulable_def2 ct_in_state_def pred_tcb_at_def obj_at_def) @@ -65,7 +64,7 @@ lemma akernel_invs_det_ext: (call_kernel e) :: (unit, det_ext) s_monad \\_ s. invs s \ (ct_running s \ ct_idle s)\" unfolding call_kernel_def preemption_path_def - apply (wpsimp wp: activate_invs check_budget_invs charge_budget_invs is_schedulable_wp + apply (wpsimp wp: activate_invs check_budget_invs charge_budget_invs update_time_stamp_invs hoare_drop_imps hoare_vcg_all_lift hoare_vcg_if_lift2) apply (fastforce intro: schact_is_rct_ct_active_sc simp: schedulable_def2 ct_in_state_def pred_tcb_at_def obj_at_def) @@ -151,7 +150,7 @@ lemma schedule_ct_activateable: apply (wpsimp simp: schedule_switch_thread_fastfail_def tcb_sched_action_def set_tcb_queue_def get_tcb_queue_def wp: thread_get_wp' stt_activatable) - apply (wp add: is_schedulable_wp)+ + apply wp+ apply (rule hoare_strengthen_post[where Q'="\_. invs and valid_sched"]) apply wp apply (subgoal_tac "\x. scheduler_action s = switch_thread x \ st_tcb_at activatable x s") @@ -174,15 +173,13 @@ crunch send_signal, do_reply_transfer, invoke_irq_control, invoke_irq_handler, s lemma sched_context_yield_to_is_active_sc[wp]: "sched_context_yield_to sc_ptr' buffer \\s. P (is_active_sc sc_ptr s)\" - apply (clarsimp simp: sched_context_yield_to_def) - apply (wpsimp wp: is_schedulable_wp hoare_drop_imps) - done + unfolding sched_context_yield_to_def + by (wpsimp wp: hoare_drop_imps) lemma sched_context_bind_tcb_is_active_sc[wp]: "sched_context_bind_tcb sc_ptr' tcb_ptr \\s. P (is_active_sc sc_ptr s)\" - apply (clarsimp simp: sched_context_bind_tcb_def if_cond_refill_unblock_check_def) - apply (wpsimp wp: is_schedulable_wp hoare_drop_imps) - done + unfolding sched_context_bind_tcb_def if_cond_refill_unblock_check_def + by (wpsimp wp: hoare_drop_imps) crunch handle_fault, check_budget_restart, charge_budget, handle_interrupt, preemption_path for is_active_sc[wp]: "\s. P (is_active_sc sc_ptr s)" @@ -226,7 +223,7 @@ lemma invoke_sched_context_cur_sc_tcb_are_bound_imp_cur_sc_active: lemma set_thread_state_schact_is_not_rct[wp]: "set_thread_state ref ts \\s. \ schact_is_rct s\" apply (clarsimp simp: set_thread_state_def set_thread_state_act_def) - apply (wpsimp wp: set_scheduler_action_wp is_schedulable_wp set_object_wp) + apply (wpsimp wp: set_scheduler_action_wp set_object_wp) apply (clarsimp simp: schact_is_rct_def) done @@ -586,14 +583,13 @@ lemma choose_thread_active_sc_tcb_at_cur_thread: apply (clarsimp simp: guarded_switch_to_def) apply (rule bind_wp[OF _ thread_get_sp]) apply (rule bind_wp[OF _ assert_opt_sp]) - apply (rule bind_wp[OF _ is_schedulable_sp]) + apply (rule bind_wp[OF _ gets_sp]) apply (rule bind_wp[OF _ assert_sp]) apply (wpsimp wp: switch_to_thread_active_sc_tcb_at_cur_thread hoare_vcg_imp_lift') apply (frule hd_max_non_empty_queue_in_ready_queues) apply (prop_tac "tcb_at (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s") apply (clarsimp simp: obj_at_def is_tcb_def) - apply (frule schedulable_unfold) - apply (clarsimp simp: vs_all_heap_simps obj_at_def pred_tcb_at_def is_sc_active_def2) + apply (clarsimp simp: vs_all_heap_simps obj_at_def pred_tcb_at_def schedulable_def2) done lemma schedule_choose_new_thread_active_sc_tcb_at_cur_thread: @@ -621,9 +617,7 @@ lemma schedule_cur_sc_active: apply (clarsimp simp: schedule_def) apply (rule bind_wp_fwd_skip, wpsimp wp: awaken_valid_sched hoare_vcg_imp_lift') apply (rule bind_wp_fwd_skip, wpsimp wp: hoare_vcg_imp_lift' cur_sc_active_lift) - apply (rule bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ is_schedulable_sp]) - apply (rule bind_wp[OF _ gets_sp], rename_tac action) + apply (rule bind_wp[OF _ gets_sp])+ apply (rule bind_wp[OF sc_and_timer_cur_sc_active]) apply (case_tac action; clarsimp) apply wpsimp @@ -761,8 +755,7 @@ lemma sched_context_bind_tcb_schact_is_rct_imp_ct_not_in_release_q: apply (rule_tac Q'="\_ s. scheduler_action s = choose_new_thread" in hoare_post_imp) apply (clarsimp simp: schact_is_rct_def) apply (wpsimp wp: reschedule_cnt) - apply wpsimp - apply (wpsimp wp: is_schedulable_wp) + apply wpsimp+ apply (wpsimp wp: hoare_drop_imps sched_context_resume_ct_not_in_release_q update_sched_context_wp set_object_wp simp: set_tcb_obj_ref_def)+ @@ -1241,9 +1234,7 @@ lemma schedule_ct_not_in_release_q: apply (clarsimp simp: schedule_def) apply (rule bind_wp_fwd_skip, wpsimp wp: awaken_valid_sched hoare_vcg_imp_lift') apply (rule bind_wp_fwd_skip, wpsimp wp: hoare_vcg_imp_lift' cur_sc_active_lift) - apply (rule bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ is_schedulable_sp']) - apply (rule bind_wp[OF _ gets_sp], rename_tac action) + apply (rule bind_wp[OF _ gets_sp])+ apply (rule bind_wp) apply wpsimp apply (case_tac action; clarsimp) @@ -1286,10 +1277,9 @@ lemma set_thread_state_Running_schact_is_rct: apply (rule bind_wp[OF _ gets_the_get_tcb_sp]) apply (rule_tac Q'="\_ s. ?pre s \ st_tcb_at ((=) Running) thread s" in bind_wp_fwd) apply (wpsimp simp: set_scheduler_action_def - wp: is_schedulable_wp hoare_vcg_if_lift2 set_object_wp) + wp: hoare_vcg_if_lift2 set_object_wp) apply (clarsimp simp: vs_all_heap_simps pred_tcb_at_def obj_at_def) apply (intro bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ is_schedulable_sp']) apply (rule hoare_when_cases) apply (clarsimp simp: schact_is_rct_def) apply (fastforce intro: st_tcb_weakenE hoare_pre_cont hoare_weaken_pre @@ -1359,7 +1349,7 @@ lemma set_thread_state_schact_is_rct_imp_ct_activatable[wp]: "set_thread_state ref ts \\s. schact_is_rct s \ ct_in_state activatable s\" apply (clarsimp simp: set_thread_state_def set_thread_state_act_def) apply (wpsimp simp: set_scheduler_action_def - wp: is_schedulable_wp set_object_wp) + wp: set_object_wp) apply (clarsimp simp: schact_is_rct_def ct_in_state_def pred_tcb_at_def obj_at_def schedulable_def2 get_tcb_def) done @@ -2270,8 +2260,7 @@ lemma choose_thread_cur_sc_offset_ready_and_sufficient: apply fastforce apply wpsimp apply (clarsimp simp: guarded_switch_to_def) - apply (wpsimp wp: switch_to_thread_cur_sc_offset_ready_and_sufficient is_schedulable_wp - thread_get_wp) + apply (wpsimp wp: switch_to_thread_cur_sc_offset_ready_and_sufficient thread_get_wp) apply (clarsimp simp: obj_at_def) apply (frule hd_max_non_empty_queue_in_ready_queues) apply (fastforce simp: valid_ready_qs_def vs_all_heap_simps in_ready_q_def) @@ -2353,7 +2342,7 @@ lemma choose_thread_ct_not_idle_imp_ct_released[wp]: apply (rule_tac Q'="\_ s. cur_thread s = idle_thread s" in hoare_post_imp) apply fastforce apply wpsimp - apply (wpsimp wp: is_schedulable_wp thread_get_wp hoare_drop_imps) + apply (wpsimp wp: thread_get_wp hoare_drop_imps) apply (clarsimp simp: obj_at_def vs_all_heap_simps valid_ready_qs_def) apply (frule hd_max_non_empty_queue_in_ready_queues) apply (fastforce simp: valid_ready_qs_def vs_all_heap_simps in_ready_q_def) @@ -2415,9 +2404,7 @@ lemma schedule_cur_sc_offset_ready_and_sufficient: apply fastforce apply (rule bind_wp_fwd_skip) apply (wpsimp wp: hoare_vcg_imp_lift' awaken_valid_sched hoare_vcg_ex_lift awaken_valid_sched) - apply (rule bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ is_schedulable_sp']) - apply (rule bind_wp[OF _ gets_sp]) + apply (rule bind_wp[OF _ gets_sp])+ apply (simp flip: bind_assoc) apply (rule bind_wp[OF sc_and_timer_cur_sc_offset_ready_and_sufficient_consumed_time]) apply (intro hoare_vcg_conj_lift_pre_fix) @@ -2560,9 +2547,8 @@ crunch schedule, activate_thread lemma preemption_path_valid_machine_time[wp]: "preemption_path \\s :: det_state. valid_machine_time s\" - apply (clarsimp simp: preemption_path_def) - apply (wpsimp wp: getActiveIRQ_wp is_schedulable_inv hoare_drop_imps) - done + unfolding preemption_path_def + by (wpsimp wp: getActiveIRQ_wp hoare_drop_imps) crunch call_kernel for valid_machine_time[wp]: "\s :: det_state. valid_machine_time s" diff --git a/proof/invariant-abstract/BCorres_AI.thy b/proof/invariant-abstract/BCorres_AI.thy index b0fc8df584..6269c85e07 100644 --- a/proof/invariant-abstract/BCorres_AI.thy +++ b/proof/invariant-abstract/BCorres_AI.thy @@ -157,6 +157,10 @@ lemma in_release_queue_truncate[simp]: "in_release_queue t (truncate_state s) = in_release_queue t s" by (simp add: in_release_queue_def) +lemma schedulable_truncate[simp]: + "schedulable t (truncate_state s) = schedulable t s" + by (simp add: schedulable_def) + lemma gets_the_tcb_bcorres[wp]: "bcorres (gets_the (get_tcb t)) (gets_the (get_tcb t))" unfolding gets_the_def by wpsimp diff --git a/proof/invariant-abstract/CSpaceInv_AI.thy b/proof/invariant-abstract/CSpaceInv_AI.thy index 4386096fc9..4bf6699ffc 100644 --- a/proof/invariant-abstract/CSpaceInv_AI.thy +++ b/proof/invariant-abstract/CSpaceInv_AI.thy @@ -84,10 +84,6 @@ lemma get_sk_obj_ref_inv[wp]: apply wpsimp done -lemma gets_the_sp: - "\ Q \ gets_the f \\rv s. f s = Some rv \ Q s\" - by wpsimp - lemma gets_the_get_tcb_sp: "\ Q \ gets_the (get_tcb thread) \\t. Q and ko_at (TCB t) thread\" by wpsimp diff --git a/proof/invariant-abstract/DetSchedAux_AI.thy b/proof/invariant-abstract/DetSchedAux_AI.thy index a709bb0b24..7b5dabe1f6 100644 --- a/proof/invariant-abstract/DetSchedAux_AI.thy +++ b/proof/invariant-abstract/DetSchedAux_AI.thy @@ -76,10 +76,6 @@ crunch update_cdt_list for valid_sched_pred[wp]: "valid_sched_pred_strong P" (wp: dxo_wp_weak crunch_wps) -lemma (in pspace_update_eq) is_sc_active_eq[iff]: - "is_sc_active t (f s) = is_sc_active t s" - using pspace by (simp add: is_sc_active_def) - lemma store_word_offs_valid_sched_pred[wp]: "store_word_offs ptr offs v \valid_sched_pred_strong P\" by (wpsimp simp: store_word_offs_def wp: dmo_valid_sched_pred) @@ -110,14 +106,6 @@ lemma set_mrs_valid_sched_pred[wp]: global_interpretation set_mrs: valid_sched_pred_locale _ "set_mrs r t mrs" by unfold_locales wp -lemma set_cap_is_sc_active[wp]: - "\is_sc_active t\ set_cap c p \\rv. is_sc_active t\" - apply (simp add: set_cap_def set_object_def split_def) - apply (wp get_object_wp | wpc)+ - apply (clarsimp simp: is_sc_active_def obj_at_def - | intro impI conjI | rule_tac x=scp in exI)+ - done - global_interpretation set_cap: valid_sched_pred_locale _ "set_cap c p" by unfold_locales wp @@ -1448,9 +1436,6 @@ lemma set_tcb_queue_wp: \\_. P\" by (wpsimp simp: set_tcb_queue_def) (auto elim!: rsubst[of P]) -lemma get_tcb_queue_wp[wp]: "\\s. P (ready_queues s t p) s\ get_tcb_queue t p \P\" - by (wpsimp simp: get_tcb_queue_def) - lemma enqueue_distinct[intro!]: "distinct queue \ distinct (tcb_sched_enqueue thread queue)" by (simp add: tcb_sched_enqueue_def) @@ -1733,18 +1718,6 @@ lemma valid_blocked_except_set_switch_thread: (* end : valid_blocked_except \ valid_blocked lemmas *) -lemma schedulable_unfold2: - "((is_schedulable_opt tp s) = Some X) - \ tcb_at tp s - \ (X = (st_tcb_at runnable tp s \ active_sc_tcb_at tp s \ \(in_release_queue tp s)))" - by (clarsimp simp: is_schedulable_opt_def obj_at_kh_kheap_simps vs_all_heap_simps - split: option.splits) - -lemma is_sc_active_detype[simp]: - "(is_sc_active t (detype S s)) - = (is_sc_active t s \ t \ S)" - by (clarsimp simp add: is_sc_active_def detype_def) - lemma bound_sc_obj_tcb_at_detype: "bound_sc_obj_tcb_at (P s) t (detype S s) \ bound_sc_obj_tcb_at (P s) t s diff --git a/proof/invariant-abstract/DetSchedDomainTime_AI.thy b/proof/invariant-abstract/DetSchedDomainTime_AI.thy index 1ce4ce8ca3..53ac9e8092 100644 --- a/proof/invariant-abstract/DetSchedDomainTime_AI.thy +++ b/proof/invariant-abstract/DetSchedDomainTime_AI.thy @@ -344,7 +344,7 @@ lemma call_kernel_domain_list_inv_det_ext: unfolding call_kernel_def preemption_path_def apply (wp) apply (simp add: schedule_def) - apply (wpsimp wp: without_preemption_wp is_schedulable_wp hoare_vcg_all_lift hoare_drop_imps + apply (wpsimp wp: without_preemption_wp hoare_vcg_all_lift hoare_drop_imps simp: if_apply_def2)+ done @@ -409,11 +409,10 @@ lemma schedule_domain_time_left: \ valid_domain_list s" in bind_wp_fwd) apply wpsimp - apply clarsimp apply (rule bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ is_schedulable_sp]) + apply (rule bind_wp[OF _ gets_sp]) apply (rule bind_wp[OF _ gets_sp], rename_tac action) - apply (case_tac action; wpsimp wp: is_schedulable_wp hoare_vcg_const_imp_lift hoare_drop_imps) + apply (case_tac action; wpsimp wp: hoare_vcg_const_imp_lift hoare_drop_imps) done end diff --git a/proof/invariant-abstract/DetSchedInvs_AI.thy b/proof/invariant-abstract/DetSchedInvs_AI.thy index 3ac4fd3e0f..a4bf1c4e9e 100644 --- a/proof/invariant-abstract/DetSchedInvs_AI.thy +++ b/proof/invariant-abstract/DetSchedInvs_AI.thy @@ -588,25 +588,6 @@ end \ \Project threads from the kernel heap\ -definition tcb_of :: "kernel_object \ tcb" where - "tcb_of ko \ case ko of TCB tcb \ Some tcb | _ \ None" - -lemmas tcb_of_simps [simp] = tcb_of_def [split_simps kernel_object.split] - -lemma tcb_of_Some[simp]: - "tcb_of ko = Some tcb \ ko = TCB tcb" - by (cases ko; simp) - -lemma tcb_of_None: - "tcb_of ko = None \ (\tcb. ko \ TCB tcb)" - by (cases ko; simp) - -definition tcbs_of_kh :: "('obj_ref \ kernel_object) \ 'obj_ref \ tcb" where - "tcbs_of_kh kh \ kh |> tcb_of" - -abbreviation tcbs_of :: "'z state \ obj_ref \ tcb" where - "tcbs_of s \ tcbs_of_kh (kheap s)" - lemmas tcb_heap_of_state_def = tcbs_of_kh_def[of "kheap s" for s :: "'z state"] global_interpretation tcb_heap: opt_map_cons_def_locale _ tcb_of tcbs_of_kh TCB @@ -722,25 +703,6 @@ abbreviation prios_of :: "'z state \ obj_ref \ prior \ \Project scheduling contexts from the kernel heap\ -definition sc_of :: "kernel_object \ sched_context" where - "sc_of ko \ case ko of SchedContext sc _ \ Some sc | _ \ None" - -lemmas sc_of_simps [simp] = sc_of_def [split_simps kernel_object.split] - -lemma sc_of_Some[simp]: - "sc_of ko = Some sc \ (\n. ko = SchedContext sc n)" - by (cases ko; simp) - -lemma sc_of_None: - "sc_of ko = None \ (\sc n. ko \ SchedContext sc n)" - by (cases ko; simp) - -definition scs_of_kh :: "('obj_ref \ kernel_object) \ 'obj_ref \ sched_context" where - "scs_of_kh kh \ kh |> sc_of" - -abbreviation scs_of :: "'z state \ obj_ref \ sched_context" where - "scs_of s \ scs_of_kh (kheap s)" - lemmas sc_heap_of_state_def = scs_of_kh_def[of "kheap s" for s :: "'z state"] global_interpretation sc_heap: opt_map_cons2_def_locale _ sc_of scs_of_kh SchedContext @@ -1426,11 +1388,6 @@ abbreviation active_scrc :: "sc_refill_cfg \ bool" where lemmas active_scrc_def = active_sc_def -lemma is_sc_active_kh_simp[obj_at_kh_kheap_simps]: - "is_sc_active scp s = pred_map active_scrc (sc_refill_cfgs_of s) scp" - by (auto simp: is_sc_active_def vs_all_heap_simps - split: option.splits kernel_object.splits) - abbreviation is_active_sc :: "obj_ref \ 'z state \ bool" where "is_active_sc scp s \ pred_map active_scrc (sc_refill_cfgs_of s) scp" @@ -1612,15 +1569,10 @@ abbreviation bound_sc_obj_tcb_at_kh :: "(sc_refill_cfg \ bool) \ bool) \ obj_ref \ 'z state \ bool" where "bound_sc_obj_tcb_at P t s \ pred_map2' P (tcb_scps_of s) (sc_refill_cfgs_of s) t" -lemma is_schedulable_opt_Some: - "is_schedulable_opt t s = Some X \ - st_tcb_at runnable t s \ active_sc_tcb_at t s \ \ (in_release_queue t s) \ X" - by (clarsimp simp: is_schedulable_opt_def vs_all_heap_simps obj_at_kh_kheap_simps - split: option.splits) - lemma schedulable_def2: "schedulable t s = (st_tcb_at runnable t s \ active_sc_tcb_at t s \ \ (in_release_queue t s))" by (clarsimp simp: schedulable_def vs_all_heap_simps obj_at_kh_kheap_simps + opt_pred_def opt_map_def pred_map_def map_join_def in_release_queue_def split: option.splits) \ \Like refill_ready', but using unat addition to avoid the need to reason about overflow.\ @@ -3831,10 +3783,7 @@ lemma budget_ready_def3: lemma active_sc_tcb_at_fold: "(\scp. bound_sc_tcb_at (\x. x = Some scp) t s \ sc_at_pred sc_active scp s) = active_sc_tcb_at t s" - apply (intro iffI) - apply (clarsimp simp: pred_tcb_at_def sc_at_pred_n_def obj_at_def vs_all_heap_simps is_sc_active_def2 split: option.splits) - apply (fastforce simp: pred_tcb_at_def sc_at_pred_n_def obj_at_def vs_all_heap_simps is_sc_active_def2 split: option.splits) - done + by (fastforce simp: pred_tcb_at_def sc_at_pred_n_def obj_at_def vs_all_heap_simps) (* valid_refills for tcb_scps_of *) definition diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index c2ba20e2a4..dc2d2e6007 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -688,14 +688,14 @@ lemma schedule_tcb_choose_new_thread_rewrite: "monadic_rewrite False True \ (schedule_tcb t) (do cur \ gets cur_thread; sched_act \ gets scheduler_action; - schedulable \ is_schedulable t; + schedulable \ gets (schedulable t); when (t = cur \ sched_act = resume_cur_thread \ \schedulable) $ set_scheduler_action choose_new_thread od)" apply (simp add: schedule_tcb_def) apply (rule monadic_rewrite_bind_tail[OF _ gets_inv]) apply (rule monadic_rewrite_bind_tail[OF _ hoare_gets_sp], simp) - apply (rule monadic_rewrite_bind_tail[OF _ is_schedulable_inv]) + apply (rule monadic_rewrite_bind_tail[OF _ gets_inv]) apply (simp add: when_def split del: if_split) apply (rule monadic_rewrite_guard_imp[OF monadic_rewrite_if]) apply (rule reschedule_required_resume_cur_thread_choose_new_thread_rewrite) @@ -704,12 +704,11 @@ lemma schedule_tcb_choose_new_thread_rewrite: lemmas schedule_tcb_def2 = monadic_rewrite_to_eq[OF schedule_tcb_choose_new_thread_rewrite] -(* FIXME RT: move near is_schedulable_wp *) -lemma is_schedulable_wp': - "\\s. P (pred_map runnable (tcb_sts_of s) t \ active_sc_tcb_at t s \ \ (in_release_queue t s)) s\ - is_schedulable t - \P\" - by (wpsimp wp: is_schedulable_wp) (auto simp: obj_at_kh_kheap_simps schedulable_def2) +lemma schedulable_def3: + "schedulable t s = (pred_map runnable (tcb_sts_of s) t \ active_sc_tcb_at t s \ \ (in_release_queue t s))" + by (clarsimp simp: schedulable_def vs_all_heap_simps obj_at_kh_kheap_simps + opt_pred_def opt_map_def pred_map_def map_join_def in_release_queue_def + split: option.splits) lemma schedule_tcb_wp: "\\s. if t = cur_thread s \ scheduler_action s = resume_cur_thread @@ -717,7 +716,7 @@ lemma schedule_tcb_wp: then P (s\scheduler_action := choose_new_thread\) else P s\ schedule_tcb t \\_. P\" - by (wpsimp simp: schedule_tcb_def2 wp: set_scheduler_action_wp is_schedulable_wp') + by (wpsimp simp: schedule_tcb_def2 schedulable_def3 wp: set_scheduler_action_wp) lemma schedule_tcb_valid_sched_misc[wp]: "schedule_tcb t \\s. P (cur_time s) (cur_domain s) (cur_thread s) (idle_thread s) @@ -771,8 +770,8 @@ abbreviation (input) reschedule_required_wp where lemma reschedule_required_wp[valid_sched_wp]: "\reschedule_required_wp P\ reschedule_required \\rv. P\" apply (wpsimp simp: reschedule_required_def - wp: set_scheduler_action_wp tcb_sched_action_wp thread_get_wp' is_schedulable_wp') - by (auto simp: vs_all_heap_simps obj_at_kh_kheap_simps) + wp: set_scheduler_action_wp tcb_sched_action_wp thread_get_wp') + by (auto simp: vs_all_heap_simps obj_at_kh_kheap_simps schedulable_def2) lemma reschedule_required_valid_sched_misc[wp]: "reschedule_required \\s. P (consumed_time s) (cur_sc s) (cur_time s) (cur_domain s) (cur_thread s) @@ -782,8 +781,8 @@ lemma reschedule_required_valid_sched_misc[wp]: lemma reschedule_required_ready_or_release[wp]: "reschedule_required \ready_or_release\" unfolding reschedule_required_def - apply (wpsimp wp: thread_get_wp is_schedulable_wp) - by (clarsimp simp: obj_at_def schedulable_def split: option.splits dest!: get_tcb_SomeD) + apply (wpsimp wp: thread_get_wp) + by (clarsimp simp: obj_at_def schedulable_def2 is_tcb_def pred_tcb_at_def split: option.splits) lemma reschedule_required_valid_ready_qs[wp]: "reschedule_required \valid_ready_qs\" @@ -794,7 +793,7 @@ lemma reschedule_required_lift: assumes B: "\P\ set_scheduler_action choose_new_thread \\_. P\" shows "\P\ reschedule_required \\_. P\" unfolding reschedule_required_def - by (wpsimp wp: A B is_schedulable_wp' thread_get_wp') + by (wpsimp wp: A B thread_get_wp') lemma reschedule_required_ct_not_in_q[wp]: "\\\ reschedule_required \\_. ct_not_in_q\" @@ -859,19 +858,6 @@ lemma reschedule_required_switch_ct_not_in_q[wp]: "\\\ reschedule_required \\_. not_cur_thread t\" by (wpsimp wp: valid_sched_wp) -lemma switch_thread_weak_valid_sched_action_is_schedulable: - "\scheduler_action s = switch_thread t; weak_valid_sched_action s\ - \ the (is_schedulable_opt t s)" - by (auto simp: is_schedulable_opt_def in_queue_2_def weak_valid_sched_action_def - obj_at_kh_kheap_simps vs_all_heap_simps - split: option.splits) - -lemma switch_thread_valid_sched_is_schedulable: - "\scheduler_action s = switch_thread t; valid_sched s\ - \ the (is_schedulable_opt t s)" - by (intro switch_thread_weak_valid_sched_action_is_schedulable - valid_sched_weak_valid_sched_action) - lemma reschedule_valid_sched_except_blocked_const: "reschedule_required \valid_sched_except_blocked\" apply (wpsimp wp: reschedule_required_valid_sched_except_blocked) @@ -989,7 +975,7 @@ lemma set_thread_state_act_wp[valid_sched_wp]: then P (s\scheduler_action := choose_new_thread\) else P s\ set_thread_state_act t \\rv. P\" - by (wpsimp simp: set_thread_state_act_def wp: set_scheduler_action_wp is_schedulable_wp') + by (wpsimp simp: set_thread_state_act_def schedulable_def3 wp: set_scheduler_action_wp) lemma set_thread_state_only_wp: "\\s. \tcb. kheap s t = Some (TCB tcb) @@ -1248,12 +1234,8 @@ lemma set_thread_state_Restart_valid_sched: lemma set_thread_state_act_sched_act_not[wp]: "\scheduler_act_not t\ set_thread_state_act tp \\_. scheduler_act_not t\" - apply (clarsimp simp: set_thread_state_act_def) - apply (rule bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ is_schedulable_inv]) - apply (wpsimp simp: set_scheduler_action_def) - done + unfolding set_thread_state_act_def set_scheduler_action_def + by wpsimp crunch set_thread_state for sched_act_not[wp]: "scheduler_act_not t" @@ -1269,12 +1251,21 @@ lemma set_thread_state_not_runnable_valid_ready_qs: lemma set_thread_state_not_runnable_valid_release_q: "\\s. valid_release_q s \ pred_map (\ts. \ runnable ts) (tcb_sts_of s) ref\ - set_thread_state ref ts + set_thread_state ref ts \\_. valid_release_q\" - apply (wpsimp simp: set_thread_state_def set_thread_state_act_def wp: set_object_wp, rename_tac tcb) - apply (simp add: vs_all_heap_simps obj_at_kh_kheap_simps) - apply (simp add: valid_release_q_def, elim conjE ballEI) - by (clarsimp simp add: vs_all_heap_simps) + apply (clarsimp simp: valid_release_q_def) + apply (intro hoare_vcg_conj_lift_pre_fix) + apply (wpsimp simp: set_thread_state_def set_thread_state_act_def wp: set_object_wp, rename_tac tcb) + apply (drule_tac x=t in bspec) + apply fastforce + apply (clarsimp simp: vs_all_heap_simps) + apply (rename_tac sc_ptr sc n) + apply (intro conjI impI; fastforce?) + apply (rule_tac x=sc_ptr in exI) + apply fastforce + apply wpsimp + apply (wpsimp wp: sorted_release_q_lift) + done lemma set_thread_state_valid_sched_except_blocked: "\\s. valid_sched_except_blocked s @@ -1305,8 +1296,8 @@ lemma set_thread_state_not_runnable_valid_sched_except_blocked: \\_. valid_sched_except_blocked\" apply (wpsimp wp: set_thread_state_valid_sched_except_blocked simp: valid_sched_def) apply (intro conjI; clarsimp) - apply (fastforce simp: valid_ready_qs_def in_queues_2_def vs_all_heap_simps) - apply (fastforce simp: valid_release_q_def in_queue_2_def vs_all_heap_simps) + subgoal by (fastforce simp: valid_ready_qs_def in_queues_2_def vs_all_heap_simps) + subgoal by (fastforce simp: valid_release_q_def in_queue_2_def vs_all_heap_simps) apply (clarsimp simp: valid_sched_action_def weak_valid_sched_action_def) done @@ -1443,10 +1434,6 @@ lemma set_tcb_obj_ref_sc_at_pred_n[wp]: "set_tcb_obj_ref f ref v \\s. R (sc_at_pred_n N proj P p s)\" by (wpsimp wp: set_tcb_obj_ref_wp simp: sc_at_pred_n_def obj_at_def) -lemma set_tcb_obj_ref_is_sc_active[wp]: - "set_tcb_obj_ref f ref tptr \\s. P (is_sc_active scp s)\" - by (wpsimp wp: set_tcb_obj_ref_wp simp: obj_at_kh_kheap_simps vs_all_heap_simps) - lemma set_tcb_obj_ref_is_refill_ready[wp]: "set_tcb_obj_ref f ref tptr \is_refill_ready scp\" by (wpsimp wp: set_tcb_obj_ref_wp simp: obj_at_kh_kheap_simps vs_all_heap_simps) @@ -1679,7 +1666,7 @@ lemma set_tcb_sched_context_valid_blocked_Some: lemma set_tcb_sched_context_valid_blocked: "\valid_blocked and (\s. case sc_opt of Some sp \ - not_queued t s \ not_in_release_q t s \ (\ st_tcb_at active t s) \ \ is_sc_active sp s + not_queued t s \ not_in_release_q t s \ (\ st_tcb_at active t s) \ \ is_active_sc sp s | _ \ True)\ set_tcb_obj_ref tcb_sched_context_update t sc_opt \\_. valid_blocked\" apply (wpsimp wp: set_tcb_obj_ref_wp) @@ -1812,9 +1799,10 @@ lemma set_tcb_sc_update_bound_sc_obj_tcb_at_neq: by (wpsimp wp: set_tcb_sc_update_bound_sc_obj_tcb_at_eq) lemma set_tcb_sc_update_active_sc_tcb_at_eq: - "\\s. P (active_sc_tcb_at t s) \ - (active_sc_tcb_at t s \ (\scp. scopt = Some scp \ is_sc_active scp s)) \ - set_tcb_obj_ref tcb_sched_context_update t scopt \\rv s. P (active_sc_tcb_at t s)\" + "\\s. P (active_sc_tcb_at t s) + \ (active_sc_tcb_at t s \ (\scp. scopt = Some scp \ is_active_sc scp s)) \ + set_tcb_obj_ref tcb_sched_context_update t scopt + \\_ s. P (active_sc_tcb_at t s)\" by (wpsimp simp: obj_at_kh_kheap_simps wp: set_tcb_sc_update_bound_sc_obj_tcb_at_eq) \ \update_sched_context, set_refills\ @@ -1983,20 +1971,12 @@ lemma set_refills_valid_sched_misc[wp]: apply (rule hoare_lift_Pf[where f=ntfns_of, rotated], wp valid_sched_wp) by (wpsimp simp: set_refills_def) -lemma update_sched_context_is_sc_active_indep: +lemma update_sched_context_is_active_sc_indep: "\sc. sc_active (f sc) \ sc_active sc - \ update_sched_context ref f \\s. P (is_sc_active scp s)\" + \ update_sched_context ref f \\s. P (is_active_sc scp s)\" apply (wpsimp simp: update_sched_context_def set_object_def wp: get_object_wp) - by (clarsimp simp: is_sc_active_def obj_at_def) - -lemma sc_tcb_update_is_sc_active[wp]: - "update_sched_context ref (sc_tcb_update f) \\s. P (is_sc_active scp s)\" - by (clarsimp simp: update_sched_context_is_sc_active_indep) - -lemma sc_replies_update_is_sc_active[wp]: - "update_sched_context ref (sc_replies_update f) \\s. P (is_sc_active t s)\" - by (clarsimp simp: update_sched_context_is_sc_active_indep) + by (clarsimp simp: vs_all_heap_simps obj_at_def) lemma update_sched_context_is_refill_sufficient_indep: "\sc. sc_refills (f sc) = sc_refills sc @@ -2651,7 +2631,7 @@ lemma guarded_switch_to_valid_sched_pred[valid_sched_wp]: guarded_switch_to t \\rv. valid_sched_pred_strong P :: 'state_ext state \ _\" by (wpsimp simp: guarded_switch_to_def released_sc_tcb_at_def - wp: valid_sched_wp thread_get_wp' is_schedulable_wp') + wp: valid_sched_wp thread_get_wp') lemma switch_to_thread_valid_sched_misc[wp]: "switch_to_thread t @@ -2770,7 +2750,7 @@ end lemma guarded_switch_to_lift: assumes "\P\ switch_to_thread thread \Q\" shows "\P\ guarded_switch_to thread \Q\" - by (wpsimp simp: guarded_switch_to_def wp: assms thread_get_wp' is_schedulable_wp') + by (wpsimp simp: guarded_switch_to_def wp: assms thread_get_wp') lemma next_domain_valid_idle[wp]: "\ valid_idle \ next_domain \ \_. valid_idle\" @@ -5355,13 +5335,9 @@ lemma unbind_from_sc_valid_sched_misc[wp]: crunch test_reschedule for valid_ready_qs[wp]: "valid_ready_qs" and valid_sched: "valid_sched" - and is_sc_active[wp]: "\s. P (is_sc_active p s)" + and is_active_sc[wp]: "\s. P (is_active_sc p s)" (wp: hoare_drop_imps hoare_vcg_if_lift2 reschedule_valid_sched_const) -crunch tcb_release_remove - for is_sc_active[wp]: "is_sc_active p" - (wp: hoare_drop_imps hoare_vcg_if_lift2) - lemma test_reschedule_not_queued[wp]: "\\s. not_queued t s \ scheduler_act_not t s\ test_reschedule thread @@ -5862,31 +5838,6 @@ crunch reply_unlink_tcb for simple_sched_action[wp]: simple_sched_action (wp: hoare_drop_imps) -lemma set_simple_ko_is_sc_active[wp]: - "set_simple_ko f p new \\s. P (is_sc_active t s)\" - apply (clarsimp simp: set_simple_ko_def) - apply (wpsimp simp: set_object_def wp: get_object_wp split: option.splits) - by (intro conjI impI; clarsimp elim!: rsubst[where P=P] split: if_splits kernel_object.splits - simp: a_type_def partial_inv_def obj_at_def is_sc_active_def) - -crunch set_thread_state_act, update_sk_obj_ref, get_sk_obj_ref - for is_sc_active[wp]: "\s. P (is_sc_active t s)" - (simp: set_scheduler_action_def) - -lemma set_thread_state_is_sc_active[wp]: - "set_thread_state st tp \\s. P (is_sc_active t s)\" - apply (clarsimp simp: set_thread_state_def) - apply (wpsimp simp: set_object_def wp: get_object_wp) - by (clarsimp simp: is_sc_active_def dest!: get_tcb_SomeD) - -lemma reply_unlink_sc_is_sc_active[wp]: - "reply_unlink_sc sp rp \\s. P (is_sc_active t s)\" - by (wpsimp wp: get_simple_ko_wp gts_wp simp: reply_unlink_sc_def) - -lemma reply_unlink_tcb_is_sc_active[wp]: - "reply_unlink_tcb tp rp \\s. P (is_sc_active t s)\" - by (wpsimp wp: get_simple_ko_wp gts_wp simp: reply_unlink_tcb_def) - lemma set_reply_obj_ref_no_tcb_update[wp]: "set_reply_obj_ref f rp new \ko_at (TCB tcb) t\" apply (clarsimp simp: update_sk_obj_ref_def set_simple_ko_def) @@ -5966,7 +5917,7 @@ lemma sched_context_donate_reply_tcb_reply_at_act_not: lemma valid_sched_not_schedulable_sc_not_queued: "\valid_sched s; \ schedulable tptr s; tcb_at tptr s\ \ in_release_queue tptr s \ not_queued tptr s" - by (fastforce simp: schedulable_def obj_at_kh_kheap_simps vs_all_heap_simps is_tcb + by (fastforce simp: schedulable_def2 obj_at_kh_kheap_simps vs_all_heap_simps is_tcb valid_sched_def valid_ready_qs_def in_ready_q_def split: option.splits) @@ -6641,9 +6592,9 @@ lemma test_possible_switch_to_valid_sched: else valid_sched s\ test_possible_switch_to target \\_. valid_sched\" - apply (wpsimp wp: possible_switch_to_valid_sched_strong is_schedulable_wp' + apply (wpsimp wp: possible_switch_to_valid_sched_strong simp: test_possible_switch_to_def) - by (auto simp: vs_all_heap_simps) + by (auto simp: vs_all_heap_simps schedulable_def3) (* sc_ptr is linked to a thread that is not in any queue *) lemma postpone_valid_sched: @@ -6722,18 +6673,16 @@ lemma sched_context_resume_valid_release_q[wp]: sched_context_resume sc_ptr_opt \\_. valid_release_q\" unfolding sched_context_resume_def - apply (wpsimp wp: postpone_valid_release_q is_schedulable_wp + apply (wpsimp wp: postpone_valid_release_q simp: thread_get_def) - by (clarsimp simp: sc_tcb_sc_at_def schedulable_def obj_at_def - is_sc_active_kh_simp vs_all_heap_simps - dest!: get_tcb_SomeD split: option.splits) + by (clarsimp simp: sc_tcb_sc_at_def obj_at_def schedulable_def3) lemma sched_context_resume_weak_valid_sched_action[wp]: "\weak_valid_sched_action and (\s. \tp. sc_tcb_sc_at ((=) (Some tp)) scp s \ scheduler_act_not tp s)\ sched_context_resume scp \\_. weak_valid_sched_action\" unfolding sched_context_resume_def - by (wpsimp wp: postpone_valid_sched_action is_schedulable_wp + by (wpsimp wp: postpone_valid_sched_action simp: thread_get_def) lemma sched_context_resume_valid_sched_action: @@ -6741,8 +6690,8 @@ lemma sched_context_resume_valid_sched_action: sched_context_resume sc_ptr \\_. valid_sched_action\ " unfolding sched_context_resume_def - apply (wpsimp wp: postpone_valid_sched_action thread_get_wp is_schedulable_wp) - by (fastforce simp: obj_at_def schedulable_def is_tcb + apply (wpsimp wp: postpone_valid_sched_action thread_get_wp) + by (clarsimp simp: obj_at_def schedulable_def3 vs_all_heap_simps is_tcb dest!: get_tcb_SomeD split: option.splits) lemma weak_valid_sched_action_contrap: @@ -6760,7 +6709,7 @@ lemma sched_context_resume_valid_sched_except_blocked: "\\s. valid_sched_except_blocked s \ heap_refs_retract_at (sc_tcbs_of s) (tcb_scps_of s) scp\ sched_context_resume scp \\_. valid_sched_except_blocked\" - apply (wpsimp wp: postpone_valid_sched_except_blocked is_schedulable_wp' get_tcb_queue_wp thread_get_wp' + apply (wpsimp wp: postpone_valid_sched_except_blocked get_tcb_queue_wp thread_get_wp' simp: sched_context_resume_def get_refills_def) apply (clarsimp simp: obj_at_def) apply (rename_tac y tcb sc tp; prop_tac "heap_ref_eq y scp (sc_tcbs_of s)") @@ -6772,7 +6721,8 @@ lemma sched_context_resume_valid_sched_except_blocked: apply (clarsimp simp: vs_all_heap_simps) apply (clarsimp simp: pred_tcb_at_def obj_at_def) apply (clarsimp simp: vs_all_heap_simps) - by (auto elim!: weak_valid_sched_action_contrap[OF valid_sched_action_weak_valid_sched_action]) + by (auto simp: schedulable_def2 + elim!: weak_valid_sched_action_contrap[OF valid_sched_action_weak_valid_sched_action]) (* FIXME RT: duplicates proof in sched_context_resume_valid_sched_except_blocked, because we're missing proofs about sched_context_resume and valid_blocked. *) @@ -6780,7 +6730,7 @@ lemma sched_context_resume_valid_sched: "\\s. valid_sched s \ heap_refs_retract_at (sc_tcbs_of s) (tcb_scps_of s) scp\ sched_context_resume scp \\_. valid_sched\" - apply (wpsimp wp: postpone_valid_sched is_schedulable_wp' get_tcb_queue_wp thread_get_wp' + apply (wpsimp wp: postpone_valid_sched get_tcb_queue_wp thread_get_wp' simp: sched_context_resume_def get_refills_def) apply (clarsimp simp: valid_sched_def sc_at_pred_n_def get_tcb_ko_at obj_at_def) apply (frule (1) heap_refs_retract_atD, clarsimp simp: vs_all_heap_simps) @@ -6790,7 +6740,8 @@ lemma sched_context_resume_valid_sched: apply (clarsimp simp: vs_all_heap_simps) apply (clarsimp simp: pred_tcb_at_def obj_at_def) apply (clarsimp simp: vs_all_heap_simps) - by (auto elim!: weak_valid_sched_action_contrap[OF valid_sched_action_weak_valid_sched_action]) + by (auto simp: schedulable_def2 + elim!: weak_valid_sched_action_contrap[OF valid_sched_action_weak_valid_sched_action]) lemma postpone_valid_blocked_except_set: "postpone sc_ptr \valid_blocked_except_set S\" @@ -7206,9 +7157,8 @@ lemma restart_thread_if_no_fault_scheduler_act_sane[wp]: \\_. scheduler_act_sane\" unfolding restart_thread_if_no_fault_def by (wpsimp simp: set_thread_state_def set_thread_state_act_def thread_get_def - wp: possible_switch_to_scheduler_act_sane set_scheduler_action_wp is_schedulable_wp - set_object_wp - hoare_vcg_imp_lift' ) + wp: possible_switch_to_scheduler_act_sane set_scheduler_action_wp + set_object_wp hoare_vcg_imp_lift') lemma tcb_sched_enqueue_ct_not_queued: "\ ct_not_queued and (\s. cur \ cur_thread s)\ @@ -7230,9 +7180,8 @@ lemma restart_thread_if_no_fault_ct_not_queued[wp]: \\_. ct_not_queued\" unfolding restart_thread_if_no_fault_def by (wpsimp simp: set_thread_state_def set_thread_state_act_def thread_get_def - wp: possible_switch_to_ct_not_queued set_scheduler_action_wp is_schedulable_wp - set_object_wp - hoare_vcg_imp_lift' ) + wp: possible_switch_to_ct_not_queued set_scheduler_action_wp + set_object_wp hoare_vcg_imp_lift') crunch cancel_all_ipc for ct_not_in_release_q[wp]: "ct_not_in_release_q" @@ -7441,7 +7390,9 @@ lemma reply_remove_cur_sc_chargeable: apply (wpsimp wp: hoare_vcg_if_lift2 hoare_drop_imp) apply (rule_tac Q'="\_. cur_sc_chargeable and cur_tcb and (\s. t \ cur_thread s)" in hoare_strengthen_post[rotated]) - apply (clarsimp simp: obj_at_kh_kheap_simps vs_all_heap_simps cur_sc_chargeable_def pred_map_simps split: if_split) + apply (fastforce dest: the_get_tcb_kheap_Some + simp: obj_at_kh_kheap_simps vs_all_heap_simps cur_sc_chargeable_def + split: if_split) apply (wpsimp wp: hoare_vcg_if_lift2 hoare_drop_imp)+ apply (clarsimp simp: obj_at_kh_kheap_simps vs_all_heap_simps cur_sc_chargeable_def pred_map_simps split: if_split) done @@ -7452,7 +7403,8 @@ lemma set_thread_state_csctb: \\xa. cur_sc_chargeable\" unfolding set_thread_state_def set_thread_state_act_def apply (wpsimp wp: set_object_wp) - by (clarsimp simp: obj_at_kh_kheap_simps vs_all_heap_simps cur_sc_chargeable_def) + by (fastforce dest: the_get_tcb_kheap_Some + simp: obj_at_kh_kheap_simps vs_all_heap_simps cur_sc_chargeable_def) lemma set_thread_state_Inactive_csctb[wp]: "set_thread_state d Inactive \cur_sc_chargeable\" @@ -7735,9 +7687,8 @@ lemma restart_thread_if_no_fault_ct_not_queued[wp]: \\_. ct_not_queued :: 'state_ext state \ _\" unfolding restart_thread_if_no_fault_def by (wpsimp simp: set_thread_state_def set_thread_state_act_def - wp: possible_switch_to_ct_not_queued set_scheduler_action_wp is_schedulable_wp - set_object_wp thread_get_wp - hoare_vcg_imp_lift' ) + wp: possible_switch_to_ct_not_queued set_scheduler_action_wp + set_object_wp thread_get_wp hoare_vcg_imp_lift' ) lemma fast_finalise_ct_not_queued[wp]: "\ct_not_queued and scheduler_act_sane and invs and ct_not_blocked\ @@ -7915,11 +7866,6 @@ crunch thread_set_priority for valid_sched_action[wp]: valid_sched_action (simp: valid_sched_action_def) -lemma is_schedulable_opt_ready_queues_update[simp]: - "is_schedulable_opt t (ready_queues_update f s) = is_schedulable_opt t s" - by (clarsimp simp: is_schedulable_opt_def get_tcb_def is_sc_active_def - split: option.splits) - lemma ct_not_in_q_not_cur_threadE: "tptr \ set (ready_queues s d p) \ ct_not_in_q s @@ -8123,7 +8069,7 @@ lemma sched_context_resume_schedulable_imp_ready: \\_ s. schedulable t s \ budget_ready t s\" unfolding sched_context_resume_def assert_opt_def when_def get_sc_refill_sufficient_def bind_assoc apply (wpsimp wp: postpone_in_release_q hoare_vcg_all_lift hoare_vcg_imp_lift' - hoare_vcg_disj_lift thread_get_wp' is_schedulable_wp + hoare_vcg_disj_lift thread_get_wp' simp: schedulable_def2) apply (intro conjI impI; clarsimp simp: obj_at_def schedulable_def2) apply (clarsimp simp: obj_at_def vs_all_heap_simps tcb_at_kh_simps sc_at_kh_simps)+ @@ -8159,7 +8105,7 @@ lemma sched_context_bind_tcb_valid_sched: \\y. valid_sched\" supply if_split[split del] apply (clarsimp simp: sched_context_bind_tcb_def) - apply (wpsimp wp: is_schedulable_wp' reschedule_valid_sched_const) + apply (wpsimp wp: reschedule_valid_sched_const) apply (rule_tac Q'="\r s. valid_sched_except_blocked s \ valid_blocked_except tcbptr s \ not_cur_thread tcbptr s @@ -11367,7 +11313,7 @@ lemma end_timeslice_valid_refills[wp]: lemma active_sc_tcb_at_budget_sufficient: "active_sc_tcb_at t s \ active_scs_valid s \ budget_sufficient t (s :: 'z :: state_ext state)" - by (fastforce simp: budget_sufficient_def2 active_sc_tcb_at_def2 is_sc_active_kh_simp + by (fastforce simp: budget_sufficient_def2 active_sc_tcb_at_def2 dest: valid_refills_refill_sufficient active_scs_validE) lemma tcb_release_dequeue_valid_ready_qs: @@ -12963,7 +12909,7 @@ lemma schedule_valid_sched_helper: and ct_ready_if_schedulable\ do check_domain_time; ct <- gets cur_thread; - ct_schedulable <- is_schedulable ct; + ct_schedulable <- gets (schedulable ct); action <- gets scheduler_action; case action of resume_cur_thread \ return () | switch_thread candidate \ @@ -12994,9 +12940,8 @@ lemma schedule_valid_sched_helper: \\_. valid_sched :: ('state_ext state) \ _\" apply (rule bind_wp_fwd_skip, wpsimp) apply clarsimp - apply (rule bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ is_schedulable_sp']) - apply (rule bind_wp[OF _ gets_sp], rename_tac action) + apply (rule bind_wp[OF _ gets_sp])+ + apply (rename_tac action) apply (case_tac action; clarsimp) (* resume_cur_thread *) @@ -13152,8 +13097,7 @@ lemma schedule_valid_sched_helper: apply (wpsimp wp: tcb_sched_enqueue_cur_ct_in_q) apply (clarsimp simp: schedulable_def2 valid_sched_def ct_ready_if_schedulable_def) apply (clarsimp simp: ct_in_state_kh_simp runnable_eq_active tcb_at_kh_simps) - apply fastforce - done + done (* choose_new_thread *) subgoal for ct ct_schedulable @@ -13444,9 +13388,9 @@ lemma sched_context_resume_ct_not_in_q[wp]: sched_context_resume sc_ptr \ \_. ct_not_in_q\" unfolding sched_context_resume_def - apply (wpsimp wp: thread_get_wp is_schedulable_wp) - by (fastforce simp: obj_at_def schedulable_def is_tcb - split: option.splits dest!: get_tcb_SomeD) + apply (wpsimp wp: thread_get_wp) + by (clarsimp simp: obj_at_def schedulable_def2 is_tcb tcb_at_kh_simps pred_map_def tcb_sts.Some + split: option.splits dest!: get_tcb_SomeD) lemma maybe_donate_sc_ct_not_in_q[wp]: "maybe_donate_sc tcb_ptr ntfnptr \ct_not_in_q\" @@ -14106,13 +14050,13 @@ lemma reply_push_valid_sched[wp]: by (wpsimp simp: valid_sched_def) lemma set_tcb_sc_update_active_sc_tcb_at': (* this is more usable *) - "\active_sc_tcb_at t and (is_sc_active scp)\ + "\active_sc_tcb_at t and (is_active_sc scp)\ set_tcb_obj_ref tcb_sched_context_update tptr (Some scp) \\rv. active_sc_tcb_at t\" apply (clarsimp simp: set_tcb_obj_ref_def pred_tcb_at_def obj_at_def) apply (rule bind_wp[OF _ assert_get_tcb_ko']) apply (wpsimp wp: set_object_wp) - by (auto simp: vs_all_heap_simps obj_at_def is_sc_active_def + by (auto simp: vs_all_heap_simps obj_at_def split: option.splits kernel_object.splits) lemma set_tcb_sc_update_active_sc_tcb_at_better: @@ -14134,14 +14078,13 @@ lemma set_tcb_sc_update_active_sc_tcb_at_better2: by (auto simp: vs_all_heap_simps obj_at_def) lemma sched_context_donate_active_sc_tcb_at: - "\is_sc_active sc_ptr and active_sc_tcb_at t + "\is_active_sc sc_ptr and active_sc_tcb_at t and sc_tcb_sc_at (\p. p \ Some t) sc_ptr\ sched_context_donate sc_ptr tcb_ptr \\_. active_sc_tcb_at t\" apply (clarsimp simp: sched_context_donate_def get_sc_obj_ref_def assert_opt_def) apply (wpsimp wp: set_tcb_sc_update_active_sc_tcb_at_better hoare_vcg_imp_lift' set_tcb_sc_update_active_sc_tcb_at_better2) - apply (clarsimp simp: is_sc_active_kh_simp) apply (clarsimp simp: sc_tcb_sc_at_def obj_at_def) done @@ -14230,15 +14173,14 @@ lemma sched_context_donate_bound_sc_tcb_at_None: done lemma sched_context_donate_released_if_bound_callee: - "\\s. bound_sc_tcb_at ((=) None) callee s \ is_sc_active sc_caller s + "\\s. bound_sc_tcb_at ((=) None) callee s \ is_active_sc sc_caller s \ is_refill_ready sc_caller s\ sched_context_donate sc_caller callee \\r. released_if_bound_sc_tcb_at callee\" - apply (clarsimp simp: released_sc_tcb_at_def) - apply (wpsimp wp: hoare_vcg_disj_lift sched_context_donate_bound_sc_tcb_at_None - sched_context_donate_bound_sc_obj_tcb_at - sched_context_donate_weak_budget_conditions) - by (clarsimp simp: obj_at_kh_kheap_simps) + unfolding released_sc_tcb_at_def + by (wpsimp wp: hoare_vcg_disj_lift sched_context_donate_bound_sc_tcb_at_None + sched_context_donate_bound_sc_obj_tcb_at + sched_context_donate_weak_budget_conditions) lemma reply_push_released_if_bound_callee: "\\s. released_if_bound_sc_tcb_at callee s @@ -14864,10 +14806,6 @@ lemma handle_timeout_valid_sched: end -lemma thread_set_is_sc_active[wp]: - "thread_set f t \\s. Q (is_sc_active scp s)\" - by (wpsimp wp: thread_set_wp, clarsimp simp: is_sc_active_def dest!: get_tcb_SomeD) - lemma send_fault_ipc_error_sched_act_not[wp]: "\scheduler_act_not t\ send_fault_ipc tptr handler_cap fault can_donate -, \\rv. scheduler_act_not t\" by (simp add: send_fault_ipc_def Let_def | @@ -15258,17 +15196,16 @@ lemma set_thread_state_st_tcb_at: set_thread_state tcbptr ts \\rv s. st_tcb_at P tcbptr s\" unfolding set_thread_state_def set_thread_state_act_def - apply (wpsimp wp: is_schedulable_wp set_object_wp) - apply (auto simp: st_tcb_at_def obj_at_def) - done + apply (wpsimp wp: set_object_wp) + by (auto simp: st_tcb_at_def obj_at_def) lemma tcb_sched_context_update_active_sc_tcb_at: - "\is_sc_active sc_ptr\ + "\is_active_sc sc_ptr\ set_tcb_obj_ref tcb_sched_context_update tcb_ptr (Some sc_ptr) \\r. active_sc_tcb_at tcb_ptr\" unfolding set_tcb_obj_ref_def apply (wpsimp wp: set_object_wp) - by (clarsimp simp: vs_all_heap_simps is_sc_active_kh_simp dest!: get_tcb_SomeD) + by (clarsimp simp: vs_all_heap_simps dest!: get_tcb_SomeD) lemma sched_context_donate_bound_sc_tcb_at[wp]: "\\\ sched_context_donate scp tptr \\rv. bound_sc_tcb_at ((=) (Some scp)) tptr\" @@ -15312,7 +15249,7 @@ lemma sched_context_resume_cond_released_sc_tcb_at: apply wpsimp apply (rule_tac Q'="\r. DetSchedInvs_AI.in_release_q tcbptr" in hoare_strengthen_post[rotated]) apply (clarsimp simp: pred_neg_def not_in_release_q_def in_release_q_def) - apply (wpsimp wp: postpone_in_release_q is_schedulable_wp + apply (wpsimp wp: postpone_in_release_q simp: thread_get_def)+ apply (intro conjI; intro allI impI; clarsimp) apply (clarsimp simp: pred_tcb_at_def obj_at_def schedulable_def2 vs_all_heap_simps @@ -15369,7 +15306,7 @@ lemma sched_context_resume_ready_or_release[wp]: sched_context_resume sc_ptr \\_. ready_or_release\" unfolding sched_context_resume_def - by (wpsimp wp: thread_get_wp is_schedulable_wp) + by (wpsimp wp: thread_get_wp) (clarsimp simp: obj_at_def schedulable_def2 pred_tcb_at_def is_tcb) lemma tcb_sched_enqueue_ready_queues_etcb_eq[wp]: @@ -15428,7 +15365,7 @@ lemma sched_context_resume_in_release_q_not_ready: \ active_sc_tcb_at t s \ \ budget_ready t s\" unfolding sched_context_resume_def assert_opt_def get_sc_refill_sufficient_def bind_assoc apply (wpsimp wp: postpone_not_in_release_q_other hoare_vcg_all_lift hoare_vcg_imp_lift' - hoare_vcg_disj_lift thread_get_wp' is_schedulable_wp) + hoare_vcg_disj_lift thread_get_wp') apply (intro conjI impI; clarsimp simp: obj_at_def schedulable_def2) apply (prop_tac "is_refill_sufficient 0 scp s") apply (erule valid_refills_refill_sufficient[OF active_scs_validE[rotated]]) @@ -15585,7 +15522,7 @@ lemma send_signal_WaitingNtfn_helper: apply (clarsimp simp: schedulable_def2) apply (wpsimp wp: possible_switch_to_valid_sched_strong simp: schedulable_def2) - apply (wpsimp wp: is_schedulable_wp)+ + apply wpsimp+ apply (rename_tac tcbptr x) apply (rule_tac Q'="\_ s. current_time_bounded s \ (in_release_q tcbptr s @@ -15967,7 +15904,7 @@ lemma send_signal_BOR_helper: y <- set_thread_state tcbptr Running; y <- as_user tcbptr (setRegister badge_register badge); y <- maybe_donate_sc tcbptr ntfnptr; - schedulable <- is_schedulable tcbptr; + schedulable <- gets (schedulable tcbptr); y \ when schedulable (possible_switch_to tcbptr); get_tcb_obj_ref tcb_sched_context tcbptr >>= if_sporadic_active_cur_sc_assert_refill_unblock_check @@ -16009,62 +15946,57 @@ lemma send_signal_BOR_helper: and valid_objs and (\s. sym_refs (state_refs_of s)) and (\s. pred_map_eq Running (tcb_sts_of s) tcbptr) and current_time_bounded" - in bind_wp_fwd) + in bind_wp_fwd) apply (wpsimp wp: set_thread_state_runnable_valid_sched_except_blocked set_thread_state_valid_blocked) - apply (clarsimp simp: valid_sched_def invs_valid_objs obj_at_kh_kheap_simps vs_all_heap_simps - tcb_non_st_state_refs_of_state_refs_of[rotated] if_fun_simp) - apply (wpsimp wp: refill_unblock_check_valid_sched get_tcb_obj_ref_wp) - apply (rename_tac sched) - apply (rule_tac Q'="\_ s. (valid_sched s \ heap_refs_inv (tcb_scps_of s) (sc_tcbs_of s) - \ current_time_bounded s - \ pred_map bound (tcb_scps_of s) tcbptr - \ st_tcb_at runnable tcbptr s - \ schedulable tcbptr s)" - in hoare_strengthen_post[rotated]) - apply clarsimp - apply (rename_tac scp sc n t) - apply (prop_tac "heap_ref_eq scp tcbptr (tcb_scps_of s)") - apply (clarsimp simp: obj_at_def vs_all_heap_simps) - apply (clarsimp simp: heap_refs_inv_def2 vs_all_heap_simps schedulable_def2) - apply (wpsimp wp: possible_switch_to_valid_sched_strong - simp: schedulable_def2) - apply (wpsimp wp: is_schedulable_wp')+ - apply (rule_tac Q'="\r s. tcbptr \ idle_thread s + apply (clarsimp simp: valid_sched_def invs_valid_objs obj_at_kh_kheap_simps vs_all_heap_simps + tcb_non_st_state_refs_of_state_refs_of[rotated] if_fun_simp) + apply (wpsimp wp: refill_unblock_check_valid_sched get_tcb_obj_ref_wp) + apply (rename_tac sched) + apply (rule_tac Q'="\_ s. (valid_sched s \ heap_refs_inv (tcb_scps_of s) (sc_tcbs_of s) + \ current_time_bounded s + \ pred_map bound (tcb_scps_of s) tcbptr + \ st_tcb_at runnable tcbptr s + \ schedulable tcbptr s)" + in hoare_strengthen_post[rotated]) + apply clarsimp + apply (rename_tac scp sc n t) + apply (prop_tac "heap_ref_eq scp tcbptr (tcb_scps_of s)") + apply (clarsimp simp: obj_at_def vs_all_heap_simps) + apply (clarsimp simp: heap_refs_inv_def2 vs_all_heap_simps schedulable_def2) + apply (wpsimp wp: possible_switch_to_valid_sched_strong + simp: schedulable_def2) + apply wpsimp+ + apply (rule_tac Q'="\r s. tcbptr \ idle_thread s \ valid_sched_except_blocked s \ valid_blocked_except_set {tcbptr} s \ (schedulable tcbptr s \ released_sc_tcb_at tcbptr s) \ heap_refs_inv (tcb_scps_of s) (sc_tcbs_of s) \ current_time_bounded s \ (in_release_q tcbptr s \ active_sc_tcb_at tcbptr s \ \ budget_ready tcbptr s)" in hoare_strengthen_post[rotated]) - apply (clarsimp simp: schedulable_def2 tcb_at_kh_simps) - apply (intro conjI; clarsimp simp: valid_sched_valid_sched_except_blocked) - apply (intro conjI impI allI; clarsimp elim!: valid_blocked_except_set_not_schedulable simp: schedulable_def2 tcb_at_kh_simps) - apply (prop_tac "active_sc_tcb_at tcbptr s") - apply (clarsimp simp: obj_at_def vs_all_heap_simps) - apply clarsimp - apply (prop_tac "heap_ref_eq x tcbptr (tcb_scps_of s)", clarsimp simp: vs_all_heap_simps obj_at_def) - apply (clarsimp simp: heap_refs_inv_def2 vs_all_heap_simps obj_at_def) - apply (rotate_tac 6) - apply (drule_tac x=x in spec, clarsimp) - apply (intro conjI; clarsimp) - apply (clarsimp simp: vs_all_heap_simps tcb_at_kh_simps) - apply (prop_tac "valid_blocked s") - apply (clarsimp elim!: valid_blocked_except_set_no_sc_bound_sum - simp: vs_all_heap_simps tcb_at_kh_simps obj_at_def) - apply (clarsimp simp: vs_all_heap_simps obj_at_def) - apply (wpsimp wp: maybe_donate_sc_in_release_q_imp_not_ready - maybe_donate_sc_cond_released_sc_tcb_at maybe_donate_sc_schedulable_imp_released - maybe_donate_sc_valid_ready_qs maybe_donate_sc_valid_release_q - maybe_donate_sc_valid_sched_action maybe_donate_sc_released_ipc_queues - maybe_donate_sc_valid_blocked_except_set maybe_donate_sc_ct_in_cur_domain - simp: valid_sched_def) - apply wpsimp - apply (wpsimp cong: conj_cong simp: obj_at_kh_kheap_simps - wp: hoare_vcg_all_lift hoare_vcg_conj_lift hoare_vcg_imp_lift') - apply (clarsimp simp: valid_sched_def) - apply (clarsimp simp: valid_sched_def obj_at_kh_kheap_simps vs_all_heap_simps - dest!: valid_ready_qs_etcb_eq) - done + apply (clarsimp simp: schedulable_def2 tcb_at_kh_simps) + apply (intro conjI; clarsimp simp: valid_sched_valid_sched_except_blocked) + apply (intro conjI impI allI; clarsimp elim!: valid_blocked_except_set_not_schedulable simp: schedulable_def2 tcb_at_kh_simps) + apply (prop_tac "active_sc_tcb_at tcbptr s") + apply (clarsimp simp: obj_at_def vs_all_heap_simps) + apply clarsimp + apply (prop_tac "heap_ref_eq x tcbptr (tcb_scps_of s)", clarsimp simp: vs_all_heap_simps obj_at_def) + apply (clarsimp simp: heap_refs_inv_def2 vs_all_heap_simps obj_at_def) + apply (intro conjI; clarsimp) + apply (clarsimp simp: vs_all_heap_simps tcb_at_kh_simps) + apply (prop_tac "valid_blocked s") + apply (fastforce elim!: valid_blocked_except_set_not_schedulable[where tcbptr=tcbptr] + simp: schedulable_def3) + apply (clarsimp simp: vs_all_heap_simps obj_at_def) + apply (wpsimp wp: maybe_donate_sc_in_release_q_imp_not_ready + maybe_donate_sc_cond_released_sc_tcb_at maybe_donate_sc_schedulable_imp_released + maybe_donate_sc_valid_ready_qs maybe_donate_sc_valid_release_q + maybe_donate_sc_valid_sched_action maybe_donate_sc_released_ipc_queues + maybe_donate_sc_valid_blocked_except_set maybe_donate_sc_ct_in_cur_domain + simp: valid_sched_def) + apply (wpsimp cong: conj_cong simp: obj_at_kh_kheap_simps + wp: hoare_vcg_all_lift hoare_vcg_conj_lift hoare_vcg_imp_lift') + by (clarsimp simp: valid_sched_def obj_at_kh_kheap_simps vs_all_heap_simps + dest!: valid_ready_qs_etcb_eq) (* what can we say about ntfn_bound_tcb? can we say it is not equal to idle_thread or cur_thread? *) lemma send_signal_valid_sched: @@ -16394,11 +16326,6 @@ end crunch do_nbrecv_failed_transfer for valid_sched[wp]: valid_sched -lemma as_user_is_sc_active[wp]: - "\is_sc_active scp\ as_user tptr f \\_. is_sc_active scp\" - apply (wpsimp simp: as_user_def wp: set_object_wp) - by (clarsimp simp: is_sc_active_def dest!: get_tcb_SomeD split: option.splits) - lemma maybe_donate_sc_bound_sc_trivial: "\bound_sc_tcb_at bound thread and P\ maybe_donate_sc thread ntfn_ptr @@ -16743,54 +16670,33 @@ lemma thread_set_domain_not_idle_valid_sched: apply (clarsimp simp: scheduler_act_not_def not_cur_thread_def) done -lemma thread_set_domain_schedulable_bool_not[wp]: - "\\s. \ schedulable t s\ - thread_set_domain t d - \\rv s. \ schedulable t s\" - apply (wpsimp simp: thread_set_domain_def thread_set_def wp: set_object_wp) - by (clarsimp simp: get_tcb_rev schedulable_def is_sc_active_def in_release_queue_def - dest!: get_tcb_SomeD split: option.splits if_split_asm) - -lemma thread_set_domain_schedulable_bool[wp]: - "\\s. schedulable t s\ - thread_set_domain t d - \\rv s. schedulable t s\" - apply (wpsimp simp: thread_set_domain_def thread_set_def wp: set_object_wp) - by (fastforce simp: get_tcb_rev schedulable_def is_sc_active_def in_release_queue_def - dest!: get_tcb_SomeD split: option.splits) - lemma tcb_sched_action_schedulable_bool[wp]: - "\\s. schedulable t s\ - tcb_sched_action f t - \\rv s. schedulable t s\" + "tcb_sched_action f t \\s. P (schedulable t s)\" apply (wpsimp simp: tcb_sched_action_def thread_set_def thread_get_def get_tcb_queue_def wp: set_object_wp set_tcb_queue_wp) - by (fastforce simp: schedulable_def' get_tcb_rev obj_at_def - dest!: get_tcb_SomeD split: option.splits) + apply (erule rsubst[where P=P]) + apply (fastforce simp: get_tcb_rev schedulable_def in_release_queue_def opt_pred_def opt_map_def + tcbs_of_kh_def scs_of_kh_def + dest!: get_tcb_SomeD split: option.splits if_split_asm) + done (* move *) + lemma valid_sched_action_switch_thread_is_schedulable: - "\valid_sched_action s; scheduler_action s = switch_thread thread\ \ - is_schedulable_opt thread s = Some True" - by (clarsimp simp: valid_sched_def valid_sched_action_def weak_valid_sched_action_def - is_schedulable_opt_def pred_tcb_at_def obj_at_def get_tcb_rev - in_release_queue_def released_sc_tcb_at_def vs_all_heap_simps is_sc_active_kh_simp) + "\valid_sched_action s; scheduler_action s = switch_thread thread\ + \ schedulable thread s" + by (clarsimp simp: valid_sched_action_def weak_valid_sched_action_def + schedulable_def2 pred_tcb_at_def obj_at_def + in_release_queue_def vs_all_heap_simps) lemma thread_set_domain_is_schedulable_opt[wp]: - "\\s. Q (is_schedulable_opt t s)\ - thread_set_domain t d - \\rv s. Q (is_schedulable_opt t s)\" + "thread_set_domain t d \\s. P (schedulable t s)\" unfolding thread_set_domain_def apply (wpsimp wp: thread_set_wp) - by (auto simp: is_schedulable_opt_def get_tcb_def is_sc_active_def in_release_queue_def - split: option.splits kernel_object.splits cong: conj_cong) - -lemma tcb_sched_dequeue_is_schedulable_opt[wp]: - "\\s. Q (is_schedulable_opt t s)\ - tcb_sched_action tcb_sched_dequeue t - \\rv s. Q (is_schedulable_opt t s)\" - unfolding tcb_sched_action_def - apply (wpsimp wp: thread_set_wp set_tcb_queue_wp) + apply (erule rsubst[where P=P]) + apply (fastforce simp: get_tcb_rev schedulable_def in_release_queue_def opt_pred_def opt_map_def + tcbs_of_kh_def scs_of_kh_def + dest!: get_tcb_SomeD split: option.splits if_split_asm) done lemma valid_blocked_valid_ready_qs_ready_and_sufficient: @@ -16825,7 +16731,7 @@ lemma invoke_domain_valid_sched: (* first case *) apply (wpsimp wp_del: reschedule_valid_sched_const wp: reschedule_required_valid_sched' - tcb_sched_enqueue_valid_blocked_except_set_const is_schedulable_wp) + tcb_sched_enqueue_valid_blocked_except_set_const) apply (clarsimp simp: schedulable_def2 split: if_split) apply (wpsimp wp: thread_set_domain_valid_ready_qs_not_q hoare_vcg_if_lift hoare_vcg_imp_lift' hoare_vcg_all_lift thread_set_domain_not_idle_valid_idle_etcb) @@ -16835,7 +16741,6 @@ lemma invoke_domain_valid_sched: apply (fastforce simp: valid_sched_def valid_blocked_defs released_sc_tcb_at_def) (* second case *) apply (wpsimp wp: tcb_sched_enqueue_valid_sched) - apply (wpsimp wp: is_schedulable_wp')+ apply (clarsimp split: if_split) apply (wpsimp wp: hoare_vcg_imp_lift') apply (simp add: valid_sched_def) @@ -16851,8 +16756,8 @@ lemma invoke_domain_valid_sched: hoare_vcg_conj_lift hoare_vcg_imp_lift' tcb_sched_dequeue_ct_not_in_q) apply (clarsimp simp: valid_blocked_thread_def) apply (intro conjI) - using valid_blocked_valid_ready_qs_ready_and_sufficient apply blast - apply (clarsimp simp: runnable_eq_active tcb_at_kh_simps) + using valid_blocked_valid_ready_qs_ready_and_sufficient schedulable_def2 apply blast + apply (clarsimp simp: runnable_eq_active tcb_at_kh_simps schedulable_def2) done lemma sched_context_bind_ntfn_valid_sched[wp]: @@ -16910,8 +16815,7 @@ lemma sched_context_yield_to_valid_sched_helper: \\_. valid_sched and simple_sched_action and (\s. sc_tcb_sc_at (\sctcb. \t. sctcb = Some t \ t \ cur_thread s) sc_ptr s) and ct_active and ct_released and invs and current_time_bounded and ct_not_in_release_q\" - by (wpsimp wp: get_sc_obj_ref_wp complete_yield_to_invs - hoare_vcg_all_lift hoare_drop_imp is_schedulable_wp + by (wpsimp wp: get_sc_obj_ref_wp complete_yield_to_invs hoare_vcg_all_lift hoare_drop_imp | wps)+ lemma schedulable_not_in_release_q: @@ -16933,7 +16837,7 @@ crunch sched_context_resume lemma schedulable_sc_not_in_release_q: "\\tp. bound_sc_tcb_at ((=) (Some scp)) tp s \ schedulable tp s\ \ sc_not_in_release_q scp s" - by (fastforce simp: schedulable_def split: option.splits) + by (fastforce simp: schedulable_def2 split: option.splits) crunch tcb_sched_action for sc_ko_at[wp]: "\s. (\n. ko_at (SchedContext sc n) sc_ptr s)" @@ -16953,7 +16857,7 @@ lemma sched_context_resume_not_in_release_q: sched_context_resume scp \\_. not_in_release_q t\" unfolding sched_context_resume_def - apply (wpsimp wp: postpone_not_in_release_q thread_get_wp' is_schedulable_wp) + apply (wpsimp wp: postpone_not_in_release_q thread_get_wp') by (clarsimp simp: obj_at_def pred_tcb_at_def sc_at_pred_n_def pred_map_def vs_all_heap_simps) lemma sched_context_resume_schedulable_imp_sc_ready: @@ -16966,7 +16870,7 @@ lemma sched_context_resume_schedulable_imp_sc_ready: apply (rule bind_wp[OF _ get_sched_context_sp]) apply (rename_tac sc; case_tac "sc_tcb sc"; simp) apply (rename_tac tp) - apply (rule bind_wp[OF _ is_schedulable_sp']) + apply (rule bind_wp[OF _ gets_sp]) apply (rule hoare_if) apply (rule bind_wp[OF _ thread_get_sp]) apply (rule bind_wp[OF _ get_sc_refill_ready_sp]) @@ -17017,7 +16921,7 @@ lemma sched_context_yield_to_valid_sched: apply (rule bind_wp[OF _ gsct_sp]) apply (case_tac sc_tcb_opt; clarsimp) apply (rename_tac tcb_ptr) - apply (rule bind_wp[OF _ is_schedulable_sp']) + apply (rule bind_wp[OF _ gets_sp]) apply (clarsimp simp: schedulable_def2) apply (case_tac schedulable; clarsimp?, (solves \wpsimp\)?) apply (intro bind_wp[OF _ gets_sp] @@ -17144,12 +17048,12 @@ lemma set_refills_ep_at_pred[wp]: done lemma refill_update_valid_blocked: - "\valid_blocked and K (0 < mrefills) and is_sc_active sc_ptr\ + "\valid_blocked and K (0 < mrefills) and is_active_sc sc_ptr\ refill_update sc_ptr period budget mrefills \\rv. valid_blocked\" unfolding valid_blocked_defs apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_imp_lift' simp: active_sc_tcb_at_def2) - by (auto simp: is_sc_active_kh_simp) + by auto lemma refill_new_active_scs_valid: "\active_scs_valid @@ -17476,13 +17380,13 @@ lemma refill_new_valid_blocked_except_set: apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_imp_lift' simp: active_sc_tcb_at_def2) by auto -lemma refill_new_is_sc_active: +lemma refill_new_is_active_sc: "\K (P (active_sc max_refills))\ refill_new sc_ptr max_refills budget period - \\rv s. P (is_sc_active sc_ptr s)\" + \\rv s. P (is_active_sc sc_ptr s)\" unfolding refill_new_def maybe_add_empty_tail_def refill_add_tail_def get_refills_def apply (wpsimp wp: update_sched_context_wp is_round_robin_wp set_refills_wp) - apply (clarsimp simp: sc_tcb_sc_at_def obj_at_def is_sc_active_def) + apply (clarsimp simp: sc_tcb_sc_at_def obj_at_def vs_all_heap_simps) done lemma reply_push_sc_tcb_sc_at: @@ -17947,7 +17851,7 @@ lemma test_possible_switch_to_scheduler_act_sane': test_possible_switch_to thread \\_. scheduler_act_sane\" unfolding test_possible_switch_to_def - apply (wpsimp wp: possible_switch_to_scheduler_act_sane' is_schedulable_wp) + apply (wpsimp wp: possible_switch_to_scheduler_act_sane') by (clarsimp simp: schedulable_def2) lemma restart_scheduler_act_sane[wp]: @@ -18339,7 +18243,7 @@ lemma charge_budget_valid_blocked[wp]: unfolding charge_budget_def refill_reset_rr_def update_refill_hd_def update_refill_tl_def update_sched_context_set_refills_rewrite by (wpsimp wp: reschedule_required_valid_blocked end_timeslice_valid_blocked - assert_inv gts_wp is_schedulable_wp' is_round_robin_wp) + assert_inv gts_wp is_round_robin_wp) lemma refill_reset_rr_valid_release_q[wp]: "\valid_release_q and sc_refills_sc_at (\refills. length refills = 2) scp\ @@ -18371,11 +18275,11 @@ lemma charge_budget_valid_release_q: apply wpsimp apply (wpsimp wp: end_timeslice_valid_release_q) apply (wpsimp wp: assert_inv) - apply (wpsimp wp: gts_wp is_schedulable_wp')+ + apply (wpsimp wp: gts_wp)+ apply (rule_tac Q'="\_ s. valid_release_q s \ cur_sc_chargeable s \ heap_refs_inv (tcb_scps_of s) (sc_tcbs_of s)" in hoare_strengthen_post[rotated]) - apply (clarsimp simp: tcb_at_kh_simps ct_in_state_def runnable_eq_active + apply (clarsimp simp: schedulable_def2 tcb_at_kh_simps ct_in_state_def runnable_eq_active split: if_splits) apply (wpsimp wp: sc_consumed_add_invs) apply (wpsimp wp: refill_budget_check_valid_release_q is_round_robin_wp)+ @@ -18383,8 +18287,10 @@ lemma charge_budget_valid_release_q: sc_at_pred_n_def obj_at_def ct_in_state_def pred_tcb_at_def runnable_eq_active split: if_splits) - by (fastforce simp: cur_sc_chargeable_def obj_at_def valid_release_q_def - in_queue_2_def vs_all_heap_simps) + by (fastforce simp: schedulable_def3 cur_sc_chargeable_def obj_at_def valid_release_q_def + opt_map_def opt_pred_def pred_map_def map_join_def runnable_eq_active + in_queue_2_def vs_all_heap_simps + split: option.splits if_splits) lemma refill_reset_rr_active_sc_tcb_at[wp]: "refill_reset_rr scp \(\s. P (active_sc_tcb_at t s)) :: 'state_ext state \ _\" @@ -18401,6 +18307,10 @@ lemma refill_reset_rr_valid_sched_action: update_refill_tl_def update_sched_context_set_refills_rewrite by (wpsimp wp: set_refills_valid_sched_action_act_not) +lemma schedulable_consumed_time_update[simp]: + "schedulable t (consumed_time_update f s) = schedulable t s" + by (clarsimp simp: schedulable_def) + lemma charge_budget_valid_sched_action: "\valid_sched_action and scheduler_act_sane and cur_sc_chargeable\ charge_budget consumed canTimeout @@ -18408,12 +18318,11 @@ lemma charge_budget_valid_sched_action: supply if_split [split del] apply (clarsimp simp: charge_budget_def) apply wpsimp - apply (wpsimp wp: gts_wp is_schedulable_wp')+ apply (rule_tac Q'="\ya s. (if (pred_map runnable (tcb_sts_of s) (cur_thread s) \ ct_not_in_release_q s \ active_sc_tcb_at (cur_thread s) s) then True else valid_sched_action s)" in hoare_strengthen_post[rotated]) - apply (clarsimp simp: tcb_at_kh_simps ct_in_state_def runnable_eq_active + apply (clarsimp simp: schedulable_def2 tcb_at_kh_simps ct_in_state_def runnable_eq_active split: if_splits) apply (wpsimp wp: hoare_vcg_if_lift_strong sc_consumed_add_invs) apply (wpsimp wp: hoare_vcg_if_lift_strong) @@ -18521,15 +18430,15 @@ lemma charge_budget_released_ipc_queues: \\_. released_ipc_queues :: 'state_ext state \ _\" supply if_split [split del] apply (clarsimp simp: charge_budget_def) - apply (wpsimp wp: end_timeslice_released_ipc_queues assert_inv gts_wp is_schedulable_wp') + apply (wpsimp wp: end_timeslice_released_ipc_queues assert_inv gts_wp) apply (rule_tac Q'="\_. released_ipc_queues and active_scs_valid and (\s. cur_sc s \ idle_sc_ptr)" in hoare_strengthen_post[rotated] - , clarsimp simp: tcb_at_kh_simps ct_in_state_def runnable_eq_active split: if_splits) + , clarsimp simp: schedulable_def3 tcb_at_kh_simps ct_in_state_def runnable_eq_active split: if_splits) apply (wpsimp wp: refill_budget_check_released_ipc_queues refill_budget_check_active_scs_valid is_round_robin_wp' get_sched_context_wp gets_wp)+ - apply (clarsimp simp: vs_all_heap_simps active_scs_valid_def split: if_splits) + apply (clarsimp simp: schedulable_def3 vs_all_heap_simps active_scs_valid_def split: if_splits) done lemma ct_not_blocked_cur_sc_not_blocked: @@ -18564,11 +18473,11 @@ lemma charge_budget_valid_ready_qs: apply wpsimp apply (wpsimp wp: end_timeslice_valid_ready_qs) apply (wpsimp wp: assert_inv) - apply (wpsimp wp: gts_wp is_schedulable_wp')+ + apply (wpsimp wp: gts_wp)+ apply (rule_tac Q'="\_ s. ct_not_queued s \ cur_sc_chargeable s \ valid_ready_qs s \ active_scs_valid s \ released_ipc_queues s \ valid_sched_action s \ scheduler_act_sane s" in hoare_strengthen_post[rotated]) - apply (clarsimp simp: tcb_at_kh_simps ct_in_state_def runnable_eq_active + apply (clarsimp simp: schedulable_def3 tcb_at_kh_simps ct_in_state_def runnable_eq_active split: if_splits) apply wpsimp apply (wpsimp wp: refill_reset_rr_valid_sched_action @@ -18579,7 +18488,7 @@ lemma charge_budget_valid_ready_qs: apply (wpsimp wp: is_round_robin_wp)+ apply (clarsimp split: if_splits) apply (subgoal_tac "sc_not_in_ready_q (cur_sc s) s \ sc_scheduler_act_not (cur_sc s) s", simp) - apply (fastforce simp: vs_all_heap_simps pred_map_def obj_at_def ct_in_state_def pred_tcb_at_def + apply (fastforce simp: schedulable_def3 vs_all_heap_simps pred_map_def obj_at_def ct_in_state_def pred_tcb_at_def active_scs_valid_def cur_sc_chargeable_def runnable_eq_active) apply (clarsimp simp: vs_all_heap_simps pred_map_def obj_at_def ct_in_state_def pred_tcb_at_def) apply (intro conjI impI allI) @@ -18608,7 +18517,7 @@ lemma charge_budget_active_scs_valid: charge_budget consumed canTimeout \\_. active_scs_valid :: 'state_ext state \ _\" apply (clarsimp simp: charge_budget_def) - apply (wpsimp wp: hoare_vcg_if_lift2 get_tcb_obj_ref_wp is_schedulable_wp + apply (wpsimp wp: hoare_vcg_if_lift2 get_tcb_obj_ref_wp refill_budget_check_round_robin_active_scs_valid refill_budget_check_active_scs_valid) apply (rule_tac Q'="\_. active_scs_valid and current_time_bounded" @@ -18631,7 +18540,7 @@ lemma charge_budget_active_reply_scs: unfolding charge_budget_def supply if_split[split del] apply (wpsimp wp: end_timeslice_active_reply_scs hoare_vcg_disj_lift hoare_vcg_imp_lift' - get_tcb_obj_ref_wp is_schedulable_wp) + get_tcb_obj_ref_wp) apply (rule_tac Q'="\_. active_reply_scs" in hoare_strengthen_post[rotated], clarsimp split: if_splits simp: schedulable_def2) apply (wpsimp simp: refill_reset_rr_def update_refill_hd_def update_sched_context_set_refills_rewrite @@ -19372,11 +19281,11 @@ end lemma ct_active_sc_cur_sc_active: "active_sc_tcb_at (cur_thread s) s \ bound_sc_tcb_at (\p. p = Some (cur_sc s)) (cur_thread s) s \ cur_sc_active s" - by (clarsimp simp: active_sc_tcb_at_def2 is_sc_active_kh_simp tcb_at_kh_simps vs_all_heap_simps) + by (clarsimp simp: active_sc_tcb_at_def2 tcb_at_kh_simps vs_all_heap_simps) lemma cur_sc_active_ct_active_sc: "cur_sc_active s \ bound_sc_tcb_at (\p. p = Some (cur_sc s)) (cur_thread s) s \ active_sc_tcb_at (cur_thread s) s" - by (fastforce simp: active_sc_tcb_at_def2 is_sc_active_kh_simp) + by (fastforce simp: active_sc_tcb_at_def2) lemma cur_sc_chargeable_when_ct_active_sc: "active_sc_tcb_at (cur_thread s) s \ cur_sc_chargeable s \ cur_sc_tcb_are_bound s" @@ -19801,14 +19710,14 @@ lemma charge_budget_scheduler_act_sane[wp]: charge_budget consumed can_timeout \\_. scheduler_act_sane ::'state_ext state \ _\" unfolding charge_budget_def - by (wpsimp wp: is_schedulable_wp hoare_drop_imp is_round_robin_wp) + by (wpsimp wp: hoare_drop_imp is_round_robin_wp) lemma check_budget_scheduler_act_sane[wp]: "\scheduler_act_sane::'state_ext state \ _\ check_budget \\_. scheduler_act_sane ::'state_ext state \ _\" unfolding check_budget_def - by (wpsimp wp: is_schedulable_wp hoare_drop_imp) + by (wpsimp wp: hoare_drop_imp) lemma send_ipc_scheduler_act_sane[wp]: "\scheduler_act_sane and ct_not_blocked\ @@ -19832,8 +19741,7 @@ lemma update_waiting_ntfn_scheduler_act_sane[wp]: update_waiting_ntfn ntfnptr queue bound_tcb sc_ptr badge \\_. scheduler_act_sane ::'state_ext state \ _\" unfolding update_waiting_ntfn_def - by (wpsimp wp: possible_switch_to_scheduler_act_sane' is_schedulable_wp - hoare_drop_imp)+ + by (wpsimp wp: possible_switch_to_scheduler_act_sane' hoare_drop_imp) lemma send_signal_scheduler_act_sane: "\scheduler_act_sane @@ -19843,7 +19751,7 @@ lemma send_signal_scheduler_act_sane: send_signal ntfnptr badge \\_. scheduler_act_sane ::'state_ext state \ _\" unfolding send_signal_def - apply (wpsimp wp: possible_switch_to_scheduler_act_sane' is_schedulable_wp)+ + apply (wpsimp wp: possible_switch_to_scheduler_act_sane') apply (wpsimp wp: hoare_drop_imps) apply (wpsimp wp: gts_wp get_simple_ko_wp)+ apply (intro conjI; clarsimp) @@ -20029,7 +19937,7 @@ lemma sched_context_resume_ct_not_in_release_q: sched_context_resume sc_ptr \\_. ct_not_in_release_q\" unfolding sched_context_resume_def - by (wpsimp wp: postpone_ct_not_in_release_q get_tcb_queue_wp is_schedulable_wp + by (wpsimp wp: postpone_ct_not_in_release_q get_tcb_queue_wp simp: thread_get_def vs_all_heap_simps obj_at_kh_kheap_simps) lemma sched_context_resume_not_queued: @@ -20046,7 +19954,7 @@ lemma sched_context_resume_ct_not_queued: sched_context_resume sc_ptr \\_. ct_not_queued :: 'state_ext state \ _\" unfolding sched_context_resume_def - by (wpsimp wp: get_tcb_queue_wp is_schedulable_wp postpone_not_queued_other + by (wpsimp wp: get_tcb_queue_wp postpone_not_queued_other simp: thread_get_def sc_at_pred_n_def obj_at_def | wps)+ lemma sched_context_donate_bound_not_cur_thread: @@ -20170,15 +20078,8 @@ lemma set_thread_state_act_schact_is_rct: and (\s. tcb_ptr = cur_thread s \ ct_schedulable s)\ set_thread_state_act tcb_ptr \\_. schact_is_rct\" - apply (clarsimp simp: set_thread_state_act_def) - apply (rule bind_wp[OF _ gets_sp])+ - apply (rule bind_wp[OF _ is_schedulable_sp]) - apply (rule hoare_when_cases; fastforce?) - apply (wpsimp wp: set_scheduler_action_wp) - apply (subst (asm) schedulable_unfold) - apply (clarsimp simp: schedulable_def2) - apply (clarsimp simp: schedulable_def2 tcb_at_kh_simps vs_all_heap_simps is_sc_active_def) - done + unfolding set_thread_state_act_def + by (wpsimp wp: set_scheduler_action_wp) lemma set_thread_state_schact_is_rct_strong: "\schact_is_rct @@ -20204,8 +20105,8 @@ lemma update_waiting_ntfn_ct_not_queued[wp]: and schact_is_rct\ update_waiting_ntfn ntfnptr queue bound_tcb sc_ptr badge \\_. ct_not_queued :: 'state_ext state \ _\" - unfolding update_waiting_ntfn_def is_schedulable_def when_def - by (wpsimp wp: possible_switch_to_ct_not_queued hoare_drop_imp + unfolding update_waiting_ntfn_def when_def + by (wpsimp wp: possible_switch_to_ct_not_queued hoare_drop_imp set_thread_state_schact_is_rct_weak) crunch cancel_ipc @@ -20233,8 +20134,8 @@ lemma send_signal_ct_not_queued[wp]: apply (case_tac "ntfn_bound_tcb ntfn"; clarsimp?, (solves \wpsimp\)?) apply (rule bind_wp[OF _ gts_sp]) apply (rule hoare_if; (solves \wpsimp\)?) - apply (wpsimp wp: possible_switch_to_not_queued hoare_drop_imp hoare_vcg_all_lift set_thread_state_schact_is_rct_weak - simp: is_schedulable_def cong: conj_cong + apply (wpsimp wp: possible_switch_to_not_queued hoare_drop_imp + set_thread_state_schact_is_rct_weak | wps)+ apply (fastforce simp: pred_tcb_at_def obj_at_def ct_in_state_def receive_blocked_def) done @@ -20399,7 +20300,7 @@ lemma sched_context_bind_tcb_not_queued_other: by (wpsimp wp: reschedule_required_not_queued tcb_sched_enqueue_not_queued update_sched_context_wp sched_context_resume_not_queued sc_tcb_update_sc_tcb_sc_at hoare_vcg_all_lift hoare_drop_imps - simp: is_schedulable_def vs_all_heap_simps) + simp: vs_all_heap_simps) lemma sched_context_yield_to_not_in_release_q_other: "\not_in_release_q t and sc_tcb_sc_at (\sctcb. sctcb \ Some t) sc_ptr\ @@ -20673,7 +20574,7 @@ lemma update_waiting_ntfn_released_sc_tcb_at[wp]: update_waiting_ntfn ntfnptr queue bound_tcb sc_ptr badge \\_. released_sc_tcb_at t\" unfolding update_waiting_ntfn_def - by (wpsimp wp: refill_unblock_check_active_scs_valid hoare_drop_imp is_schedulable_wp) + by (wpsimp wp: refill_unblock_check_active_scs_valid hoare_drop_imp) crunch send_signal for released_sc_tcb_at[wp]: "released_sc_tcb_at t" @@ -21313,16 +21214,14 @@ crunch activate_thread, schedule_choose_new_thread, awaken for valid_list[wp]: valid_list (wp: crunch_wps) -lemma schedule_valid_list[wp]: "\valid_list\ Schedule_A.schedule \\_. valid_list\" - apply (simp add: Schedule_A.schedule_def) - apply (wp add: tcb_sched_action_valid_list gts_wp hoare_drop_imps - is_schedulable_wp hoare_vcg_all_lift - | wpc | simp)+ - done +lemma schedule_valid_list[wp]: + "schedule \valid_list\" + unfolding schedule_def + by (wpsimp wp: tcb_sched_action_valid_list gts_wp hoare_drop_imps hoare_vcg_all_lift) lemma call_kernel_valid_list[wp]: "\valid_list\ call_kernel e \\_. valid_list\" apply (simp add: call_kernel_def preemption_path_def) - by (wpsimp wp: is_schedulable_wp hoare_drop_imps hoare_vcg_all_lift)+ + by (wpsimp wp: hoare_drop_imps hoare_vcg_all_lift)+ lemma handle_event_consumed_time_bounded[wp]: "\consumed_time_bounded and valid_machine_time\ @@ -22328,9 +22227,6 @@ lemma charge_budget_ready_if_schedulable[wp]: \\_. ct_ready_if_schedulable :: det_state \ _\" unfolding charge_budget_def apply (wpsimp wp: assert_inv) - apply (wpsimp wp: is_schedulable_wp) - apply wpsimp - apply wpsimp apply (rule_tac Q'="\_. cur_sc_chargeable and active_scs_valid and (\s. heap_refs_inv (sc_tcbs_of s) (tcb_scps_of s))" in hoare_post_imp) @@ -22345,7 +22241,9 @@ lemma charge_budget_ready_if_schedulable[wp]: apply (wpsimp wp: is_round_robin_wp) apply wpsimp apply wpsimp - apply (fastforce simp: vs_all_heap_simps obj_at_def cur_sc_chargeable_def split: if_splits) + apply (fastforce simp: ct_ready_if_schedulable_def2 schedulable_def2 + vs_all_heap_simps obj_at_def cur_sc_chargeable_def + ct_in_state_def pred_tcb_at_def is_blocked_on_receive_def) done lemma check_budget_ct_ready_if_schedulable[wp]: @@ -23336,13 +23234,16 @@ lemma sched_context_resume_cur_sc_not_in_release_q: else heap_refs_retract (sc_tcbs_of s) (tcb_scps_of s))\ sched_context_resume sc_ptr \\_ s. sc_not_in_release_q (cur_sc s) s\" - apply (clarsimp simp: sched_context_resume_def is_schedulable_def thread_get_def postpone_def + apply (clarsimp simp: sched_context_resume_def schedulable_def thread_get_def postpone_def get_sc_obj_ref_def) apply (wpsimp wp: tcb_release_enqueue_wp tcb_sched_action_wp) apply (clarsimp simp: vs_all_heap_simps obj_at_def in_queue_2_def) apply (intro conjI impI allI; fastforce?) - apply (case_tac "sc_ptr = cur_sc s"; (solves \simp\)?) - apply (prop_tac "y \ t") + apply (case_tac "sc_ptr = cur_sc s") + apply (clarsimp split: kernel_object.splits option.splits) + apply clarsimp + apply (rename_tac tcb_ptr tcb rt tcb') + apply (prop_tac "tcb_ptr \ t") apply (metis (no_types, opaque_lifting) kernel_object.simps(2) option.simps(1) heap_refs_inv_sc_tcb) apply (prop_tac "t \ set (release_queue s)", blast) @@ -25933,7 +25834,7 @@ lemma sched_context_resume_ct_ready_if_schedulable_two: sched_context_resume scp \\_. ct_ready_if_schedulable\" unfolding sched_context_resume_def - apply (wpsimp wp: postpone_ct_ready_if_schedulable thread_get_wp' is_schedulable_wp + apply (wpsimp wp: postpone_ct_ready_if_schedulable thread_get_wp' split: if_splits) apply (prop_tac "bound_sc_tcb_at (\x. x = Some scp) (cur_thread s) s") apply (clarsimp simp: tcb_at_kh_simps sc_at_kh_simps heap_refs_inv_def2 pred_map_eq_normalise) @@ -26160,7 +26061,7 @@ lemma sched_context_bind_tcb_released_if_bound[wp]: sched_context_bind_tcb sc_ptr tcb_ptr \\_. released_if_bound_sc_tcb_at t\" unfolding sched_context_bind_tcb_def if_cond_refill_unblock_check_def - apply (wpsimp wp: valid_sched_wp is_schedulable_wp) + apply (wpsimp wp: valid_sched_wp) apply (rule_tac Q'="\_. released_if_bound_sc_tcb_at t" in hoare_post_imp) apply clarsimp apply wpsimp @@ -27035,8 +26936,7 @@ lemma preemption_path_cur_sc_in_release_q_imp_zero_consumed: apply (fastforce intro: cur_sc_chargeable_cur_sc_in_release_q_imp_zero_consumed) apply (clarsimp simp: preemption_path_def) apply (rule bind_wp_fwd_skip, solves wpsimp) - apply (rule bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ is_schedulable_sp']) + apply (rule bind_wp[OF _ gets_sp])+ apply (rule_tac Q'="\_. cur_sc_in_release_q_imp_zero_consumed and invs and active_scs_valid and valid_release_q and cur_sc_more_than_ready and current_time_bounded and cur_sc_in_release_q_imp_zero_consumed" @@ -27065,7 +26965,7 @@ lemma preemption_path_cur_sc_more_than_ready: (is "valid (?cond) _ _") apply (clarsimp simp: preemption_path_def) apply (rule bind_wp_fwd_skip, wpsimp) - apply (wpsimp wp: is_schedulable_wp | intro conjI impI)+ + apply (wpsimp | intro conjI impI)+ done lemma preemption_path_ct_ready_if_schedulable: @@ -27078,8 +26978,7 @@ lemma preemption_path_ct_ready_if_schedulable: (is "valid (?cond and _ ) _ _") apply (clarsimp simp: preemption_path_def) apply (rule bind_wp_fwd_skip, wpsimp simp: ct_in_state_def) - apply (rule bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ is_schedulable_sp']) + apply (rule bind_wp[OF _ gets_sp])+ apply (rule_tac Q'="\_. ct_not_blocked_on_receive and ct_not_blocked_on_ntfn and invs and ct_ready_if_schedulable" in bind_wp) @@ -27110,8 +27009,7 @@ lemma preemption_path_valid_sched: \\_. valid_sched :: det_state \ _\" apply (clarsimp simp: preemption_path_def) apply (rule bind_wp_fwd_skip, wpsimp simp: ct_in_state_def) - apply (rule bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ is_schedulable_sp']) + apply (rule bind_wp[OF _ gets_sp])+ apply (rule_tac Q'="\_. invs and valid_sched and scheduler_act_sane and current_time_bounded" in bind_wp) apply (wpsimp wp: handle_interrupt_valid_sched) @@ -27133,33 +27031,27 @@ lemma preemption_path_valid_sched: lemma preemption_path_invs[wp]: "preemption_path \invs\" - apply (wpsimp simp: preemption_path_def schedulable_def2 - wp: is_schedulable_wp hoare_drop_imps hoare_vcg_if_lift2) - done + by (wpsimp simp: preemption_path_def schedulable_def2 wp: hoare_drop_imps hoare_vcg_if_lift2) lemma preemption_path_current_time_bounded: "\current_time_bounded and valid_machine_time\ preemption_path \\_. current_time_bounded :: det_state \ _\" - apply (wpsimp simp: preemption_path_def schedulable_def2 - wp: is_schedulable_wp hoare_drop_imps hoare_vcg_if_lift2 - update_time_stamp_current_time_bounded) - done + by (wpsimp simp: preemption_path_def schedulable_def2 + wp: hoare_drop_imps hoare_vcg_if_lift2 update_time_stamp_current_time_bounded) lemma preemption_path_consumed_time_bounded: "\consumed_time_bounded and valid_machine_time\ preemption_path \\_. consumed_time_bounded :: det_state \ _\" - apply (wpsimp simp: preemption_path_def schedulable_def2 - wp: is_schedulable_wp hoare_drop_imps hoare_vcg_if_lift2) - done + by (wpsimp simp: preemption_path_def schedulable_def2) lemma preemption_point_scheduler_act_sane: "\scheduler_act_sane and invs and ct_not_blocked\ preemption_path \\_. scheduler_act_sane :: det_state \ _\" apply (clarsimp simp: preemption_path_def) - apply (wpsimp wp: is_schedulable_wp hoare_vcg_if_lift2 hoare_drop_imps) + apply (wpsimp wp: hoare_vcg_if_lift2 hoare_drop_imps) apply (fastforce simp: ct_in_state_def is_blocked_on_receive_def schedulable_def2) apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def is_blocked_on_receive_def) apply (rename_tac tcb, case_tac "tcb_state tcb"; clarsimp) diff --git a/proof/invariant-abstract/Deterministic_AI.thy b/proof/invariant-abstract/Deterministic_AI.thy index 3358c74775..02d0f9339e 100644 --- a/proof/invariant-abstract/Deterministic_AI.thy +++ b/proof/invariant-abstract/Deterministic_AI.thy @@ -3885,7 +3885,7 @@ lemma tcb_release_remove_cdt_cdt_list[wp]: lemma reschedule_required_cdt_cdt_list[wp]: "\\s. P (cdt s) (cdt_list s)\ reschedule_required \\_ s. P (cdt s) (cdt_list s)\" - by (wpsimp simp: reschedule_required_def thread_get_def wp: is_schedulable_wp hoare_drop_imp) + by (wpsimp simp: reschedule_required_def thread_get_def wp: hoare_drop_imp) lemma test_reschedule_cdt_cdt_list[wp]: "\\s. P (cdt s) (cdt_list s)\ test_reschedule r \\_ s. P (cdt s) (cdt_list s)\" diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy index 59790db47a..a16bbba8f1 100644 --- a/proof/invariant-abstract/Finalise_AI.thy +++ b/proof/invariant-abstract/Finalise_AI.thy @@ -831,7 +831,7 @@ lemma sched_context_unbind_tcb_sc_yf_helper[wp]: st_tcb_at (\st. tcb_st_refs_of st = {}) tp s) p s\" apply (clarsimp simp: sched_context_unbind_tcb_def get_sc_obj_ref_def tcb_release_remove_def tcb_sched_action_def set_tcb_queue_def get_tcb_queue_def - reschedule_required_def set_scheduler_action_def is_schedulable_def + reschedule_required_def set_scheduler_action_def cong: scheduler_action.case_cong) apply (rule bind_wp[OF _ get_sched_context_sp]) by (wpsimp wp: thread_get_wp') diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index d012d54109..75875dc128 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -1006,7 +1006,7 @@ lemma reply_unlink_sc_invs: lemma set_thread_state_act_inv: "(\s. P (s\scheduler_action := choose_new_thread\) = P s) \ set_thread_state_act t \P\" - by (wpsimp simp: set_thread_state_act_def set_scheduler_action_def is_schedulable_def) + by (wpsimp simp: set_thread_state_act_def set_scheduler_action_def) lemma state_refs_of_scheduler_action_kheap[simp]: "state_refs_of (s\scheduler_action := sa, kheap := h\) = state_refs_of (s\kheap := h\)" diff --git a/proof/invariant-abstract/IpcDet_AI.thy b/proof/invariant-abstract/IpcDet_AI.thy index f07e8d56a6..c72a5d2453 100644 --- a/proof/invariant-abstract/IpcDet_AI.thy +++ b/proof/invariant-abstract/IpcDet_AI.thy @@ -1561,7 +1561,7 @@ lemma reschedule_required_cur_sc_tcb': supply set_scheduler_action_cur_sc_tcb [wp del] unfolding reschedule_required_def by (wpsimp simp: reschedule_required_def set_scheduler_action_def tcb_sched_action_def - set_tcb_queue_def get_tcb_queue_def thread_get_def is_schedulable_def + set_tcb_queue_def get_tcb_queue_def thread_get_def cur_sc_tcb_def sc_tcb_sc_at_def obj_at_def) lemma maybe_return_sc_cur_sc_tcb[wp]: @@ -2793,13 +2793,13 @@ lemma schedule_tcb_invs': apply (rule hoare_vcg_disj_lift[where Q = "\_. invs" and Q' = "\_. invs", simplified]) apply (simp add: schedule_tcb_def) apply (rule bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ gets_sp]) - apply (rule bind_wp[OF _ is_schedulable_sp]) + apply (rule bind_wp[OF _ gets_sp])+ apply (simp add: when_def reschedule_required_def) apply (intro conjI) prefer 2 apply (wpsimp wp: hoare_pre_cont) - apply (clarsimp simp: is_schedulable_opt_def pred_tcb_at_def obj_at_def get_tcb_def) + apply (clarsimp simp: schedulable_def pred_tcb_at_def obj_at_def opt_pred_def opt_map_def + opt_map_red tcbs_of_kh_def) apply clarsimp apply (rule bind_wp[OF _ gets_sp]) apply (case_tac action; simp) diff --git a/proof/invariant-abstract/Ipc_AI.thy b/proof/invariant-abstract/Ipc_AI.thy index 47f067d43e..7e180b96c4 100644 --- a/proof/invariant-abstract/Ipc_AI.thy +++ b/proof/invariant-abstract/Ipc_AI.thy @@ -2889,13 +2889,6 @@ lemma ep_queue_cap_to: crunch set_message_info for pred_tcb_at[wp]: "pred_tcb_at proj P t" -lemma reschedule_required_pred_tcb_at: - "\pred_tcb_at proj P t\ reschedule_required \\rv. pred_tcb_at proj P t\" - supply if_cong[cong] - by (wpsimp simp: reschedule_required_def set_scheduler_action_def tcb_sched_action_def - set_tcb_queue_def get_tcb_queue_def thread_get_def - wp: hoare_drop_imps is_schedulable_wp) - lemma schedule_tcb_pred_tcb_at: "\pred_tcb_at proj P t'\ schedule_tcb t \\rv. pred_tcb_at proj P t'\" by (wpsimp simp: schedule_tcb_def wp: reschedule_required_pred_tcb_at) diff --git a/proof/invariant-abstract/KHeap_AI.thy b/proof/invariant-abstract/KHeap_AI.thy index 8f0f18bc3f..a33ce72d19 100644 --- a/proof/invariant-abstract/KHeap_AI.thy +++ b/proof/invariant-abstract/KHeap_AI.thy @@ -238,7 +238,7 @@ lemma dxo_wp_weak[wp]: crunch set_thread_state for ct[wp]: "\s. P (cur_thread s)" -crunch set_scheduler_action, is_schedulable +crunch set_scheduler_action for typ_at[wp]: "\s. P (typ_at T p s)" lemma set_thread_state_typ_at[wp]: @@ -1687,7 +1687,7 @@ lemma no_ofail_read_object[simp]: lemma stsa_caps_of_state[wp]: "set_thread_state_act t \\s. P (caps_of_state s)\" - unfolding set_thread_state_act_def set_scheduler_action_def is_schedulable_def by wpsimp + unfolding set_thread_state_act_def set_scheduler_action_def by wpsimp lemma shows sts_caps_of_state[wp]: @@ -2219,58 +2219,10 @@ lemma assert_get_tcb_ko': obj_at_def split: option.splits Structures_A.kernel_object.splits) -(* is_schedulable lemmas *) -lemma is_schedulable_wp: - "\\s. \t. schedulable tcb_ptr s = t \ P t s\ is_schedulable tcb_ptr \P\" - apply (clarsimp simp: is_schedulable_def) - apply (rule bind_wp[OF _ assert_get_tcb_ko']) - apply (case_tac "tcb_sched_context tcb"; clarsimp) - apply (wpsimp simp: schedulable_def obj_at_def get_tcb_rev) - by (wpsimp simp: schedulable_def obj_at_def get_tcb_rev is_sc_active_def - wp: get_sched_context_wp) - -lemma is_schedulable_sp: - "\P\ is_schedulable tp \\rv. (\s. rv = the (is_schedulable_opt tp s)) and P\" - apply (clarsimp simp: is_schedulable_def) - apply (wpsimp simp: hoare_vcg_if_lift2 obj_at_def is_tcb wp: get_sched_context_wp) - apply(rule conjI) - apply (clarsimp simp: Option.is_none_def is_schedulable_opt_def get_tcb_def) - by (clarsimp simp: is_schedulable_opt_def get_tcb_def is_sc_active_def split: option.splits) - -lemma is_schedulable_sp': - "\P\ is_schedulable tp \\rv. (\s. rv = schedulable tp s) and P\" - by (wpsimp wp: is_schedulable_wp) - -lemma schedulable_unfold: - "tcb_at tp s \ - is_schedulable_opt tp s - = Some (st_tcb_at runnable tp s - \ bound_sc_tcb_at (\spo. \sp. spo = Some sp \ is_sc_active sp s) tp s - \ \ (in_release_queue tp s))" - by (clarsimp simp: is_schedulable_opt_def get_tcb_rev is_tcb pred_tcb_at_def obj_at_def - split: option.splits) - -lemma is_sc_active_def2: - "(is_sc_active scp s) = (\sc n. kheap s scp = Some (SchedContext sc n) \ sc_active sc)" - unfolding is_sc_active_def - apply (clarsimp split: option.splits) - apply (case_tac x2; simp) - done - -lemma schedulable_def': - "schedulable t s = ((\scp. bound_sc_tcb_at (\x. x = Some scp) t s - \ sc_at_pred sc_active scp s) - \ st_tcb_at active t s - \ \(in_release_queue t s))" - unfolding schedulable_def - apply (rule iffI) - apply (clarsimp simp: pred_tcb_at_def obj_at_def is_sc_active_def2 active_sc_def sc_at_pred_n_def - runnable_eq_active split: option.splits - dest!: get_tcb_SomeD) - apply (fastforce simp: pred_tcb_at_def obj_at_def is_sc_active_def2 active_sc_def get_tcb_def sc_at_pred_n_def - runnable_eq_active split: option.splits - dest!: get_tcb_SomeD) - done +(* FIXME RT: move to Lib *) +lemma gets_the_sp: + "\Q\ gets_the f \\rv s. f s = Some rv \ Q s\" + by wpsimp lemma update_sched_context_obj_at_impossible: "\ \np n. \ (P (SchedContext np n)) \ \ diff --git a/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy index dc1961727e..8de253aba9 100644 --- a/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy @@ -381,7 +381,7 @@ lemma call_kernel_valid_vspace_objs'[wp]: apply (rule valid_validE) apply (wpsimp) apply (fastforce simp: ct_in_state_def pred_tcb_weakenE) - apply (wpsimp wp: is_schedulable_wp hoare_vcg_all_lift hoare_drop_imps hoare_vcg_if_lift2) + apply (wpsimp wp: hoare_vcg_all_lift hoare_drop_imps hoare_vcg_if_lift2) apply wpsimp (***) apply (rule_tac Q'="\_. valid_vspace_objs'" in bind_wp_fwd) @@ -391,7 +391,9 @@ lemma call_kernel_valid_vspace_objs'[wp]: valid_vspace_objs' and (\s. bound_sc_tcb_at (\a. \y. a = Some y) (cur_thread s) s)" in bind_wp_fwd) apply wpsimp - apply (clarsimp simp: pred_tcb_at_def obj_at_def schedulable_def') + apply (clarsimp simp: pred_tcb_at_def obj_at_def schedulable_def opt_pred_def opt_map_def + tcbs_of_kh_def + split: option.splits) apply (rule_tac Q'="\rv. invs and (\s. rv \ ct_running s) and valid_vspace_objs'" in bind_wp_fwd) apply (wpsimp wp: check_budget_restart_true) @@ -404,7 +406,9 @@ lemma call_kernel_valid_vspace_objs'[wp]: valid_vspace_objs' and (\s. bound_sc_tcb_at (\a. \y. a = Some y) (cur_thread s) s)" in bind_wp_fwd) apply wpsimp - apply (clarsimp simp: pred_tcb_at_def obj_at_def schedulable_def') + apply (clarsimp simp: pred_tcb_at_def obj_at_def schedulable_def opt_pred_def opt_map_def + tcbs_of_kh_def + split: option.splits) apply (rule_tac Q'="\rv. invs and (\s. rv \ ct_running s) and valid_vspace_objs'" in bind_wp_fwd) apply (wpsimp wp: check_budget_restart_true) @@ -419,7 +423,9 @@ lemma call_kernel_valid_vspace_objs'[wp]: valid_vspace_objs' and (\s. bound_sc_tcb_at (\a. \y. a = Some y) (cur_thread s) s)" in bind_wp_fwd) apply wpsimp - apply (clarsimp simp: pred_tcb_at_def obj_at_def schedulable_def') + apply (clarsimp simp: pred_tcb_at_def obj_at_def schedulable_def opt_pred_def opt_map_def + tcbs_of_kh_def + split: option.splits) apply (rule_tac Q'="\rv. invs and (\s. rv \ ct_running s) and valid_vspace_objs'" in bind_wp_fwd) apply (wpsimp wp: check_budget_restart_true) diff --git a/proof/invariant-abstract/RealTime_AI.thy b/proof/invariant-abstract/RealTime_AI.thy index fbe61a295d..7bba81908c 100644 --- a/proof/invariant-abstract/RealTime_AI.thy +++ b/proof/invariant-abstract/RealTime_AI.thy @@ -1296,7 +1296,7 @@ lemma sched_context_update_consumed_cap_to[wp]: lemma schedule_tcb_is_original_cap[wp]: "\\s. P (is_original_cap s)\ schedule_tcb param_a \\_ s. P (is_original_cap s)\" by (wpsimp simp: schedule_tcb_def reschedule_required_def set_scheduler_action_def - tcb_sched_action_def set_tcb_queue_def get_tcb_queue_def is_schedulable_def + tcb_sched_action_def set_tcb_queue_def get_tcb_queue_def get_sched_context_def get_object_def thread_get_def) lemma get_sched_context_inv[wp]: "\P\ get_sched_context sc_ptr \\_. P\" diff --git a/proof/invariant-abstract/SchedContextInv_AI.thy b/proof/invariant-abstract/SchedContextInv_AI.thy index 993465bf3c..a1313f273b 100644 --- a/proof/invariant-abstract/SchedContextInv_AI.thy +++ b/proof/invariant-abstract/SchedContextInv_AI.thy @@ -487,8 +487,7 @@ lemma sched_context_yield_to_invs: apply (wpsimp simp: invs_def valid_state_def valid_pspace_def get_sc_obj_ref_def split_del: if_split wp: valid_irq_node_typ hoare_vcg_if_lift2 thread_get_inv hoare_drop_imp - valid_ioports_lift update_sched_context_valid_idle) - apply (clarsimp cong: conj_cong) + valid_ioports_lift update_sched_context_valid_idle hoare_vcg_all_lift) apply (intro conjI; clarsimp simp: cur_tcb_def) apply (clarsimp simp: sc_at_pred_n_def obj_at_def is_sc_obj_def) apply (fastforce dest!: valid_objs_valid_sched_context_size) @@ -1517,12 +1516,13 @@ lemma charge_budget_invs[wp]: unfolding charge_budget_def is_round_robin_def apply clarsimp apply (rule bind_wp[OF _ gets_sp]) - apply (wpsimp wp: end_timeslice_invs assert_inv hoare_vcg_if_lift2 gts_wp is_schedulable_wp) + apply (wpsimp wp: end_timeslice_invs assert_inv hoare_vcg_if_lift2 gts_wp) apply (rule_tac Q'="\_. invs" in hoare_strengthen_post[rotated]) apply (clarsimp simp: ct_in_state_def runnable_eq pred_tcb_at_def obj_at_def schedulable_def split: option.splits) apply (subgoal_tac "cur_tcb s") - apply (clarsimp simp: get_tcb_def cur_tcb_def tcb_at_def is_tcb split: option.splits kernel_object.splits) + apply (clarsimp simp: runnable_eq opt_pred_def opt_map_def tcbs_of_kh_def + split: option.splits) apply (wpsimp wp: end_timeslice_invs assert_inv hoare_vcg_if_lift2 gts_wp hoare_vcg_all_lift sc_consumed_add_invs refill_budget_check_invs simp: Let_def)+ @@ -1530,7 +1530,9 @@ lemma charge_budget_invs[wp]: apply (clarsimp simp: ct_in_state_def schedulable_def pred_tcb_at_def obj_at_def get_tcb_def cur_tcb_def split: kernel_object.splits if_splits) - by (metis (no_types, lifting) option.case_eq_if runnable_eq) + apply (clarsimp simp: runnable_eq opt_pred_def opt_map_def tcbs_of_kh_def + split: option.splits) + done lemma check_budget_invs[wp]: "\\s. invs s\ check_budget \\rv. invs \" diff --git a/proof/invariant-abstract/SchedContext_AI.thy b/proof/invariant-abstract/SchedContext_AI.thy index b83edfdc01..793e8fac0e 100644 --- a/proof/invariant-abstract/SchedContext_AI.thy +++ b/proof/invariant-abstract/SchedContext_AI.thy @@ -1198,8 +1198,6 @@ lemma sched_context_unbind_ntfn_invs[wp]: apply (clarsimp simp: valid_idle_def obj_at_def) done -lemmas is_schedulable_inv[wp] = is_schedulable_wp[where P="\_. P" for P, simplified] - declare reprogram_timer_update_arch.state_refs_update[simp] crunch sched_context_resume, test_possible_switch_to, tcb_release_remove, postpone @@ -1295,7 +1293,7 @@ lemma possible_switch_to_cur_sc_tcb[wp]: "\cur_sc_tcb\ possible_switch_to tcb \\_. cur_sc_tcb\" by (wpsimp simp: possible_switch_to_def tcb_sched_action_def set_tcb_queue_def get_tcb_queue_def thread_get_def reschedule_required_def set_scheduler_action_def - is_schedulable_def get_tcb_obj_ref_def cur_sc_tcb_def sc_tcb_sc_at_def + get_tcb_obj_ref_def cur_sc_tcb_def sc_tcb_sc_at_def obj_at_def) lemma test_possible_switch_to_cur_sc_tcb[wp]: @@ -1333,7 +1331,7 @@ lemma tcb_sched_action_cur_sc_tcb [wp]: lemma reschedule_required_cur_sc_tcb [wp]: "\cur_sc_tcb\ reschedule_required \\_. cur_sc_tcb\" by (wpsimp simp: reschedule_required_def set_scheduler_action_def tcb_sched_action_def - set_tcb_queue_def get_tcb_queue_def thread_get_def is_schedulable_def + set_tcb_queue_def get_tcb_queue_def thread_get_def cur_sc_tcb_def sc_tcb_sc_at_def obj_at_def) lemma sched_context_bind_tcb_invs[wp]: @@ -1380,7 +1378,7 @@ crunch tcb_release_remove, tcb_sched_action, set_tcb_obj_ref lemma reschedule_required_cur_sc [wp]: "\\s. P (cur_sc s)\ reschedule_required \\rv s. P (cur_sc s)\" by (wpsimp simp: reschedule_required_def set_scheduler_action_def tcb_sched_action_def - set_tcb_queue_def get_tcb_queue_def thread_get_def is_schedulable_def + set_tcb_queue_def get_tcb_queue_def thread_get_def cur_sc_tcb_def sc_tcb_sc_at_def obj_at_def) lemma reschedule_required_scheduler_action [wp]: @@ -1388,7 +1386,7 @@ lemma reschedule_required_scheduler_action [wp]: reschedule_required \\rv s. scheduler_action s \ resume_cur_thread\" by (wpsimp simp: reschedule_required_def set_scheduler_action_def tcb_sched_action_def - set_tcb_queue_def get_tcb_queue_def thread_get_def is_schedulable_def + set_tcb_queue_def get_tcb_queue_def thread_get_def cur_sc_tcb_def sc_tcb_sc_at_def obj_at_def) lemma sched_context_unbind_tcb_invs_helper: @@ -1440,7 +1438,7 @@ lemma reschedule_required_sc_ptr [wp]: reschedule_required \\rv s. (\n. ko_at (SchedContext sc n) sc_ptr s)\" by (wpsimp simp: reschedule_required_def set_scheduler_action_def tcb_sched_action_def - set_tcb_queue_def get_tcb_queue_def thread_get_def is_schedulable_def + set_tcb_queue_def get_tcb_queue_def thread_get_def cur_sc_tcb_def sc_tcb_sc_at_def obj_at_def) lemma sched_context_unbind_tcb_invs[wp]: @@ -1598,10 +1596,18 @@ lemma postpone_invs[wp]: "postpone t \invs\" by (wpsimp simp: invs_def valid_state_def valid_pspace_def wp: valid_ioports_lift) +lemma get_tcb_queue_wp[wp]: "\\s. P (ready_queues s t p) s\ get_tcb_queue t p \P\" + by (wpsimp simp: get_tcb_queue_def) + lemma sched_context_resume_invs[wp]: "\invs\ sched_context_resume scptr \\_. invs\" - by (wpsimp simp: sched_context_resume_def get_tcb_queue_def is_schedulable_def is_tcb - wp: thread_get_wp) + unfolding sched_context_resume_def + apply (wpsimp wp: get_tcb_queue_wp thread_get_wp) + apply (auto simp: obj_at_def schedulable_def opt_map_def opt_pred_def) + apply (frule invs_sym_refs) + apply (drule (2) sym_ref_sc_tcb) + apply (clarsimp simp: is_obj_defs) + done lemma set_sc_obj_ref_invs_no_change: "\ \sc. sc_replies (f (\_. x) sc) = sc_replies sc; @@ -1679,8 +1685,8 @@ lemma set_scheduler_action_invs[wp]: done lemma reschedule_required_invs[wp]: - "\invs\ reschedule_required \\rv. invs\" - by (wpsimp simp: reschedule_required_def wp: is_schedulable_wp hoare_drop_imps hoare_vcg_all_lift) + "reschedule_required \invs\" + by (wpsimp simp: reschedule_required_def wp: hoare_drop_imps) lemma possible_switch_to_invs[wp]: "\invs\ possible_switch_to target \\rv. invs\" diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index a867d4819d..42a9eb06e3 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -150,11 +150,10 @@ proof - show ?thesis unfolding choose_thread_def guarded_switch_to_def apply (wpsimp wp: stit_activatable stt_activatable split_del: if_split wp_del: get_sched_context_wp) - apply (wpsimp wp: is_schedulable_wp) - apply (wpsimp wp: assert_wp) apply (wpsimp simp: thread_get_def)+ - apply (clarsimp simp: schedulable_def pred_tcb_at_def obj_at_def - dest!: get_tcb_SomeD split: option.splits) + apply (fastforce simp: schedulable_def pred_tcb_at_def obj_at_def opt_pred_def opt_map_def + tcbs_of_kh_def + split: option.splits) done qed @@ -165,11 +164,11 @@ lemma schedule_choose_new_thread_ct_activatable[wp]: lemma guarded_switch_to_ct_in_state_activatable[wp]: "\\\ guarded_switch_to t \\a. ct_in_state activatable\" unfolding guarded_switch_to_def - apply (wpsimp wp: hoare_vcg_imp_lift gts_wp is_schedulable_wp stt_activatable assert_wp + apply (wpsimp wp: hoare_vcg_imp_lift gts_wp stt_activatable assert_wp simp: thread_get_def) - apply (clarsimp simp: schedulable_def get_tcb_ko_at st_tcb_at_def obj_at_def - split: option.splits) - done + by (fastforce simp: schedulable_def pred_tcb_at_def obj_at_def opt_pred_def opt_map_def + tcbs_of_kh_def + split: option.splits) declare sc_and_timer_activatable[wp] @@ -1069,13 +1068,11 @@ lemma cur_sc_tcb_invs: obj_at_def sym_refs_bound_sc_tcb_iff_sc_tcb_sc_at[symmetric]) lemma stsa_schedulable_scheduler_action: - "\\s. P (scheduler_action s) \ - schedulable thread s\ + "\\s. P (scheduler_action s) \ schedulable thread s\ set_thread_state_act thread \\_ s. P (scheduler_action s)\" apply (simp add: set_thread_state_act_def) apply (rule bind_wp[OF _ hoare_gets_sp])+ - apply (rule bind_wp[OF _ is_schedulable_sp']) apply (simp add: when_def) apply (intro conjI) apply (wpsimp wp: hoare_pre_cont) @@ -1083,15 +1080,14 @@ lemma stsa_schedulable_scheduler_action: done lemma sts_schedulable_scheduler_action: - "\\s. P (scheduler_action s) \ - schedulable thread s\ + "\\s. P (scheduler_action s) \ schedulable thread s\ set_thread_state thread Restart \\_ s. P (scheduler_action s)\" + unfolding set_thread_state_def apply (wpsimp wp: stsa_schedulable_scheduler_action set_object_wp simp: set_thread_state_def) - apply (fastforce simp: schedulable_def is_sc_active_def get_tcb_def - in_release_queue_def - split: option.splits kernel_object.splits) - done + by (force simp: schedulable_def opt_pred_def opt_map_def tcbs_of_kh_def scs_of_kh_def + get_tcb_def + split: option.splits) lemma hinv_invs': fixes Q :: "'state_ext state \ bool" and calling blocking @@ -1111,10 +1107,9 @@ lemma hinv_invs': assumes sts_Q[wp]: "\a b. \invs and Q\ set_thread_state a b \\_.Q\" shows - "\invs and Q and (\s. scheduler_action s = resume_cur_thread) and - ct_schedulable\ - handle_invocation calling blocking can_donate first_phase cptr - \\rv s. invs s \ Q s\" + "\\s. invs s \ Q s \ scheduler_action s = resume_cur_thread \ ct_schedulable s\ + handle_invocation calling blocking can_donate first_phase cptr + \\_ s. invs s \ Q s\" apply (simp add: handle_invocation_def ts_Restart_case_helper split_def liftE_liftM_liftME liftME_def bindE_assoc) apply (wpsimp wp: syscall_valid sts_invs_minor2 rfk_invs split_del: if_split)+ @@ -1132,9 +1127,10 @@ lemma hinv_invs': apply (simp only: simp_thms K_def if_apply_def2) apply (rule hoare_vcg_conj_elimE) apply (wpsimp wp: decode_inv_inv simp: if_apply_def2)+ - apply (auto simp: ct_in_state_def cur_sc_tcb_invs fault_tcbs_valid_states_active schedulable_def' - dest: invs_fault_tcbs_valid_states - elim: st_tcb_ex_cap) + apply (fastforce intro!: st_tcb_ex_cap[rotated, where P=runnable] + simp: schedulable_def pred_tcb_at_def obj_at_def opt_pred_def opt_map_def + tcbs_of_kh_def runnable_eq_active + split: option.splits if_splits) done lemmas hinv_invs[wp] = hinv_invs' @@ -1144,7 +1140,7 @@ lemma get_cap_reg_inv[wp]: "\P\ get_cap_reg r \\ by (wpsimp simp: get_cap_reg_def) lemma hs_invs[wp]: - "\invs and (\s. scheduler_action s = resume_cur_thread) and ct_schedulable\ + "\\s. invs s \ scheduler_action s = resume_cur_thread \ ct_schedulable s\ handle_send blocking \\_. invs :: 'state_ext state \ bool\" apply (rule validE_valid) @@ -1303,7 +1299,7 @@ lemma do_reply_transfer_nonz_cap: | rule conjI)+ lemma hc_invs[wp]: - "\invs and (\s. scheduler_action s = resume_cur_thread) and ct_schedulable\ + "\\s. invs s \ scheduler_action s = resume_cur_thread \ ct_schedulable s\ handle_call \\_. invs :: 'state_ext state \ bool\" by (simp add: handle_call_def) wpsimp @@ -1315,11 +1311,8 @@ lemma select_insert: by (simp add: alternative_def select_def return_def) lemma update_time_stamp_ct_in_release_queue [wp]: - "update_time_stamp - \\s. P (in_release_queue (cur_thread s) s)\" - by (wpsimp simp: update_time_stamp_def do_machine_op_def - is_sc_active_def get_tcb_def in_release_queue_def - split: option.splits) + "update_time_stamp \\s. P (in_release_queue (cur_thread s) s)\" + by (wpsimp simp: update_time_stamp_def in_release_queue_def) lemma update_time_stamp_invs[wp]: "update_time_stamp \invs\" @@ -1350,10 +1343,13 @@ crunch preemption_point and scheduler_action[wp]: "\s. P (scheduler_action s)" (rule: preemption_point_inv simp: cur_sc_tcb_def ignore_del: preemption_point) +lemma update_time_stamp_schedulable[wp]: + "update_time_stamp \schedulable t\" + by (wpsimp simp: schedulable_def wp: hoare_vcg_ex_lift update_time_stamp_wp) + lemma update_time_stamp_ct_schedulable[wp]: "update_time_stamp \ct_schedulable\" - by (wpsimp simp: schedulable_def' in_release_queue_def - wp: hoare_vcg_ex_lift update_time_stamp_wp) + by (wps | wpsimp)+ crunch thread_set for scheduler_action[wp]: "\s. P (scheduler_action s)" diff --git a/proof/invariant-abstract/TcbAcc_AI.thy b/proof/invariant-abstract/TcbAcc_AI.thy index afef4e4efe..a5388332de 100644 --- a/proof/invariant-abstract/TcbAcc_AI.thy +++ b/proof/invariant-abstract/TcbAcc_AI.thy @@ -794,7 +794,7 @@ lemma idle_thread_idle[wp]: lemma set_thread_state_act_valid_objs[wp]: "set_thread_state_act t \valid_objs\" - unfolding set_thread_state_act_def set_scheduler_action_def is_schedulable_def + unfolding set_thread_state_act_def set_scheduler_action_def by wpsimp lemma set_thread_state_valid_objs[wp]: @@ -1194,7 +1194,7 @@ crunch set_thread_state_act lemma set_thread_state_act_cur_sc_tcb [wp]: "\cur_sc_tcb\ set_thread_state_act tcb_ptr \\_. cur_sc_tcb\" - by (wpsimp simp: set_thread_state_act_def set_scheduler_action_def is_schedulable_def + by (wpsimp simp: set_thread_state_act_def set_scheduler_action_def cur_sc_tcb_def sc_tcb_sc_at_def obj_at_def) lemma sts_cur_tcb [wp]: diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy index 274ab0b192..a792616e67 100644 --- a/proof/invariant-abstract/Tcb_AI.thy +++ b/proof/invariant-abstract/Tcb_AI.thy @@ -319,7 +319,7 @@ lemma set_thread_state_valid_tcb[wp]: apply (rule bind_wp_fwd_skip, wpsimp) apply (rule_tac Q'="\_. valid_tcb ptr tcb" in bind_wp_fwd) apply (wpsimp wp: set_object_valid_tcbs) - apply (wpsimp wp: set_object_valid_tcbs update_valid_tcb is_schedulable_inv hoare_vcg_if_lift2 + apply (wpsimp wp: set_object_valid_tcbs update_valid_tcb hoare_vcg_if_lift2 hoare_vcg_conj_lift hoare_drop_imps simp: set_scheduler_action_def update_valid_tcb) done @@ -333,8 +333,7 @@ lemma set_thread_state_valid_tcbs[wp]: apply (fastforce simp: valid_tcbs_def obj_at_def intro: valid_tcb_state_update) apply (clarsimp simp: valid_tcbs_def) - apply (wpsimp wp: is_schedulable_inv hoare_vcg_if_lift2 hoare_vcg_conj_lift hoare_drop_imps - simp: set_scheduler_action_def) + apply (wpsimp wp: hoare_drop_imps) done lemma reply_unlink_tcb_valid_tcbs[wp]: diff --git a/proof/refine/RISCV64/EmptyFail_H.thy b/proof/refine/RISCV64/EmptyFail_H.thy index 8082b8ae5b..71ad372425 100644 --- a/proof/refine/RISCV64/EmptyFail_H.thy +++ b/proof/refine/RISCV64/EmptyFail_H.thy @@ -321,13 +321,13 @@ theorem call_kernel_serial: (\s. cur_sc_offset_sufficient (consumed_time s) s) and (\s. 0 < domain_time s \ valid_domain_list s)) s; \s'. (s, s') \ state_relation \ - (invs' and (\s. event \ Interrupt \ ct_running' s) and (ct_running' or ct_idle') and - (\s. ksSchedulerAction s = ResumeCurrentThread) and - (\s. vs_valid_duplicates' (ksPSpace s))) s' \ + (invs' and (\s. event \ Interrupt \ schedulable' (ksCurThread s) s) and (ct_running' or ct_idle') and + (\s. ksSchedulerAction s = ResumeCurrentThread)) s' \ \ fst (call_kernel event s) \ {}" apply (cut_tac m = "call_kernel event" in corres_underlying_serial) apply (rule kernel_corres) apply (rule callKernel_empty_fail) + apply (drule spec[where x=s]) apply auto done diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy index 8023742bf6..bc49836e69 100644 --- a/proof/refine/RISCV64/IpcCancel_R.thy +++ b/proof/refine/RISCV64/IpcCancel_R.thy @@ -3240,8 +3240,8 @@ lemma rescheduleRequired_unlive[wp]: "rescheduleRequired \ko_wp_at' (Not \ live') p\" supply comp_apply[simp del] unfolding rescheduleRequired_def - apply (wpsimp wp: isSchedulable_wp tcbSchedEnqueue_unlive_other) - apply (fastforce simp: isSchedulable_bool_def pred_map_simps ko_wp_at'_def opt_map_def o_def) + apply (wpsimp wp: getSchedulable_wp tcbSchedEnqueue_unlive_other) + apply (fastforce simp: schedulable'_def opt_pred_def obj_at'_def ko_wp_at'_def opt_map_def o_def) done crunch scheduleTCB diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index 7ff60049c5..2468a45e59 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -2780,10 +2780,6 @@ lemma valid_sched_weak_strg: "valid_sched s \ weak_valid_sched_action s" by (simp add: valid_sched_def valid_sched_action_def) -lemma runnable_tsr: - "thread_state_relation ts ts' \ runnable' ts' = runnable ts" - by (case_tac ts, auto) - lemma idle_tsr: "thread_state_relation ts ts' \ idle' ts' = idle ts" by (case_tac ts, auto) @@ -3571,9 +3567,7 @@ lemma tcbReleaseEnqueue_corres: apply (wpsimp wp: get_tcb_ready_time_wp) apply (fastforce simp: queue_end_valid_def) apply wpsimp - apply blast apply wpsimp - apply blast apply (rule_tac R="A and K (\ tcbQueueEmpty queue)" and A=A for A in orM_corres'[where R'=A' and A'=A' for A', simplified]) apply corres @@ -3583,7 +3577,6 @@ lemma tcbReleaseEnqueue_corres: apply fastforce apply wpsimp apply wpsimp - apply force \ \deal with the reprogramming of the timer\ apply (simp add: bind_assoc) @@ -3856,7 +3849,7 @@ lemma schedContextResume_corres: apply (rule corres_split_eqr) apply (clarsimp simp: sc_relation_def) apply (rule corres_guard_imp) - apply (rule isSchedulable_corres) + apply (rule getSchedulable_corres) apply (prop_tac "(valid_objs and tcb_at (the (sc_tcb sc)) and pspace_aligned and pspace_distinct) s") apply assumption @@ -3909,8 +3902,8 @@ lemma schedContextResume_corres: apply (rule no_fail_pre) apply (wpsimp simp: thread_get_def) apply (clarsimp simp: tcb_at_def) - apply (wp is_schedulable_wp) - apply (wp isSchedulable_wp) + apply wp + apply (wp getSchedulable_wp) apply wp apply wp apply (subgoal_tac "sc_tcb_sc_at (\t. bound_sc_tcb_at (\sc. sc = Some ptr) (the t) s) ptr s ") @@ -3919,20 +3912,21 @@ lemma schedContextResume_corres: apply (intro conjI; (clarsimp simp: invs_def valid_state_def; fail)?) apply (fastforce simp: invs_def valid_state_def valid_pspace_def valid_obj_def) - apply (clarsimp simp: schedulable_def get_tcb_def obj_at_kh_kheap_simps) + apply (clarsimp simp: schedulable_def2 get_tcb_def obj_at_kh_kheap_simps) apply (rename_tac t; prop_tac "budget_sufficient t s") apply (erule active_valid_budget_sufficient) - apply (clarsimp simp: vs_all_heap_simps) + apply (clarsimp simp: schedulable_def2) + apply (prop_tac "is_active_sc ptr s") + apply (fastforce simp: vs_all_heap_simps) + apply clarsimp + apply (frule (1) active_scs_validE) + apply (frule valid_refills_nonempty_refills) apply (intro conjI impI) - apply (fastforce simp: valid_refills_def vs_all_heap_simps rr_valid_refills_def - opt_map_red opt_pred_def MIN_REFILLS_def - dest!: active_scs_validE split: if_split_asm) - apply (fastforce simp: valid_refills_def vs_all_heap_simps rr_valid_refills_def - dest!: active_scs_validE) - apply (fastforce simp: vs_all_heap_simps valid_ready_qs_2_def - valid_ready_queued_thread_2_def in_ready_q_def) + apply (fastforce simp: valid_refills_def vs_all_heap_simps rr_valid_refills_def) + apply fastforce + apply (fastforce simp: vs_all_heap_simps) apply (fastforce simp: vs_all_heap_simps valid_ready_qs_2_def - valid_ready_queued_thread_2_def in_ready_q_def) + valid_ready_queued_thread_2_def in_ready_q_def) apply (fastforce simp: vs_all_heap_simps valid_ready_qs_2_def valid_ready_queued_thread_2_def in_ready_q_def) apply (fastforce simp: vs_all_heap_simps valid_ready_qs_2_def @@ -3955,10 +3949,10 @@ lemma schedContextResume_corres: apply (erule (1) valid_sched_context_size_objsI, simp) apply (clarsimp simp: sc_relation_def projection_rewrites obj_at_simps opt_map_red) apply (frule_tac x=y in pspace_relation_absD[OF _ state_relation_pspace_relation]; simp) - apply (clarsimp simp: obj_at'_def isSchedulable_bool_def projection_rewrites + apply (clarsimp simp: obj_at'_def schedulable'_def projection_rewrites tcb_relation_cut_def tcb_relation_def) apply (drule sym[where s="Some ptr"]) - apply (clarsimp simp: projection_rewrites isScActive_def opt_map_red) + apply (clarsimp simp: projection_rewrites opt_map_red) apply (erule (1) valid_objsE') apply (clarsimp simp: valid_obj'_def valid_sched_context'_def sc_relation_def valid_refills'_def opt_map_def opt_pred_def is_active_sc'_def) @@ -4272,7 +4266,7 @@ lemma sendSignal_corres: apply (simp add: badgeRegister_def badge_register_def) apply (rule corres_split[OF asUser_setRegister_corres]) apply (rule corres_split[OF maybeDonateSc_corres]) - apply (rule corres_split[OF isSchedulable_corres]) + apply (rule corres_split[OF getSchedulable_corres]) apply (rule corres_split[OF corres_when], simp) apply (rule possibleSwitchTo_corres; (solves simp)?) apply (rule corres_split_eqr[OF get_tcb_obj_ref_corres]) @@ -4291,8 +4285,8 @@ lemma sendSignal_corres: apply (rule_tac Q'="\_. tcb_at' a and valid_objs'" in hoare_strengthen_post[rotated]) apply (clarsimp simp: obj_at'_def split: option.split) apply wpsimp - apply (wpsimp wp: is_schedulable_wp) - apply (wpsimp wp: isSchedulable_wp) + apply wpsimp + apply (wpsimp wp: getSchedulable_wp) apply (rule_tac Q'="\_. valid_objs and pspace_aligned and pspace_distinct and tcb_at a and valid_sched_action and active_scs_valid and in_correct_ready_q and ready_qs_distinct @@ -4364,7 +4358,7 @@ lemma sendSignal_corres: apply (simp add: badgeRegister_def badge_register_def) apply (rule corres_split[OF asUser_setRegister_corres]) apply (rule corres_split[OF maybeDonateSc_corres]) - apply (rule corres_split[OF isSchedulable_corres]) + apply (rule corres_split[OF getSchedulable_corres]) apply (rule corres_split[OF corres_when], simp) apply (rule possibleSwitchTo_corres; (solves simp)?) apply (rule corres_split_eqr[OF get_tcb_obj_ref_corres]) @@ -4383,8 +4377,8 @@ lemma sendSignal_corres: apply (rule_tac Q'="\_. tcb_at' (hd list) and valid_objs'" in hoare_strengthen_post[rotated]) apply (clarsimp simp: obj_at'_def split: option.split) apply wpsimp - apply (wpsimp wp: is_schedulable_wp) - apply (wpsimp wp: isSchedulable_wp) + apply wpsimp + apply (wpsimp wp: getSchedulable_wp) apply (rule_tac Q'="\_. valid_objs and pspace_aligned and pspace_distinct and tcb_at (hd list) and valid_sched_action and active_scs_valid and in_correct_ready_q and ready_qs_distinct and ready_or_release" @@ -4715,9 +4709,9 @@ lemma sai_invs'[wp]: apply (case_tac "ntfnBoundTCB nTFN"; clarsimp) apply (wp setNotification_invs') apply (clarsimp simp: valid_ntfn'_def) - apply (wp isSchedulable_wp) + apply (wp getSchedulable_wp) apply (rule_tac Q'="\_. invs'" in hoare_strengthen_post[rotated]) - apply (clarsimp simp: isSchedulable_bool_def isSchedulable_bool_runnableE) + apply (clarsimp simp: schedulable'_def) apply (wpsimp wp: maybeDonateSc_invs' setThreadState_Running_invs' setNotification_invs' gts_wp' cancelIPC_simple simp: o_def @@ -4733,9 +4727,9 @@ lemma sai_invs'[wp]: \ \WaitingNtfn\ apply (rename_tac list) apply (case_tac list; clarsimp) - apply (wp isSchedulable_wp) + apply (wp getSchedulable_wp) apply (rule_tac Q'="\_. invs'" in hoare_strengthen_post[rotated]) - apply (clarsimp simp: isSchedulable_bool_def isSchedulable_bool_runnableE) + apply (clarsimp simp: schedulable'_def) apply (wp maybeDonateSc_invs' setThreadState_Running_invs' setNotification_invs')+ apply (clarsimp cong: conj_cong simp: valid_ntfn'_def) apply (rule conjI) @@ -6965,7 +6959,8 @@ lemma doReplyTransfer_corres: apply wpsimp apply (clarsimp split: option.splits) apply (clarsimp split: option.splits simp: valid_pspace'_def) - apply (clarsimp simp: isRunnable_def get_tcb_obj_ref_def) + apply (clarsimp simp: isRunnable_def readRunnable_def get_tcb_obj_ref_def + simp flip: getThreadState_def threadGet_def) (* solve remaining corres goals *) apply (rule corres_split [OF getThreadState_corres]) apply (rule corres_split [OF threadGet_corres[where r="(=)"]]) diff --git a/proof/refine/RISCV64/Refine.thy b/proof/refine/RISCV64/Refine.thy index bb5cff9b31..eadb8f646a 100644 --- a/proof/refine/RISCV64/Refine.thy +++ b/proof/refine/RISCV64/Refine.thy @@ -495,30 +495,22 @@ lemma akernel_invariant: done lemma ckernel_invs: - "\invs' and (\s. sym_refs (state_refs_of' s)) - and (\s. e \ Interrupt \ ct_running' s) and (ct_running' or ct_idle') - and (\s. is_active_sc' (ksCurSc s) s) and sym_heap_tcbSCs - and (\s. obj_at' (\sc. scTCB sc = Some (ksCurThread s)) (ksCurSc s) s) - and (\s. pred_map (\tcb. \ tcbInReleaseQueue tcb) (tcbs_of' s) (ksCurThread s)) + "\invs' and (\s. e \ Interrupt \ schedulable' (ksCurThread s) s) and (\s. ksSchedulerAction s = ResumeCurrentThread)\ callKernel e \\_. invs'\" - apply (simp add: callKernel_def mcsPreemptionPoint_def) - apply (rule hoare_pre) - apply (wpsimp wp: hoare_drop_imp[where Q'="\_. kernelExitAssertions"] activate_invs') - apply (rule hoare_drop_imp) - apply (wpsimp wp: schedule_invs') - apply (wpsimp wp: stateAssert_wp) - apply (wpsimp wp: isSchedulable_wp hoare_drop_imp) - apply (intro iffI; clarsimp simp: isScActive_def isSchedulable_bool_def) - apply (rule hoare_strengthen_postE[where E'="\_. invs'" and Q=Q and Q'=Q for Q]) - apply wpsimp - apply (clarsimp simp: active_from_running')+ - apply wp - apply (clarsimp simp: sym_heap_def pred_map_def) - apply (rule_tac x="ksCurSc s" in exI) - apply (clarsimp simp: obj_at_simps is_active_sc'_def isScActive_def opt_map_red pred_map_def - opt_pred_def) + apply (simp add: callKernel_def mcsPreemptionPoint_def cur_tcb'_asrt_def) + apply (wpsimp wp: hoare_drop_imp[where Q'="\_. kernelExitAssertions"] activate_invs') + apply (rule hoare_drop_imp) + apply (wpsimp wp: schedule_invs') + apply (wpsimp wp: stateAssert_wp) + apply (wpsimp wp: getSchedulable_wp hoare_drop_imp) + apply (intro iffI; clarsimp simp: schedulable'_def) + apply (rule hoare_strengthen_postE[where E'="\_. invs'" and Q=Q and Q'=Q for Q]) + apply wpsimp + apply (clarsimp simp: active_from_running')+ + apply wp+ + apply clarsimp done (* abstract and haskell have identical domain list fields *) @@ -578,30 +570,17 @@ lemma threadSet_sym_heap_tcbSCs: done lemma kernelEntry_invs': - "\ invs' and (\s. sym_refs (state_refs_of' s)) and (\s. e \ Interrupt \ ct_running' s) + "\invs' and (\s. e \ Interrupt \ ct_running' s) and (ct_running' or ct_idle') - and (\s. is_active_sc' (ksCurSc s) s) and sym_heap_tcbSCs - and (\s. obj_at' (\sc. scTCB sc = Some (ksCurThread s)) (ksCurSc s) s) - and (\s. pred_map (\tcb. \ tcbInReleaseQueue tcb) (tcbs_of' s) (ksCurThread s)) + and (\s. e \ Interrupt \ schedulable' (ksCurThread s) s) and (\s. ksSchedulerAction s = ResumeCurrentThread) and valid_domain_list' \ kernelEntry e tc \\_. invs'\" - apply (rule_tac P'1="\s. obj_at' (\tcb. tcbSchedContext tcb = Some (ksCurSc s)) (ksCurThread s) s" - in hoare_pre_add[THEN iffD2]) - apply (clarsimp simp: obj_at'_tcb_scs_of_equiv obj_at'_sc_tcbs_of_equiv sym_heap_def) - apply (fastforce simp: ct_in_state'_def pred_tcb_at'_def obj_at'_def) - apply (simp add: kernelEntry_def) - apply (wpsimp wp: ckernel_invs threadSet_invs_trivial threadSet_state_refs_of'[where f'=id and g'=id] - threadSet_ct_in_state' hoare_weak_lift_imp hoare_vcg_disj_lift threadSet_sym_heap_tcbSCs - simp: tcb_bound_refs'_def - | wps)+ - apply (rule hoare_vcg_conj_lift) - apply (wpsimp wp: threadSet_wp) - apply (wpsimp wp: threadSet_invs_trivial; simp?) - apply (wpsimp wp: threadSet_ct_running' hoare_weak_lift_imp)+ - apply (fastforce simp: obj_at'_def pred_map_def opt_map_red) - done + unfolding kernelEntry_def + by (wpsimp wp: ckernel_invs threadSet_invs_trivial threadSet_ct_in_state' hoare_weak_lift_imp + hoare_vcg_disj_lift threadSet_schedulable'_fields_inv + | wps)+ lemma absKState_correct': "\einvs s; invs' s'; (s,s') \ state_relation\ @@ -693,14 +672,14 @@ lemma kernel_preemption_corres: apply (rule no_fail_getActiveIRQ) apply (clarsimp simp: dc_def[symmetric]) apply (rule corres_split_eqr[OF getCurThread_corres]) - apply (rule corres_split_eqr[OF isSchedulable_corres]) + apply (rule corres_split_eqr[OF getSchedulable_corres]) apply (rename_tac irq ct sched) apply (rule corres_split[OF corres_if2]) apply simp apply (rule_tac P="?P and (\s. ct = cur_thread s) and (\s. sched = schedulable ct s) and K sched" and P'="?P' and (\s. ct = ksCurThread s) - and (\s. sched = isSchedulable_bool ct s)" + and (\s. sched = schedulable' ct s)" in corres_inst) apply (rule corres_gen_asm') apply(rule corres_guard_imp) @@ -753,8 +732,8 @@ lemma kernel_preemption_corres: apply clarsimp apply (wpsimp wp: hoare_vcg_imp_lift') apply clarsimp - apply (wpsimp wp: is_schedulable_wp') - apply (wpsimp wp: isSchedulable_wp cong: conj_cong imp_cong) + apply wpsimp + apply (wpsimp wp: getSchedulable_wp cong: conj_cong imp_cong) apply wpsimp apply wpsimp apply (rule_tac Q'="\_ s. invs s \ valid_sched s \ valid_list s \ scheduler_act_sane s \ @@ -829,7 +808,8 @@ lemma kernel_corres': and (\s. scheduler_action s = resume_cur_thread)) invs' (call_kernel event) - (do _ \ runExceptT $ + (do _ \ stateAssert cur_tcb'_asrt []; + _ \ runExceptT $ handleEvent event `~catchError~` (\_. withoutPreemption $ do irq_opt <- doMachineOp (getActiveIRQ True); @@ -846,37 +826,21 @@ lemma kernel_corres': apply add_sym_refs apply (rule_tac Q'="\s. ksSchedulerAction s = ResumeCurrentThread" in corres_cross_add_guard) apply (fastforce intro!: resume_cur_thread_cross) - apply (rule_tac Q'="\s. event \ Interrupt \ ct_running' s" in corres_cross_add_guard) - apply (fastforce intro!: ct_running_cross) + apply (rule_tac Q'="\s'. event \ Interrupt \ schedulable' (ksCurThread s') s'" + in corres_cross_add_guard) + apply (frule curthread_relation) + apply clarsimp + apply (erule schedulable_schedulable'_eq[THEN iffD1], fastforce+) + apply (clarsimp simp: schedulable_def2) + apply (rule conjI) + apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def) + apply (fastforce intro: schact_is_rct_ct_active_sc) apply (rule_tac Q'="ct_running' or ct_idle'" in corres_cross_add_guard) apply (simp only: pred_disj_def) apply (rule ct_running_or_idle_cross, fastforce+) - apply (rule_tac Q'="\s. obj_at' (\sc. scTCB sc = Some (ksCurThread s)) (ksCurSc s) s" in corres_cross_add_guard) - apply (fastforce simp: invs_def valid_state_def valid_pspace_def intro!: cur_sc_tcb_cross) - apply (rule_tac Q'="\s'. pred_map (\tcb. \ tcbInReleaseQueue tcb) (tcbs_of' s') (ksCurThread s')" - in corres_cross_add_guard) - apply clarsimp - apply (rule ct_not_in_release_q_cross) - apply fastforce - apply (simp add: state_relation_def) - apply (simp add: state_relation_def) - apply fastforce - apply simp - apply (rule_tac Q'="\s'. pred_map (\scPtr. isScActive scPtr s') (tcbSCs_of s') (ksCurThread s')" - in corres_cross_add_guard) - apply clarsimp - apply (frule invs_cur_sc_tcb_symref, clarsimp simp: schact_is_rct) - apply (prop_tac "sc_at (cur_sc s) s") - apply (frule invs_cur_sc_tcb) - apply (clarsimp simp: cur_sc_tcb_def sc_tcb_sc_at_def obj_at_def is_sc_obj) - apply (erule (1) valid_sched_context_size_objsI[OF invs_valid_objs]) - apply (frule (4) active_sc_at'_cross[OF _ invs_psp_aligned invs_distinct]) - apply (clarsimp simp: active_sc_at'_def obj_at'_def projectKOs cur_tcb'_def pred_tcb_at_def - is_sc_obj obj_at_def pred_map_def isScActive_def - dest!: state_relationD) - apply (rule_tac x="cur_sc s" in exI, clarsimp simp: opt_map_red) - apply (frule_tac x="ksCurThread s'" in pspace_relation_absD, simp) - subgoal by (fastforce simp: tcb_relation_cut_def tcb_relation_def) + apply (rule corres_stateAssert_ignore) + apply (clarsimp simp: cur_tcb'_asrt_def) + apply simp apply (rule corres_guard_imp) apply (rule corres_split) apply (rule corres_split_handle[OF handleEvent_corres]) @@ -958,9 +922,9 @@ lemma kernel_corres': | strengthen ct_not_blocked_imp_ct_not_blocked_on_receive ct_not_blocked_imp_ct_not_blocked_on_ntfn)+)[1] apply (wpsimp wp: he_invs') - apply (wpsimp simp: mcsPreemptionPoint_def wp: isSchedulable_wp) + apply (wpsimp simp: mcsPreemptionPoint_def wp: getSchedulable_wp) apply (wpsimp wp: dmo_getirq_inv) - apply (clarsimp simp: isSchedulable_bool_def isScActive_def) + apply (clarsimp simp: schedulable'_def) apply (rule_tac Q'="\_. invs'" and E'="\_. invs'" in hoare_strengthen_postE) apply (wpsimp wp: he_invs') apply simp @@ -980,7 +944,10 @@ lemma kernel_corres': apply (clarsimp simp: invs_def valid_state_def valid_pspace_def invs_strengthen_cur_sc_tcb_are_bound) apply simp - apply (clarsimp simp: active_from_running') + apply clarsimp + apply (frule schedulable'_runnableE) + apply (clarsimp simp: cur_tcb'_def) + apply (clarsimp simp: st_tcb_at'_def obj_at'_def ct_in_state'_def) done lemma kernel_corres: @@ -1268,37 +1235,27 @@ lemma ckernel_invariant: apply (rule hoare_weaken_pre) apply (rule kernelEntry_invs') apply clarsimp + apply (frule_tac a=sa and b=s in curthread_relation) apply (rename_tac s' s; intro conjI) - apply (frule_tac s=s in invs_sym_refs) - apply (frule_tac s'=s' in state_refs_of_cross_eq) - apply fastforce - apply fastforce - apply force - apply clarsimp - apply (erule (1) ct_running_cross) - apply fastforce - apply fastforce - apply (erule (1) ct_running_or_idle_cross) - apply fastforce + apply (frule_tac s=s in invs_sym_refs) + apply (frule_tac s'=s' in state_refs_of_cross_eq) apply fastforce - apply (prop_tac "cur_sc s = ksCurSc s'", fastforce dest!: state_relationD) - apply (prop_tac "sc_at (cur_sc s) s") - apply (rule cur_sc_tcb_sc_at_cur_sc[OF invs_valid_objs invs_cur_sc_tcb]; simp) - apply (prop_tac "sc_at' (ksCurSc s') s'") - apply (rule sc_at_cross[OF state_relation_pspace_relation invs_psp_aligned invs_distinct]; simp) - apply (prop_tac "is_active_sc' (ksCurSc s') s'") - apply (rule is_active_sc'2_cross[OF _ invs_psp_aligned invs_distinct], simp+) - apply (clarsimp simp: invs'_def valid_pspace'_def, rule sym_refs_tcbSCs; simp?) - apply (clarsimp simp: invs_def valid_state_def valid_pspace_def state_refs_of_cross_eq) - apply (fastforce dest!: cur_sc_tcb_cross[simplified schact_is_rct_def] - simp: invs_def valid_state_def valid_pspace_def) - apply (clarsimp simp: invs'_def) - apply (prop_tac "cur_tcb' s'") - apply (rule cur_tcb_cross[OF invs_cur invs_psp_aligned invs_distinct]; simp?) - apply (rule_tac s=s and s'=s' in ct_not_in_release_q_cross) - apply blast - apply (erule state_relation_release_queue_relation) - apply (erule curthread_relation[symmetric]) + apply fastforce + apply clarsimp + apply (erule (1) ct_running_cross) + apply fastforce + apply fastforce + apply (erule (1) ct_running_or_idle_cross) + apply fastforce + apply fastforce + apply clarsimp + apply (erule schedulable_schedulable'_eq[THEN iffD1], fastforce+) + apply (clarsimp simp: schedulable_def2) + apply (rule conjI) + apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def) + apply (rule schact_is_rct_ct_active_sc) + apply fastforce + apply (clarsimp simp: schact_is_rct_def) apply fastforce apply (rule_tac a=s in resume_cur_thread_cross) apply assumption diff --git a/proof/refine/RISCV64/SchedContextInv_R.thy b/proof/refine/RISCV64/SchedContextInv_R.thy index 7866b94f19..44dc838882 100644 --- a/proof/refine/RISCV64/SchedContextInv_R.thy +++ b/proof/refine/RISCV64/SchedContextInv_R.thy @@ -563,7 +563,7 @@ lemma schedContextYieldTo_corres: apply (rename_tac tp) apply (simp only: option.sel pred_conj_def simp_thms(21)) apply (rule corres_guard_imp) - apply (rule corres_split_eqr[OF isSchedulable_corres]) + apply (rule corres_split_eqr[OF getSchedulable_corres]) apply (rename_tac sched) apply (rule corres_split_eqr) apply (rule_tac P="?abs_buf and sc_yf_sc_at ((=) None) scp and ?ct and ?scp @@ -687,8 +687,7 @@ lemma schedContextYieldTo_corres: apply (clarsimp simp:obj_at'_def) apply (wpsimp wp: thread_get_wp hoare_case_option_wp)+ apply (wpsimp wp: threadGet_wp)+ - apply (wpsimp wp: is_schedulable_wp) - apply (wpsimp wp: isSchedulable_wp) + apply (wpsimp wp: getSchedulable_wp) apply (clarsimp simp: invs_def valid_state_def valid_pspace_def valid_objs_valid_tcbs cong: conj_cong imp_cong if_cong) apply (rule context_conjI; @@ -697,8 +696,9 @@ lemma schedContextYieldTo_corres: apply (fastforce simp: valid_obj_def obj_at_def valid_sched_context_def) apply (intro conjI impI; clarsimp simp: is_tcb pred_tcb_at_def obj_at_def) apply (erule (1) valid_sched_context_size_objsI)+ - apply (clarsimp simp: invs'_def valid_pspace'_def valid_objs'_valid_tcbs') - apply (clarsimp simp: obj_at'_def opt_map_red) + apply (fastforce dest: sc_ko_at_valid_objs_valid_sc' + simp: valid_sched_context'_def valid_bound_obj'_def obj_at'_def + opt_map_red) apply (rule_tac Q'="\rv. (case buf of None \ \_. True | Some x \ in_user_frame x) and einvs and sc_yf_sc_at ((=) None) scp and ct_active and ct_not_in_release_q and diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index 39a2ac6216..e852491b62 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -202,7 +202,6 @@ lemma tcbSchedAppend_corres: apply (rule corres_symb_exec_r[OF _ isRunnable_sp]; wpsimp?) apply (rule corres_symb_exec_r[OF _ assert_sp, rotated]; (solves wpsimp)?) apply wpsimp - apply (fastforce simp: st_tcb_at'_def runnable_eq_active' obj_at'_def) apply (rule corres_symb_exec_r[OF _ threadGet_sp]; (solves wpsimp)?) apply (subst if_distrib[where f="set_tcb_queue domain prio" for domain prio]) apply (rule corres_if_strong') @@ -944,22 +943,22 @@ lemma obj_tcb_at': by (clarsimp simp: obj_at'_def) lemma scheduleTCB_rct: - "\\s. (t = ksCurThread s \ isSchedulable_bool t s) + "\\s. (t = ksCurThread s \ schedulable' t s) \ ksSchedulerAction s = ResumeCurrentThread\ scheduleTCB t \\_ s. ksSchedulerAction s = ResumeCurrentThread\" unfolding scheduleTCB_def - by (wpsimp wp: isSchedulable_wp | rule hoare_pre_cont)+ + by (wpsimp wp: getSchedulable_wp | rule hoare_pre_cont)+ lemma setThreadState_rct: "\\s. (t = ksCurThread s \ runnable' st - \ pred_map (\tcb. \(tcbInReleaseQueue tcb)) (tcbs_of' s) t - \ pred_map (\scPtr. isScActive scPtr s) (tcbSCs_of s) t) + \ (Not \ tcbInReleaseQueue |< (tcbs_of' s)) t + \ ((\sc. 0 < scRefillMax sc) |< (tcbs_of' s |> tcbSchedContext |> scs_of' s)) t) \ ksSchedulerAction s = ResumeCurrentThread\ setThreadState st t \\_ s. ksSchedulerAction s = ResumeCurrentThread\" unfolding setThreadState_def - by (wpsimp wp: scheduleTCB_rct hoare_vcg_all_lift hoare_vcg_imp_lift' threadSet_isSchedulable_bool) + by (wpsimp wp: scheduleTCB_rct hoare_vcg_all_lift hoare_vcg_imp_lift' threadSet_schedulable') lemma bitmapQ_lookupBitmapPriority_simp: (* neater unfold, actual unfold is really ugly *) "\ ksReadyQueuesL1Bitmap s d \ 0 ; @@ -1160,14 +1159,6 @@ crunch tcbSchedEnqueue for cur[wp]: cur_tcb' (simp: unless_def) -lemma is_schedulable_exs_valid[wp]: - "active_sc_tcb_at t s \ \(=) s\ is_schedulable t \\\r. (=) s\" - apply (clarsimp simp: is_schedulable_def exs_valid_def Bex_def pred_map_def vs_all_heap_simps - split: option.splits) - apply (clarsimp simp: in_monad get_tcb_ko_at obj_at_def get_sched_context_def Option.is_none_def - get_object_def) - done - lemma gts_exs_valid[wp]: "tcb_at t s \ \(=) s\ get_thread_state t \\\r. (=) s\" apply (clarsimp simp: get_thread_state_def assert_opt_def fail_def @@ -1187,16 +1178,15 @@ lemma guarded_switch_to_corres: apply (rule corres_guard_imp) apply (rule corres_symb_exec_l'[OF _ thread_get_exs_valid]) apply (rule corres_assert_opt_assume_l) - apply (rule corres_symb_exec_l'[OF _ is_schedulable_exs_valid]) + apply (rule corres_symb_exec_l'[OF _ gets_exs_valid]) apply (rule corres_assert_assume_l) apply (rule switchToThread_corres) - apply assumption - apply (wpsimp wp: is_schedulable_wp) + apply wpsimp apply assumption apply (wpsimp wp: thread_get_wp') apply (clarsimp simp: schedulable_def2 tcb_at_kh_simps pred_map_def vs_all_heap_simps obj_at_def is_tcb) - apply simp + apply simp+ done abbreviation "enumPrio \ [0.e.maxPriority]" @@ -1270,112 +1260,11 @@ lemma ntfn_at'_cross_rel: apply clarsimp by (erule (3) ntfn_at_cross) -lemma runnable_cross_rel: - "cross_rel (pspace_aligned and pspace_distinct and st_tcb_at runnable t) - (\s'. pred_map (\tcb. runnable' (tcbState tcb)) (tcbs_of' s') t)" - apply (rule cross_rel_imp[OF tcb_at'_cross_rel[where t=t]]) - apply (clarsimp simp: cross_rel_def) - apply (subgoal_tac "pspace_relation (kheap s) (ksPSpace s')") - apply (clarsimp simp: tcb_at_kh_simps pred_map_def cross_rel_def obj_at'_def) - apply (clarsimp simp: vs_all_heap_simps pspace_relation_def) - apply (drule_tac x=t in bspec; clarsimp) - apply (clarsimp simp: opt_map_def) - apply (clarsimp simp: tcb_relation_cut_def tcb_relation_def thread_state_relation_def) - apply (case_tac "tcb_state b"; simp add: runnable_def) - apply clarsimp - apply clarsimp - done - -lemma tcbInReleaseQueue_cross_rel: - "cross_rel (pspace_aligned and pspace_distinct and tcb_at t and not_in_release_q t) - (\s'. pred_map (\tcb. \ tcbInReleaseQueue tcb) (tcbs_of' s') t)" - apply (clarsimp simp: cross_rel_def) - apply (clarsimp simp: pred_map_def cross_rel_def obj_at'_def obj_at_def is_tcb) - apply (frule state_relation_pspace_relation) - apply (frule (2) tcb_at_cross) - apply (fastforce simp: obj_at_def is_tcb) - apply normalise_obj_at' - apply (rename_tac tcb') - apply (rule_tac x=tcb' in exI) - apply (rule conjI) - apply (clarsimp simp: opt_map_def obj_at'_def) - apply (drule state_relation_release_queue_relation) - apply (clarsimp simp: release_queue_relation_def list_queue_relation_def) - apply (force simp: not_in_release_q_def opt_pred_def opt_map_def obj_at'_def) - done - -lemma isScActive_cross_rel: - "cross_rel (pspace_aligned and pspace_distinct and valid_objs and active_sc_tcb_at t) - (\s'. pred_map ((\scPtr. isScActive scPtr s')) (tcbSCs_of s') t)" - supply projectKOs[simp del] - apply (rule cross_rel_imp[OF tcb_at'_cross_rel[where t=t]]) - apply (clarsimp simp: cross_rel_def) - apply (subgoal_tac "pspace_relation (kheap s) (ksPSpace s')") - apply (clarsimp simp: pred_map_def obj_at'_real_def ko_wp_at'_def vs_all_heap_simps) - apply (subgoal_tac "sc_at' ref' s'") - apply (clarsimp simp: vs_all_heap_simps pspace_relation_def) - apply (drule_tac x=t in bspec, clarsimp) - apply (clarsimp simp: other_obj_relation_def split: option.splits) - apply (rename_tac s s' scp ko' tcb sc n x) - apply (case_tac "ko'"; simp add: tcb_relation_cut_def) - apply (subgoal_tac "pspace_relation (kheap s) (ksPSpace s')") - apply (clarsimp simp: vs_all_heap_simps pspace_relation_def) - apply (drule_tac x=scp in bspec, clarsimp) - apply (subgoal_tac "valid_sched_context_size n") - apply (clarsimp simp: other_obj_relation_def split: option.splits) - apply (clarsimp simp: obj_at'_def projectKO_eq Bits_R.projectKO_sc) - apply (clarsimp simp: opt_map_def tcb_relation_def) - apply (rule_tac x=scp in exI, simp) - apply (clarsimp simp: isScActive_def active_sc_def) - apply (clarsimp simp: obj_at'_def projectKO_eq Bits_R.projectKO_sc pred_map_def opt_map_def) - apply (clarsimp simp: sc_relation_def) - apply (rule_tac sc=sc in valid_objs_valid_sched_context_size, assumption) - apply fastforce - apply clarsimp - apply (erule (2) sc_at_cross) - apply (clarsimp simp: obj_at_def is_sc_obj_def) - apply (rule_tac sc=ya in valid_objs_valid_sched_context_size, assumption) - apply fastforce - apply clarsimp - apply (clarsimp simp: obj_at_kh_kheap_simps pred_map_def vs_all_heap_simps is_tcb) - done - -lemma isSchedulable_bool_cross_rel: - "cross_rel (pspace_aligned and pspace_distinct and valid_objs and schedulable t) - (isSchedulable_bool t)" - apply (rule cross_rel_imp[OF isScActive_cross_rel[where t=t]]) - apply (rule cross_rel_imp[OF tcbInReleaseQueue_cross_rel[where t=t]]) - apply (rule cross_rel_imp[OF runnable_cross_rel[where t=t]]) - apply (clarsimp simp: isSchedulable_bool_def pred_map_conj[simplified pred_conj_def]) - apply (clarsimp simp: schedulable_def2)+ - done - lemmas tcb_at'_example = corres_cross[where Q' = "tcb_at' t" for t, OF tcb_at'_cross_rel] -(* FIXME RT: move to AInvs? *) -lemma no_fail_is_schedulable: - "no_fail (tcb_at t and valid_tcbs) (is_schedulable t)" - unfolding is_schedulable_def - apply wpsimp - apply (intro conjI impI allI) - apply (clarsimp simp: obj_at_def get_tcb_def is_tcb_def - split: option.splits Structures_A.kernel_object.splits) - apply (clarsimp simp: obj_at_def get_tcb_def is_tcb_def - split: option.splits Structures_A.kernel_object.splits) - apply (clarsimp simp: obj_at_def get_tcb_def is_tcb_def Option.is_none_def - split: option.splits Structures_A.kernel_object.splits) - apply (rename_tac sc_ptr) - apply (prop_tac "sc_at sc_ptr s") - subgoal - by (fastforce simp: valid_tcbs_def obj_at_def valid_tcb_def valid_bound_obj_def - split: option.splits) - apply (clarsimp simp: obj_at_def is_sc_obj_def) - apply (rename_tac ko n, case_tac ko; clarsimp) - done - lemma schedulable_imp_tcb_at: "schedulable t s \ tcb_at t s" - by (clarsimp simp: schedulable_def get_tcb_def obj_at_def is_tcb_def + by (clarsimp simp: schedulable_def opt_pred_def opt_map_def obj_at_def is_tcb_def tcbs_of_kh_def split: option.splits Structures_A.kernel_object.splits) lemma guarded_switch_to_chooseThread_fragment_corres: @@ -1383,8 +1272,6 @@ lemma guarded_switch_to_chooseThread_fragment_corres: (P and schedulable t and invs and valid_ready_qs and ready_or_release) (P' and invs') (guarded_switch_to t) (ThreadDecls_H.switchToThread t)" - apply (rule corres_cross[where Q' = "isSchedulable_bool t", OF isSchedulable_bool_cross_rel], - fastforce) apply (clarsimp simp: guarded_switch_to_def) apply (rule corres_symb_exec_l[rotated, OF _ thread_get_sp]) apply (rule thread_get_exs_valid) @@ -1393,22 +1280,17 @@ lemma guarded_switch_to_chooseThread_fragment_corres: apply (fastforce intro: schedulable_imp_tcb_at) apply (rule corres_symb_exec_l[rotated, OF _ assert_opt_sp]) apply wpsimp - apply (clarsimp simp: schedulable_def get_tcb_def obj_at_def is_tcb_def - split: option.splits Structures_A.kernel_object.splits) + apply (clarsimp simp: schedulable_def opt_pred_def opt_map_def obj_at_def is_tcb_def tcbs_of_kh_def + split: option.splits) apply wpsimp - apply (clarsimp simp: schedulable_def get_tcb_def obj_at_def is_tcb_def - split: option.splits Structures_A.kernel_object.splits) - apply (rule corres_symb_exec_l[rotated, OF _ is_schedulable_sp']) - apply wpsimp - apply (clarsimp simp: schedulable_def get_tcb_def vs_all_heap_simps is_sc_active_def - split: option.splits Structures_A.kernel_object.splits) + apply (clarsimp simp: schedulable_def opt_pred_def opt_map_def obj_at_def is_tcb_def tcbs_of_kh_def + split: option.splits) + apply (rule corres_symb_exec_l[rotated, OF _ gets_sp]) apply wpsimp - apply (wpsimp wp: no_fail_is_schedulable) - apply (fastforce intro: schedulable_imp_tcb_at) + apply (clarsimp simp: schedulable_def get_tcb_def vs_all_heap_simps) apply (rule corres_symb_exec_l[rotated, OF _ assert_sp]; wpsimp) apply (rule corres_guard_imp) apply (rule switchToThread_corres) - apply (wpsimp wp: is_schedulable_wp) apply (fastforce simp: schedulable_def2) apply fastforce done @@ -2251,29 +2133,22 @@ lemma switchSchedContext_invs': simp: getCurSc_def) done -lemma isSchedulable_bool_runnableE: - "isSchedulable_bool t s \ tcb_at' t s \ st_tcb_at' runnable' t s" - unfolding isSchedulable_bool_def - by (clarsimp simp: pred_tcb_at'_def obj_at'_def pred_map_def - elim!: opt_mapE) - lemma rescheduleRequired_invs'[wp]: "rescheduleRequired \invs'\" unfolding rescheduleRequired_def - apply (wpsimp wp: ssa_invs' isSchedulable_wp) - done + by (wpsimp wp: ssa_invs' getSchedulable_wp) lemma rescheduleRequired_ksSchedulerAction[wp]: "\\_. P ChooseNewThread\ rescheduleRequired \\_ s. P (ksSchedulerAction s)\" - unfolding rescheduleRequired_def by (wpsimp wp: isSchedulable_wp) + unfolding rescheduleRequired_def by (wpsimp wp: getSchedulable_wp) lemma inReleaseQueue_wp: "\\s. \ko. ko_at' ko tcb_ptr s \ P (tcbInReleaseQueue ko) s\ inReleaseQueue tcb_ptr \P\" - unfolding inReleaseQueue_def threadGet_getObject + unfolding inReleaseQueue_def readInReleaseQueue_def threadGet_getObject apply (wpsimp wp: getObject_tcb_wp) - apply (clarsimp simp: obj_at'_def) + apply (clarsimp dest!: threadRead_SomeD simp: obj_at'_def) done crunch possibleSwitchTo @@ -2376,11 +2251,11 @@ lemma schedule_invs': apply (rule_tac P'="invs' and cur_tcb'" in hoare_weaken_pre) apply (rule bind_wp_fwd_skip, wpsimp) apply (rule_tac bind_wp[OF _ getCurThread_sp]) - apply (rule_tac bind_wp[OF _ isSchedulable_sp]) + apply (rule_tac bind_wp[OF _ getSchedulable_sp]) apply (rule_tac bind_wp[OF _ getSchedulerAction_sp]) apply (rule bind_wp) apply (wpsimp wp: switchSchedContext_invs' hoare_drop_imp) - apply (wpsimp wp: scheduleChooseNewThread_invs' isSchedulable_wp setSchedulerAction_invs' + apply (wpsimp wp: scheduleChooseNewThread_invs' getSchedulable_wp setSchedulerAction_invs' ssa_invs' hoare_vcg_disj_lift) apply (wpsimp simp: isHighestPrio_def') apply (wpsimp wp: curDomain_wp) @@ -2399,9 +2274,9 @@ lemma schedule_invs': apply (rename_tac tPtr x) apply (rule_tac Q'="\_. invs'" in hoare_strengthen_post[rotated]) apply (subst obj_at_ko_at'_eq[symmetric], simp) - apply (wpsimp wp: isSchedulable_wp) + apply (wpsimp wp: getSchedulable_wp) apply (wpsimp wp: tcbSchedEnqueue_invs') - apply (fastforce split: if_split dest: isSchedulable_bool_runnableE simp: cur_tcb'_def) + apply (fastforce split: if_split simp: cur_tcb'_def) apply assumption apply (wpsimp wp: awaken_invs') done @@ -2435,7 +2310,7 @@ lemma stit_nosch[wp]: lemma chooseThread_nosch: "chooseThread \\s. P (ksSchedulerAction s)\" unfolding chooseThread_def - by (wpsimp wp: stt_nosch isSchedulable_wp simp: bitmap_fun_defs) + by (wpsimp wp: stt_nosch simp: bitmap_fun_defs) crunch switchSchedContext, setNextInterrupt for ksSchedulerAction[wp]: "\s. P (ksSchedulerAction s)" @@ -2444,7 +2319,7 @@ crunch switchSchedContext, setNextInterrupt lemma schedule_sch: "\\\ schedule \\rv s. ksSchedulerAction s = ResumeCurrentThread\" unfolding schedule_def scAndTimer_def - by (wpsimp wp: setSchedulerAction_direct isSchedulable_wp + by (wpsimp wp: setSchedulerAction_direct getSchedulable_wp simp: getReprogramTimer_def scheduleChooseNewThread_def | wp (once) hoare_drop_imp)+ @@ -2492,9 +2367,8 @@ lemma threadSet_sch_act_sane[wp]: lemma rescheduleRequired_sch_act_sane[wp]: "\\\ rescheduleRequired \\_. sch_act_sane\" - apply (simp add: rescheduleRequired_def sch_act_sane_def - setSchedulerAction_def) - by (wp isSchedulable_wp | wpc | clarsimp)+ + apply (simp add: rescheduleRequired_def sch_act_sane_def setSchedulerAction_def) + by (wpsimp wp: getSchedulable_wp) crunch setThreadState, setBoundNotification for sch_act_sane[wp]: "sch_act_sane" @@ -4526,38 +4400,36 @@ lemma tcb_sched_action_valid_state[wp]: wp: hoare_drop_imps hoare_vcg_all_lift) crunch setQueue, addToBitmap - for isSchedulable_bool[wp]: "isSchedulable_bool tcbPtr" - (simp: bitmap_fun_defs isSchedulable_bool_def isScActive_def) + for schedulable'[wp]: "schedulable' tcbPtr" + (simp: bitmap_fun_defs schedulable'_def) -lemma threadSet_isSchedulable_bool_fields_inv: +lemma threadSet_schedulable'_fields_inv: "\\tcb. tcbState (f tcb) = tcbState tcb; \tcb. tcbSchedContext (f tcb) = tcbSchedContext tcb; \tcb. tcbInReleaseQueue (f tcb) = tcbInReleaseQueue tcb\ - \ threadSet f tcbPtr \\s. P (isSchedulable_bool tcbPtr' s)\" - unfolding isSchedulable_bool_def threadSet_def + \ threadSet f tcbPtr \\s. P (schedulable' tcbPtr' s)\" + unfolding schedulable'_def threadSet_def apply (wpsimp wp: setObject_tcb_wp getTCB_wp) apply (erule rsubst[where P=P]) - apply (wpsimp wp: setObject_tcb_wp simp: pred_map_def obj_at'_def opt_map_def) - apply (fastforce simp: pred_map_def isScActive_def elim!: opt_mapE split: if_splits) + apply (wpsimp wp: setObject_tcb_wp simp: obj_at'_def) + apply (clarsimp simp: opt_pred_def opt_map_def split: option.splits) done -lemma tcbQueued_update_isSchedulable_bool[wp]: - "threadSet (tcbQueued_update f) tcbPtr \isSchedulable_bool tcbPtr'\" - by (fastforce intro: threadSet_isSchedulable_bool_fields_inv) +lemma tcbQueued_update_schedulable'[wp]: + "threadSet (tcbQueued_update f) tcbPtr \schedulable' tcbPtr'\" + by (fastforce intro: threadSet_schedulable'_fields_inv) -lemma tcbSchedPrev_update_isSchedulable_bool[wp]: - "threadSet (tcbSchedPrev_update f) tcbPtr \isSchedulable_bool tcbPtr'\" - by (fastforce intro: threadSet_isSchedulable_bool_fields_inv) +lemma tcbSchedPrev_update_schedulable'[wp]: + "threadSet (tcbSchedPrev_update f) tcbPtr \schedulable' tcbPtr'\" + by (fastforce intro: threadSet_schedulable'_fields_inv) -lemma tcbSchedNext_update_isSchedulable_bool[wp]: - "threadSet (tcbSchedNext_update f) tcbPtr \isSchedulable_bool tcbPtr'\" - by (fastforce intro: threadSet_isSchedulable_bool_fields_inv) +lemma tcbSchedNext_update_schedulable'[wp]: + "threadSet (tcbSchedNext_update f) tcbPtr \schedulable' tcbPtr'\" + by (fastforce intro: threadSet_schedulable'_fields_inv) -lemma tcbSchedEnqueue_isSchedulable_bool[wp]: - "tcbSchedEnqueue tcbPtr \isSchedulable_bool tcbPtr'\" - supply if_split[split del] - apply (clarsimp simp: tcbSchedEnqueue_def tcbQueuePrepend_def unless_def) - apply (wpsimp wp: threadSet_isSchedulable_bool hoare_vcg_if_lift2 hoare_drop_imps) - done +lemma tcbSchedEnqueue_schedulable'[wp]: + "tcbSchedEnqueue tcbPtr \schedulable' tcbPtr'\" + unfolding tcbSchedEnqueue_def tcbQueuePrepend_def + by (wpsimp wp: threadSet_schedulable' hoare_vcg_if_lift2 hoare_drop_imps) lemma schedule_switch_thread_branch_sc_at_cur_sc: "\valid_objs and cur_sc_tcb\ @@ -4625,8 +4497,8 @@ lemma schedule_corres: apply corresKsimp apply clarsimp apply (rename_tac curThread) - apply (rule corres_underlying_split[rotated 2, OF is_schedulable_sp' isSchedulable_sp]) - apply (corresKsimp corres: isSchedulable_corres) + apply (rule corres_underlying_split[rotated 2, OF gets_sp getSchedulable_sp]) + apply (corresKsimp corres: getSchedulable_corres) apply (fastforce simp: invs_def valid_state_def state_relation_def cur_tcb_def) apply (rule corres_underlying_split[rotated 2, OF gets_sp getSchedulerAction_sp]) apply (corresKsimp corres: getSchedulerAction_corres) @@ -4657,7 +4529,7 @@ lemma schedule_corres: simp: schedulable_def2 pred_tcb_at_def obj_at_def get_tcb_def invs_def cur_tcb_def is_tcb_def ct_ready_if_schedulable_def vs_all_heap_simps valid_sched_def) - apply (fastforce simp: invs'_def isSchedulable_bool_def st_tcb_at'_def pred_map_simps + apply (fastforce simp: invs'_def schedulable'_def st_tcb_at'_def pred_map_simps obj_at_simps cur_tcb'_def elim!: opt_mapE) @@ -4683,24 +4555,20 @@ lemma schedule_corres: apply (rule_tac Q'="\_ s. invs' s \ curThread = ksCurThread s" in bind_wp_fwd) apply wpsimp - apply (clarsimp simp: invs'_def isSchedulable_bool_def st_tcb_at'_def pred_map_simps - obj_at_simps cur_tcb'_def sch_act_wf_cases - split: scheduler_action.splits - elim!: opt_mapE) apply (rule bind_wp_fwd_skip, solves wpsimp)+ apply (rule_tac Q'="\_. invs'" in hoare_post_imp) apply (clarsimp simp: invs'_def) apply (wpsimp wp: scheduleChooseNewThread_invs' ksReadyQueuesL1Bitmap_return_wp simp: isHighestPrio_def scheduleSwitchThreadFastfail_def) - apply (clarsimp simp: invs'_def) apply (rename_tac candidate) apply (rule corres_split_skip[where r'="(=)"]) apply wpsimp - apply (clarsimp simp: schedulable_def2 pred_tcb_at_def obj_at_def valid_sched_def - ct_ready_if_schedulable_def vs_all_heap_simps) + subgoal + by (clarsimp simp: schedulable_def3 pred_tcb_at_def obj_at_def valid_sched_def + ct_ready_if_schedulable_def vs_all_heap_simps) apply wpsimp - apply (clarsimp simp: invs'_def isSchedulable_bool_def st_tcb_at'_def pred_map_simps + apply (clarsimp simp: invs'_def valid_pspace'_def schedulable'_def st_tcb_at'_def pred_map_simps obj_at_simps vs_all_heap_simps cur_tcb'_def elim!: opt_mapE) apply (corresKsimp corres: tcbSchedEnqueue_corres) diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 728ec4e2d1..50f571a464 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -351,28 +351,28 @@ lemma threadSet_tcbDomain_update_sch_act_wf[wp]: lemma tcb_sched_action_schedulable_bool[wp]: "tcb_sched_action f t \\s. P (schedulable t' s)\" - apply (wpsimp simp: tcb_sched_action_def thread_get_def wp: set_tcb_queue_wp) - by (fastforce simp: schedulable_def') + apply (wpsimp simp: tcb_sched_action_def thread_get_def wp: set_tcb_queue_wp) + by (fastforce simp: schedulable_def) -lemma isSchedulableBool_ksReadyQueuesL2Bitmap_update[simp]: - "isSchedulable_bool t (ksReadyQueuesL2Bitmap_update f s) = isSchedulable_bool t s" - by (simp add: isSchedulable_bool_def bitmap_fun_defs pred_map_simps opt_map_def isScActive_def) +lemma schedulable'_ksReadyQueuesL2Bitmap_update[simp]: + "schedulable' t (ksReadyQueuesL2Bitmap_update f s) = schedulable' t s" + by (simp add: schedulable'_def bitmap_fun_defs pred_map_simps opt_map_def) -lemma isSchedulableBool_ksReadyQueuesL1Bitmap_update[simp]: - "isSchedulable_bool t (ksReadyQueuesL1Bitmap_update f s) = isSchedulable_bool t s" - by (simp add: isSchedulable_bool_def bitmap_fun_defs pred_map_simps opt_map_def isScActive_def) +lemma schedulable'_ksReadyQueuesL1Bitmap_update[simp]: + "schedulable' t (ksReadyQueuesL1Bitmap_update f s) = schedulable' t s" + by (simp add: schedulable'_def bitmap_fun_defs pred_map_simps opt_map_def) -lemma isSchedulableBool_ksReadyQueues_update[simp]: - "isSchedulable_bool t (ksReadyQueues_update f s) = isSchedulable_bool t s" - by (simp add: isSchedulable_bool_def bitmap_fun_defs pred_map_simps opt_map_def isScActive_def) +lemma schedulable'_ksReadyQueues_update[simp]: + "schedulable' t (ksReadyQueues_update f s) = schedulable' t s" + by (simp add: schedulable'_def bitmap_fun_defs pred_map_simps opt_map_def) crunch removeFromBitmap - for isSchedulable_bool[wp]: "\s. P (isSchedulable_bool tcbPtr s)" + for schedulable'[wp]: "\s. P (schedulable' tcbPtr s)" -lemma tcbSchedDequeue_isSchedulable_bool[wp]: - "tcbSchedDequeue tcbPtr \\s. P (isSchedulable_bool tcbPtr' s)\" +lemma tcbSchedDequeue_schedulable'[wp]: + "tcbSchedDequeue tcbPtr \\s. P (schedulable' tcbPtr' s)\" unfolding tcbSchedDequeue_def tcbQueueRemove_def setQueue_def - by (wpsimp wp: threadSet_isSchedulable_bool_fields_inv getTCB_wp threadGet_wp hoare_drop_imps) + by (wpsimp wp: threadSet_schedulable'_fields_inv getTCB_wp threadGet_wp hoare_drop_imps) lemma setDomain_corres: "corres dc @@ -390,20 +390,20 @@ lemma setDomain_corres: apply (rule corres_split[OF tcbSchedDequeue_corres], simp) apply (rule corres_split[OF threadSet_not_queued_corres]; simp add: tcb_relation_def tcb_cap_cases_def tcb_cte_cases_def cteSizeBits_def) - apply (rule corres_split[OF isSchedulable_corres]) + apply (rule corres_split[OF getSchedulable_corres]) apply (rule corres_split[OF corres_when[OF _ tcbSchedEnqueue_corres]], simp, simp) apply (rule corres_when[OF _ rescheduleRequired_corres], simp) apply (wpsimp wp: hoare_vcg_const_imp_lift) apply (wpsimp wp: hoare_vcg_const_imp_lift tcbSchedEnqueue_valid_tcbs') - apply (wpsimp wp: is_schedulable_wp) - apply (wpsimp wp: isSchedulable_wp) + apply wpsimp + apply (wpsimp wp: getSchedulable_wp) apply (wpsimp wp: hoare_vcg_imp_lift' thread_set_valid_tcbs thread_set_weak_valid_sched_action thread_set_in_correct_ready_q_not_queued thread_set_no_change_tcb_state thread_set_schedulable) apply (wpsimp wp: hoare_vcg_imp_lift' threadSet_valid_tcbs' threadSet_sched_pointers threadSet_valid_sched_pointers - threadSet_isSchedulable_bool_fields_inv) + threadSet_schedulable'_fields_inv) apply (wpsimp wp: hoare_vcg_imp_lift' tcb_dequeue_not_queued') apply wpsimp apply (clarsimp cong: conj_cong) @@ -559,12 +559,12 @@ global_interpretation handleFault: typ_at_all_props' "handleFault t ex" by typ_at_props' lemma pinv_tcb'[wp]: - "\invs' and (\s. sym_refs (state_refs_of' s)) and st_tcb_at' active' tptr + "\invs' and st_tcb_at' active' tptr and valid_invocation' i and ct_active'\ RetypeDecls_H.performInvocation block call can_donate i \\rv. tcb_at' tptr\" unfolding performInvocation_def - by (cases i; simp; wpsimp wp: invokeArch_tcb_at' stateAssertE_inv simp: pred_tcb_at') + by (cases i; simp; wpsimp wp: invokeArch_tcb_at' simp: stateAssertE_def sym_refs_asrt_def) lemma sts_mcpriority_tcb_at'[wp]: "\mcpriority_tcb_at' P t\ @@ -941,32 +941,19 @@ lemma contextYieldToUpdateQueues_invs': \\_. invs'\" apply (clarsimp simp: contextYieldToUpdateQueues_def) apply (rule bind_wp[OF _ get_sc_sp'], rename_tac sc) - apply (rule bind_wp[OF _ isSchedulable_sp]) + apply (rule bind_wp[OF _ getSchedulable_sp]) apply (rule hoare_if; (solves wpsimp)?) apply (rule bind_wp[OF _ getCurThread_sp], rename_tac ctPtr) apply (rule bind_wp_fwd_skip, solves wpsimp)+ apply (rule hoare_if) apply wpsimp - apply (clarsimp simp: valid_sched_context'_def valid_bound_obj'_def obj_at_simps opt_map_def) + apply clarsimp apply (subst bind_assoc[symmetric]) - apply (rule_tac Q'="\_. invs' and ct_active' and (\s. st_tcb_at' runnable' (the (scTCB sc)) s) - and (\s. ctPtr = ksCurThread s)" - in bind_wp_fwd) - apply (clarsimp simp: pred_conj_def) - apply (intro hoare_vcg_conj_lift_pre_fix) - apply (rule hoare_weaken_pre) - apply (rule contextYieldToUpdateQueues_invs'_helper) - apply (fastforce dest: sc_ko_at_valid_objs_valid_sc' - simp: valid_sched_context'_def valid_sched_context_size'_def cur_tcb'_def) - apply (wpsimp wp: threadSet_ct_in_state' setSchedContext_ct_in_state') - apply (wpsimp wp: threadSet_st_tcb_at2) - apply (erule isSchedulable_bool_runnableE) - apply (frule sc_ko_at_valid_objs_valid_sc') - apply fastforce - apply (frule sc_ko_at_valid_objs_valid_sc') - apply fastforce - apply (clarsimp simp: valid_sched_context'_def obj_at_simps) - apply (wpsimp | wps)+ + apply (rule_tac Q'="\_. invs'" in bind_wp_fwd) + apply (wp contextYieldToUpdateQueues_invs'_helper) + apply (fastforce dest: sc_ko_at_valid_objs_valid_sc' + simp: cur_tcb'_def) + apply wpsimp done crunch schedContextResume @@ -1021,9 +1008,9 @@ lemma setDomain_invs': \\_. invs'\" supply comp_apply[simp del] unfolding setDomain_def - apply (wpsimp wp: isSchedulable_wp hoare_vcg_if_lift2) + apply (wpsimp wp: getSchedulable_wp hoare_vcg_if_lift2) apply (rule_tac Q'="\_. invs'" in hoare_post_imp) - apply (fastforce intro: isSchedulable_bool_runnableE) + apply fastforce by (wpsimp wp: threadSet_tcbDomain_update_invs' tcbSchedDequeue_not_queued)+ crunch refillNew, refillUpdate, commitTime @@ -1064,14 +1051,14 @@ lemma invokeSchedControlConfigureFlags_invs': by (fastforce simp: st_tcb_at'_def obj_at_simps valid_refills_number'_def) lemma performInv_invs'[wp]: - "\invs' and (\s. sym_refs (state_refs_of' s)) and (\s. ksSchedulerAction s = ResumeCurrentThread) - and ct_active' and valid_invocation' i - and (\s. can_donate \ bound_sc_tcb_at' bound (ksCurThread s) s)\ + "\invs' and ct_active' and valid_invocation' i + and (\s. can_donate \ bound_sc_tcb_at' bound (ksCurThread s) s) + and (\s. ksSchedulerAction s = ResumeCurrentThread)\ performInvocation block call can_donate i \\_. invs'\" apply (clarsimp simp: performInvocation_def) apply (cases i) - by (clarsimp simp: sym_refs_asrt_def ct_in_state'_def sch_act_simple_def + by (clarsimp simp: stateAssertE_def sym_refs_asrt_def ct_in_state'_def sch_act_simple_def | wp tcbinv_invs' arch_performInvocation_invs' setDomain_invs' stateAssertE_inv stateAssertE_wp invokeSchedControlConfigureFlags_invs' invokeSchedContext_invs' | erule active_ex_cap'[simplified ct_in_state'_def])+ @@ -1269,6 +1256,8 @@ lemma handleInvocation_corres: apply (clarsimp simp: ct_not_inQ_asrt_def) apply (rule corres_stateAssertE_add_assertion[rotated]) apply (clarsimp simp: valid_idle'_asrt_def) + apply (rule corres_stateAssertE_add_assertion[rotated]) + apply (clarsimp simp: cur_tcb'_asrt_def) apply (rule stronger_corres_guard_imp) apply (rule corres_split_eqr[OF getCurThread_corres]) apply (rule corres_split [OF getMessageInfo_corres]) @@ -1355,23 +1344,22 @@ lemma handleInvocation_corres: apply (erule st_tcb_ex_cap, clarsimp+) apply (case_tac st; clarsimp) apply (clarsimp cong: conj_cong) - apply (subgoal_tac "ct_schedulable s") - apply (clarsimp simp: invs'_def valid_pspace'_def cur_tcb'_def) - apply (frule valid_objs'_valid_tcbs') - apply (frule ct_active_cross, fastforce, fastforce, simp) - apply (clarsimp simp: ct_in_state'_def cong: conj_cong) - apply (frule pred_tcb'_weakenE [where P=active' and P'=simple'], clarsimp) - apply (frule(1) st_tcb_ex_cap'', fastforce) - apply (clarsimp simp: valid_pspace'_def schact_is_rct_def) - apply (frule state_relation_sched_act_relation, simp) - apply (subgoal_tac "isSchedulable_bool (ksCurThread s') s'") - apply (clarsimp simp: isSchedulable_bool_def pred_map_conj[simplified pred_conj_def]) - apply (frule active'_st_tcb_at_state_refs_ofD') - apply (clarsimp simp: pred_tcb_at'_def) - apply (frule curthread_relation, simp) - apply (frule_tac t1="cur_thread s" in cross_relF[OF _ isSchedulable_bool_cross_rel]; - simp add: invs_def valid_state_def valid_pspace_def) - apply (clarsimp simp: schedulable_def2 ct_in_state_def runnable_eq_active) + apply (frule curthread_relation) + apply (prop_tac "ct_schedulable s") + apply (clarsimp simp: schedulable_def2 ct_in_state_def runnable_eq_active) + apply (clarsimp simp: invs'_def valid_pspace'_def cur_tcb'_def) + apply (frule valid_objs'_valid_tcbs') + apply (frule ct_active_cross, fastforce, fastforce, simp) + apply (clarsimp simp: ct_in_state'_def cong: conj_cong) + apply (frule pred_tcb'_weakenE [where P=active' and P'=simple'], clarsimp) + apply (frule(1) st_tcb_ex_cap'', fastforce) + apply (clarsimp simp: valid_pspace'_def schact_is_rct_def) + apply (frule state_relation_sched_act_relation, simp) + apply (subgoal_tac "schedulable' (ksCurThread s') s'") + apply (clarsimp simp: schedulable'_def pred_map_conj[simplified pred_conj_def]) + apply (frule active'_st_tcb_at_state_refs_ofD') + apply (clarsimp simp: pred_tcb_at'_def) + apply (force intro!: schedulable_schedulable'_eq[THEN iffD1] schedulable_imp_tcb_at) done lemma ts_Restart_case_helper': @@ -1403,7 +1391,8 @@ lemma rfk_ksQ[wp]: done lemma hinv_invs'[wp]: - "\invs' and (\s. sym_refs (state_refs_of' s)) and ct_isSchedulable + "\invs' and cur_tcb' + and (\s. schedulable' (ksCurThread s) s) and (\s. ksSchedulerAction s = ResumeCurrentThread)\ handleInvocation calling blocking can_donate first_phase cptr \\_. invs'\" @@ -1420,22 +1409,22 @@ lemma hinv_invs'[wp]: apply clarsimp apply (fastforce elim!: pred_tcb'_weakenE st_tcb_ex_cap'') apply wp+ - apply (rule_tac Q'="\rv'. invs' and (\s. sym_refs (state_refs_of' s)) and ct_not_inQ - and valid_invocation' rv - and (\s. ksSchedulerAction s = ResumeCurrentThread) - and (\s. ksCurThread s = thread) - and st_tcb_at' active' thread - and (\s. bound_sc_tcb_at' bound (ksCurThread s) s)" - in hoare_post_imp) + apply (rule_tac Q'="\_. invs' and cur_tcb' + and ct_not_inQ + and valid_invocation' rv + and (\s. ksSchedulerAction s = ResumeCurrentThread) + and (\s. ksCurThread s = thread) + and st_tcb_at' active' thread + and (\s. bound_sc_tcb_at' bound (ksCurThread s) s)" + in hoare_post_imp) apply (clarsimp simp: ct_in_state'_def) apply (wpsimp wp: sts_invs_minor' sts_sym_refs' setThreadState_st_tcb setThreadState_rct setThreadState_ct_not_inQ hoare_vcg_imp_lift' | wps)+ - apply (fastforce simp: ct_in_state'_def simple_sane_strg sch_act_simple_def pred_map_simps - obj_at_simps pred_tcb_at'_def - elim!: pred_tcb'_weakenE st_tcb_ex_cap'' opt_mapE - dest: st_tcb_at_idle_thread')+ - done + by (fastforce simp: ct_in_state'_def simple_sane_strg sch_act_simple_def pred_map_simps + obj_at_simps pred_tcb_at'_def st_tcb_at'_def schedulable'_def + opt_pred_def opt_map_def runnable_eq_active' cur_tcb'_def + intro: st_tcb_ex_cap''[where P=runnable'] split: option.splits) (* NOTE: This is a good candidate for corressimp at some point. For now there are some missing lemmas regarding corresK and liftM. *) @@ -1469,14 +1458,12 @@ lemma handleSend_corres: done lemma hs_invs'[wp]: - "\invs' and (\s. sym_refs (state_refs_of' s)) and ct_isSchedulable and - (\s. vs_valid_duplicates' (ksPSpace s)) and - (\s. ksSchedulerAction s = ResumeCurrentThread)\ - handleSend blocking \\r. invs'\" - apply (rule validE_valid) + "\invs' and cur_tcb' and (\s. schedulable' (ksCurThread s) s) + and (\s. ksSchedulerAction s = ResumeCurrentThread)\ + handleSend blocking + \\_. invs'\" apply (simp add: handleSend_def getCapReg_def) - apply (wp | simp)+ - done + by wpsimp lemma tcb_at_cte_at_map: "\ tcb_at' t s; offs \ dom tcb_cap_cases \ \ cte_at' (cte_map (t, offs)) s" @@ -2018,7 +2005,7 @@ lemma chargeBudget_corres: apply (simp add: andM_def whenM_def ifM_def when_def[symmetric] bind_assoc) apply (rule corres_split_eqr[OF getCurThread_corres _ gets_sp getCurThread_sp]) apply (rule corres_guard_imp) - apply (rule corres_split_eqr[OF isSchedulable_corres _ is_schedulable_sp' isSchedulable_sp]) + apply (rule corres_split_eqr[OF getSchedulable_corres _ gets_sp getSchedulable_sp]) apply (rename_tac sched) apply (rule corres_guard_imp) apply (rule corres_when2, simp) @@ -2043,9 +2030,9 @@ lemma chargeBudget_corres: apply (rule hoare_strengthen_post [where Q'="\_. invs' and cur_tcb'", rotated]) apply (clarsimp simp: invs'_def valid_pspace'_def valid_objs'_valid_tcbs' cur_tcb'_def - isSchedulable_bool_def runnable_eq_active' pred_map_def + schedulable'_def runnable_eq_active' opt_pred_def opt_map_def obj_at'_def pred_tcb_at'_def ct_in_state'_def - elim!: opt_mapE) + split: option.splits) apply wpsimp apply (fastforce simp: schedulable_def2 ct_in_state_def runnable_eq_active current_time_bounded_def invs_def valid_state_def valid_pspace_def cur_tcb_def @@ -2077,8 +2064,7 @@ lemma chargeBudget_corres: apply (clarsimp simp: vs_all_heap_simps) apply (simp only: scheduler_act_not_def, rule notI) apply (drule (1) valid_sched_action_switch_thread_is_schedulable) - apply (clarsimp simp: is_schedulable_opt_def tcb_at_kh_simps[symmetric] pred_tcb_at_def obj_at_def - split: option.split_asm dest!: get_tcb_SomeD) + apply (clarsimp simp: schedulable_def3 vs_all_heap_simps) apply (frule ct_not_blocked_cur_sc_not_blocked, clarsimp) apply (rule conjI; clarsimp) apply (drule (1) active_scs_validE, clarsimp) @@ -2220,12 +2206,11 @@ lemma chargeBudget_invs'[wp]: "chargeBudget consumed canTimeout Flag \invs'\" unfolding chargeBudget_def ifM_def bind_assoc apply (rule bind_wp[OF _ getCurSc_sp]) - apply (wpsimp wp: isSchedulable_wp) + apply (wpsimp wp: getSchedulable_wp) apply (rule hoare_strengthen_post[where Q'="\_. invs'"]) apply wpsimp - apply (clarsimp simp: isSchedulable_bool_def obj_at'_def - pred_map_def ct_in_state'_def pred_tcb_at'_def runnable_eq_active' - elim!: opt_mapE) + apply (clarsimp simp: schedulable'_def obj_at'_def opt_map_def opt_pred_def + ct_in_state'_def pred_tcb_at'_def runnable_eq_active') by (wpsimp wp: hoare_drop_imp updateSchedContext_invs' | strengthen live_sc'_ex_cap[OF invs_iflive'] valid_sc_strengthen[OF invs_valid_objs'])+ @@ -2292,8 +2277,9 @@ lemma handleCall_corres: done lemma hc_invs'[wp]: - "\invs' and (\s. sym_refs (state_refs_of' s)) and (\s. ksSchedulerAction s = ResumeCurrentThread) - and ct_isSchedulable\ + "\invs' and cur_tcb' + and (\s. ksSchedulerAction s = ResumeCurrentThread) + and (\s. schedulable' (ksCurThread s) s)\ handleCall \\_. invs'\" apply (clarsimp simp: handleCall_def) @@ -2432,11 +2418,8 @@ lemma invs'_ksCurTime_update[iff]: crunch setDomainTime, setCurTime, setConsumedTime, setExtraBadge, setReleaseQueue, setQueue, modifyReadyQueuesL1Bitmap, modifyReadyQueuesL2Bitmap, setReprogramTimer for ct_in_state'[wp]: "ct_in_state' P" - and isSchedulable[wp]: "isSchedulable_bool p" - and scs_of'_ct[wp]: "\s. P (scs_of' s) (ksCurThread s)" - and isScActive_ct[wp]: "\s. P (isScActive p s) (tcbSCs_of s) (ksCurThread s)" - and pred_map_sc_active_ct[wp]: "\s. pred_map (\p. isScActive p s) (tcbSCs_of s) (ksCurThread s)" - (simp: ct_in_state'_def isScActive_def isSchedulable_bool_def) + and schedulable'[wp]: "schedulable' p" + (simp: ct_in_state'_def schedulable'_def) crunch updateTimeStamp, tcbSchedAppend, postpone for invs'[wp]: invs' @@ -2449,8 +2432,6 @@ crunch updateTimeStamp for tcbSCs_of_scTCBs_of[wp]: "\s. P (tcbSCs_of s) (scTCBs_of s)" and tcbs_of'_ct[wp]: "\s. P (tcbs_of' s) (ksCurThread s)" and tcbSCs_of_ct[wp]: "\s. P (tcbSCs_of s) (ksCurThread s)" - and isScActive_ct[wp]: "\s. P (isScActive p s) (tcbSCs_of s) (ksCurThread s)" - and pred_map_sc_active_ct[wp]: "\s. pred_map (\p. isScActive p s) (tcbSCs_of s) (ksCurThread s)" and typ_at[wp]: "\s. P (typ_at' T p s)" and pred_tcb_at'[wp]: "\s. P (pred_tcb_at' proj Q p s)" @@ -2475,11 +2456,19 @@ crunch performInvocation crunch updateTimeStamp for state_refs_of'[wp]: "\s. P (state_refs_of' s)" + and schedulable'[wp]: "schedulable' t" + and ct_schedulable'[wp]: "\s. schedulable' (ksCurThread s) s" + and cur_tcb'[wp]: cur_tcb' + (rule: hoare_lift_Pf2[where f=ksCurThread] simp: cur_tcb'_def) + +lemma schedulable'_runnableE: + "schedulable' t s \ tcb_at' t s \ st_tcb_at' runnable' t s" + unfolding schedulable'_def + by (clarsimp simp: pred_tcb_at'_def obj_at'_def opt_pred_def opt_map_def) lemma he_invs'[wp]: - "\invs' and (\s. sym_refs (state_refs_of' s)) and - (\s. event \ Interrupt \ ct_running' s) and - (\s. ct_running' s \ ct_isSchedulable s) and + "\invs' and cur_tcb' and + (\s. event \ Interrupt \ schedulable' (ksCurThread s) s) and (\s. ksSchedulerAction s = ResumeCurrentThread)\ handleEvent event \\rv. invs'\" @@ -2496,6 +2485,8 @@ proof - simp del: split_paired_All | rule hoare_strengthen_postE_R[where Q'="\_. invs'", rotated], clarsimp simp: ct_active'_asrt_def + | clarsimp dest!: schedulable'_runnableE intro!: pred_tcb'_weakenE + simp: ct_in_state'_def cur_tcb'_def runnable_eq_active' | rule conjI active_ex_cap' | strengthen nidle)+) apply (rule hoare_strengthen_post, @@ -2506,7 +2497,8 @@ proof - apply (wp hv_inv' hh_inv' hoare_vcg_if_lift2 checkBudgetRestart_true checkBudgetRestart_false updateTimeStamp_ct_in_state'[simplified ct_in_state'_def] | strengthen active_ex_cap'[OF _ invs_iflive'] - | clarsimp simp: ct_in_state'_def + | clarsimp dest!: schedulable'_runnableE intro!: pred_tcb'_weakenE + simp: ct_in_state'_def cur_tcb'_def runnable_eq_active' | wpc)+ done qed @@ -2577,27 +2569,15 @@ lemma handleInv_handleRecv_corres: odE)" apply add_cur_tcb' apply add_sym_refs - apply (rule_tac Q'="\s'. pred_map (\scPtr. isScActive scPtr s') (tcbSCs_of s') (ksCurThread s')" - in corres_cross_add_guard) - apply (clarsimp simp: released_sc_tcb_at_def active_sc_tcb_at_def2) - apply (prop_tac "scp = cur_sc s") - apply (drule invs_cur_sc_tcb_symref, clarsimp simp: schact_is_rct_def) - apply (clarsimp simp: pred_tcb_at_def obj_at_def) - apply (prop_tac "sc_at (cur_sc s) s") - apply (frule invs_cur_sc_tcb) - apply (fastforce simp: cur_sc_tcb_def sc_tcb_sc_at_def obj_at_def is_sc_obj - dest: valid_sched_context_size_objsI[OF invs_valid_objs]) - apply (frule (4) active_sc_at'_cross[OF _ invs_psp_aligned invs_distinct]) - apply (clarsimp simp: active_sc_at'_def obj_at'_def cur_tcb'_def pred_tcb_at_def - is_sc_obj obj_at_def) - apply (clarsimp simp: pred_map_def isScActive_def) - apply (rule_tac x="cur_sc s" in exI) - apply (clarsimp simp: opt_map_red dest!: state_relationD) - apply (frule_tac x="ksCurThread s'" in pspace_relation_absD, simp) - apply (fastforce simp: tcb_relation_cut_def tcb_relation_def) - apply (rule_tac Q'="\s'. pred_map (\tcb. \ tcbInReleaseQueue tcb) (tcbs_of' s') (ksCurThread s')" - in corres_cross_add_guard) - apply (fastforce intro: ct_not_in_release_q_cross curthread_relation[symmetric]) + apply (rule_tac Q'="\s'. schedulable' (ksCurThread s') s'" + in corres_cross_add_guard) + apply (frule curthread_relation) + apply clarsimp + apply (erule schedulable_schedulable'_eq[THEN iffD1], fastforce+) + apply (clarsimp simp: schedulable_def2) + apply (rule conjI) + apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def) + apply (fastforce intro: schact_is_rct_ct_active_sc) apply (rule corres_rel_imp) apply (rule corres_guard_imp) apply (rule corres_split_liftEE[OF getCapReg_corres_gen]) @@ -2640,7 +2620,8 @@ lemma handleInv_handleRecv_corres: apply (clarsimp simp: invs_def valid_state_def valid_pspace_def active_from_running schedulable_def2 released_sc_tcb_at_def) apply (clarsimp simp: ct_in_state_def st_tcb_weakenE) - apply (clarsimp simp: active_from_running') + apply (fastforce simp: schedulable'_def opt_pred_def opt_map_def pred_map_def + ct_in_state'_def st_tcb_at'_def obj_at'_def) apply simp done diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy index e3ec1acc03..777424795f 100644 --- a/proof/refine/RISCV64/TcbAcc_R.thy +++ b/proof/refine/RISCV64/TcbAcc_R.thy @@ -1501,10 +1501,9 @@ lemma inReleaseQueue_wp: "\\s. tcb_at' t s \ (\tcb. ko_at' tcb t s \ P (tcbInReleaseQueue tcb) s)\ inReleaseQueue t \P\" - apply (simp add: inReleaseQueue_def) - apply (wp threadGet_wp) - apply (clarsimp simp: obj_at'_def) - done + unfolding inReleaseQueue_def readInReleaseQueue_def + apply (wpsimp wp: threadGet_wp) + by (fastforce dest!: threadRead_SomeD simp: obj_at'_def) lemma asUser_invs[wp]: "\invs' and tcb_at' t\ asUser t m \\rv. invs'\" @@ -1725,10 +1724,10 @@ lemma isStopped_def2: lemma isRunnable_def2: "isRunnable t = liftM runnable' (getThreadState t)" - apply (simp add: isRunnable_def liftM_def) + apply (simp add: isRunnable_def readRunnable_def liftM_def getThreadState_def + flip: threadGet_def) apply (rule bind_eqI, rule ext, rule arg_cong) - apply (case_tac state) - apply (clarsimp)+ + apply (rename_tac state, case_tac state; clarsimp) done lemma isBlocked_inv[wp]: @@ -2223,30 +2222,28 @@ lemma ready_queues_disjoint: apply (fastforce simp: vs_all_heap_simps valid_ready_qs_2_def) done -lemma isRunnable_sp: - "\P\ - isRunnable tcb_ptr - \\rv s. \tcb'. ko_at' tcb' tcb_ptr s - \ (rv = (tcbState tcb' = Running \ tcbState tcb' = Restart)) - \ P s\" - unfolding isRunnable_def getThreadState_def - apply (wpsimp wp: hoare_case_option_wp getObject_tcb_wp simp: threadGet_getObject) - apply (fastforce simp: obj_at'_def split: Structures_H.thread_state.splits) +lemma readRunnable_SomeD: + "readRunnable t s = Some y \ \tcb. ko_at' tcb t s \ y = runnable' (tcbState tcb)" + apply (clarsimp simp: readRunnable_def) + apply (drule threadRead_SomeD) + apply clarsimp + apply (case_tac "tcbState tcb"; fastforce) done -lemma isRunnable_sp': - "\P\ - isRunnable tcb_ptr - \\rv s. (rv = st_tcb_at' active' tcb_ptr s) \ P s\" - apply (clarsimp simp: isRunnable_def getThreadState_def) - apply (wpsimp wp: hoare_case_option_wp getObject_tcb_wp - simp: threadGet_getObject) - apply (fastforce simp: obj_at'_def st_tcb_at'_def - split: Structures_H.thread_state.splits) - done +lemmas isRunnable_sp' = + gets_the_sp[where f="readRunnable tcb_ptr" for tcb_ptr, simplified isRunnable_def[symmetric]] -crunch isRunnable - for (no_fail) no_fail[wp] +lemma isRunnable_sp: + "\Q\ isRunnable t \\rv s. (st_tcb_at' runnable' t s = rv) \ Q s\" + by wpsimp + +lemma no_ofail_readRunnable[wp]: + "no_ofail (tcb_at' tcbPtr) (readRunnable tcbPtr)" + unfolding readRunnable_def + by wpsimp + +lemmas no_fail_isRunnable[wp] = + no_ofail_gets_the[OF no_ofail_readRunnable, simplified isRunnable_def[symmetric]] defs ksReadyQueues_asrt_def: "ksReadyQueues_asrt @@ -2773,8 +2770,6 @@ lemma tcbSchedEnqueue_corres: apply (fastforce intro: ksReleaseQueue_asrt_cross) apply (rule corres_symb_exec_r[OF _ isRunnable_sp]; (solves wpsimp)?) apply (rule corres_symb_exec_r[OF _ assert_sp, rotated]; (solves wpsimp)?) - apply wpsimp - apply (fastforce simp: st_tcb_at'_def runnable_eq_active' obj_at'_def) apply (rule corres_symb_exec_r[OF _ threadGet_sp]; (solves wpsimp)?) apply (subst if_distrib[where f="set_tcb_queue domain prio" for domain prio]) apply (rule corres_if_strong') @@ -2952,16 +2947,24 @@ lemma threadGet_obj_at'_bool_field: by (wpsimp wp: threadGet_wp simp: obj_at'_def) -crunch inReleaseQueue, getReleaseQueue, setReleaseQueue +crunch getReleaseQueue, setReleaseQueue for (no_fail) no_fail[wp] +lemma no_ofail_readInReleaseQueue[wp]: + "no_ofail (tcb_at' tcbPtr) (readInReleaseQueue tcbPtr)" + unfolding readInReleaseQueue_def + by wpsimp + +lemmas no_fail_inReleaseQueue[wp] = + no_ofail_gets_the[OF no_ofail_readInReleaseQueue, simplified inReleaseQueue_def[symmetric]] + lemma inReleaseQueue_sp: "\P\ inReleaseQueue tcb_ptr \\rv s. \tcb'. ko_at' tcb' tcb_ptr s \ rv = (tcbInReleaseQueue tcb') \ P s\" - unfolding inReleaseQueue_def + unfolding inReleaseQueue_def readInReleaseQueue_def apply (wpsimp wp: hoare_case_option_wp getObject_tcb_wp simp: threadGet_getObject) - apply (clarsimp simp: obj_at'_def) + apply (clarsimp dest!: threadRead_SomeD simp: obj_at'_def) done lemma inReleaseQueue_corres: @@ -2988,7 +2991,8 @@ lemma isRunnable_corres: (ko_at' tcb_conc t) (return (runnable (tcb_state tcb_abs))) (isRunnable t)" - unfolding isRunnable_def getThreadState_def + apply (clarsimp simp: isRunnable_def readRunnable_def getThreadState_def + simp flip: threadGet_def) apply (rule corres_symb_exec_r[where Q'="\rv s. tcbState tcb_conc = rv"]) apply (case_tac "tcb_state tcb_abs"; clarsimp simp: tcb_relation_def) apply (wpsimp wp: threadGet_wp) @@ -3035,57 +3039,126 @@ lemma ko_at'_valid_tcbs'_valid_tcb': defs valid_tcbs'_asrt_def: "valid_tcbs'_asrt \ valid_tcbs'" -lemma isSchedulable_corres: +declare valid_tcbs'_asrt_def[simp] + +(* FIXME RT: move to Lib *) +lemma corres_gets_return_trivial: + "(\s s'. \(s, s') \ sr; P s; P' s'\ \ f s = v) + \ corres_underlying sr nf nf' (=) P P' (gets f) (return v)" + unfolding corres_underlying_def gets_def get_def return_def bind_def + by clarsimp + +definition schedulable' :: "machine_word \ kernel_state \ bool" where + "schedulable' tcbPtr s' \ + (runnable' |< (tcbs_of' s' ||> tcbState)) tcbPtr + \ ((\sc. 0 < scRefillMax sc) |< (tcbs_of' s' |> tcbSchedContext |> scs_of' s')) tcbPtr + \ (Not \ tcbInReleaseQueue |< tcbs_of' s') tcbPtr" + +lemma getSchedulable_wp: + "\\s. \t. schedulable' tcbPtr s = t \ tcb_at' tcbPtr s \ P t s\ getSchedulable tcbPtr \P\" + apply (clarsimp simp: getSchedulable_def readSchedulable_def + ohaskell_state_assert_def gets_the_if_distrib) + apply (subst gets_the_obind inReleaseQueue_def[symmetric] scActive_def[symmetric] + isRunnable_def[symmetric] threadGet_def[symmetric] gets_the_ostate_assert)+ + apply (wpsimp wp: inReleaseQueue_wp threadGet_wp) + apply normalise_obj_at' + apply (fastforce elim!: rsubst2[where P=P] + simp: schedulable'_def opt_pred_def opt_map_def obj_at'_def) + done + +lemma getSchedulable_sp: + "\P\ getSchedulable tcbPtr \\rv s. (rv = schedulable' tcbPtr s) \ P s\" + by (wpsimp wp: getSchedulable_wp) + +lemma isSchedulable_inv[wp]: + "getSchedulable tcbPtr \P\" + by (wpsimp wp: getSchedulable_wp) + +(* FIXME RT: move *) +lemma ovalid_if_lift2: + "\P\ f \\rv s. (Q rv s \ X rv s) \ (\ Q rv s \ Y rv s)\ \ + \P\ f \\rv s. if Q rv s then X rv s else Y rv s\" + + "\P\ f \\rv s. (Q' rv \ X rv s) \ (\ Q' rv \ Y rv s)\ \ + \P\ f \\rv. if Q' rv then X rv else Y rv\" + by (auto simp: ovalid_def split_def) + +lemma no_ofail_readSchedulable[wp]: + "no_ofail (tcb_at' tcbPtr and valid_tcbs') (readSchedulable tcbPtr)" + apply (clarsimp simp: readSchedulable_def readSchedContext_def ohaskell_state_assert_def) + apply (wpsimp wp: ovalid_inv ovalid_wp_comb3 ovalid_if_lift2 ovalid_threadRead) + apply normalise_obj_at' + apply (fastforce dest: ko_at'_valid_tcbs'_valid_tcb' simp: valid_tcb'_def valid_bound_obj'_def) + done + +lemma runnable_tsr: + "thread_state_relation ts ts' \ runnable' ts' = runnable ts" + by (case_tac ts, auto) + +lemma runnable_runnable'_eq: + "\(s, s') \ state_relation; pspace_aligned s; pspace_distinct s; tcb_at t s\ + \ (runnable |< (tcbs_of s ||> tcb_state)) t = (runnable' |< (tcbs_of' s' ||> tcbState)) t" + apply (frule state_relation_pspace_relation) + apply (frule (3) tcb_at_cross) + apply (clarsimp simp: obj_at_def is_tcb_def) + by (fastforce dest: pspace_relation_tcb_relation[where ptr=t] runnable_tsr + simp: obj_at'_def tcb_relation_def opt_pred_def opt_map_def tcbs_of_kh_def + split: Structures_A.kernel_object.splits) + +lemma sc_active_cross_eq: + "\(s, s') \ state_relation; pspace_aligned s; pspace_distinct s; tcb_at t s; valid_tcbs' s'\ + \ (sc_active |< (tcbs_of s |> tcb_sched_context |> scs_of s)) t + = ((\sc. 0 < scRefillMax sc) |< (tcbs_of' s' |> tcbSchedContext |> scs_of' s')) t" + apply (frule state_relation_pspace_relation) + apply (frule (3) tcb_at_cross) + apply normalise_obj_at' + apply (frule (1) ko_at'_valid_tcbs'_valid_tcb') + apply (clarsimp simp: obj_at_def is_tcb_def) + apply (rename_tac ko, case_tac ko; clarsimp) + apply (rename_tac tcb) + apply (clarsimp simp: obj_at'_def) + apply (frule (2) pspace_relation_tcb_relation[where ptr=t]) + apply (case_tac "tcb_sched_context tcb = None") + apply (clarsimp simp: tcb_relation_def opt_pred_def opt_map_def tcbs_of_kh_def) + apply clarsimp + apply (rename_tac scPtr) + apply (prop_tac "sc_at' scPtr s'") + apply (clarsimp simp: valid_tcb'_def valid_bound_obj'_def tcb_relation_def split: option.splits) + apply (frule (1) sc_at'_cross) + apply (clarsimp simp: obj_at_def is_sc_obj_def) + by (auto dest: pspace_relation_sc_relation + simp: tcb_relation_def opt_pred_def opt_map_def tcbs_of_kh_def scs_of_kh_def + sc_relation_def active_sc_def obj_at'_def + split: Structures_A.kernel_object.splits option.splits) + +lemma in_release_q_inReleaseQueue_eq: + "\(s, s') \ state_relation; pspace_aligned s; pspace_distinct s\ + \ t \ set (release_queue s) = (tcbInReleaseQueue |< (tcbs_of' s')) t" + by (fastforce dest!: state_relation_release_queue_relation + simp: release_queue_relation_def opt_pred_def opt_map_def obj_at'_def) + +lemma schedulable_schedulable'_eq: + "\(s, s') \ state_relation; pspace_aligned s; pspace_distinct s; tcb_at t s; valid_tcbs' s'\ + \ schedulable t s = schedulable' t s'" + apply (clarsimp simp: schedulable_def schedulable'_def) + apply (intro conj_cong) + apply (fastforce dest: runnable_runnable'_eq) + apply (fastforce dest: sc_active_cross_eq) + apply (force dest!: in_release_q_inReleaseQueue_eq simp: opt_pred_def opt_map_def + split: option.splits) + done + +lemma getSchedulable_corres: "corres (=) (valid_tcbs and pspace_aligned and pspace_distinct and tcb_at t) valid_tcbs' - (is_schedulable t) (isSchedulable t)" + (gets (schedulable t)) (getSchedulable t)" apply (rule corres_cross_add_guard[where Q'="tcb_at' t"]) apply (fastforce intro: tcb_at_cross) - apply (clarsimp simp: is_schedulable_def isSchedulable_def Option.is_none_def) - apply (rule corres_symb_exec_l[OF _ _ gets_the_sp]) - apply (rule corres_symb_exec_r[OF _ isRunnable_sp]) - apply (rule corres_symb_exec_r[OF _ threadGet_sp]) - apply (rule corres_stateAssert_add_assertion) - apply (rule corres_if_strong') - apply clarsimp - apply normalise_obj_at' - apply (frule state_relation_pspace_relation) - apply (frule pspace_relation_tcb_relation) - apply (fastforce dest: get_tcb_ko_atD simp: obj_at_def) - apply (fastforce simp: obj_at'_def) - apply (clarsimp simp: tcb_relation_def) - apply corres - apply clarsimp - apply (rule corres_symb_exec_l[OF _ _ get_sched_context_sp]) - apply (rule corres_symb_exec_r[OF _ scActive_sp]) - apply (rule corres_symb_exec_l[OF _ _ gets_sp]) - apply (rule corres_symb_exec_r[OF _ inReleaseQueue_sp]) - apply clarsimp - apply normalise_obj_at' - apply (frule state_relation_pspace_relation) - apply (frule pspace_relation_tcb_relation[where ptr=t]) - apply (fastforce dest: get_tcb_ko_atD simp: tcb_at_def obj_at_def) - apply (fastforce simp: obj_at'_def) - apply (rule conj_cong) - apply (clarsimp simp: tcb_relation_def) - apply (case_tac "tcb_state tcb"; clarsimp) - apply (rule conj_cong) - apply (force dest!: pspace_relation_sc_relation - simp: obj_at_def obj_at'_def active_sc_def - tcb_relation_def sc_relation_def) - apply (drule state_relation_release_queue_relation) - apply (clarsimp simp: release_queue_relation_def list_queue_relation_def - in_queue_2_def obj_at'_def opt_pred_def opt_map_def - split: option.splits) - apply wpsimp+ - apply (fastforce simp: valid_tcbs'_def valid_tcb'_def obj_at'_def) - apply (rule get_sched_context_exs_valid) - apply (fastforce dest!: get_tcb_SomeD intro: sc_atD1 - simp: valid_tcbs_def obj_at_def valid_tcb_def) - apply wpsimp - apply (fastforce dest!: get_tcb_SomeD intro: sc_atD1 - simp: valid_tcbs_def obj_at_def valid_tcb_def) - apply (wpsimp simp: tcb_at_def valid_tcbs'_asrt_def)+ + apply (rule corres_bind_return2) + apply (rule corres_symb_exec_r[OF _ getSchedulable_sp, rotated]; (solves wpsimp)?) + apply (wpsimp simp: getSchedulable_def wp: no_ofail_gets_the) + apply (rule corres_gets_return_trivial) + apply (fastforce dest: schedulable_schedulable'_eq) done lemma get_simple_ko_exs_valid: @@ -3101,41 +3174,6 @@ lemmas get_reply_exs_valid[wp] = lemmas get_endpoint_exs_valid[wp] = get_simple_ko_exs_valid[where C=kernel_object.Endpoint, simplified] -lemma conjunct_rewrite: - "P = P' \ Q = Q' \ R = R' \ (P \ Q \ R) = (P' \ Q' \ R')" - by simp - -definition isScActive :: "machine_word \ kernel_state \ bool" where - "isScActive scPtr s' \ pred_map (\sc. 0 < scRefillMax sc) (scs_of' s') scPtr" - -abbreviation ct_isSchedulable :: "kernel_state \ bool" where - "ct_isSchedulable \ ct_active' - and (\s. pred_map (\tcb. \ tcbInReleaseQueue tcb) (tcbs_of' s) (ksCurThread s)) - and (\s. pred_map (\scPtr. isScActive scPtr s) (tcbSCs_of s) (ksCurThread s))" - -definition isSchedulable_bool :: "machine_word \ kernel_state \ bool" where - "isSchedulable_bool tcbPtr s' - \ pred_map (\tcb. runnable' (tcbState tcb) \ \ tcbInReleaseQueue tcb) (tcbs_of' s') tcbPtr - \ pred_map (\scPtr. isScActive scPtr s') (tcbSCs_of s') tcbPtr" - -lemma isSchedulable_wp: - "\\s. \t. isSchedulable_bool tcbPtr s = t \ tcb_at' tcbPtr s \ P t s\ isSchedulable tcbPtr \P\" - apply (clarsimp simp: isSchedulable_def) - apply (wpsimp simp: hoare_vcg_if_lift2 obj_at_def is_tcb inReleaseQueue_def - wp: threadGet_wp getTCB_wp) - apply (fastforce elim: rsubst2[where P=P] - simp: isSchedulable_bool_def isScActive_def obj_at'_def - pred_tcb_at'_def pred_map_simps in_opt_map_eq) - done - -lemma isSchedulable_sp: - "\P\ isSchedulable tcbPtr \\rv. (\s. rv = isSchedulable_bool tcbPtr s) and P\" - by (wpsimp wp: isSchedulable_wp) - -lemma isSchedulable_inv[wp]: - "isSchedulable tcbPtr \P\" - by (wpsimp wp: isSchedulable_wp) - \ \In sched_context_donate, weak_valid_sched_action does not propagate backwards over the statement where from_tptr's sched context is set to None because it requires the thread associated with a switch_thread action to have a sched context. For this instance, we introduce a weaker version @@ -3168,20 +3206,24 @@ lemma rescheduleRequired_corres_weak: apply (corresKsimp corres: setSchedulerAction_corres) apply (case_tac action; clarsimp?) apply (rename_tac tp) - apply (rule corres_underlying_split[OF _ _ is_schedulable_sp' isSchedulable_inv, rotated 2]) - apply (corresKsimp corres: isSchedulable_corres) + apply (rule corres_underlying_split[OF _ _ gets_sp isSchedulable_inv, rotated 2]) + apply (corresKsimp corres: getSchedulable_corres) apply (clarsimp simp: weaker_valid_sched_action_def obj_at_def vs_all_heap_simps is_tcb_def) apply (clarsimp simp: when_def) apply (rule corres_symb_exec_l[OF _ thread_get_exs_valid thread_get_sp , rotated]) apply (clarsimp simp: weaker_valid_sched_action_def vs_all_heap_simps obj_at_def is_tcb_def) apply (wpsimp simp: thread_get_def get_tcb_def weaker_valid_sched_action_def vs_all_heap_simps) - + (* FIXME Michael: use new corres rule for assert_opt on the rhs *) apply (rule corres_symb_exec_l[OF _ _ assert_opt_sp, rotated]) apply wpsimp - apply (clarsimp simp: obj_at_def schedulable_def get_tcb_def split: option.splits) + apply (clarsimp simp: obj_at_def schedulable_def opt_pred_def + opt_map_def tcbs_of_kh_def + split: option.splits) apply wpsimp - apply (clarsimp simp: obj_at_def schedulable_def get_tcb_def split: option.splits) + apply (clarsimp simp: obj_at_def schedulable_def opt_pred_def + opt_map_def tcbs_of_kh_def + split: option.splits) apply (rule corres_symb_exec_l[OF _ _ get_sc_refill_sufficient_sp, rotated]) apply (rule get_sc_refill_sufficient_exs_valid) @@ -3387,18 +3429,6 @@ lemma thread_get_test: "do cur_ts \ get_thread_state cur; g (test cur apply (simp add: get_thread_state_def thread_get_def) done -lemma thread_get_isRunnable_corres: - "corres (=) (tcb_at t and pspace_aligned and pspace_distinct) \ - (thread_get (\tcb. runnable (tcb_state tcb)) t) (isRunnable t)" - apply (simp add: isRunnable_def getThreadState_def threadGet_getObject thread_get_def) - apply (fold liftM_def) - apply simp - apply (rule corres_rel_imp) - apply (rule getObject_TCB_corres) - apply (clarsimp simp add: tcb_relation_def thread_state_relation_def) - apply (case_tac "tcb_state x",simp_all) - done - lemma setObject_tcbState_update_corres: "\thread_state_relation ts ts'; tcb_relation tcb tcb'\ \ corres dc @@ -3425,12 +3455,12 @@ lemma scheduleTCB_corres: apply (rule corres_guard_imp) apply (rule corres_split [OF getCurThread_corres]) apply (rule corres_split [OF getSchedulerAction_corres], rename_tac sched_action) - apply (rule corres_split [OF isSchedulable_corres]) + apply (rule corres_split [OF getSchedulable_corres]) apply (clarsimp simp: when_def) apply (intro conjI impI; (clarsimp simp: sched_act_relation_def)?) apply (rule rescheduleRequired_corres) apply (case_tac sched_act; clarsimp) - apply (wpsimp wp: isSchedulable_wp)+ + apply (wpsimp wp: getSchedulable_wp)+ done lemma set_thread_state_act_corres: @@ -3443,8 +3473,8 @@ lemma set_thread_state_act_corres: apply (corres corres: getCurThread_corres) apply (rule corres_split_forwards'[OF _ gets_sp getSchedulerAction_sp]) apply (corres corres: getSchedulerAction_corres) - apply (rule corres_split_forwards'[OF _ is_schedulable_sp isSchedulable_sp]) - apply (corres corres: isSchedulable_corres) + apply (rule corres_split_forwards'[OF _ gets_sp getSchedulable_sp]) + apply (corres corres: getSchedulable_corres) apply (clarsimp simp: when_def split del: if_split) apply (rule corres_if_split) apply (case_tac sched_act; clarsimp) @@ -3840,37 +3870,27 @@ lemma rescheduleRequired_sch_act'[wp]: "\\\ rescheduleRequired \\rv s. sch_act_wf (ksSchedulerAction s) s\" - by (wpsimp simp: rescheduleRequired_def wp: isSchedulable_wp) + by (wpsimp simp: rescheduleRequired_def wp: getSchedulable_wp) lemma sts_weak_sch_act_wf[wp]: "setThreadState st t \\s. weak_sch_act_wf (ksSchedulerAction s) s\" unfolding setThreadState_def scheduleTCB_def apply (wpsimp wp: hoare_vcg_if_lift2 hoare_vcg_imp_lift hoare_vcg_all_lift - hoare_pre_cont[where f="isSchedulable x" and P="\rv _. rv" for x] - hoare_pre_cont[where f="isSchedulable x" and P="\rv _. \rv" for x] + hoare_pre_cont[where f="getSchedulable x" and P="\rv _. rv" for x] + hoare_pre_cont[where f="getSchedulable x" and P="\rv _. \rv" for x] simp: weak_sch_act_wf_def) done -lemma threadSet_isSchedulable_bool_nochange: - "\\s. runnable' st \ isSchedulable_bool t s\ - threadSet (tcbState_update (\_. st)) t - \\_. isSchedulable_bool t\" - unfolding isSchedulable_bool_def threadSet_def - apply (rule bind_wp[OF _ getObject_tcb_sp]) - apply (wpsimp wp: setObject_tcb_wp simp: pred_map_def obj_at'_def opt_map_def) - apply (fastforce simp: pred_map_def isScActive_def elim!: opt_mapE) - done - -lemma threadSet_isSchedulable_bool: +lemma threadSet_schedulable': "\\s. runnable' st - \ pred_map (\tcb. \(tcbInReleaseQueue tcb)) (tcbs_of' s) t - \ pred_map (\scPtr. isScActive scPtr s) (tcbSCs_of s) t\ + \ ((\sc. 0 < scRefillMax sc) |< (tcbs_of' s |> tcbSchedContext |> scs_of' s)) t + \ (Not \ tcbInReleaseQueue |< tcbs_of' s) t\ threadSet (tcbState_update (\_. st)) t - \\_. isSchedulable_bool t\" - unfolding isSchedulable_bool_def threadSet_def + \\_. schedulable' t\" + unfolding schedulable'_def threadSet_def apply (rule bind_wp[OF _ getObject_tcb_sp]) - apply (wpsimp wp: setObject_tcb_wp simp: pred_map_def obj_at'_def opt_map_def) - apply (fastforce simp: pred_map_def isScActive_def elim!: opt_mapE) + apply (wpsimp wp: setObject_tcb_wp) + apply (fastforce simp: opt_pred_def opt_map_def obj_at'_def split: option.splits) done lemma setObject_queued_pred_tcb_at'[wp]: @@ -3937,13 +3957,13 @@ lemma tcbSchedDequeue_sch_act_wf[wp]: | wp sch_act_wf_lift | simp add: if_apply_def2)+ lemma scheduleTCB_sch_act_wf: - "\\s. \(t = ksCurThread s \ ksSchedulerAction s = ResumeCurrentThread - \ \ pred_map (\tcb. runnable' (tcbState tcb)) (tcbs_of' s) t) + "\\s. \ (t = ksCurThread s \ ksSchedulerAction s = ResumeCurrentThread + \ \ (runnable' |< (tcbs_of' s ||> tcbState)) t) \ (sch_act_wf (ksSchedulerAction s) s)\ scheduleTCB t \\_ s. sch_act_wf (ksSchedulerAction s) s\" - apply (simp add: scheduleTCB_def) - by (wpsimp wp: isSchedulable_wp simp: isSchedulable_bool_def pred_map_def opt_map_Some) + unfolding scheduleTCB_def + by (wpsimp wp: getSchedulable_wp simp: schedulable'_def) lemma sts_sch_act': "\\s. (\ runnable' st \ sch_act_not t s) \ sch_act_wf (ksSchedulerAction s) s\ @@ -3958,7 +3978,7 @@ lemma sts_sch_act': (ksCurThread s \ t \ ksSchedulerAction s \ ResumeCurrentThread \ sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp) - apply (clarsimp simp: pred_tcb_at'_def obj_at'_def pred_map_def elim!: opt_mapE) + apply (clarsimp simp: pred_tcb_at'_def obj_at'_def opt_pred_def opt_map_def) apply (simp only: imp_conv_disj) apply (wpsimp wp: threadSet_pred_tcb_at_state threadSet_sch_act_wf hoare_vcg_disj_lift) done @@ -3978,7 +3998,7 @@ lemma sts_sch_act[wp]: (ksCurThread s \ t \ ksSchedulerAction s \ ResumeCurrentThread \ sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp) - apply (clarsimp simp: pred_tcb_at'_def obj_at'_def pred_map_def elim!: opt_mapE) + apply (clarsimp simp: pred_tcb_at'_def obj_at'_def opt_pred_def opt_map_def elim!: opt_mapE) apply (simp only: imp_conv_disj) apply (wpsimp wp: threadSet_pred_tcb_at_state threadSet_sch_act_wf hoare_vcg_disj_lift) apply (fastforce simp: sch_act_simple_def) @@ -4437,7 +4457,8 @@ lemma rescheduleRequired_valid_tcbs'[wp]: rescheduleRequired \\_. valid_tcbs'\" apply (clarsimp simp: rescheduleRequired_def) - apply (rule bind_wp_fwd_skip, wpsimp wp: tcbSchedEnqueue_valid_tcbs' update_valid_tcb' isSchedulable_wp)+ + apply (rule bind_wp_fwd_skip, + wpsimp wp: tcbSchedEnqueue_valid_tcbs' update_valid_tcb' getSchedulable_wp)+ apply (wpsimp wp: update_valid_tcb') done @@ -5429,7 +5450,7 @@ lemma setThreadState_if_unsafe_then_cap'[wp]: apply (rule bind_wp_fwd_skip) apply (rule threadSet_ifunsafe'T) apply (clarsimp simp: tcb_cte_cases_def objBits_simps') - apply (wpsimp wp: isSchedulable_wp) + apply (wpsimp wp: getSchedulable_wp) done crunch setBoundNotification diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy index acb1869da2..9d35f99036 100644 --- a/proof/refine/RISCV64/Tcb_R.thy +++ b/proof/refine/RISCV64/Tcb_R.thy @@ -159,9 +159,9 @@ lemma restart_corres: apply (rule corres_split[OF corres_when2]) apply clarsimp apply (rule schedContextResume_corres) - apply (rule corres_split[OF isSchedulable_corres]) + apply (rule corres_split[OF getSchedulable_corres]) apply (rule corres_when2 [OF _ possibleSwitchTo_corres]; (solves simp)?) - apply (wpsimp wp: is_schedulable_wp isSchedulable_wp)+ + apply (wpsimp wp: getSchedulable_wp)+ apply (rule_tac Q'="\_. invs and valid_sched_action and active_scs_valid and in_correct_ready_q and ready_qs_distinct and ready_or_release and tcb_at t" @@ -250,20 +250,20 @@ lemma restart_invs': ThreadDecls_H.restart t \\rv. invs'\" unfolding restart_def apply (simp add: isStopped_def2) - apply (wp setThreadState_nonqueued_state_update isSchedulable_wp + apply (wp setThreadState_nonqueued_state_update getSchedulable_wp cancelIPC_simple setThreadState_st_tcb) - apply (rule_tac Q'="\_. invs'" in hoare_strengthen_post[rotated]) - apply wpsimp - apply (clarsimp simp: isSchedulable_bool_def pred_map_pred_conj[simplified pred_conj_def] + apply (rule_tac Q'="\_. invs'" in hoare_strengthen_post[rotated]) + apply wpsimp + apply (clarsimp simp: schedulable'_def pred_map_pred_conj[simplified pred_conj_def] projectKO_opt_tcb pred_map_def pred_tcb_at'_def obj_at'_real_def ko_wp_at'_def elim!: opt_mapE) - apply (wpsimp wp: hoare_vcg_imp_lift') - apply (rule_tac Q'="\_. invs'" in hoare_strengthen_post[rotated]) - apply (fastforce elim: isSchedulable_bool_runnableE) - apply (wpsimp wp: ifCondRefillUnblockCheck_invs' hoare_vcg_imp_lift') - apply (wpsimp wp: setThreadState_nonqueued_state_update setThreadState_st_tcb - hoare_vcg_if_lift2) + apply (wpsimp wp: hoare_vcg_imp_lift') + apply (rule_tac Q'="\_. invs'" in hoare_strengthen_post[rotated]) + apply fastforce + apply (wpsimp wp: ifCondRefillUnblockCheck_invs' hoare_vcg_imp_lift') + apply (wpsimp wp: setThreadState_nonqueued_state_update setThreadState_st_tcb + hoare_vcg_if_lift2) apply clarsimp apply wp+ apply (clarsimp simp: comp_def) @@ -512,7 +512,7 @@ lemma isRunnable_corres': (get_thread_state t) (isRunnable t')" apply (rule_tac Q'="tcb_at' t" in corres_cross_add_guard) apply (fastforce dest!: state_relationD elim!: tcb_at_cross) - apply (simp add: isRunnable_def) + apply (simp add: isRunnable_def readRunnable_def flip: threadGet_def getThreadState_def) apply (subst bind_return[symmetric]) apply (rule corres_guard_imp) apply (rule corres_split[OF getThreadState_corres'], simp) @@ -1847,7 +1847,7 @@ lemma sched_context_resume_weak_valid_sched_action: sched_context_resume scp \\_. weak_valid_sched_action\" unfolding sched_context_resume_def - by (wpsimp wp: postpone_weak_valid_sched_action thread_get_wp' is_schedulable_wp') + by (wpsimp wp: postpone_weak_valid_sched_action thread_get_wp') crunch sched_context_resume for sc_at_ppred[wp]: "sc_at_ppred n P ptr" @@ -1883,15 +1883,15 @@ lemma schedContextBindTCB_corres: apply (rule corres_split_nor) apply (rule schedContextResume_corres) apply (rule corres_split_eqr) - apply (rule isSchedulable_corres) + apply (rule getSchedulable_corres) apply (rule corres_when, simp) apply (rule corres_split_nor) apply (rule tcbSchedEnqueue_corres, simp) apply (rule rescheduleRequired_corres) apply wp apply (wpsimp wp: tcbSchedEnqueue_valid_tcbs') - apply (wpsimp wp: is_schedulable_wp) - apply (wpsimp wp: threadGet_wp getTCB_wp isSchedulable_wp simp: inReleaseQueue_def) + apply wpsimp + apply (wpsimp wp: threadGet_wp getTCB_wp getSchedulable_wp simp: inReleaseQueue_def) apply (rule_tac Q'="\rv. valid_objs and pspace_aligned and pspace_distinct and (\s. sym_refs (state_refs_of s)) and weak_valid_sched_action and active_scs_valid and sc_tcb_sc_at ((=) (Some t)) ptr and current_time_bounded and @@ -2334,8 +2334,8 @@ lemma schedContextBindTCB_invs': apply (subst bind_assoc[symmetric, where m="threadSet _ _"]) apply (rule bind_wp)+ apply wpsimp - apply (wpsimp wp: isSchedulable_wp) - apply (clarsimp simp: isSchedulable_bool_runnableE) + apply (wpsimp wp: getSchedulable_wp) + apply clarsimp apply (wp (once) hoare_drop_imps) apply (wp hoare_vcg_imp_lift') apply (wp hoare_drop_imps) diff --git a/spec/abstract/Ipc_A.thy b/spec/abstract/Ipc_A.thy index 1048ab8d00..1e111a6923 100644 --- a/spec/abstract/Ipc_A.thy +++ b/spec/abstract/Ipc_A.thy @@ -450,7 +450,7 @@ where set_thread_state dest Running; as_user dest $ setRegister badge_register badge; maybe_donate_sc dest ntfnptr; - schedulable <- is_schedulable dest; + schedulable <- gets (schedulable dest); when schedulable $ possible_switch_to dest; scopt \ get_tcb_obj_ref tcb_sched_context dest; if_sporadic_active_cur_sc_assert_refill_unblock_check scopt @@ -482,7 +482,7 @@ where set_thread_state tcb Running; as_user tcb $ setRegister badge_register badge; maybe_donate_sc tcb ntfnptr; - schedulable <- is_schedulable tcb; + schedulable <- gets (schedulable tcb); when schedulable $ possible_switch_to tcb; scopt \ get_tcb_obj_ref tcb_sched_context tcb; if_sporadic_active_cur_sc_assert_refill_unblock_check scopt @@ -694,8 +694,8 @@ where od; modify $ consumed_time_update (K 0); ct \ gets cur_thread; - sched \ is_schedulable ct; - when (sched) $ do + sched \ gets (schedulable ct); + when sched $ do end_timeslice canTimeout; reschedule_required; modify (\s. s\reprogram_timer := True\) diff --git a/spec/abstract/KHeap_A.thy b/spec/abstract/KHeap_A.thy index 6185272e65..34f339b390 100644 --- a/spec/abstract/KHeap_A.thy +++ b/spec/abstract/KHeap_A.thy @@ -11,12 +11,55 @@ Functions to access kernel memory. chapter \Accessing the Kernel Heap\ theory KHeap_A -imports Exceptions_A +imports Exceptions_A Lib.SplitRule begin +section "Projection from the Kernel Heap" + text \This theory gives auxiliary getter and setter methods for kernel objects.\ +section "Projection from the Kernel Heap" + +definition tcb_of :: "kernel_object \ tcb" where + "tcb_of ko \ case ko of TCB tcb \ Some tcb | _ \ None" + +lemmas tcb_of_simps [simp] = tcb_of_def [split_simps kernel_object.split] + +lemma tcb_of_Some[simp]: + "tcb_of ko = Some tcb \ ko = TCB tcb" + by (cases ko; simp) + +lemma tcb_of_None: + "tcb_of ko = None \ (\tcb. ko \ TCB tcb)" + by (cases ko; simp) + +definition tcbs_of_kh :: "('obj_ref \ kernel_object) \ 'obj_ref \ tcb" where + "tcbs_of_kh kh \ kh |> tcb_of" + +abbreviation tcbs_of :: "'z state \ obj_ref \ tcb" where + "tcbs_of s \ tcbs_of_kh (kheap s)" + +definition sc_of :: "kernel_object \ sched_context" where + "sc_of ko \ case ko of SchedContext sc _ \ Some sc | _ \ None" + +lemmas sc_of_simps [simp] = sc_of_def [split_simps kernel_object.split] + +lemma sc_of_Some[simp]: + "sc_of ko = Some sc \ (\n. ko = SchedContext sc n)" + by (cases ko; simp) + +lemma sc_of_None: + "sc_of ko = None \ (\sc n. ko \ SchedContext sc n)" + by (cases ko; simp) + +definition scs_of_kh :: "('obj_ref \ kernel_object) \ 'obj_ref \ sched_context" where + "scs_of_kh kh \ kh |> sc_of" + +abbreviation scs_of :: "'z state \ obj_ref \ sched_context" where + "scs_of s \ scs_of_kh (kheap s)" + + section "General Object Access" text \The kernel reader option monad\ @@ -304,50 +347,11 @@ definition where "in_release_queue tcb_ptr \ \s. tcb_ptr \ set (release_queue s)" -definition - is_schedulable :: "obj_ref \ ('z::state_ext state, bool) nondet_monad" -where - "is_schedulable tcb_ptr \ do - tcb \ gets_the $ get_tcb tcb_ptr; - if Option.is_none (tcb_sched_context tcb) - then return False - else do - sc \ get_sched_context $ the $ tcb_sched_context tcb; - is_runnable \ return (runnable (tcb_state tcb)); - in_release_q \ gets $ in_release_queue tcb_ptr; - return (is_runnable \ sc_active sc \ \in_release_q) - od - od" - -definition - is_sc_active :: "obj_ref \ 'z::state_ext state \ bool" -where - "is_sc_active sp \ (\s. - case kheap s sp of - Some (SchedContext sc _) \ sc_active sc - | _ \ False)" - -definition - is_schedulable_opt :: "obj_ref \ 'z::state_ext state \ bool option" -where - "is_schedulable_opt tcb_ptr \ \s. - case get_tcb tcb_ptr s of None \ None - | Some tcb \ - (case tcb_sched_context tcb of None => Some False - | Some sc_ptr => - Some (runnable (tcb_state tcb) \ (is_sc_active sc_ptr s) - \ \(in_release_queue tcb_ptr s)))" - -definition - schedulable :: "obj_ref \ 'z::state_ext state \ bool" -where - "schedulable tcb_ptr \ \s. - case get_tcb tcb_ptr s of None \ False - | Some tcb \ - (case tcb_sched_context tcb of None => False - | Some sc_ptr => - (runnable (tcb_state tcb) \ (is_sc_active sc_ptr s) - \ \(in_release_queue tcb_ptr s)))" +definition schedulable :: "obj_ref \ 'z::state_ext state \ bool" where + "schedulable t s \ + (runnable |< (tcbs_of s ||> tcb_state)) t + \ (sc_active |< (tcbs_of s |> tcb_sched_context |> scs_of s)) t + \ t \ set (release_queue s)" abbreviation ct_schedulable where "ct_schedulable s \ schedulable (cur_thread s) s" @@ -517,7 +521,7 @@ definition reschedule_required :: "(unit, 'z::state_ext) s_monad" where action \ gets scheduler_action; case action of switch_thread t \ do - sched \ is_schedulable t; + sched \ gets (schedulable t); when sched $ do sc_opt \ thread_get tcb_sched_context t; scp \ assert_opt sc_opt; @@ -537,7 +541,7 @@ where "schedule_tcb tcb_ptr \ do cur \ gets cur_thread; sched_act \ gets scheduler_action; - schedulable \ is_schedulable tcb_ptr; + schedulable \ gets (schedulable tcb_ptr); when (tcb_ptr = cur \ sched_act = resume_cur_thread \ \schedulable) $ reschedule_required od" @@ -547,7 +551,7 @@ where "set_thread_state_act tcb_ptr \ do cur \ gets cur_thread; sched_act \ gets scheduler_action; - schedulable \ is_schedulable tcb_ptr; + schedulable \ gets (schedulable tcb_ptr); when (tcb_ptr = cur \ sched_act = resume_cur_thread \ \schedulable) $ set_scheduler_action choose_new_thread od" diff --git a/spec/abstract/SchedContext_A.thy b/spec/abstract/SchedContext_A.thy index 37bef80595..cceff81c9d 100644 --- a/spec/abstract/SchedContext_A.thy +++ b/spec/abstract/SchedContext_A.thy @@ -273,7 +273,7 @@ where "sched_context_resume sc_ptr \ do sc \ get_sched_context sc_ptr; tptr \ assert_opt $ sc_tcb sc; - sched \ is_schedulable tptr; + sched \ gets (schedulable tptr); when sched $ do ts \ thread_get tcb_state tptr; ready \ get_sc_refill_ready sc_ptr; @@ -357,7 +357,7 @@ definition test_possible_switch_to :: "obj_ref \ (unit, 'z::state_ext) s_monad" where "test_possible_switch_to tcb_ptr = do - sched \ is_schedulable tcb_ptr; + sched \ gets (schedulable tcb_ptr); when sched $ possible_switch_to tcb_ptr od" @@ -369,7 +369,7 @@ where set_sc_obj_ref sc_tcb_update sc_ptr (Some tcb_ptr); if_sporadic_active_cur_sc_test_refill_unblock_check (Some sc_ptr); sched_context_resume sc_ptr; - sched <- is_schedulable tcb_ptr; + sched \ gets (schedulable tcb_ptr); when sched $ do tcb_sched_action tcb_sched_enqueue tcb_ptr; reschedule_required diff --git a/spec/abstract/Schedule_A.thy b/spec/abstract/Schedule_A.thy index bf7e47772d..0ae17e1a3a 100644 --- a/spec/abstract/Schedule_A.thy +++ b/spec/abstract/Schedule_A.thy @@ -33,7 +33,7 @@ definition guarded_switch_to :: "obj_ref \ (unit, 'z::state_ext) s_m "guarded_switch_to thread \ do sc_opt \ thread_get tcb_sched_context thread; scp \ assert_opt sc_opt; - sched \ is_schedulable thread; + sched \ gets (schedulable thread); assert sched; switch_to_thread thread od" @@ -240,7 +240,7 @@ definition awaken; check_domain_time; ct \ gets cur_thread; - ct_schdble \ is_schedulable ct; + ct_schdble \ gets (schedulable ct); action \ gets scheduler_action; (case action of resume_cur_thread \ return () @@ -279,7 +279,7 @@ where sc_tcb_opt \ get_sc_obj_ref sc_tcb sc_ptr; tcb_ptr \ assert_opt sc_tcb_opt; - schedulable <- is_schedulable tcb_ptr; + schedulable <- gets (schedulable tcb_ptr); if schedulable then do ct_ptr \ gets cur_thread; prios \ thread_get tcb_priority tcb_ptr; diff --git a/spec/abstract/Syscall_A.thy b/spec/abstract/Syscall_A.thy index c503089aa0..912dc001c4 100644 --- a/spec/abstract/Syscall_A.thy +++ b/spec/abstract/Syscall_A.thy @@ -422,7 +422,7 @@ definition preemption_path where "preemption_path \ do irq \ do_machine_op (getActiveIRQ True); ct \ gets cur_thread; - schedulable \ is_schedulable ct; + schedulable \ gets (schedulable ct); if schedulable then do check_budget; return () od diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy index 1dcd308541..e69e3fb4bb 100644 --- a/spec/abstract/Tcb_A.thy +++ b/spec/abstract/Tcb_A.thy @@ -262,7 +262,7 @@ definition cur \ gets cur_thread; tcb_sched_action tcb_sched_dequeue tptr; thread_set_domain tptr new_dom; - sched \ is_schedulable tptr; + sched \ gets (schedulable tptr); when sched $ tcb_sched_action tcb_sched_enqueue tptr; \ \schedulable and dequeued\ when (tptr = cur) $ reschedule_required od" diff --git a/spec/haskell/src/SEL4.lhs b/spec/haskell/src/SEL4.lhs index 8553c1c8e2..b464989ccc 100644 --- a/spec/haskell/src/SEL4.lhs +++ b/spec/haskell/src/SEL4.lhs @@ -22,7 +22,7 @@ This is the top-level module; it defines the interface between the kernel and th > import SEL4.API.Types > import SEL4.Kernel.CSpace(lookupCap) > import SEL4.Kernel.Thread(schedule, activateThread) -> import SEL4.Model.StateData(KernelState, Kernel, getCurThread, doMachineOp, stateAssert, rct_imp_activatable'_asrt) +> import SEL4.Model.StateData(KernelState, Kernel, getCurThread, doMachineOp, stateAssert, rct_imp_activatable'_asrt, cur_tcb'_asrt) > import SEL4.Model.Preemption(withoutPreemption) > import SEL4.Object.Structures > import SEL4.Object.TCB(asUser, mcsPreemptionPoint) @@ -40,6 +40,8 @@ faults, and system calls; the set of possible events is defined in > callKernel :: Event -> Kernel () > callKernel ev = do > stateAssert fastpathKernelAssertions "Fast path assertions must hold" +> stateAssert cur_tcb'_asrt +> "Assert that `cur_tcb' s` holds" > runExceptT $ handleEvent ev > `catchError` (\_ -> withoutPreemption $ do > irq_opt <- doMachineOp (getActiveIRQ True) diff --git a/spec/haskell/src/SEL4/API/Syscall.lhs b/spec/haskell/src/SEL4/API/Syscall.lhs index 9394d3e8cd..9b8580dfaa 100644 --- a/spec/haskell/src/SEL4/API/Syscall.lhs +++ b/spec/haskell/src/SEL4/API/Syscall.lhs @@ -243,6 +243,8 @@ The following function implements the "Send" and "Call" system calls. It determi > "Assert that `ct_not_inQ s` holds" > stateAssert valid_idle'_asrt > "Assert that `valid_idle' s` holds" +> stateAssert cur_tcb'_asrt +> "Assert that `cur_tcb' s` holds" > thread <- withoutPreemption getCurThread > info <- withoutPreemption $ getMessageInfo thread > syscall diff --git a/spec/haskell/src/SEL4/Kernel/Thread.lhs b/spec/haskell/src/SEL4/Kernel/Thread.lhs index 93a4392bf3..beb9c6f97c 100644 --- a/spec/haskell/src/SEL4/Kernel/Thread.lhs +++ b/spec/haskell/src/SEL4/Kernel/Thread.lhs @@ -19,7 +19,7 @@ We use the C preprocessor to select a target architecture. \begin{impdetails} % {-# BOOT-IMPORTS: SEL4.Model SEL4.Machine SEL4.Object.Structures SEL4.Object.Instances() SEL4.API.Types #-} -% {-# BOOT-EXPORTS: setDomain setMCPriority setPriority getThreadState setThreadState setBoundNotification getBoundNotification doIPCTransfer isRunnable restart suspend doReplyTransfer tcbQueueEmpty tcbQueuePrepend tcbQueueAppend tcbQueueInsert tcbQueueRemove tcbSchedEnqueue tcbSchedDequeue rescheduleRequired scheduleTCB isSchedulable possibleSwitchTo endTimeslice inReleaseQueue tcbReleaseRemove tcbSchedAppend switchToThread #-} +% {-# BOOT-EXPORTS: setDomain setMCPriority setPriority getThreadState setThreadState setBoundNotification getBoundNotification doIPCTransfer isRunnable restart suspend doReplyTransfer tcbQueueEmpty tcbQueuePrepend tcbQueueAppend tcbQueueInsert tcbQueueRemove tcbSchedEnqueue tcbSchedDequeue rescheduleRequired scheduleTCB getSchedulable possibleSwitchTo endTimeslice inReleaseQueue tcbReleaseRemove tcbSchedAppend switchToThread #-} > import Prelude hiding (Word) > import SEL4.Config @@ -101,27 +101,33 @@ The following function is used by the scheduler to determine whether a particular thread is ready to run. Note that the idle thread is not considered runnable; this is to prevent it being inserted in the scheduler queue. -> isRunnable :: PPtr TCB -> Kernel Bool -> isRunnable thread = do -> state <- getThreadState thread +> readRunnable :: PPtr TCB -> KernelR Bool +> readRunnable thread = do +> state <- threadRead tcbState thread > return $ case state of > Running -> True > Restart -> True > _ -> False -> isSchedulable :: PPtr TCB -> Kernel Bool -> isSchedulable tcbPtr = do -> runnable <- isRunnable tcbPtr -> scPtrOpt <- threadGet tcbSchedContext tcbPtr -> stateAssert valid_tcbs'_asrt "valid_tcbs' holds" +> isRunnable :: PPtr TCB -> Kernel Bool +> isRunnable thread = getsJust (readRunnable thread) + +> readSchedulable :: PPtr TCB -> KernelR Bool +> readSchedulable tcbPtr = do +> runnable <- readRunnable tcbPtr +> scPtrOpt <- threadRead tcbSchedContext tcbPtr +> readStateAssert valid_tcbs'_asrt "valid_tcbs' holds" > if scPtrOpt == Nothing > then return False > else do > let scPtr = fromJust scPtrOpt -> active <- scActive scPtr -> inReleaseQ <- inReleaseQueue tcbPtr +> active <- readScActive scPtr +> inReleaseQ <- readInReleaseQueue tcbPtr > return $ runnable && active && not inReleaseQ +> getSchedulable :: PPtr TCB -> Kernel Bool +> getSchedulable tcbPtr = getsJust (readSchedulable tcbPtr) + \subsubsection{Suspending a Thread} When a thread is suspended, either explicitly by a TCB invocation or implicitly when it is being destroyed, any operation that it is currently performing must be cancelled. @@ -158,7 +164,7 @@ The invoked thread will return to the instruction that caused it to enter the ke > setThreadState Restart target > ifCondRefillUnblockCheck scOpt (Just True) (Just False) > when (isJust scOpt) $ schedContextResume (fromJust scOpt) -> schedulable <- isSchedulable target +> schedulable <- getSchedulable target > when schedulable $ possibleSwitchTo target \subsection{IPC Transfers} @@ -369,7 +375,7 @@ has the highest runnable priority in the system on kernel entry (unless idle). > awaken > checkDomainTime > curThread <- getCurThread -> isSchedulable <- isSchedulable curThread +> getSchedulable <- getSchedulable curThread > action <- getSchedulerAction > case action of @@ -381,7 +387,7 @@ An IPC operation may request that the scheduler switch to a specific thread. We check here that the candidate has the highest priority in the system. > SwitchToThread candidate -> do -> when isSchedulable (tcbSchedEnqueue curThread) +> when getSchedulable (tcbSchedEnqueue curThread) > > idleThread <- getIdleThread > targetPrio <- threadGet tcbPriority candidate @@ -396,7 +402,7 @@ We check here that the candidate has the highest priority in the system. > tcbSchedEnqueue candidate > setSchedulerAction ChooseNewThread > scheduleChooseNewThread -> else if isSchedulable && curPrio == targetPrio +> else if getSchedulable && curPrio == targetPrio > then do > tcbSchedAppend candidate > setSchedulerAction ChooseNewThread @@ -408,7 +414,7 @@ We check here that the candidate has the highest priority in the system. If the current thread is no longer runnable, has used its entire timeslice, an IPC cancellation has potentially woken multiple higher priority threads, or the domain timeslice is exhausted, then we scan the scheduler queues to choose a new thread. In the last case, we switch to the next domain beforehand. > ChooseNewThread -> do -> when isSchedulable $ tcbSchedEnqueue curThread +> when getSchedulable $ tcbSchedEnqueue curThread > scheduleChooseNewThread > scAndTimer @@ -475,7 +481,7 @@ Note also that the level 2 bitmap array is stored in reverse in order to get bet > scheduleTCB tcbPtr = do > curThread <- getCurThread > action <- getSchedulerAction -> schedulable <- isSchedulable tcbPtr +> schedulable <- getSchedulable tcbPtr > when (tcbPtr == curThread && action == ResumeCurrentThread && not schedulable) $ rescheduleRequired \subsubsection{Switching Threads} @@ -512,7 +518,7 @@ The following function is used to alter a thread's domain. > curThread <- getCurThread > tcbSchedDequeue tptr > threadSet (\t -> t { tcbDomain = newdom }) tptr -> schedulable <- isSchedulable tptr +> schedulable <- getSchedulable tptr > when schedulable $ tcbSchedEnqueue tptr > when (tptr == curThread) $ rescheduleRequired @@ -594,7 +600,7 @@ This function is called when the system state has changed sufficiently that the > action <- getSchedulerAction > case action of > SwitchToThread target -> do -> sched <- isSchedulable target +> sched <- getSchedulable target > when sched $ tcbSchedEnqueue target > _ -> return () > setSchedulerAction ChooseNewThread @@ -837,9 +843,12 @@ Kernel init will created a initial thread whose tcbPriority is max priority. > tcbSchedAppend ct > else postpone scPtr +> readInReleaseQueue :: PPtr TCB -> KernelR Bool +> readInReleaseQueue tcbPtr = do +> threadRead tcbInReleaseQueue tcbPtr + > inReleaseQueue :: PPtr TCB -> Kernel Bool -> inReleaseQueue tcbPtr = do -> threadGet tcbInReleaseQueue tcbPtr +> inReleaseQueue tcbPtr = getsJust (readInReleaseQueue tcbPtr) > tcbReleaseRemove :: PPtr TCB -> Kernel () > tcbReleaseRemove tcbPtr = do diff --git a/spec/haskell/src/SEL4/Object/Notification.lhs b/spec/haskell/src/SEL4/Object/Notification.lhs index 761dd22679..6026a3444e 100644 --- a/spec/haskell/src/SEL4/Object/Notification.lhs +++ b/spec/haskell/src/SEL4/Object/Notification.lhs @@ -69,7 +69,7 @@ mark the notification object as active. > setThreadState Running tcb > asUser tcb $ setRegister badgeRegister badge > maybeDonateSc tcb ntfnPtr -> schedulable <- isSchedulable tcb +> schedulable <- getSchedulable tcb > when schedulable $ possibleSwitchTo tcb > scOpt <- threadGet tcbSchedContext tcb > ifCondRefillUnblockCheck scOpt (Just True) (Just True) @@ -88,7 +88,7 @@ If the notification object is waiting, a thread is removed from its queue and th > setThreadState Running dest > asUser dest $ setRegister badgeRegister badge > maybeDonateSc dest ntfnPtr -> schedulable <- isSchedulable dest +> schedulable <- getSchedulable dest > when schedulable $ possibleSwitchTo dest > scOpt <- threadGet tcbSchedContext dest > ifCondRefillUnblockCheck scOpt (Just True) (Just True) diff --git a/spec/haskell/src/SEL4/Object/SchedContext.lhs b/spec/haskell/src/SEL4/Object/SchedContext.lhs index 21e0309df6..f4d963e2a0 100644 --- a/spec/haskell/src/SEL4/Object/SchedContext.lhs +++ b/spec/haskell/src/SEL4/Object/SchedContext.lhs @@ -468,7 +468,7 @@ This module uses the C preprocessor to select a target architecture. > setSchedContext scPtr $ sc { scTCB = Just tcbPtr } > ifCondRefillUnblockCheck (Just scPtr) (Just True) (Just False) > schedContextResume scPtr -> schedulable <- isSchedulable tcbPtr +> schedulable <- getSchedulable tcbPtr > when schedulable $ do > tcbSchedEnqueue tcbPtr > rescheduleRequired @@ -589,7 +589,7 @@ This module uses the C preprocessor to select a target architecture. > tptrOpt <- return $ scTCB sc > assert (tptrOpt /= Nothing) "schedContextResume: option of TCB pointer must not be Nothing" > tptr <- return $ fromJust tptrOpt -> schedulable <- isSchedulable tptr +> schedulable <- getSchedulable tptr > when schedulable $ do > ready <- refillReady scPtr > sufficient <- getRefillSufficient scPtr 0 @@ -599,7 +599,7 @@ This module uses the C preprocessor to select a target architecture. > contextYieldToUpdateQueues scPtr = do > sc <- getSchedContext scPtr > tptr <- return $ fromJust $ scTCB sc -> schedulable <- isSchedulable tptr +> schedulable <- getSchedulable tptr > if schedulable > then do > ctPtr <- getCurThread diff --git a/spec/haskell/src/SEL4/Object/TCB.lhs b/spec/haskell/src/SEL4/Object/TCB.lhs index 1c8ec189f9..2f34538966 100644 --- a/spec/haskell/src/SEL4/Object/TCB.lhs +++ b/spec/haskell/src/SEL4/Object/TCB.lhs @@ -1018,7 +1018,7 @@ On some architectures, the thread context may include registers that may be modi > (refillBudgetCheck consumed) > updateSchedContext scPtr $ \sc -> sc { scConsumed = scConsumed sc + consumed } > setConsumedTime 0 -> whenM ((return isCurCPU) `andM` (getCurThread >>= isSchedulable)) $ do +> whenM ((return isCurCPU) `andM` (getCurThread >>= getSchedulable)) $ do > endTimeslice canTimeoutFault > rescheduleRequired > setReprogramTimer True @@ -1049,7 +1049,7 @@ On some architectures, the thread context may include registers that may be modi > mcsPreemptionPoint :: Maybe IRQ -> Kernel () > mcsPreemptionPoint irq_opt = do > curThread <- getCurThread -> isschedulable <- isSchedulable curThread +> isschedulable <- getSchedulable curThread > if isschedulable > then do > checkBudget