From 55544107f13f8859f34ac6d248b7db6b6471958e Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 11:41:38 +0930 Subject: [PATCH] rt spec+proof: prove awaken_ccorres Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Finalise_C.thy | 13 +- proof/crefine/RISCV64/Ipc_C.thy | 20 - proof/crefine/RISCV64/SR_lemmas_C.thy | 5 + proof/crefine/RISCV64/Schedule_C.thy | 194 ++++++++++ proof/crefine/RISCV64/Tcb_C.thy | 2 +- .../DetSchedSchedule_AI.thy | 68 ++-- proof/invariant-abstract/Syscall_AI.thy | 2 +- proof/refine/RISCV64/EmptyFail_H.thy | 2 +- proof/refine/RISCV64/Ipc_R.thy | 2 +- proof/refine/RISCV64/KHeap_R.thy | 4 +- proof/refine/RISCV64/Schedule_R.thy | 344 ++++++++---------- proof/refine/RISCV64/TcbAcc_R.thy | 27 +- spec/abstract/Schedule_A.thy | 21 +- spec/design/skel/KernelStateData_H.thy | 4 +- spec/haskell/src/SEL4/Model/StateData.lhs | 10 +- spec/haskell/src/SEL4/Object/SchedContext.lhs | 15 +- spec/haskell/src/SEL4/Object/TCB.lhs | 36 +- 17 files changed, 444 insertions(+), 325 deletions(-) diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy index 4526800986..99474d3382 100644 --- a/proof/crefine/RISCV64/Finalise_C.thy +++ b/proof/crefine/RISCV64/Finalise_C.thy @@ -637,14 +637,19 @@ lemma merge_overlapping_head_refill_ccorres: done (* FIXME RT: move to Corres_UL_C? *) -lemma ccorres_to_vcg_Normal: - "\ccorres_underlying srel \ rrel xf arrel axf P P' [] a c; no_fail Q a\ - \ \ \ {s'. P s \ Q s \ s' \ P' \ (s, s') \ srel} c UNIV" - apply (frule (1) ccorres_to_vcg_with_prop[where R="\\" and s=s]) +lemma ccorres_to_vcg_Normal': + "\ccorres_underlying srel \ rrel xf arrel axf P P' [] a c\ + \ \ \ {s'. P s \ \ snd (a s) \ s' \ P' \ (s, s') \ srel} c UNIV" + apply (frule ccorres_to_vcg_with_prop'[where R="\\" and s=s]) apply wpsimp apply (fastforce elim: conseqPost) done +lemma ccorres_to_vcg_Normal: + "\ccorres_underlying srel \ rrel xf arrel axf P P' [] a c; no_fail Q a\ + \ \ \ {s'. P s \ Q s \ s' \ P' \ (s, s') \ srel} c UNIV" + by (fastforce elim: ccorres_to_vcg_Normal' intro: conseqPre simp: no_fail_def) + crunch scActive for (empty_fail) empty_fail[wp] diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index 31584cccaf..1f80932177 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -5015,26 +5015,6 @@ lemma schedContext_donate_ccorres: (schedContextDonate scPtr tcbPtr) (Call schedContext_donate_'proc)" sorry (* FIXME RT: schedContext_donate_ccorres *) -lemma tcbReleaseDequeue_ccorres: - "ccorres (\ptr ptr'. ptr' = tcb_ptr_to_ctcb_ptr ptr) ret__ptr_to_struct_tcb_C_' - (\s. \ tcbQueueEmpty (ksReleaseQueue s) \ valid_objs' s) UNIV [] - tcbReleaseDequeue (Call tcbReleaseDequeue_'proc)" - apply (clarsimp simp: tcbReleaseDequeue_def) - apply (rule ccorres_symb_exec_l'[OF _ _ getReleaseQueue_sp]; wpsimp?) - apply cinit' - apply (rule ccorres_symb_exec_r) - apply (ctac add: tcbReleaseRemove_ccorres) - apply (fastforce intro: ccorres_return_C) - apply wpsimp - apply (vcg exspec=tcbReleaseRemove_modifies) - apply vcg - apply (rule conseqPre, vcg) - apply clarsimp - apply wpsimp - apply (clarsimp simp: rf_sr_def cstate_relation_def ctcb_queue_relation_def option_to_ctcb_ptr_def - Let_def tcbQueueEmpty_def) - done - lemma sendIPC_ccorres [corres]: "ccorres dc xfdc (invs' and st_tcb_at' simple' thread and sch_act_not thread and ep_at' epptr) diff --git a/proof/crefine/RISCV64/SR_lemmas_C.thy b/proof/crefine/RISCV64/SR_lemmas_C.thy index 8db22e5f90..f004d6ca24 100644 --- a/proof/crefine/RISCV64/SR_lemmas_C.thy +++ b/proof/crefine/RISCV64/SR_lemmas_C.thy @@ -2237,6 +2237,11 @@ lemma rf_sr_ctcb_queue_relation: apply (clarsimp simp: Let_def seL4_MinPrio_def minDom_def maxDom_to_H maxPrio_to_H) done +lemma rf_sr_ctcb_queue_relation_release_queue: + "(s, s') \ rf_sr \ ctcb_queue_relation (ksReleaseQueue s) (ksReleaseQueue_' (globals s'))" + unfolding rf_sr_def cstate_relation_def cready_queues_relation_def + by (clarsimp simp: Let_def seL4_MinPrio_def minDom_def maxDom_to_H maxPrio_to_H) + lemma rf_sr_sched_action_relation: "(s, s') \ rf_sr \ cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))" diff --git a/proof/crefine/RISCV64/Schedule_C.thy b/proof/crefine/RISCV64/Schedule_C.thy index f6f679b3c1..a312834f69 100644 --- a/proof/crefine/RISCV64/Schedule_C.thy +++ b/proof/crefine/RISCV64/Schedule_C.thy @@ -631,6 +631,200 @@ lemma commitTime_ccorres: "ccorres dc xfdc \ UNIV [] commitTime (Call commitTime_'proc)" sorry (* FIXME RT: commitTime_ccorres *) +lemma ccorres_pre_getReleaseQueue: + assumes cc: "\rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" + shows + "ccorres r xf + (\s. \rv. ksReleaseQueue s = rv \ P rv s) + {s'. \rv s. (s, s') \ rf_sr \ ksReleaseQueue s = rv \ P rv s + \ ctcb_queue_relation rv (ksReleaseQueue_' (globals s')) + \ s' \ P' rv} hs + (getReleaseQueue >>= (\rv. f rv)) c" + apply (rule ccorres_guard_imp) + apply (rule ccorres_symb_exec_l) + defer + apply wp[1] + apply (rule getReleaseQueue_sp) + apply wpsimp + apply assumption + apply clarsimp + defer + apply (rule ccorres_guard_imp) + apply (rule cc) + apply clarsimp + apply assumption + apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) + by fast + +lemma scActive_exs_valid[wp]: + "sc_at' scPtr s \ \(=) s\ scActive scPtr \\\r. (=) s\" + unfolding scActive_def + apply wpsimp + by (fastforce dest: no_ofailD[OF no_ofail_readScActive]) + +lemma release_q_non_empty_and_ready_ccorres: + "ccorres (\rv rv'. rv = to_bool rv') ret__unsigned_long_' + (valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct' + and (\s. \head. tcbQueueHead (ksReleaseQueue s) = Some head \ active_sc_tcb_at' head s)) + UNIV [] + (gets_the releaseQNonEmptyAndReady) + (Call release_q_non_empty_and_ready_'proc)" + apply cinit' + apply (simp add: releaseQNonEmptyAndReady_def gets_the_if_distrib readReleaseQueue_def + gets_the_ogets + flip: getReleaseQueue_def) + apply (rule ccorres_pre_getReleaseQueue) + apply (rename_tac releaseQueue) + apply (rule_tac xf'=ret__int_' + and val="from_bool (tcbQueueHead releaseQueue \ None)" + and R="\s. ksReleaseQueue s = releaseQueue + \ (\head. tcbQueueHead (ksReleaseQueue s) = Some head \ tcb_at' head s)" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (fastforce dest: tcb_at_not_NULL rf_sr_ctcb_queue_relation_release_queue + simp: ctcb_queue_relation_def option_to_ctcb_ptr_def + split: option.splits) + apply ceqv + apply (subst if_swap) + apply (rule ccorres_cond_seq) + apply ccorres_rewrite + apply (rule_tac Q="\s. ksReleaseQueue s = releaseQueue" in ccorres_cond_both'[where Q'=\]) + apply fastforce + apply (rule ccorres_rhs_assoc)+ + apply (clarsimp simp: gets_the_obind) + apply (rule ccorres_Guard_Seq) + apply (simp flip: threadGet_def refillReady_def) + apply (drule Some_to_the) + apply clarsimp + apply (rule ccorres_pre_threadGet) + apply (simp add: gets_the_ohaskell_assert) + apply (rule ccorres_assert2) + apply (simp flip: scActive_def) + apply (rule ccorres_symb_exec_l') + apply (rule ccorres_assert2_abs) + apply (rule ccorres_add_return2) + apply (ctac add: refill_ready_ccorres) + apply csymbr + apply (fastforce intro: ccorres_return_C') + apply wpsimp + apply (vcg exspec=refill_ready_modifies) + apply wpsimp+ + apply (fastforce intro: ccorres_return_C) + apply vcg + apply (rule conjI) + apply (fastforce intro!: aligned'_distinct'_obj_at'I + simp: active_sc_tcb_at'_def active_sc_at'_def obj_at'_def + opt_pred_def opt_map_def + split: option.splits) + apply clarsimp + apply (intro conjI) + apply (clarsimp simp: ctcb_relation_def typ_heap_simps' option_to_ctcb_ptr_def + ctcb_queue_relation_def) + apply (clarsimp simp: to_bool_def split: if_splits) + apply (force dest: obj_at_cslift_tcb + simp: typ_heap_simps' ctcb_queue_relation_def option_to_ctcb_ptr_def) + done + +lemma tcbReleaseDequeue_ccorres: + "ccorres dc xfdc + (valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct' + and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and (\s. ksCurDomain s \ maxDomain) + and (\s. releaseQNonEmptyAndReady s = Some True)) + UNIV [] + tcbReleaseDequeue + (Call tcbReleaseDequeue_'proc)" + apply cinit + apply (rule ccorres_stateAssert)+ + apply (rule ccorres_pre_getReleaseQueue, rename_tac releaseQueue) + apply (rule_tac P="tcbQueueHead releaseQueue \ None" in ccorres_gen_asm) + apply (rule ccorres_symb_exec_l') + apply (rule ccorres_assert2_abs) + apply (rule_tac xf'=awakened_' + and val="option_to_ctcb_ptr (tcbQueueHead releaseQueue)" + and R="\s. ksReleaseQueue s = releaseQueue" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply clarsimp + apply (drule rf_sr_ctcb_queue_relation_release_queue) + apply (clarsimp simp: ctcb_queue_relation_def) + apply ceqv + apply (ctac add: tcbReleaseRemove_ccorres) + apply (rule ccorres_add_return2) + apply (simp only: bind_assoc) + apply (subst ccorres_seq_skip'[symmetric]) + apply (ctac add: possibleSwitchTo_ccorres) + apply (rule ccorres_stateAssert)+ + apply (rule ccorres_return_Skip') + apply wpsimp + apply (vcg exspec=possibleSwitchTo_modifies) + apply wpsimp + apply (vcg exspec=tcbReleaseRemove_modifies) + apply vcg + apply wpsimp+ + apply (frule releaseQNonEmptyAndReady_implies_releaseQNonEmpty) + by (fastforce dest: obj_at'_tcbQueueHead_ksReleaseQueue simp: option_to_ctcb_ptr_def) + +lemma no_ofail_releaseQNonEmptyAndReady: + "no_ofail (invs' + and (\s. \head. tcbQueueHead (ksReleaseQueue s) = Some head + \ active_sc_tcb_at' head s)) + releaseQNonEmptyAndReady" + unfolding releaseQNonEmptyAndReady_def readReleaseQueue_def + apply (wpsimp wp: ovalid_threadRead) + apply (clarsimp split: if_splits) + apply (intro conjI) + apply (fastforce intro!: aligned'_distinct'_obj_at'I + simp: active_sc_tcb_at'_def opt_pred_def opt_map_def obj_at_simps + split: option.splits) + apply normalise_obj_at' + apply (fastforce intro!: aligned'_distinct'_obj_at'I + simp: active_sc_tcb_at'_def obj_at'_def opt_pred_def opt_map_def + split: option.splits) + done + +lemma awaken_ccorres: + "ccorres dc xfdc (invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) UNIV [] + awaken (Call awaken_'proc)" + (is "ccorres _ _ ?abs _ _ _ _") + apply (cinit simp: runReaderT_def whileAnno_def) + apply (rule ccorres_stateAssert)+ + apply (rule ccorres_handlers_weaken) + apply (rule_tac G="\_. ?abs + and (\s. \head. tcbQueueHead (ksReleaseQueue s) = Some head + \ active_sc_tcb_at' head s)" + in ccorres_While'[where G'=UNIV]) + apply (rule ccorres_guard_imp) + apply (ctac add: tcbReleaseDequeue_ccorres) + apply fastforce + apply fastforce + apply (rule ccorres_guard_imp) + apply (ctac add: release_q_non_empty_and_ready_ccorres) + apply fastforce + apply fastforce + apply (wpsimp wp: no_ofail_releaseQNonEmptyAndReady) + apply (clarsimp simp: pred_conj_def) + apply (intro hoare_vcg_conj_lift_pre_fix; (solves wpsimp)?) + apply (clarsimp simp: tcbReleaseDequeue_def) + apply (wpsimp simp: tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt_def) + apply (rule conseqPre) + apply (rule ccorres_to_vcg_Normal'[where xf=xfdc]) + apply (fastforce intro: ccorres_call[OF tcbReleaseDequeue_ccorres]) + apply fastforce + apply clarsimp + apply (rule conseqPre) + apply (rule_tac xf=ret__unsigned_long_' in ccorres_to_vcg_Normal) + apply (fastforce intro: ccorres_call[OF release_q_non_empty_and_ready_ccorres]) + apply (fastforce intro: no_ofail_gets_the no_ofail_releaseQNonEmptyAndReady) + apply fastforce + apply (clarsimp simp: tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def ksReleaseQueue_asrt_def + list_queue_relation_def) + apply (frule heap_path_head') + apply (clarsimp simp: tcbQueueEmpty_def) + apply (case_tac "ts = []"; force) + done + lemma schedule_ccorres: "ccorres dc xfdc invs' UNIV [] schedule (Call schedule_'proc)" sorry (* FIXME RT: schedule_ccorres diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy index 00df4d7c4d..ac68d104a2 100644 --- a/proof/crefine/RISCV64/Tcb_C.thy +++ b/proof/crefine/RISCV64/Tcb_C.thy @@ -4952,7 +4952,7 @@ lemma find_time_after_ccorres: (is "ccorres _ _ (?abs_inv and _) _ _ _ _") supply sched_context_C_size[simp del] refill_C_size[simp del] apply (cinit lift: new_time_' tcb_' - simp: runReaderT_def whileAnno_def tcbInReleaseQueue_imp_active_sc_tc_at'_asrt_def) + simp: runReaderT_def whileAnno_def tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def) apply (rule ccorres_stateAssert) apply (rule ccorres_symb_exec_r) apply (rule ccorres_add_return2) diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index e30840929c..79f069d9ae 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -10816,41 +10816,26 @@ lemma active_sc_tcb_at_budget_sufficient: by (fastforce simp: budget_sufficient_def2 active_sc_tcb_at_def2 is_sc_active_kh_simp dest: valid_refills_refill_sufficient active_scs_validE) -lemma awaken_body_valid_ready_qs: - "\\s. valid_ready_qs s \ valid_release_q s \ active_scs_valid s +lemma tcb_release_dequeue_valid_ready_qs: + "\\s. valid_ready_qs s \ valid_release_q s \ release_queue s \ [] \ budget_ready (hd (release_queue s)) s\ - awaken_body + tcb_release_dequeue \\_. valid_ready_qs\" - apply (clarsimp simp: awaken_body_def tcb_release_dequeue_def bind_assoc) - apply (rule bind_wp[OF _ gets_sp], rename_tac rq) - apply (rule_tac Q'="\_ s. valid_ready_qs s \ st_tcb_at runnable (hd rq) s - \ released_sc_tcb_at (hd rq) s" - in bind_wp_fwd) - apply (intro hoare_vcg_conj_lift_pre_fix; (solves wpsimp)?) - apply (wpsimp simp: valid_release_q_def obj_at_kh_kheap_simps) - apply (wpsimp simp: valid_release_q_def obj_at_kh_kheap_simps released_sc_tcb_at_def) - apply (clarsimp intro!: active_sc_tcb_at_budget_sufficient) - apply (wpsimp wp: possible_switch_to_valid_ready_qs - simp: released_sc_tcb_at_def) - apply (clarsimp simp: pred_tcb_at_def obj_at_def) + unfolding tcb_release_dequeue_def + apply (wpsimp wp: possible_switch_to_valid_ready_qs hoare_disjI2 hoare_vcg_all_lift + hoare_vcg_imp_lift') + apply (clarsimp simp: valid_release_q_def) + apply (fastforce dest: hd_in_set simp: vs_all_heap_simps obj_at_kh_kheap_simps) done -lemma awaken_body_valid_sched_action: - "\\s. valid_sched_action s \ valid_release_q s \ active_scs_valid s +lemma tcb_release_dequeue_valid_sched_action: + "\\s. valid_sched_action s \ valid_release_q s \ release_queue s \ [] \ budget_ready (hd (release_queue s)) s\ - awaken_body + tcb_release_dequeue \\_. valid_sched_action\" - apply (clarsimp simp: awaken_body_def tcb_release_dequeue_def bind_assoc) - apply (rule bind_wp[OF _ gets_sp], rename_tac rq) - apply (rule_tac Q'="\_ s. valid_sched_action s \ st_tcb_at runnable (hd rq) s - \ released_sc_tcb_at (hd rq) s" - in bind_wp_fwd) - apply (intro hoare_vcg_conj_lift_pre_fix; (solves wpsimp)?) - apply (wpsimp simp: valid_release_q_def obj_at_kh_kheap_simps) - apply wpsimp - apply (fastforce intro: active_sc_tcb_at_budget_sufficient - simp: released_sc_tcb_at_def valid_release_q_def) - apply (wpsimp simp: obj_at_kh_kheap_simps) + unfolding tcb_release_dequeue_def + apply (wpsimp wp: hoare_drop_imps) + apply (fastforce simp: released_sc_tcb_at_def valid_release_q_def) done lemma read_tcb_refill_ready_SomeD: @@ -10985,16 +10970,16 @@ lemma awaken_valid_sched: read_tcb_obj_ref_SomeD read_sched_context_SomeD read_release_q_non_empty_and_ready_SomeD simp: vs_all_heap_simps) - apply (intro hoare_vcg_conj_lift_pre_fix - ; (solves \wpsimp simp: awaken_body_def tcb_release_dequeue_def\)?) - apply (wpsimp wp: awaken_body_valid_ready_qs) - apply (wpsimp wp: possible_switch_to_not_it_ct_not_in_q simp: awaken_body_def tcb_release_dequeue_def) + apply (intro hoare_vcg_conj_lift_pre_fix; + (solves \wpsimp simp: tcb_release_dequeue_def\)?) + apply (wpsimp wp: tcb_release_dequeue_valid_ready_qs) + apply (wpsimp wp: possible_switch_to_not_it_ct_not_in_q simp: tcb_release_dequeue_def) apply (clarsimp simp: valid_release_q_def valid_idle_def vs_all_heap_simps pred_tcb_at_def obj_at_def) apply (fastforce dest: hd_in_set) - apply (wpsimp wp: awaken_body_valid_sched_action) + apply (wpsimp wp: tcb_release_dequeue_valid_sched_action) apply (wpsimp wp: possible_switch_to_valid_blocked tcb_release_remove_valid_blocked_except - simp: awaken_body_def tcb_release_dequeue_def) + simp: tcb_release_dequeue_def tcb_release_dequeue_def) done end @@ -12337,9 +12322,10 @@ lemma not_schedulable_in_release_q_case: by (clarsimp simp: schedulable_def2 ct_in_state_def tcb_at_kh_simps runnable_eq_active) lemma awaken_valid_sched_misc[wp]: - "awaken \\s. P (consumed_time s) (cur_sc s) (cur_time s) (cur_domain s) - (cur_thread s) (idle_thread s) (kheap s) \" - apply (wpsimp simp: awaken_def awaken_body_def tcb_release_dequeue_def) + "awaken + \\s. P (consumed_time s) (cur_sc s) (cur_time s) (cur_domain s) (cur_thread s) (idle_thread s) + (kheap s)\" + apply (wpsimp simp: awaken_def tcb_release_dequeue_def) apply (rule whileLoop_wp) apply wpsimp+ done @@ -12401,7 +12387,7 @@ lemma possible_switch_to_scheduler_act_sane'': lemma awaken_cur_sc_in_release_q_imp_zero_consumed[wp]: "awaken \cur_sc_in_release_q_imp_zero_consumed ::'state_ext state \ _\" - apply (wpsimp simp: awaken_def awaken_body_def tcb_release_dequeue_def) + apply (wpsimp simp: awaken_def tcb_release_dequeue_def) apply (clarsimp simp: cur_sc_in_release_q_imp_zero_consumed_def) apply (rule whileLoop_wp) apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_imp_lift')+ @@ -12433,8 +12419,8 @@ lemma awaken_in_release_q: "\in_release_q t and valid_release_q and (not budget_ready t) and active_scs_valid\ awaken \\_ s. in_release_q t s\" - (is "valid ?pre _ _") - apply (wpsimp simp: awaken_def awaken_body_def tcb_release_dequeue_def) + (is "valid ?pre _ _") + apply (wpsimp simp: awaken_def tcb_release_dequeue_def) apply (rule_tac I="\_. ?pre" in valid_whileLoop; (solves simp)?) apply (clarsimp simp: pred_conj_def pred_neg_def) apply (intro hoare_vcg_conj_lift_pre_fix; (solves \wpsimp wp: hoare_drop_imps\)?) diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index ec04f2b2cb..182e4c001f 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -161,7 +161,7 @@ declare sc_and_timer_activatable[wp] lemma awaken_schact_not_rct[wp]: "awaken \\s. scheduler_action s \ resume_cur_thread\" - unfolding awaken_def awaken_body_def tcb_release_dequeue_def possible_switch_to_def + unfolding awaken_def tcb_release_dequeue_def possible_switch_to_def apply (rule whileLoop_wp) apply (wpsimp wp: hoare_drop_imps simp: set_scheduler_action_def)+ done diff --git a/proof/refine/RISCV64/EmptyFail_H.thy b/proof/refine/RISCV64/EmptyFail_H.thy index 6d9f340a15..30d9db8bed 100644 --- a/proof/refine/RISCV64/EmptyFail_H.thy +++ b/proof/refine/RISCV64/EmptyFail_H.thy @@ -291,7 +291,7 @@ crunch tcbReleaseDequeue lemma awaken_empty_fail[intro!, wp, simp]: "empty_fail awaken" - apply (clarsimp simp: awaken_def awakenBody_def) + apply (clarsimp simp: awaken_def tcbReleaseDequeue_def) apply (wpsimp wp: empty_fail_whileLoop) done diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index 6f8671e771..9b321d418f 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -3445,7 +3445,7 @@ lemma findTimeAfter_corres: apply (rule corres_gen_asm') apply (clarsimp simp: find_time_after_def findTimeAfter_def runReaderT_def) apply (rule corres_stateAssert_implied[where P=P and P'=P for P, simplified, rotated]) - apply (fastforce simp: tcbInReleaseQueue_imp_active_sc_tc_at'_asrt_def + apply (fastforce simp: tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def dest!: release_queue_active_sc_tcb_at_cross) apply (rule stronger_corres_guard_imp) apply (rule_tac P="\r s. ?abs s \ suffix r ls" diff --git a/proof/refine/RISCV64/KHeap_R.thy b/proof/refine/RISCV64/KHeap_R.thy index f66f847a3b..e1efe240eb 100644 --- a/proof/refine/RISCV64/KHeap_R.thy +++ b/proof/refine/RISCV64/KHeap_R.thy @@ -5086,8 +5086,8 @@ lemma active_sc_tcb_at_cross: apply (clarsimp simp: active_sc_tcb_at'_def in_omonad obj_at'_def active_sc_at'_def) done -defs tcbInReleaseQueue_imp_active_sc_tc_at'_asrt_def: - "tcbInReleaseQueue_imp_active_sc_tc_at'_asrt \ +defs tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def: + "tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt \ \s'. \tcbPtr. (tcbInReleaseQueue |< tcbs_of' s') tcbPtr \ (tcb_at' tcbPtr s' \ active_sc_tcb_at' tcbPtr s')" diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index d9986b314b..f634ef8b9c 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -64,9 +64,6 @@ crunch commitTime, refillNew, refillUpdate end -global_interpretation tcbReleaseDequeue: typ_at_all_props' tcbReleaseDequeue - by typ_at_props' - global_interpretation refillPopHead: typ_at_all_props' "refillPopHead scPtr" by typ_at_props' @@ -2507,13 +2504,8 @@ lemma possibleSwitchTo_utr[wp]: "possibleSwitchTo t \untyped_ranges_zero'\" by (wpsimp simp: cteCaps_of_def o_def wp: untyped_ranges_zero_lift) -lemma possibleSwitchTo_invs'[wp]: - "\invs' and st_tcb_at' runnable' tptr\ - possibleSwitchTo tptr - \\_. invs'\" - apply (simp add: possibleSwitchTo_def) - apply (wpsimp wp: hoare_vcg_imp_lift threadGet_wp inReleaseQueue_wp ssa_invs') - done +crunch possibleSwitchTo + for invs'[wp]: invs' lemma possibleSwitchTo_sch_act_not_other: "\\s. sch_act_not t' s \ t' \ t\ @@ -2533,22 +2525,16 @@ lemma getReleaseQueue_sp: by wpsimp lemma releaseQNonEmptyAndReady_implies_releaseQNonEmpty: - "the (releaseQNonEmptyAndReady s) \ tcbQueueHead (ksReleaseQueue s) \ None" + "releaseQNonEmptyAndReady s = Some True \ tcbQueueHead (ksReleaseQueue s) \ None" by (clarsimp simp: releaseQNonEmptyAndReady_def readReleaseQueue_def obind_def omonad_defs split: if_splits) -lemma awaken_invs': - "awaken \invs'\" - apply (clarsimp simp: awaken_def awakenBody_def) - apply (rule_tac I="\_. invs'" in valid_whileLoop; simp add: runReaderT_def) - apply wpsimp - apply (wpsimp wp: tcbReleaseDequeue_invs' hoare_drop_imps) - apply (fastforce intro!: releaseQNonEmptyAndReady_implies_releaseQNonEmpty) - done +crunch awaken + for invs'[wp]: invs' + (wp: crunch_wps) -crunch tcbReleaseDequeue - for st_tcb_at'[wp]: "\s. Q (st_tcb_at' P p s)" - and valid_replies' [wp]: valid_replies' +crunch tcbReleaseRemove + for valid_replies' [wp]: valid_replies' (wp: crunch_wps threadSet_pred_tcb_no_state valid_replies'_lift) crunch awaken @@ -2813,54 +2799,6 @@ lemma setReprogramTimer_corres[corres]: apply (simp add: state_relation_def swp_def) done -lemma readTCBRefillReady_no_ofail: - "no_ofail (\s'. obj_at' (\tcb. \sc. tcbSchedContext tcb = Some sc \ sc_at' sc s') t s') - (readTCBRefillReady t)" - unfolding readTCBRefillReady_def - apply (wpsimp wp: ovalid_threadRead) - apply (clarsimp simp: obj_at'_def) - done - -lemma gets_the_readTCBRefillReady_corres: - "t = t' \ - corres (=) - (active_sc_tcb_at t and active_scs_valid and valid_objs and pspace_aligned and pspace_distinct) - (valid_objs' and pspace_bounded') - (gets_the (read_tcb_refill_ready t )) (gets_the (readTCBRefillReady t'))" - apply (clarsimp simp: read_tcb_refill_ready_def readTCBRefillReady_def read_tcb_obj_ref_def - gets_the_thread_read gets_the_assert_opt - simp flip: threadGet_def get_sc_refill_ready_def[simplified fun_app_def] - refillReady_def) - apply (rule stronger_corres_guard_imp) - apply (rule_tac r'="(=)" in corres_split[OF threadGet_corres]) - apply (clarsimp simp: tcb_relation_def) - apply (rule corres_assert_opt_l) - apply (rule refillReady_corres) - apply fastforce - apply (wpsimp wp: thread_get_wp) - apply (wpsimp wp: threadGet_wp) - apply (clarsimp simp: vs_all_heap_simps obj_at_def is_tcb_def is_sc_obj_def) - apply (intro conjI) - apply (fastforce elim: valid_objs_valid_sched_context_size) - apply (fastforce elim!: active_scs_validE[rotated] - intro!: valid_refills_nonempty_refills - simp: vs_all_heap_simps obj_at_def is_tcb_def is_sc_obj_def) - apply (normalise_obj_at', rename_tac ko) - apply (frule cross_relF[OF _ isScActive_cross_rel]) - apply fastforce - apply (prop_tac "bound (tcbSchedContext ko)") - apply (clarsimp simp: obj_at'_def opt_map_def pred_map_simps) - apply (erule valid_objs'_valid_refills') - apply (rule aligned'_distinct'_obj_at'I) - apply (clarsimp simp: obj_at'_def opt_map_def isScActive_def pred_map_simps - split: option.splits) - apply (fastforce intro: pspace_aligned_cross) - apply (fastforce intro!: pspace_distinct_cross) - apply fastforce - apply (fastforce simp: is_active_sc'_def opt_pred_def opt_map_def obj_at'_def isScActive_def - pred_map_simps) - done - lemma getReleaseQueue_corres: "corres (\ls q. (ls = [] \ tcbQueueEmpty q) \ (ls \ [] \ tcbQueueHead q = Some (hd ls)) \ queue_end_valid ls q) @@ -2871,24 +2809,73 @@ lemma getReleaseQueue_corres: simp: release_queue_relation_def list_queue_relation_def tcbQueueEmpty_def) done +lemma scActive_inv: + "scActive scPtr \P\" + by wpsimp + lemma gets_the_releaseQNonEmptyAndReady_corres: "corres (=) (valid_release_q and active_scs_valid and valid_objs and pspace_aligned and pspace_distinct) (valid_objs' and pspace_bounded') (gets_the (read_release_q_non_empty_and_ready)) (gets_the (releaseQNonEmptyAndReady))" - apply (clarsimp simp: read_release_q_non_empty_and_ready_def releaseQNonEmptyAndReady_def - gets_the_ogets getReleaseQueue_def[symmetric] readReleaseQueue_def - gets_the_if_distrib) + apply (rule_tac Q'=pspace_aligned' in corres_cross_add_guard) + apply (fastforce dest: pspace_aligned_cross) + apply (rule_tac Q'=pspace_distinct' in corres_cross_add_guard) + apply (fastforce dest: pspace_distinct_cross) + apply (simp add: read_release_q_non_empty_and_ready_def releaseQNonEmptyAndReady_def + gets_the_ogets readReleaseQueue_def gets_the_if_distrib + flip: getReleaseQueue_def) apply (rule stronger_corres_guard_imp) apply (rule corres_split[OF getReleaseQueue_corres]) - apply (rule corres_if_strong[where R=\ and R'=\ and P=\]) + apply (rule corres_if_strong[where R=\ and R'=\ and P=\ and P'=\]) apply (fastforce simp: tcbQueueEmpty_def) apply clarsimp - apply (rule gets_the_readTCBRefillReady_corres) - apply wpsimp+ - apply (fastforce elim: valid_release_q_active_sc) - apply fastforce - done + apply (simp add: read_tcb_refill_ready_def read_tcb_obj_ref_def gets_the_thread_read + gets_the_assert_opt gets_the_ohaskell_assert + flip: threadGet_def get_sc_refill_ready_def refillReady_def) + apply (rule_tac r'="(=)" in corres_split[OF threadGet_corres]) + apply (clarsimp simp: tcb_relation_def) + apply (rule corres_assert_opt_l) + apply (rule corres_assert_gen_asm2) + apply (simp flip: scActive_def) + apply (rule corres_symb_exec_r'[where Q'=\]) + apply (rule corres_assert_gen_asm2) + apply (rule refillReady_corres) + apply fastforce + apply wpsimp + apply (rule scActive_inv) + apply clarsimp + apply wpsimp + apply (wpsimp wp: thread_get_wp) + apply (rule_tac Q'="\rv s. \scPtr. rv = Some scPtr \ active_sc_at' scPtr s \ valid_objs' s" + in hoare_post_imp) + apply (fastforce intro: valid_objs'_valid_refills' + simp: active_sc_at'_def is_active_sc'_def obj_at'_def + opt_pred_def opt_map_def) + apply clarsimp + apply (drule Some_to_the) + apply (wpsimp wp: hoare_vcg_ex_lift threadGet_wp) + apply wpsimp + apply wpsimp + apply (clarsimp simp: valid_release_q_def) + apply (drule_tac x="hd (release_queue s)" in bspec) + apply fastforce + apply (fastforce elim!: valid_objs_valid_sched_context_size active_scs_validE[rotated] + intro!: valid_refills_nonempty_refills + simp: vs_all_heap_simps obj_at_def is_tcb_def is_sc_obj_def) + apply (clarsimp split: if_splits) + apply (rename_tac head) + apply (frule (4) release_queue_active_sc_tcb_at_cross) + apply (frule state_relation_release_queue_relation) + apply (drule_tac x=head in spec) + apply (clarsimp simp: release_queue_relation_def) + apply (frule (3) obj_at'_tcbQueueHead_ksReleaseQueue) + apply (clarsimp simp: tcbQueueEmpty_def) + apply normalise_obj_at' + apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') + by (fastforce simp: active_sc_tcb_at'_def opt_pred_def opt_map_def + obj_at'_def active_sc_at'_def valid_bound_obj'_def valid_tcb'_def + split: option.splits) lemma release_queue_length_well_founded: "wf {((r :: unit, s :: 'a state), (r', s')). length (release_queue s) < length (release_queue s')}" @@ -2914,21 +2901,14 @@ lemma tcb_release_dequeue_release_queue_length: apply (clarsimp simp: read_release_q_non_empty_and_ready_simp) done -lemma awaken_body_release_queue_length: - "\\s'. the (read_release_q_non_empty_and_ready s') \ s' = s\ - awaken_body - \\_ s'. length (release_queue s') < length (release_queue s)\" - apply (clarsimp simp: awaken_body_def) - apply (wpsimp wp: tcb_release_dequeue_release_queue_length hoare_drop_imps) - done - lemma awaken_terminates: - "whileLoop_terminates (\_ s. (the (read_release_q_non_empty_and_ready s))) (\_. awaken_body) r' s" + "whileLoop_terminates (\_ s. (the (read_release_q_non_empty_and_ready s))) + (\_. tcb_release_dequeue) r' s" apply (rule_tac R="{((r', s'), (r, s)). length (release_queue s') < length (release_queue s)}" in whileLoop_terminates_inv) apply simp apply clarsimp - apply (rule awaken_body_release_queue_length) + apply (rule tcb_release_dequeue_release_queue_length) apply (rule release_queue_length_well_founded) done @@ -3146,28 +3126,6 @@ lemma tcbReleaseRemove_corres: by (auto dest!: hd_in_set simp: opt_pred_def opt_map_def fun_upd_apply split: option.splits) by (auto simp: in_opt_pred opt_map_red fun_upd_apply split: option.splits) -lemma tcbReleaseDequeue_corres: - "corres (=) - (pspace_aligned and pspace_distinct and valid_release_q and (\s. release_queue s \ []) - and ready_or_release) - (sym_heap_sched_pointers and valid_objs') - tcb_release_dequeue tcbReleaseDequeue" - apply (clarsimp simp: tcb_release_dequeue_def tcbReleaseDequeue_def) - apply (rule corres_symb_exec_l[rotated, OF _ gets_sp]; wpsimp?) - apply (rename_tac rlq) - apply (rule corres_symb_exec_r[rotated, OF getReleaseQueue_sp]; wpsimp?) - apply (rename_tac queue) - apply (rule_tac F="rlq \ [] \ hd rlq = the (tcbQueueHead queue)" in corres_req) - apply (drule state_relation_release_queue_relation) - apply (clarsimp simp: list_queue_relation_def release_queue_relation_def) - apply (fastforce dest: heap_path_head heap_ls_unique) - apply (corresKsimp corres: tcbReleaseRemove_corres) - apply (drule state_relation_release_queue_relation) - apply (clarsimp simp: release_queue_relation_def list_queue_relation_def) - apply (fastforce dest: heap_path_head - simp: valid_release_q_def vs_all_heap_simps obj_at_def is_tcb_def) - done - lemma tcbInReleaseQueue_update_valid_tcbs'[wp]: "threadSet (tcbInReleaseQueue_update f) tcbPtr \valid_tcbs'\" by (wpsimp wp: threadSet_valid_tcbs') @@ -3181,107 +3139,91 @@ lemma tcbQueueRemove_valid_tcbs'[wp]: crunch tcbReleaseDequeue for valid_tcbs'[wp]: valid_tcbs' + and valid_sched_pointers[wp]: valid_sched_pointers + (wp: crunch_wps) -crunch tcbReleaseDequeue - for valid_sched_pointers[wp]: valid_sched_pointers - -lemma tcb_release_dequeue_runnable_tcb_at_rv: - "\\s. release_queue s \ [] \ valid_release_q s\ - tcb_release_dequeue - \\rv s. st_tcb_at runnable rv s\" - apply (clarsimp simp: tcb_release_dequeue_def) - apply wpsimp - apply (fastforce simp: valid_release_q_def vs_all_heap_simps obj_at_kh_kheap_simps is_tcb_def) - done - -crunch tcb_release_dequeue - for valid_sched_action[wp]: valid_sched_action - and pspace_aligned[wp]: pspace_aligned - and pspace_distinct[wp]: pspace_distinct - and valid_tcbs[wp]: valid_tcbs - and active_sc_valid_refills[wp]: active_scs_valid - and ready_or_release[wp]: ready_or_release - and valid_ready_qs[wp]: valid_ready_qs +crunch tcb_release_remove + for ready_qs_distinct[wp]: ready_qs_distinct and in_correct_ready_q[wp]: in_correct_ready_q - and ready_qs_distinct[wp]: ready_qs_distinct - and valid_objs[wp]: valid_objs (rule: in_correct_ready_q_lift simp: crunch_simps ready_qs_distinct_def) -lemma tcb_release_dequeue_not_in_release_q[wp]: - "\\\ tcb_release_dequeue \not_in_release_q\" - unfolding tcb_release_dequeue_def - by wpsimp +defs tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt_def: + "tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt s \ + \head. tcbQueueHead (ksReleaseQueue s) = Some head \ active_sc_tcb_at' head s" -lemma awakenBody_corres: +lemma tcbReleaseDequeue_corres: "corres dc - (pspace_aligned and pspace_distinct and valid_objs and valid_sched_action - and valid_tcbs and in_correct_ready_q and ready_qs_distinct + (pspace_aligned and pspace_distinct and valid_sched_action + and valid_objs and in_correct_ready_q and ready_qs_distinct and active_scs_valid and ready_or_release - and (\s. valid_release_q s \ release_queue s \ [])) - (valid_objs' and valid_sched_pointers and sym_heap_sched_pointers - and pspace_aligned' and pspace_distinct' and pspace_bounded') - awaken_body awakenBody" - (is "corres _ (?abs_inv and _) ?conc _ _") - apply (clarsimp simp: awaken_body_def awakenBody_def) - apply (rule_tac P="\rv. ?abs_inv and not_in_release_q rv and st_tcb_at runnable rv" - and P'="\_. ?conc" - in corres_underlying_split_ex_abs) - apply (corres corres: tcbReleaseDequeue_corres) - apply clarsimp - apply (rule corres_symb_exec_r_conj_ex_abs_forwards[OF _ isRunnable_sp, rotated]; - (solves wpsimp)?) - apply wpsimp - apply (fastforce elim!: tcb_at_cross dest: state_relation_pspace_relation simp: ex_abs_def) - apply (rule corres_symb_exec_r_conj_ex_abs_forwards[OF _ assert_sp, rotated]; (solves wpsimp)?) - apply wpsimp - apply (fastforce dest: st_tcb_at_runnable_cross - simp: ex_abs_def pred_tcb_at'_def obj_at'_def runnable_eq_active') - apply (corres corres: possibleSwitchTo_corres) - apply (wpsimp wp: tcb_release_dequeue_runnable_tcb_at_rv) - apply wpsimp + and valid_release_q and (\s. release_queue s \ [])) + (valid_objs' and valid_sched_pointers and sym_heap_sched_pointers and pspace_bounded') + tcb_release_dequeue tcbReleaseDequeue" + apply (rule_tac Q'=pspace_aligned' in corres_cross_add_guard) + apply (fastforce dest: pspace_aligned_cross) + apply (rule_tac Q'=pspace_distinct' in corres_cross_add_guard) + apply (fastforce dest: pspace_distinct_cross) + apply (clarsimp simp: tcb_release_dequeue_def tcbReleaseDequeue_def) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (fastforce intro: ksReleaseQueue_asrt_cross) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (fastforce simp: tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def + dest!: release_queue_active_sc_tcb_at_cross) + apply (rule stronger_corres_guard_imp) + apply (rule corres_split[OF getReleaseQueue_corres]) + apply clarsimp + apply (rename_tac rlq queue) + apply (rule corres_symb_exec_r_conj_ex_abs_forwards) + apply (rule corres_assert_assume_r) + apply (rule_tac F="rlq \ []" in corres_gen_asm) + apply simp + apply (rule corres_split[OF tcbReleaseRemove_corres]) + apply fastforce + apply (rule corres_add_noop_lhs2) + apply (rule corres_add_noop_rhs2) + apply (simp only: bind_assoc) + apply (rule corres_split[OF possibleSwitchTo_corres]) + apply fastforce + apply (rule corres_symb_exec_r_conj_ex_abs[where P'=\ and P=\]) + apply (rule corres_symb_exec_r_conj_ex_abs + [where P'=\ + and P="valid_release_q and pspace_aligned and pspace_distinct + and valid_objs"]) + apply (rule corres_return_trivial) + apply wpsimp + apply wpsimp + apply (wpsimp wp: no_fail_stateAssert) + apply (clarsimp simp: ex_abs_def) + apply (frule (4) release_queue_active_sc_tcb_at_cross) + apply (fastforce dest!: state_relation_release_queue_relation + tcbQueueHead_ksReleaseQueue + simp: tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt_def + release_queue_relation_def tcbQueueEmpty_def) + apply wpsimp+ + apply (wpsimp wp: no_fail_stateAssert) + apply (fastforce intro: ksReleaseQueue_asrt_cross simp: ex_abs_def) + apply wpsimp+ + apply (fastforce dest!: hd_in_set + simp: valid_release_q_def vs_all_heap_simps pred_tcb_at_def obj_at_def is_tcb_def) + apply (fastforce dest: state_relation_release_queue_relation heap_path_head + intro!: st_tcb_at_runnable_cross + simp: valid_release_q_def vs_all_heap_simps pred_tcb_at_def obj_at_def + release_queue_relation_def list_queue_relation_def) done -crunch tcb_release_dequeue - for weak_valid_sched_action[wp]: weak_valid_sched_action - -crunch awakenBody - for sym_heap_sched_pointers[wp]: sym_heap_sched_pointers - (wp: crunch_wps) - crunch tcbReleaseDequeue for weak_sch_act_wf[wp]: "\s'. weak_sch_act_wf (ksSchedulerAction s') s'" + (wp: crunch_wps) crunch tcb_release_dequeue for pred_tcb_at[wp]: "\s. Q (pred_tcb_at proj P tptr s)" and released_sc_tcb_at[wp]: "released_sc_tcb_at t" -lemma read_tcb_refill_ready_released_sc_tcb_at: - "\active_sc_tcb_at tcb_ptr s; read_tcb_refill_ready tcb_ptr s = Some True\ - \ released_sc_tcb_at tcb_ptr s" - by (fastforce dest: read_refill_head_SomeD - simp: read_tcb_refill_ready_def vs_all_heap_simps read_tcb_obj_ref_def - thread_read_def omonad_defs oliftM_def get_tcb_def read_sc_refill_ready_def - read_sched_context_def) - -lemma awaken_body_valid_ready_qs: - "\\s. valid_release_q s \ valid_ready_qs s \ read_release_q_non_empty_and_ready s = Some True\ - awaken_body - \\_. valid_ready_qs\" - apply (clarsimp simp: awaken_body_def) - apply (wpsimp wp: possible_switch_to_valid_ready_qs hoare_disjI2 hoare_vcg_all_lift - hoare_vcg_imp_lift' - simp: tcb_release_dequeue_def) - apply (simp add: read_release_q_non_empty_and_ready_simp split: if_splits) - apply (rule conjI) - apply (fastforce dest: hd_in_set simp: valid_release_q_def vs_all_heap_simps obj_at_def) - apply (fastforce intro: valid_release_q_active_sc read_tcb_refill_ready_released_sc_tcb_at) - done - -crunch awaken_body +crunch tcb_release_dequeue for in_correct_ready_q[wp]: in_correct_ready_q (rule: in_correct_ready_q_lift ignore: tcb_sched_action) -crunch awaken_body +crunch tcb_release_dequeue for ready_qs_distinct[wp]: ready_qs_distinct (rule: ready_qs_distinct_lift ignore: tcb_sched_action wp: crunch_wps) @@ -3294,6 +3236,11 @@ lemma awaken_corres: and pspace_aligned' and pspace_distinct' and pspace_bounded') Schedule_A.awaken awaken" apply (clarsimp simp: awaken_def Schedule_A.awaken_def runReaderT_def) + apply (rule corres_stateAssert_ignore) + apply (fastforce intro: ksReleaseQueue_asrt_cross) + apply (rule corres_stateAssert_ignore) + apply (fastforce simp: tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def + dest!: release_queue_active_sc_tcb_at_cross) apply (rule corres_whileLoop_abs; simp) apply (rule_tac f=read_release_q_non_empty_and_ready and f'=releaseQNonEmptyAndReady @@ -3304,16 +3251,17 @@ lemma awaken_corres: apply fastforce apply (clarsimp simp: no_ofail_def) apply (erule (1) valid_release_q_read_release_q_non_empty_and_ready_bound) - apply (corresKsimp corres: awakenBody_corres) - apply (fastforce simp: read_release_q_non_empty_and_ready_simp) + apply (corres corres: tcbReleaseDequeue_corres) + apply (fastforce simp: read_release_q_non_empty_and_ready_simp) + apply fastforce apply (clarsimp simp: pred_conj_def) apply (intro hoare_vcg_conj_lift_pre_fix; - (solves \wpsimp simp: awaken_body_def tcb_release_dequeue_def\)?) - apply (wpsimp wp: awaken_body_valid_sched_action) + (solves \wpsimp simp: tcb_release_dequeue_def\)?) + apply (wpsimp wp: tcb_release_dequeue_valid_sched_action) apply (frule valid_release_q_read_release_q_non_empty_and_ready_bound) apply fastforce apply (fastforce dest: read_release_q_non_empty_and_ready_True_simp) - apply ((wpsimp simp: awakenBody_def | wpsimp wp: hoare_drop_imps)+)[1] + apply ((wpsimp simp: tcbReleaseDequeue_def | wpsimp wp: hoare_drop_imps)+)[1] apply (fastforce intro!: awaken_terminates) done diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy index 204f79e9d0..9bd166d61d 100644 --- a/proof/refine/RISCV64/TcbAcc_R.thy +++ b/proof/refine/RISCV64/TcbAcc_R.thy @@ -2116,8 +2116,8 @@ crunch setReprogramTimer, setReleaseQueue, setQueue, removeFromBitmap simp: crunch_simps tcb_cte_cases_def tcb_bound_refs'_def cur_tcb'_def threadSet_cur bitmap_fun_defs valid_machine_state'_def) -crunch tcbReleaseDequeue, tcbReleaseEnqueue, - tcbSchedEnqueue, tcbSchedAppend, tcbSchedDequeue, setQueue +crunch tcbReleaseRemove, tcbReleaseEnqueue, + tcbSchedEnqueue, tcbSchedAppend, tcbSchedDequeue, setQueue for pspace_aligned'[wp]: pspace_aligned' and state_refs_of'[wp]: "\s. P (state_refs_of' s)" and pspace_distinct'[wp]: pspace_distinct' @@ -2147,7 +2147,7 @@ crunch tcbReleaseDequeue, tcbReleaseEnqueue, (wp: crunch_wps threadSet_state_refs_of'[where f'=id and g'=id] simp: crunch_simps tcb_cte_cases_def tcb_bound_refs'_def bitmap_fun_defs) -crunch tcbReleaseDequeue, tcbReleaseEnqueue +crunch tcbReleaseRemove, tcbReleaseEnqueue for valid_machine_state'[wp]: valid_machine_state' (wp: crunch_wps) @@ -6087,19 +6087,19 @@ lemma setReleaseQueue_pred_tcb_at'[wp]: global_interpretation tcbReleaseRemove: typ_at_all_props' "tcbReleaseRemove tptr" by typ_at_props' -crunch tcbReleaseDequeue, tcbQueueRemove, tcbReleaseEnqueue +crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue for valid_irq_handlers'[wp]: valid_irq_handlers' (wp: valid_irq_handlers_lift'') -crunch tcbReleaseDequeue, tcbQueueRemove, tcbReleaseEnqueue +crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue for ct_idle_or_in_cur_domain'[wp]: ct_idle_or_in_cur_domain' (wp: crunch_wps threadSet_ct_idle_or_in_cur_domain') -crunch tcbReleaseDequeue, tcbQueueRemove, tcbReleaseEnqueue +crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue for if_unsafe_then_cap'[wp]: if_unsafe_then_cap' (wp: crunch_wps threadSet_ifunsafe'T simp: tcb_cte_cases_def cteSizeBits_def) -crunch tcbReleaseDequeue, tcbQueueRemove, tcbReleaseEnqueue +crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue for ctes_of[wp]: "\s. P (ctes_of s)" and valid_idle'[wp]: valid_idle' (simp: crunch_simps wp: crunch_wps threadSet_idle') @@ -6108,14 +6108,14 @@ crunch setReleaseQueue, tcbQueueRemove, setReprogramTimer for valid_objs'[wp]: valid_objs' (wp: crunch_wps hoare_vcg_all_lift simp: crunch_simps) -crunch tcbReleaseDequeue +crunch tcbReleaseRemove for valid_objs'[wp]: valid_objs' -crunch tcbReleaseDequeue, tcbQueueRemove, tcbReleaseEnqueue +crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue for pred_tcb_at'[wp]: "\s. P' (pred_tcb_at' P obj t s)" (wp: crunch_wps threadSet_pred_tcb_no_state simp: tcb_to_itcb'_def) -crunch tcbReleaseDequeue, tcbQueueRemove, tcbReleaseEnqueue +crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue for tcbDomain[wp]: "obj_at' (\tcb. P (tcbDomain tcb)) t" and tcb_in_cur_domain'[wp]: "tcb_in_cur_domain' t" and sch_act_wf[wp]: "\s. sch_act_wf (ksSchedulerAction s) s" @@ -6478,7 +6478,7 @@ lemma tcbReleaseRemove_sym_heap_sched_pointers[wp]: apply (fastforce simp: ksReleaseQueue_asrt_def opt_pred_def obj_at'_def opt_map_red) done -crunch tcbReleaseDequeue +crunch tcbReleaseRemove for sym_heap_sched_pointers[wp]: sym_heap_sched_pointers crunch setReprogramTimer @@ -6574,11 +6574,6 @@ lemma tcbReleaseRemove_invs': simp: cteCaps_of_def o_def) done -lemma tcbReleaseDequeue_invs'[wp]: - "tcbReleaseDequeue \invs'\" - unfolding tcbReleaseDequeue_def - by (wpsimp wp: tcbReleaseRemove_invs') - crunch setReleaseQueue, setReprogramTimer for valid_bitmapQ[wp]: valid_bitmapQ and bitmapQ_no_L2_orphans[wp]: bitmapQ_no_L2_orphans diff --git a/spec/abstract/Schedule_A.thy b/spec/abstract/Schedule_A.thy index f8237edfcf..6e1c3d50a6 100644 --- a/spec/abstract/Schedule_A.thy +++ b/spec/abstract/Schedule_A.thy @@ -146,24 +146,17 @@ where else read_tcb_refill_ready (hd rq) }" -definition tcb_release_dequeue :: "(obj_ref, 'z::state_ext) s_monad" -where - "tcb_release_dequeue = do +definition tcb_release_dequeue :: "(unit, 'z::state_ext) s_monad" where + "tcb_release_dequeue \ do rq \ gets release_queue; + assert (rq \ []); tcb_release_remove (hd rq); - return (hd rq) + possible_switch_to (hd rq) od" -definition awaken_body :: "(unit, 'z::state_ext) s_monad" -where - "awaken_body = do - awakened \ tcb_release_dequeue; - possible_switch_to awakened - od" - -definition awaken :: "(unit, 'z::state_ext) s_monad" -where - "awaken \ whileLoop (\r s. the (read_release_q_non_empty_and_ready s)) (\_. awaken_body) ()" +definition awaken :: "(unit, 'z::state_ext) s_monad" where + "awaken \ whileLoop (\r s. the (read_release_q_non_empty_and_ready s)) + (\_. tcb_release_dequeue) ()" definition max_non_empty_queue :: "(priority \ ready_queue) \ ready_queue" where "max_non_empty_queue queues \ queues (Max {prio. queues prio \ []})" diff --git a/spec/design/skel/KernelStateData_H.thy b/spec/design/skel/KernelStateData_H.thy index b67579130b..40179a2dce 100644 --- a/spec/design/skel/KernelStateData_H.thy +++ b/spec/design/skel/KernelStateData_H.thy @@ -100,7 +100,7 @@ where return r od" -#INCLUDE_HASKELL SEL4/Model/StateData.lhs decls_only ONLY capHasProperty sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tc_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt -#INCLUDE_HASKELL SEL4/Model/StateData.lhs NOT doMachineOp KernelState ReadyQueue ReleaseQueue ReaderM Kernel KernelR getsJust assert stateAssert funOfM condition whileLoop findM funArray newKernelState capHasProperty ifM whenM whileM andM orM sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tc_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt +#INCLUDE_HASKELL SEL4/Model/StateData.lhs decls_only ONLY capHasProperty sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt +#INCLUDE_HASKELL SEL4/Model/StateData.lhs NOT doMachineOp KernelState ReadyQueue ReleaseQueue ReaderM Kernel KernelR getsJust assert stateAssert funOfM condition whileLoop findM funArray newKernelState capHasProperty ifM whenM whileM andM orM sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt end diff --git a/spec/haskell/src/SEL4/Model/StateData.lhs b/spec/haskell/src/SEL4/Model/StateData.lhs index 589bcd7972..adc2e392c5 100644 --- a/spec/haskell/src/SEL4/Model/StateData.lhs +++ b/spec/haskell/src/SEL4/Model/StateData.lhs @@ -494,8 +494,14 @@ An assert that will say that the tcbInReleaseQueue flag is not set. An assert that will say that every thread in the release queue is associated with an active scheduling context. -> tcbInReleaseQueue_imp_active_sc_tc_at'_asrt :: KernelState -> Bool -> tcbInReleaseQueue_imp_active_sc_tc_at'_asrt _ = True +> tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt :: KernelState -> Bool +> tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt _ = True + +An assert that will say that if the release queue is not empty, then the head +of the release queue is associated with an active scheduling context. + +> tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt :: KernelState -> Bool +> tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt _ = True An assert that will say that the tcbQueued flag of the thread is not set. diff --git a/spec/haskell/src/SEL4/Object/SchedContext.lhs b/spec/haskell/src/SEL4/Object/SchedContext.lhs index d36482fe7e..ea3711294f 100644 --- a/spec/haskell/src/SEL4/Object/SchedContext.lhs +++ b/spec/haskell/src/SEL4/Object/SchedContext.lhs @@ -24,7 +24,7 @@ This module uses the C preprocessor to select a target architecture. > refillCapacity, readRefillCapacity, getRefillCapacity, refillBudgetCheck, > refillBudgetCheckRoundRobin, updateSchedContext, emptyRefill, > isCurDomainExpired, refillUnblockCheck,ifCondRefillUnblockCheck, -> readRefillReady, refillReady, tcbReleaseEnqueue, tcbQueueRemove, tcbReleaseDequeue, +> readRefillReady, refillReady, tcbReleaseEnqueue, tcbQueueRemove, > refillSufficient, readRefillSufficient, getRefillSufficient, postpone, > schedContextDonate, maybeDonateSc, maybeReturnSc, schedContextUnbindNtfn, > schedContextMaybeUnbindNtfn, isRoundRobin, getRefills, setRefills, getRefillFull, @@ -32,7 +32,7 @@ This module uses the C preprocessor to select a target architecture. > schedContextUnbindReply, schedContextSetInactive, unbindFromSC, > schedContextCancelYieldTo, refillAbsoluteMax, schedContextUpdateConsumed, > scReleased, setConsumed, refillResetRR, preemptionPoint, refillHdInsufficient, -> nonOverlappingMergeRefills, headInsufficientLoop, maxReleaseTime, scActive +> nonOverlappingMergeRefills, headInsufficientLoop, maxReleaseTime, readScActive, scActive > ) where \begin{impdetails} @@ -803,8 +803,8 @@ This module uses the C preprocessor to select a target architecture. > findTimeAfter :: Maybe (PPtr TCB) -> Time -> Kernel (Maybe (PPtr TCB)) > findTimeAfter tcbPtrOpt newTime = do -> stateAssert tcbInReleaseQueue_imp_active_sc_tc_at'_asrt -> "Every thread in the release queue is associated with an active scheduling context" +> stateAssert tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt +> "every thread in the release queue is associated with an active scheduling context" > whileLoop (\afterPtrOpt -> fromJust . runReaderT (timeAfter afterPtrOpt newTime)) > (\afterPtrOpt -> do > tcb <- getObject (fromJust afterPtrOpt) @@ -848,13 +848,6 @@ This module uses the C preprocessor to select a target architecture. > tcbQueueInsert tcbPtr afterPtr) > threadSet (\t -> t { tcbInReleaseQueue = True }) tcbPtr -> tcbReleaseDequeue :: Kernel (PPtr TCB) -> tcbReleaseDequeue = do -> queue <- getReleaseQueue -> tcbPtr <- return $ fromJust $ tcbQueueHead queue -> tcbReleaseRemove tcbPtr -> return tcbPtr - In preemptible code, the kernel may explicitly mark a preemption point with the "preemptionPoint" function. The preemption will only be taken if an interrupt has occurred and the preemption point has been called "workUnitsLimit" times. > workUnitsLimit = error "see Kernel_Config" diff --git a/spec/haskell/src/SEL4/Object/TCB.lhs b/spec/haskell/src/SEL4/Object/TCB.lhs index 7e30165bed..8a357d8385 100644 --- a/spec/haskell/src/SEL4/Object/TCB.lhs +++ b/spec/haskell/src/SEL4/Object/TCB.lhs @@ -1077,27 +1077,41 @@ On some architectures, the thread context may include registers that may be modi > commitTime > setCurSc ctScPtr -> readTCBRefillReady :: PPtr TCB -> KernelR Bool -> readTCBRefillReady tcbPtr = do -> scOpt <- threadRead tcbSchedContext tcbPtr -> readRefillReady $ fromJust scOpt - > releaseQNonEmptyAndReady :: KernelR Bool > releaseQNonEmptyAndReady = do > rq <- readReleaseQueue > if (tcbQueueHead rq == Nothing) > then return False -> else readTCBRefillReady (fromJust $ tcbQueueHead rq) - -> awakenBody :: Kernel () -> awakenBody = do -> awakened <- tcbReleaseDequeue +> else do +> let head = fromJust (tcbQueueHead rq) +> scOpt <- threadRead tcbSchedContext head +> assert (scOpt /= Nothing) "the head of the release queue must have an associated scheduling context" +> let scPtr = fromJust scOpt +> active <- readScActive scPtr +> assert active "the scheduling context associated with the head of the release queue must be active" +> readRefillReady scPtr + +> tcbReleaseDequeue :: Kernel () +> tcbReleaseDequeue = do +> stateAssert ksReleaseQueue_asrt "" +> stateAssert tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt +> "every thread in the release queue is associated with an active scheduling context" +> queue <- getReleaseQueue +> awakened <- return $ fromJust $ tcbQueueHead queue > runnable <- isRunnable awakened > assert runnable "the awakened thread must be runnable" +> tcbReleaseRemove awakened > possibleSwitchTo awakened +> stateAssert ksReleaseQueue_asrt "" +> stateAssert tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt +> "if the release queue is not empty, then the head of the release queue is associated with an active scheduling context" > awaken :: Kernel () -> awaken = whileLoop (const (fromJust . runReaderT releaseQNonEmptyAndReady)) (const awakenBody) () +> awaken = do +> stateAssert ksReleaseQueue_asrt "" +> stateAssert tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt +> "every thread in the release queue is associated with an active scheduling context" +> whileLoop (const (fromJust . runReaderT releaseQNonEmptyAndReady)) (const tcbReleaseDequeue) () > tcbEPFindIndex :: PPtr TCB -> [PPtr TCB] -> Int -> Kernel Int > tcbEPFindIndex tptr queue curIndex = do