From bb4cfd6cf036813a043d7de97f62e51f92588761 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 17 Jul 2024 01:43:17 +0930 Subject: [PATCH 1/3] rt haskell+riscv refine: use updateSchedContext more in the Haskell This rewrites the definitions of schedContextUnbindNtfn and schedContextUnbindTCB to use updateSchedContext, in preference to setSchedContext. Signed-off-by: Michael McInerney --- proof/refine/RISCV64/CNodeInv_R.thy | 10 +- proof/refine/RISCV64/Finalise_R.thy | 188 ++++++++++-------- proof/refine/RISCV64/SchedContextInv_R.thy | 2 - proof/refine/RISCV64/Syscall_R.thy | 5 - spec/haskell/src/SEL4/Object/SchedContext.lhs | 4 +- 5 files changed, 104 insertions(+), 105 deletions(-) diff --git a/proof/refine/RISCV64/CNodeInv_R.thy b/proof/refine/RISCV64/CNodeInv_R.thy index 5897e6c460..32bef0ecba 100644 --- a/proof/refine/RISCV64/CNodeInv_R.thy +++ b/proof/refine/RISCV64/CNodeInv_R.thy @@ -588,15 +588,7 @@ lemma suspend_ctes_of_thread: apply (case_tac cte, simp) done -lemma schedContextUnbindTCB_ctes_of[wp]: - "\\s. P (ctes_of s)\ - schedContextUnbindTCB t - \\_ s. P (ctes_of s)\" - apply (wpsimp simp: schedContextUnbindTCB_def wp: threadSet_ctes_ofT) - apply (clarsimp simp: ran_def tcb_cte_cases_def cteSizeBits_def split: if_splits) - by wpsimp+ - -crunch setConsumed, schedContextCompleteYieldTo, unbindNotification, unbindFromSC +crunches setConsumed, schedContextCompleteYieldTo, unbindNotification, unbindFromSC for ctes_of[wp]: "\s. P (ctes_of s)" (simp: crunch_simps wp: crunch_wps) diff --git a/proof/refine/RISCV64/Finalise_R.thy b/proof/refine/RISCV64/Finalise_R.thy index a341e510da..ae896719bb 100644 --- a/proof/refine/RISCV64/Finalise_R.thy +++ b/proof/refine/RISCV64/Finalise_R.thy @@ -2351,7 +2351,7 @@ lemma setNotification_invs': lemma schedContextUnbindNtfn_valid_objs'[wp]: "schedContextUnbindNtfn scPtr \valid_objs'\" - unfolding schedContextUnbindNtfn_def + unfolding schedContextUnbindNtfn_def updateSchedContext_def apply (wpsimp wp: getNotification_wp hoare_vcg_all_lift hoare_vcg_imp_lift') apply normalise_obj_at' apply (rename_tac ntfnPtr ntfn sc) @@ -2365,7 +2365,7 @@ lemma schedContextUnbindNtfn_invs'[wp]: "schedContextUnbindNtfn scPtr \invs'\" unfolding invs'_def valid_pspace'_def valid_dom_schedule'_def apply wpsimp \ \this handles valid_objs' separately\ - unfolding schedContextUnbindNtfn_def + unfolding schedContextUnbindNtfn_def updateSchedContext_def apply (wpsimp wp: getNotification_wp hoare_vcg_all_lift hoare_vcg_imp_lift' typ_at_lifts valid_ntfn_lift') by (auto simp: ko_wp_at'_def obj_at'_def live_sc'_def live_ntfn'_def o_def @@ -2966,52 +2966,90 @@ crunch cancelSignal, cancelAllIPC (wp: sts_bound_tcb_at' threadSet_cteCaps_of crunch_wps getObject_inv ignore: threadSet) -lemma schedContextUnbindTCB_invs'_helper: - "\\s. invs' s \ valid_idle' s \ cur_tcb' s \ scPtr \ idle_sc_ptr - \ ko_at' sc scPtr s - \ scTCB sc = Some tcbPtr - \ bound_sc_tcb_at' ((=) (Some scPtr)) tcbPtr s\ - do threadSet (tcbSchedContext_update (\_. Nothing)) tcbPtr; - setSchedContext scPtr $ scTCB_update (\_. Nothing) sc - od - \\_. invs'\" - unfolding schedContextUnbindTCB_def invs'_def - apply (wp threadSet_not_inQ threadSet_idle' threadSet_iflive' threadSet_ifunsafe'T - threadSet_valid_pspace'T threadSet_sch_actT_P[where P=False, simplified] - threadSet_ctes_ofT threadSet_ct_idle_or_in_cur_domain' threadSet_cur - threadSet_global_refsT irqs_masked_lift untyped_ranges_zero_lift - valid_irq_node_lift valid_irq_handlers_lift'' - sym_heap_sched_pointers_lift threadSet_tcbSchedNexts_of threadSet_tcbSchedPrevs_of - threadSet_tcbInReleaseQueue threadSet_tcbQueued valid_bitmaps_lift - threadSet_valid_sched_pointers - | (rule hoare_vcg_conj_lift, rule threadSet_wp) - | clarsimp simp: tcb_cte_cases_def cteSizeBits_def cteCaps_of_def valid_dom_schedule'_def)+ - apply (frule ko_at_valid_objs'_pre[where p=scPtr], clarsimp) - (* slow 60s *) - by (auto elim!: ex_cap_to'_after_update[OF if_live_state_refsE[where p=scPtr]] - elim: valid_objs_sizeE'[OF valid_objs'_valid_objs_size'] ps_clear_domE - split: option.splits - simp: pred_tcb_at'_def ko_wp_at'_def obj_at'_def objBits_def objBitsKO_def refillSize_def - tcb_cte_cases_def cteSizeBits_def valid_sched_context'_def valid_sched_context_size'_def - valid_bound_obj'_def valid_obj'_def valid_obj_size'_def valid_idle'_def - valid_pspace'_def untyped_ranges_zero_inv_def - idle_tcb'_def state_refs_of'_def comp_def valid_idle'_asrt_def) +lemma scTCB_update_Nothing_valid_objs': + "\valid_objs' and sc_at' scPtr\ + updateSchedContext scPtr (scTCB_update (\_. Nothing)) + \\_. valid_objs'\" + apply wpsimp + by (clarsimp simp: valid_obj'_def opt_pred_def opt_map_def obj_at'_def valid_sched_context'_def + refillSize_def objBits_simps valid_sched_context_size'_def) + +lemma schedContextUnbindTCB_valid_objs'[wp]: + "\valid_objs' and pspace_aligned' and pspace_distinct'\ + schedContextUnbindTCB scPtr + \\_. valid_objs'\" + unfolding schedContextUnbindTCB_def + by (wpsimp wp: scTCB_update_Nothing_valid_objs') + +lemma schedContextUnbindTCB_valid_mdb'[wp]: + "schedContextUnbindTCB scPtr \valid_mdb'\" + unfolding schedContextUnbindTCB_def + by (wpsimp wp: valid_mdb'_lift threadSet_ctes_of) + +lemma tcbSchedContext_update_update_tcb_cte_cases: + "(a, b) \ ran tcb_cte_cases \ a (tcbSchedContext_update f tcb) = a tcb" + unfolding tcb_cte_cases_def + by (case_tac tcb; fastforce simp: objBits_simps') + +crunches schedContextUnbindTCB + for ex_nonz_cap_to'[wp]: "ex_nonz_cap_to' ptr" + and if_unsafe_then_cap'[wp]: if_unsafe_then_cap' + (wp: threadSet_ifunsafe'T threadSet_cap_to simp: tcbSchedContext_update_update_tcb_cte_cases) + +lemma scTCB_update_Nothing_if_live_then_nonz_cap'[wp]: + "updateSchedContext scPtr (scTCB_update (\_. Nothing)) \if_live_then_nonz_cap'\" + unfolding updateSchedContext_def + apply (wpsimp wp: setSchedContext_iflive') + by (fastforce elim: if_live_then_nonz_capE' simp: live_sc'_def ko_wp_at'_def obj_at'_def) + +lemma tcbSchedContext_update_Nothing_if_live_then_nonz_cap'[wp]: + "threadSet (tcbSchedContext_update (\_. Nothing)) tptr \if_live_then_nonz_cap'\" + apply (wpsimp wp: threadSet_iflive') + by (fastforce simp: live_sc'_def ko_wp_at'_def obj_at'_def) + +lemma schedContextUnbindTCB_if_live_then_nonz_cap'[wp]: + "\if_live_then_nonz_cap' and pspace_aligned' and pspace_distinct' and valid_objs' + and sym_heap_sched_pointers and valid_sched_pointers\ + schedContextUnbindTCB scPtr + \\_. if_live_then_nonz_cap'\" + unfolding schedContextUnbindTCB_def + by wpsimp + +crunches schedContextUnbindTCB + for valid_bitmaps[wp]: valid_bitmaps + and valid_replies'[wp]: valid_replies' + and pspace_in_kernel_mappings'[wp]: pspace_in_kernel_mappings' + and no_0_obj'[wp]: no_0_obj' + and replies_of'[wp]: "\s. P (replies_of' s)" + and valid_global_refs'[wp]: valid_global_refs' + and valid_arch_state'[wp]: valid_arch_state' + and ctes_of[wp]: "\s. P (ctes_of s)" + and ksInterruptState[wp]: "\s. P (ksInterruptState s)" + and valid_irq_states'[wp]: "valid_irq_states'" + and valid_machine_state'[wp]: valid_machine_state' + and irqs_masked'[wp]: irqs_masked' + and pspace_domain_valid[wp]: pspace_domain_valid + and ksCurDomain[wp]: "\s. P (ksCurDomain s)" + and ksDomSchedule[wp]: "\s. P (ksDomSchedule s)" + and ksDomScheduleIdx[wp]: "\s. P (ksDomScheduleIdx s)" + (wp: crunch_wps valid_mdb'_lift getTCB_wp simp: crunch_simps o_def) + +crunches schedContextUnbindTCB + for sym_heap_sched_pointers[wp]: sym_heap_sched_pointers + and valid_sched_pointers[wp]: valid_sched_pointers + and untyped_ranges_zero'[wp]: untyped_ranges_zero' + (wp: crunch_wps threadSet_sched_pointers threadSet_valid_sched_pointers threadSet_urz + ignore: threadSet) + +lemma schedContextUnbindTCB_invs'[wp]: + "schedContextUnbindTCB scPtr \invs'\" + apply (simp add: invs'_def valid_pspace'_def valid_dom_schedule'_def) + by (wpsimp wp: valid_irq_node_lift valid_irq_handlers_lift'' simp: o_def) crunch tcbReleaseRemove, tcbSchedDequeue for cur_tcb'[wp]: cur_tcb' (wp: cur_tcb_lift) -lemma schedContextUnbindTCB_invs'[wp]: - "\\s. invs' s \ scPtr \ idle_sc_ptr\ schedContextUnbindTCB scPtr \\_. invs'\" - unfolding schedContextUnbindTCB_def - apply (rule schedContextUnbindTCB_invs'_helper[simplified] bind_wp | clarsimp)+ - apply (wpsimp wp: tcbReleaseRemove_invs' tcbSchedDequeue_invs' hoare_vcg_all_lift)+ - apply (fastforce dest: sym_refs_obj_atD' - simp: invs_valid_objs' invs'_valid_tcbs' valid_idle'_asrt_def - sym_refs_asrt_def if_cancel_eq_True ko_wp_at'_def refs_of_rev' - pred_tcb_at'_def obj_at'_def cur_tcb'_asrt_def) - done - (* FIXME RT: bound_tcb_at' is an outdated name? *) lemma threadSet_sc_bound_tcb_at'[wp]: "threadSet (tcbSchedContext_update f) t' \bound_tcb_at' P t\" @@ -3228,7 +3266,8 @@ lemma schedContextUnbindNtfn_obj_at'_ntfnSc: \\_ s. obj_at' (\ntfn. ntfnSc ntfn = None) ntfnPtr s\" apply (simp add: schedContextUnbindNtfn_def sym_refs_asrt_def) apply (wpsimp wp: stateAssert_wp set_ntfn'.obj_at'_strongest getNotification_wp - hoare_vcg_all_lift hoare_vcg_imp_lift') + hoare_vcg_all_lift hoare_vcg_imp_lift' + simp: updateSchedContext_def) apply (drule ntfnSc_sym_refsD; assumption?) apply (clarsimp simp: obj_at'_def) done @@ -3437,19 +3476,19 @@ lemma schedContextUnbindReply_obj_at'_reply_None: lemma schedContextUnbindNtfn_obj_at'_not_ntfn: "(\ko f. P (scNtfn_update f ko) = P ko) \ schedContextUnbindNtfn scPtr \obj_at' P p\" - apply (clarsimp simp: schedContextUnbindNtfn_def) + unfolding schedContextUnbindNtfn_def updateSchedContext_def apply (wpsimp wp: set_sc'.obj_at'_strongest set_ntfn'.set_wp getNotification_wp) by (auto simp: obj_at'_def) lemma schedContextUnbindNtfn_obj_at'_ntfn_None: "\\\ schedContextUnbindNtfn scPtr \\_. obj_at' (\sc. scNtfn sc = None) scPtr\" - apply (clarsimp simp: schedContextUnbindNtfn_def) + unfolding schedContextUnbindNtfn_def updateSchedContext_def apply (wpsimp wp: set_sc'.obj_at'_strongest) by (auto simp: obj_at'_def) lemma schedContextUnbindTCB_obj_at'_tcb_None: "\\\ schedContextUnbindTCB scPtr \\_. obj_at' (\sc. scTCB sc = None) scPtr\" - apply (clarsimp simp: schedContextUnbindTCB_def) + unfolding schedContextUnbindTCB_def updateSchedContext_def by (wpsimp wp: set_sc'.obj_at'_strongest) lemma schedContextUnbindAllTCBs_obj_at'_tcb_None: @@ -3467,7 +3506,7 @@ crunch schedContextMaybeUnbindNtfn and valid_tcbs'[wp]: valid_tcbs' lemma unbindFromSC_invs'[wp]: - "\invs' and tcb_at' t and K (t \ idle_thread_ptr)\ unbindFromSC t \\_. invs'\" + "unbindFromSC t \invs'\" apply (clarsimp simp: unbindFromSC_def sym_refs_asrt_def) apply (wpsimp split_del: if_split) apply (rule_tac Q'="\_. sc_at' y and invs'" in hoare_post_imp) @@ -3476,11 +3515,6 @@ lemma unbindFromSC_invs'[wp]: apply (wpsimp wp: typ_at_lifts threadGet_wp)+ apply (drule obj_at_ko_at', clarsimp) apply (frule ko_at_valid_objs'; clarsimp simp: valid_obj'_def valid_tcb'_def) - apply (frule sym_refs_tcbSchedContext; assumption?) - apply (subgoal_tac "ex_nonz_cap_to' idle_sc_ptr s") - apply (fastforce simp: invs'_def global'_sc_no_ex_cap) - apply (fastforce intro!: if_live_then_nonz_capE' - simp: obj_at'_def ko_wp_at'_def live_sc'_def) done lemma (in delete_one_conc_pre) finaliseCap_replaceable: @@ -3545,17 +3579,15 @@ lemma (in delete_one_conc_pre) finaliseCap_replaceable: not_Final_removeable finaliseCap_def, simp_all add: removeable'_def) (* ThreadCap *) - apply (frule capAligned_capUntypedPtr [OF valid_capAligned], simp) - apply (clarsimp simp: valid_cap'_def) - apply (drule valid_globals_cte_wpD'_idleThread[rotated], clarsimp) - apply (fastforce simp: invs'_def valid_pspace'_def valid_idle'_asrt_def valid_idle'_def) - (* NotificationCap *) - apply (fastforce simp: obj_at'_def sch_act_wf_asrt_def) - (* EndpointCap *) + apply (frule capAligned_capUntypedPtr [OF valid_capAligned], simp) + apply (clarsimp simp: valid_cap'_def) + apply (drule valid_globals_cte_wpD'_idleThread[rotated], clarsimp) + apply (fastforce simp: invs'_def valid_pspace'_def valid_idle'_asrt_def valid_idle'_def) + (* EndpointCap *) apply (fastforce simp: sch_act_wf_asrt_def valid_cap'_def) (* ArchObjectCap *) apply (fastforce simp: obj_at'_def sch_act_wf_asrt_def) - (* ReplyCap *) + (* ReplyCap *) apply (rule conjI; clarsimp) apply (fastforce simp: obj_at'_def sch_act_wf_asrt_def) apply (frule (1) obj_at_replyTCBs_of[OF ko_at_obj_at', simplified]) @@ -3853,32 +3885,16 @@ lemma schedContextUnbindReply_invs'[wp]: objBits_simps' refillSize_def) done -lemma schedContextUnbindAllTCBs_invs'[wp]: - "\invs' and K (scPtr \ idle_sc_ptr)\ - schedContextUnbindAllTCBs scPtr - \\rv. invs'\" - apply (clarsimp simp: schedContextUnbindAllTCBs_def) - by wpsimp +crunches schedContextUnbindAllTCBs + for invs'[wp]: invs' lemma finaliseCap_invs: "\invs' and valid_cap' cap and cte_wp_at' (\cte. cteCap cte = cap) sl\ finaliseCap cap fin flag \\_. invs'\" - apply (simp add: finaliseCap_def Let_def - cong: if_cong split del: if_split) - apply (rule hoare_pre) - apply (wpsimp wp: hoare_vcg_all_lift) - apply (case_tac cap; clarsimp simp: isCap_simps) - apply (frule invs_valid_global', drule(1) valid_globals_cte_wpD'_idleThread) - apply (frule valid_capAligned, drule capAligned_capUntypedPtr) - apply clarsimp - apply (clarsimp dest!: simp: valid_cap'_def valid_idle'_def valid_idle'_asrt_def) - apply (subgoal_tac "ex_nonz_cap_to' (ksIdleThread s) s") - apply (fastforce simp: invs'_def global'_no_ex_cap) - apply (frule invs_valid_global', drule(1) valid_globals_cte_wpD'_idleSC) - apply (frule valid_capAligned, drule capAligned_capUntypedPtr) - apply clarsimp - apply clarsimp + apply (simp add: finaliseCap_def Let_def split del: if_split) + apply (wpsimp wp: hoare_vcg_all_lift) + apply (cases cap; clarsimp simp: isCap_simps) done lemma finaliseCap_zombie_cap[wp]: @@ -4121,8 +4137,7 @@ lemma schedContextUnbindNtfn_corres: apply (rule corres_split[OF getNotification_corres]) apply (rule corres_split[OF setNotification_corres]) apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits) - apply (rule_tac f'="scNtfn_update (\_. None)" - in update_sc_no_reply_stack_update_ko_at'_corres) + apply (rule updateSchedContext_no_stack_update_corres) apply (clarsimp simp: sc_relation_def objBits_def objBitsKO_def refillSize_def)+ apply wpsimp+ apply (frule invs_valid_objs) @@ -4165,8 +4180,7 @@ lemma sched_context_maybe_unbind_ntfn_corres: apply (rule corres_split[OF getNotification_corres]) apply (rule corres_split[OF setNotification_corres]) apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits) - apply (rule_tac f'="scNtfn_update (\_. None)" - in update_sc_no_reply_stack_update_ko_at'_corres) + apply (rule updateSchedContext_no_stack_update_corres) apply (clarsimp simp: sc_relation_def objBits_def objBitsKO_def refillSize_def)+ apply wpsimp+ apply (frule invs_valid_objs) @@ -4348,7 +4362,7 @@ lemma schedContextUnbindTCB_corres: apply (clarsimp simp: sc_relation_def) apply (rule corres_split[OF set_tcb_obj_ref_corres]; clarsimp simp: tcb_relation_def inQ_def) - apply (rule_tac sc'=sc' in update_sc_no_reply_stack_update_ko_at'_corres) + apply (rule updateSchedContext_no_stack_update_corres) apply (clarsimp simp: sc_relation_def objBits_def objBitsKO_def refillSize_def)+ apply wpsimp+ apply (case_tac sc'; clarsimp) diff --git a/proof/refine/RISCV64/SchedContextInv_R.thy b/proof/refine/RISCV64/SchedContextInv_R.thy index 78865be38a..9c33d30e1e 100644 --- a/proof/refine/RISCV64/SchedContextInv_R.thy +++ b/proof/refine/RISCV64/SchedContextInv_R.thy @@ -791,8 +791,6 @@ lemma invokeSchedContext_corres: apply wpsimp+ apply (fastforce dest!: ex_nonz_cap_to_not_idle_sc_ptr) apply wpsimp - apply (frule invs_valid_global') - apply (fastforce dest!: invs_valid_pspace' global'_sc_no_ex_cap) apply (rule corres_guard_imp) apply (rule corres_rel_imp) apply (rule schedContextYieldTo_corres) diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 4e125b6dc2..5bec899e9b 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -1004,13 +1004,8 @@ lemma invokeSchedContext_invs': apply (wpsimp wp: schedContextBindTCB_invs') apply (clarsimp simp: pred_tcb_at'_def obj_at_simps) apply (wpsimp wp: schedContextBindNtfn_invs') - apply (rename_tac scPtr cap) - apply (case_tac cap; clarsimp) - apply wpsimp - using global'_sc_no_ex_cap apply fastforce apply wpsimp apply wpsimp - using global'_sc_no_ex_cap apply fastforce apply (wpsimp wp: schedContextYiedTo_invs') apply (fastforce simp: obj_at_simps) done diff --git a/spec/haskell/src/SEL4/Object/SchedContext.lhs b/spec/haskell/src/SEL4/Object/SchedContext.lhs index 776736ccc8..db938d48d3 100644 --- a/spec/haskell/src/SEL4/Object/SchedContext.lhs +++ b/spec/haskell/src/SEL4/Object/SchedContext.lhs @@ -501,7 +501,7 @@ This module uses the C preprocessor to select a target architecture. > tcbSchedDequeue tptr > tcbReleaseRemove tptr > threadSet (\tcb -> tcb { tcbSchedContext = Nothing }) tptr -> setSchedContext scPtr $ sc { scTCB = Nothing } +> updateSchedContext scPtr (\sc -> sc { scTCB = Nothing }) > schedContextUnbindNtfn :: PPtr SchedContext -> Kernel () > schedContextUnbindNtfn scPtr = do @@ -513,7 +513,7 @@ This module uses the C preprocessor to select a target architecture. > Just ntfnPtr -> do > ntfn <- getNotification ntfnPtr > setNotification ntfnPtr (ntfn { ntfnSc = Nothing }) -> setSchedContext scPtr (sc { scNtfn = Nothing }) +> updateSchedContext scPtr (\sc -> sc { scNtfn = Nothing }) > schedContextMaybeUnbindNtfn :: PPtr Notification -> Kernel () > schedContextMaybeUnbindNtfn ntfnPtr = do From 9e3c801b3d23a4e8346e88914a73e5b772a57a47 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 17 Jul 2024 01:47:45 +0930 Subject: [PATCH 2/3] rt crefine: prove several ccorres rules related to unbinding Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Finalise_C.thy | 212 +++++++++++++++++++++++++-- proof/crefine/RISCV64/Tcb_C.thy | 18 --- proof/refine/RISCV64/CNodeInv_R.thy | 2 +- proof/refine/RISCV64/Finalise_R.thy | 13 +- 4 files changed, 211 insertions(+), 34 deletions(-) diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy index 5db0345fcc..c557f61422 100644 --- a/proof/crefine/RISCV64/Finalise_C.thy +++ b/proof/crefine/RISCV64/Finalise_C.thy @@ -2740,17 +2740,213 @@ lemma prepareThreadDelete_ccorres: apply fastforce done +lemma option_to_ctcb_ptr_canonical: + "\pspace_canonical' s; tcb_at' tcb s\ + \ option_to_ctcb_ptr (Some tcb) + = tcb_Ptr (sign_extend canonical_bit (ptr_val (tcb_ptr_to_ctcb_ptr tcb)))" + apply (clarsimp simp: option_to_ctcb_ptr_def) + apply (frule (1) obj_at'_is_canonical) + by (fastforce dest: canonical_address_tcb_ptr + simp: obj_at'_def objBits_simps' projectKOs canonical_address_sign_extended + sign_extended_iff_sign_extend) + +lemma bindNTFN_alignment_junk: + "\ is_aligned tcb tcbBlockSizeBits; bits \ ctcb_size_bits \ + \ ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask bits = ptr_val (tcb_ptr_to_ctcb_ptr tcb)" + apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def projectKOs) + apply (rule is_aligned_neg_mask_eq) + apply (erule aligned_add_aligned) + apply (erule is_aligned_weaken[rotated]) + by (auto simp add: is_aligned_def objBits_defs ctcb_offset_defs) + lemma schedContext_unbindNtfn_ccorres: "ccorres dc xfdc - (invs' and sc_at' scPtr) \\sc = Ptr scPtr\ [] + (invs' and sc_at' scPtr) \\sc = Ptr scPtr\ hs (schedContextUnbindNtfn scPtr) (Call schedContext_unbindNtfn_'proc)" -sorry (* FIXME RT: schedContext_unbindNtfn_ccorres *) + supply Collect_const[simp del] + apply (cinit lift: sc_') + apply (rule ccorres_stateAssert) + apply (rule ccorres_pre_getObject_sc, rename_tac sc) + apply (rule_tac val="from_bool True" + and R="sc_at' scPtr and no_0_obj'" + and R'=UNIV + and xf'=ret__int_' + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (fastforce split: if_splits) + apply ceqv + apply ccorres_rewrite + apply (rule ccorres_move_c_guard_sc) + apply (rule_tac val="from_bool (scNtfn sc \ None)" + and R="ko_at' sc scPtr and no_0_obj' and valid_objs'" + and R'=UNIV + and xf'=ret__int_' + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (clarsimp split: if_splits) + apply (frule (1) obj_at_cslift_sc) + apply (frule (1) sc_ko_at_valid_objs_valid_sc') + apply clarsimp + apply (intro conjI impI allI) + apply (clarsimp simp: typ_heap_simps csched_context_relation_def option_to_ptr_def + option_to_0_def + split: option.splits) + apply (clarsimp simp: typ_heap_simps csched_context_relation_def option_to_ptr_def + option_to_0_def valid_sched_context'_def + split: option.splits) + apply ceqv + apply (simp add: option.case_eq_if) + apply (subst if_swap) + apply (rule ccorres_cond_both'[where Q=\ and Q'="\"]) + apply fastforce + apply (rule ccorres_pre_getNotification, rename_tac ntfn) + apply (rule_tac P="\s. invs' s \ sym_refs (state_refs_of' s) + \ ko_at' sc scPtr s \ ko_at' ntfn (the (scNtfn sc)) s" + and P'=UNIV + in ccorres_split_nothrow_novcg) + apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) + apply (rule allI, rule conseqPre, vcg) + apply clarsimp + apply (rename_tac ntfnPtr) + apply (frule cmap_relation_ntfn) + apply (frule (1) obj_at_cslift_sc) + apply (frule (1) invs'_ko_at_valid_sched_context') + apply normalise_obj_at' + apply (rename_tac sc') + apply (erule (1) cmap_relation_ko_atE) + apply (rule conjI) + apply (erule h_t_valid_clift) + apply (rule conjI) + apply (clarsimp simp: typ_heap_simps' csched_context_relation_def) + apply (clarsimp simp: setNotification_def split_def) + apply (rule bexI[OF _ setObject_eq]) + apply (simp add: rf_sr_def cstate_relation_def Let_def init_def + cpspace_relation_def update_ntfn_map_tos + csched_context_relation_def typ_heap_simps') + apply (prop_tac "scNotification_C sc' = ntfn_Ptr ntfnPtr", simp) + apply clarsimp + apply (intro conjI) + apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) + apply (clarsimp simp: cnotification_relation_def Let_def split: ntfn.splits) + apply fastforce + apply (simp add: refill_buffer_relation_def image_def dom_def Let_def typ_heap_simps + update_ntfn_map_tos) + apply (simp add: carch_state_relation_def) + apply (simp add: cmachine_state_relation_def) + apply (simp add: h_t_valid_clift_Some_iff) + apply (simp add: objBits_simps') + apply (simp add: objBits_simps) + apply assumption + apply ceqv + apply clarsimp + apply (rule ccorres_move_c_guard_sc) + apply (rule updateSchedContext_ccorres_lemma2[where P=\]) + apply vcg + apply fastforce + apply clarsimp + apply (rule_tac sc'="scNotification_C_update (\_. NULL) sc'" + in rf_sr_sc_update_no_refill_buffer_update2; + fastforce?) + apply (clarsimp simp: typ_heap_simps') + apply (clarsimp simp: csched_context_relation_def) + apply (fastforce intro: refill_buffer_relation_sc_no_refills_update) + apply clarsimp + apply (wpsimp wp: hoare_vcg_conj_lift) + apply (clarsimp simp: guard_is_UNIV_def) + apply (rule ccorres_return_Skip) + apply vcg + apply vcg + apply (fastforce simp: sym_refs_asrt_def) + done lemma schedContext_unbindTCB_ccorres: "ccorres dc xfdc - (invs' and sc_at' scPtr) (\\sc = Ptr scPtr\ \ \\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\) [] - (schedContextUnbindTCB scPtr) (Call schedContext_unbindTCB_'proc)" -sorry (* FIXME RT: schedContext_unbindTCB_ccorres *) + (invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and sc_at' scPtr) \\sc = Ptr scPtr\ hs + (schedContextUnbindTCB scPtr) (Call schedContext_unbindTCB_'proc)" + apply (cinit lift: sc_') + apply (rule ccorres_stateAssert)+ + apply (rule ccorres_pre_getObject_sc, rename_tac sc) + apply (rule ccorres_assert2) + apply (rule ccorres_pre_getCurThread) + apply (rule_tac val="tcb_ptr_to_ctcb_ptr (the (scTCB sc))" + and R="ko_at' sc scPtr and no_0_obj' and valid_objs'" + and R'=UNIV + and xf'=tcb_' + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg, clarsimp) + apply (frule (1) obj_at_cslift_sc) + apply (clarsimp simp: typ_heap_simps csched_context_relation_def option_to_ctcb_ptr_def) + apply ceqv + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply (simp add: when_def) + apply (rule_tac R="\s. cur = ksCurThread s" in ccorres_cond) + apply (fastforce dest: rf_sr_ksCurThread) + apply (ctac add: rescheduleRequired_ccorres) + apply (rule ccorres_return_Skip) + apply ceqv + apply (ctac add: tcbSchedDequeue_ccorres) + apply (ctac add: tcbReleaseRemove_ccorres) + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply (rule_tac P'="ko_at' sc scPtr and valid_objs'" + in threadSet_ccorres_lemma3[where P=\]) + apply vcg + apply clarsimp + apply (frule (1) sc_ko_at_valid_objs_valid_sc') + apply (rule conjI) + apply (clarsimp simp: typ_heap_simps valid_sched_context'_def valid_bound_obj'_def + split: option.splits) + apply (fastforce elim!: rf_sr_tcb_update_no_queue_gen2 + simp: typ_heap_simps' ctcb_relation_def tcb_cte_cases_def + cteSizeBits_def) + apply ceqv + apply (rule updateSchedContext_ccorres_lemma2[where P=\]) + apply vcg + apply fastforce + apply clarsimp + apply (rule conjI) + apply (clarsimp simp: typ_heap_simps') + apply (rule_tac sc'="scTcb_C_update (\_. NULL) sc'" + in rf_sr_sc_update_no_refill_buffer_update2; + fastforce?) + apply (clarsimp simp: typ_heap_simps') + apply (clarsimp simp: csched_context_relation_def option_to_ctcb_ptr_def) + apply (fastforce intro: refill_buffer_relation_sc_no_refills_update) + apply wpsimp + apply vcg + apply wpsimp + apply (vcg exspec=tcbReleaseRemove_modifies) + apply wpsimp + apply clarsimp + apply (vcg exspec=tcbSchedDequeue_modifies) + apply wpsimp + apply (vcg exspec=rescheduleRequired_modifies) + apply vcg + apply (fastforce dest: invs_valid_objs' sc_ko_at_valid_objs_valid_sc' + simp: valid_sched_context'_def split: option.splits if_splits) + done + +lemma schedContext_unbindAllTCBs_ccorres: + "ccorres dc xfdc + (invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and sc_at' scPtr) \\sc = Ptr scPtr\ hs + (schedContextUnbindAllTCBs scPtr) (Call schedContext_unbindAllTCBs_'proc)" + apply (cinit lift: sc_') + apply (rule ccorres_pre_getObject_sc, rename_tac sc) + apply (rule ccorres_move_c_guard_sc) + apply (clarsimp simp: when_def) + apply (rule_tac R="ko_at' sc scPtr and valid_objs' and no_0_obj'" in ccorres_cond) + apply clarsimp + apply (frule (1) obj_at_cslift_sc) + apply (frule (1) sc_ko_at_valid_objs_valid_sc') + apply normalise_obj_at' + subgoal + by (fastforce dest!: tcb_at_not_NULL + simp: typ_heap_simps valid_sched_context'_def valid_bound_obj'_def + csched_context_relation_def option_to_ctcb_ptr_def + split: option.splits) + apply (ctac add: schedContext_unbindTCB_ccorres) + apply (rule ccorres_return_Skip) + apply fastforce + done lemma schedContext_completeYieldTo_ccorres: "ccorres dc xfdc @@ -2758,12 +2954,6 @@ lemma schedContext_completeYieldTo_ccorres: (schedContextCompleteYieldTo tptr) (Call schedContext_completeYieldTo_'proc)" sorry (* FIXME RT: schedContext_completeYieldTo_ccorres *) -lemma schedContext_unbindAllTCBs_ccorres: - "ccorres dc xfdc - (invs' and sc_at' scPtr) \\sc = Ptr scPtr\ [] - (schedContextUnbindAllTCBs scPtr) (Call schedContext_unbindAllTCBs_'proc)" -sorry (* FIXME RT: schedContext_unbindAllTCBs_ccorres *) - lemma finaliseCap_ccorres: "\final. ccorres (\rv rv'. ccap_relation (fst rv) (finaliseCap_ret_C.remainder_C rv') diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy index ac68d104a2..511a284a06 100644 --- a/proof/crefine/RISCV64/Tcb_C.thy +++ b/proof/crefine/RISCV64/Tcb_C.thy @@ -3943,24 +3943,6 @@ sorry (* FIXME RT: decodeSetIPCBuffer_ccorres apply clarsimp done *) -lemma bindNTFN_alignment_junk: - "\ is_aligned tcb tcbBlockSizeBits; bits \ ctcb_size_bits \ - \ ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask bits = ptr_val (tcb_ptr_to_ctcb_ptr tcb)" - apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def projectKOs) - apply (rule is_aligned_neg_mask_eq) - apply (erule aligned_add_aligned) - apply (erule is_aligned_weaken[rotated]) - by (auto simp add: is_aligned_def objBits_defs ctcb_offset_defs) - -lemma option_to_ctcb_ptr_canonical: - "\pspace_canonical' s; tcb_at' tcb s\ \ - option_to_ctcb_ptr (Some tcb) = tcb_Ptr (sign_extend canonical_bit (ptr_val (tcb_ptr_to_ctcb_ptr tcb)))" - apply (clarsimp simp: option_to_ctcb_ptr_def) - apply (frule (1) obj_at'_is_canonical) - by (fastforce dest: canonical_address_tcb_ptr - simp: obj_at'_def objBits_simps' projectKOs canonical_address_sign_extended - sign_extended_iff_sign_extend) - lemma bindNotification_ccorres: "ccorres dc xfdc (invs' and (\s. sym_refs (state_refs_of' s)) and tcb_at' tcb) (UNIV \ {s. tcb_' s = tcb_ptr_to_ctcb_ptr tcb} diff --git a/proof/refine/RISCV64/CNodeInv_R.thy b/proof/refine/RISCV64/CNodeInv_R.thy index 32bef0ecba..df87fe3fae 100644 --- a/proof/refine/RISCV64/CNodeInv_R.thy +++ b/proof/refine/RISCV64/CNodeInv_R.thy @@ -588,7 +588,7 @@ lemma suspend_ctes_of_thread: apply (case_tac cte, simp) done -crunches setConsumed, schedContextCompleteYieldTo, unbindNotification, unbindFromSC +crunch setConsumed, schedContextCompleteYieldTo, unbindNotification, unbindFromSC for ctes_of[wp]: "\s. P (ctes_of s)" (simp: crunch_simps wp: crunch_wps) diff --git a/proof/refine/RISCV64/Finalise_R.thy b/proof/refine/RISCV64/Finalise_R.thy index ae896719bb..d5cd3a40d3 100644 --- a/proof/refine/RISCV64/Finalise_R.thy +++ b/proof/refine/RISCV64/Finalise_R.thy @@ -2991,7 +2991,7 @@ lemma tcbSchedContext_update_update_tcb_cte_cases: unfolding tcb_cte_cases_def by (case_tac tcb; fastforce simp: objBits_simps') -crunches schedContextUnbindTCB +crunch schedContextUnbindTCB for ex_nonz_cap_to'[wp]: "ex_nonz_cap_to' ptr" and if_unsafe_then_cap'[wp]: if_unsafe_then_cap' (wp: threadSet_ifunsafe'T threadSet_cap_to simp: tcbSchedContext_update_update_tcb_cte_cases) @@ -3015,7 +3015,7 @@ lemma schedContextUnbindTCB_if_live_then_nonz_cap'[wp]: unfolding schedContextUnbindTCB_def by wpsimp -crunches schedContextUnbindTCB +crunch schedContextUnbindTCB, schedContextBindTCB for valid_bitmaps[wp]: valid_bitmaps and valid_replies'[wp]: valid_replies' and pspace_in_kernel_mappings'[wp]: pspace_in_kernel_mappings' @@ -3032,9 +3032,14 @@ crunches schedContextUnbindTCB and ksCurDomain[wp]: "\s. P (ksCurDomain s)" and ksDomSchedule[wp]: "\s. P (ksDomSchedule s)" and ksDomScheduleIdx[wp]: "\s. P (ksDomScheduleIdx s)" + and pspace_aligned'[wp]: pspace_aligned' + and pspace_distinct'[wp]: pspace_distinct' + and pspace_bounded'[wp]: pspace_bounded' + and pspace_canonical'[wp]: pspace_canonical' + and typ_at'[wp]: "\s. P (typ_at' T p s)" (wp: crunch_wps valid_mdb'_lift getTCB_wp simp: crunch_simps o_def) -crunches schedContextUnbindTCB +crunch schedContextUnbindTCB for sym_heap_sched_pointers[wp]: sym_heap_sched_pointers and valid_sched_pointers[wp]: valid_sched_pointers and untyped_ranges_zero'[wp]: untyped_ranges_zero' @@ -3885,7 +3890,7 @@ lemma schedContextUnbindReply_invs'[wp]: objBits_simps' refillSize_def) done -crunches schedContextUnbindAllTCBs +crunch schedContextUnbindAllTCBs for invs'[wp]: invs' lemma finaliseCap_invs: From 027d2152e5408dfe2c8bf044283dbb54e82794e5 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 10 Sep 2024 19:51:14 +0930 Subject: [PATCH 3/3] rt spec+proof: align decodeSetSchedParams with the C The C code for decodeSetSchedParams was updated to match the API reference. This aligns the ASpec and Haskell with the latest version of the C, and updates AInvs and Refine. Signed-off-by: Michael McInerney --- proof/invariant-abstract/AInvs.thy | 10 +- .../DetSchedSchedule_AI.thy | 110 +++---- proof/invariant-abstract/IpcCancel_AI.thy | 2 +- .../invariant-abstract/RISCV64/ArchTcb_AI.thy | 3 +- proof/invariant-abstract/SchedContext_AI.thy | 17 -- proof/invariant-abstract/Tcb_AI.thy | 10 +- proof/refine/RISCV64/Tcb_R.thy | 278 +++++++++++------- spec/abstract/Decode_A.thy | 23 +- spec/abstract/SchedContext_A.thy | 8 - spec/abstract/Tcb_A.thy | 2 +- spec/haskell/src/SEL4/Object/TCB.lhs | 28 +- 11 files changed, 245 insertions(+), 246 deletions(-) diff --git a/proof/invariant-abstract/AInvs.thy b/proof/invariant-abstract/AInvs.thy index 5df6ff4184..9bbaca463d 100644 --- a/proof/invariant-abstract/AInvs.thy +++ b/proof/invariant-abstract/AInvs.thy @@ -428,7 +428,6 @@ lemma invoke_tcb_schact_is_rct_imp_cur_sc_active: apply (intro conjI impI) apply (clarsimp simp: maybe_sched_context_unbind_tcb_def) apply (wpsimp wp: thread_get_wp simp: get_tcb_obj_ref_def) - apply (clarsimp simp: maybe_sched_context_bind_tcb_def) apply (wpsimp wp: hoare_vcg_imp_lift' cur_sc_active_lift) apply wpsimp apply (rename_tac t ntfn) @@ -875,10 +874,7 @@ lemma invoke_tcb_schact_is_rct_imp_ct_not_in_release_q: apply (clarsimp split: option.splits) apply (intro conjI) apply (wpsimp wp: hoare_drop_imps) - apply (clarsimp simp: maybe_sched_context_bind_tcb_def bind_assoc) - apply (wpsimp wp: sched_context_bind_tcb_schact_is_rct_imp_ct_not_in_release_q hoare_vcg_if_lift2) - apply (wpsimp wp: hoare_drop_imps) - apply wpsimp + apply (wpsimp wp: sched_context_bind_tcb_schact_is_rct_imp_ct_not_in_release_q) apply (clarsimp simp: pred_tcb_at_def obj_at_def) done @@ -1667,7 +1663,7 @@ lemma install_tcb_frame_cap_schact_is_rct_imp_ct_activatable: apply (fastforce simp: ct_in_state_def pred_tcb_at_def obj_at_def get_tcb_def) done -crunch set_priority, maybe_sched_context_unbind_tcb, maybe_sched_context_bind_tcb +crunch set_priority, maybe_sched_context_unbind_tcb, sched_context_bind_tcb for ct_in_state[wp]: "ct_in_state P" (wp: crunch_wps) @@ -1716,7 +1712,7 @@ lemma invoke_tcb_schact_is_rct_imp_ct_activatable: apply (wpsimp wp: install_tcb_cap_schact_is_rct_imp_ct_activatable) apply (fastforce simp: ct_in_state_def pred_tcb_at_def obj_at_def) apply (rule bindE_wp_fwd_skip, solves \wpsimp wp: hoare_vcg_imp_lift'\)+ - apply (wpsimp wp: hoare_vcg_imp_lift') + apply (wpsimp wp: hoare_vcg_imp_lift' sched_context_bind_tcb_ct_in_state) apply wpsimp apply (fastforce simp: ct_in_state_def pred_tcb_at_def obj_at_def) apply wpsimp diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index 79f069d9ae..24fdd4d55f 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -7633,12 +7633,12 @@ crunch if_cond_refill_unblock_check (wp: crunch_wps) lemma sched_context_bind_tcb_valid_sched: - "\\s. valid_sched s \ simple_sched_action s \ current_time_bounded s - \ pred_map_eq None (tcb_scps_of s) tcbptr - \ not_cur_thread tcbptr s \ sc_not_in_release_q scptr s - \ sched_context_donate_ipc_queues_precond tcbptr scptr s\ + "\\s. valid_sched s \ simple_sched_action s \ bound_sc_tcb_at ((=) None) tcbptr s + \ not_cur_thread tcbptr s + \ sched_context_donate_ipc_queues_precond tcbptr scptr s \current_time_bounded s + \ sc_not_in_release_q scptr s\ sched_context_bind_tcb scptr tcbptr - \\y. valid_sched\" + \\_. 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) @@ -7675,20 +7675,10 @@ lemma sched_context_bind_tcb_valid_sched: simp: valid_sched_def) apply (subst op_equal[symmetric]) apply (wpsimp wp: ssc_bound_sc_tcb_at) - apply (clarsimp simp: valid_sched_def cong: conj_cong) - apply (fastforce simp: in_queues_2_def valid_release_q_def vs_all_heap_simps in_queue_2_def - dest!: valid_ready_qs_no_sc_not_queued) - done - -lemma maybe_sched_context_bind_tcb_valid_sched: - "\\s. valid_sched s \ simple_sched_action s \ bound_sc_tcb_at ((=) None) tcbptr s \ not_cur_thread tcbptr s - \ sched_context_donate_ipc_queues_precond tcbptr scptr s \ current_time_bounded s - \ sc_not_in_release_q scptr s\ - maybe_sched_context_bind_tcb scptr tcbptr - \\y. valid_sched\" - unfolding maybe_sched_context_bind_tcb_def - apply (wpsimp wp: sched_context_bind_tcb_valid_sched get_tcb_obj_ref_wp) - by (auto simp: obj_at_kh_kheap_simps vs_all_heap_simps split: if_splits) + apply (clarsimp simp: valid_sched_def tcb_at_kh_simps(4) cong: conj_cong) + apply (drule valid_ready_qs_no_sc_not_queued[where ref=tcbptr]) + apply (fastforce simp: pred_map_eq_def) + by (fastforce simp: in_queues_2_def valid_release_q_def vs_all_heap_simps in_queue_2_def) context DetSchedSchedule_AI_det_ext begin @@ -7892,8 +7882,8 @@ crunch cancel_all_ipc context DetSchedSchedule_AI begin crunch restart, install_tcb_frame_cap, install_tcb_cap, maybe_sched_context_unbind_tcb, - maybe_sched_context_bind_tcb, bind_notification, invoke_sched_context, - invoke_sched_control_configure_flags + sched_context_bind_tcb, bind_notification, invoke_sched_context, + invoke_sched_control_configure_flags for current_time_bounded[wp]: "current_time_bounded :: 'state_ext state \ _" (wp: crunch_wps check_cap_inv simp: crunch_simps) @@ -8095,14 +8085,14 @@ lemma tcs_valid_sched: and tcb_inv_wf (ThreadControlSched target slot fault_handler mcp priority sc) and (\s. heap_refs_inv (tcb_scps_of s) (sc_tcbs_of s)) and ct_active and ct_released and ct_not_in_release_q\ - invoke_tcb (ThreadControlSched target slot fault_handler mcp priority sc) - \\rv. valid_sched :: det_state \ _\" + invoke_tcb (ThreadControlSched target slot fault_handler mcp priority sc) + \\_ s :: det_state. valid_sched s\" supply if_split[split del] apply (simp add: split_def cong: option.case_cong) apply (wp maybeM_wp_drop_None) \ \bind/unbind sched context\ apply (clarsimp cong: conj_cong) - apply (wpsimp wp: maybe_sched_context_bind_tcb_valid_sched + apply (wpsimp wp: sched_context_bind_tcb_valid_sched maybe_sched_context_unbind_tcb_valid_sched, assumption) apply (strengthen not_cur_thread_2_simps) \ \set priority\ @@ -8120,20 +8110,22 @@ lemma tcs_valid_sched: apply (rule valid_validE_R) apply ((wpsimp wp: hoare_vcg_all_lift install_tcb_cap_ct_active hoare_vcg_imp_lift install_tcb_cap_timeout_faulted_tcb_at - split: if_split - | rule valid_validE, wps)+)[1] + split: if_split + | rule valid_validE, wps)+)[1] \ \resolve using preconditions\ apply (clarsimp, frule tcb_at_invs, frule valid_sched_active_scs_valid) apply (prop_tac "active_scs_valid s \ released_ipc_queues s", fastforce) - apply (clarsimp simp: obj_at_def is_tcb) - apply (clarsimp simp: tcb_at_kh_simps[symmetric] - pred_tcb_at_def obj_at_def sc_at_released_kh_simps released_sc_at_def - split: option.splits cong: conj_cong; - intro conjI; (erule disjE)?; - clarsimp dest!: active_scs_validE - simp: ipc_queued_thread_state_def2 sc_tcb_sc_at_def obj_at_def - dest!: sym[of _ "tcb_sched_context _"]) - by (drule_tac tp=x in sym_ref_tcb_sc[OF invs_sym_refs], fastforce+)+ + apply (clarsimp simp: obj_at_def is_tcb pred_tcb_at_def released_sc_at_def + cong: conj_cong) + apply (prop_tac "\sc_ptr. sc = Some (Some sc_ptr) \ sc_not_in_release_q sc_ptr s") + apply (clarsimp simp: sc_tcb_sc_at_def obj_at_def vs_all_heap_simps) + apply (fastforce dest!: sym_ref_tcb_sc[OF invs_sym_refs]) + by (intro conjI; + clarsimp simp: sc_tcb_sc_at_def obj_at_def pred_map_simps(1) tcb_at_kh_simps(3) tcb_scps.Some; + intro conjI impI allI; + fastforce intro!: active_scs_validE + simp: ipc_queued_thread_state_def2 vs_all_heap_simps + sc_at_released_kh_simps tcb_at_kh_simps) end @@ -17319,8 +17311,8 @@ lemma tcc_cur_sc_chargeable: apply (all \clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\) by auto -crunch maybe_sched_context_unbind_tcb, maybe_sched_context_bind_tcb, set_priority - , bind_notification +crunch maybe_sched_context_unbind_tcb, sched_context_bind_tcb, set_priority, + bind_notification for scheduler_act_sane[wp]: scheduler_act_sane (wp: crunch_wps simp: crunch_simps) @@ -20388,8 +20380,8 @@ lemma rec_del_consumed_time_bounded[wp]: done crunch restart, install_tcb_frame_cap, install_tcb_cap, maybe_sched_context_unbind_tcb, - maybe_sched_context_bind_tcb, bind_notification, invoke_sched_context, - invoke_sched_control_configure_flags + sched_context_bind_tcb, bind_notification, invoke_sched_context, + invoke_sched_control_configure_flags for consumed_time_bounded[wp]: "consumed_time_bounded :: 'state_ext state \ _" (wp: crunch_wps check_cap_inv simp: crunch_simps) @@ -21065,7 +21057,7 @@ lemma restart_ct_not_blocked[wp]: apply (wpsimp wp: hoare_vcg_imp_lift' sts_ctis_neq cancel_ipc_ct_in_state get_tcb_obj_ref_wp gts_wp maybeM_inv) done -crunch maybe_sched_context_unbind_tcb, maybe_sched_context_bind_tcb +crunch maybe_sched_context_unbind_tcb, sched_context_bind_tcb for ct_not_blocked[wp]: "ct_not_blocked :: 'state_ext state \ _" (simp: crunch_simps wp: crunch_wps set_tcb_obj_ref_ct_in_state) @@ -21632,8 +21624,8 @@ crunch handle_interrupt check_cap_inv filterM_preserved simp: crunch_simps) -crunch do_reply_transfer, restart, maybe_sched_context_unbind_tcb, maybe_sched_context_bind_tcb, - set_priority, bind_notification +crunch do_reply_transfer, restart, maybe_sched_context_unbind_tcb, sched_context_bind_tcb, + set_priority, bind_notification for vmt[wp]: "(\s. P (last_machine_time_of s) (cur_time s)) :: det_state \ _" and pnt[wp]: "(\s. P (last_machine_time_of s) (time_state_of s)) :: det_state \ _" (wp: crunch_wps simp: crunch_simps) @@ -21816,8 +21808,7 @@ lemma sched_context_bind_tcb_cur_sc_more_than_ready[wp]: \cur_sc_more_than_ready\" unfolding sched_context_bind_tcb_def by wpsimp -crunch suspend, bind_notification, maybe_sched_context_unbind_tcb, - maybe_sched_context_bind_tcb +crunch suspend, bind_notification, maybe_sched_context_unbind_tcb, sched_context_bind_tcb for cur_sc_more_than_ready[wp]: cur_sc_more_than_ready (wp: crunch_wps hoare_vcg_if_lift2 simp: crunch_simps ignore: update_sched_context) @@ -22357,17 +22348,17 @@ lemma maybe_sched_context_unbind_tcb_cur_sc_offset_sufficient[wp]: apply wpsimp done -lemma maybe_sched_context_bind_tcb_cur_sc_offset_ready[wp]: - "maybe_sched_context_bind_tcb sc_ptr tcb_ptr +lemma sched_context_bind_tcb_cur_sc_offset_ready[wp]: + "sched_context_bind_tcb sc_ptr tcb_ptr \\s. cur_sc_active s \ cur_sc_offset_ready (consumed_time s) s\" - apply (clarsimp simp: maybe_sched_context_bind_tcb_def sched_context_bind_tcb_def) + apply (clarsimp simp: sched_context_bind_tcb_def) apply wpsimp done -lemma maybe_sched_context_bind_tcb_cur_sc_offset_sufficient[wp]: - "maybe_sched_context_bind_tcb sc_ptr tcb_ptr +lemma sched_context_bind_tcb_cur_sc_offset_sufficient[wp]: + "sched_context_bind_tcb sc_ptr tcb_ptr \\s. cur_sc_active s \ cur_sc_offset_sufficient (consumed_time s) s\" - apply (clarsimp simp: maybe_sched_context_bind_tcb_def sched_context_bind_tcb_def) + apply (clarsimp simp: sched_context_bind_tcb_def) apply wpsimp done @@ -24476,8 +24467,8 @@ lemma install_tcb_cap_release_q_not_blocked_on_reply[wp]: done crunch sched_context_yield_to, sched_context_bind_tcb, - cancel_badged_sends, restart, maybe_sched_context_unbind_tcb, maybe_sched_context_bind_tcb, - sched_context_bind_tcb, bind_notification, send_signal + cancel_badged_sends, restart, maybe_sched_context_unbind_tcb, sched_context_bind_tcb, + sched_context_bind_tcb, bind_notification, send_signal for cur_sc[wp]: "\s. P (cur_sc s)" (wp: crunch_wps check_cap_inv filterM_preserved simp: crunch_simps) @@ -24610,12 +24601,6 @@ lemma invoke_tcb_cur_sc_in_release_q_imp_zero_consumed[wp]: apply (case_tac sc_ptr_opt; clarsimp) apply (wpsimp wp: hoare_drop_imps) apply (clarsimp simp: cur_sc_in_release_q_imp_zero_consumed_def) - - apply (clarsimp simp: maybe_sched_context_bind_tcb_def) - apply (rule bind_wp[OF _ gsc_sp]) - apply (rule hoare_when_cases; (solves \wpsimp\)?) - apply wpsimp - apply (fastforce simp: cur_sc_in_release_q_imp_zero_consumed_def) apply wpsimp apply (fastforce simp: pred_tcb_at_def sc_at_pred_n_def obj_at_def vs_all_heap_simps pred_neg_def is_blocked_on_reply_def @@ -25521,14 +25506,7 @@ lemma sched_context_bind_tcb_released_if_bound[wp]: split: if_splits option.splits) done -lemma maybe_sched_context_bind_tcb_released_if_bound[wp]: - "\\s. released_if_bound_sc_tcb_at t s \ tcb_ptr \ t \ active_scs_valid s\ - maybe_sched_context_bind_tcb sc_ptr tcb_ptr - \\_. released_if_bound_sc_tcb_at t\" - unfolding maybe_sched_context_bind_tcb_def - by (wpsimp wp: hoare_drop_imp hoare_vcg_if_lift2) - -crunch install_tcb_frame_cap, maybe_sched_context_bind_tcb, maybe_sched_context_unbind_tcb +crunch install_tcb_frame_cap, sched_context_bind_tcb, maybe_sched_context_unbind_tcb for cur_thread[wp]: "\s. P (cur_thread s)" (wp: check_cap_inv crunch_wps) diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index e58794000f..8b4d506008 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -1759,7 +1759,7 @@ lemma reply_unlink_tcb_bound_sc_tcb_at[wp]: by (wpsimp wp: hoare_drop_imp) crunch blocked_cancel_ipc, cancel_signal, test_reschedule - for bound_sc_tcb_at[wp]: "bound_sc_tcb_at P t" + for bound_sc_tcb_at[wp]: "\s. Q (bound_sc_tcb_at P t s)" (wp: crunch_wps) lemma sched_context_cancel_yield_to_not_live0: diff --git a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy index d62e5b3c36..4ebb54baea 100644 --- a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy @@ -404,7 +404,8 @@ lemma tcs_invs[Tcb_AI_asms]: apply (intro conjI; intro allI impI) apply (clarsimp simp: pred_tcb_at_def obj_at_def is_tcb) apply (clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ) - apply (clarsimp simp: obj_at_def is_ep sc_at_pred_n_def) + apply (fastforce dest: invs_sym_refs sym_ref_sc_tcb + simp: obj_at_def is_ep sc_at_pred_n_def pred_tcb_at_def) apply clarsimp apply (drule bound_sc_tcb_at_idle_sc_idle_thread[rotated, rotated], clarsimp, clarsimp) apply (fastforce simp: invs_def valid_state_def sc_at_pred_n_def diff --git a/proof/invariant-abstract/SchedContext_AI.thy b/proof/invariant-abstract/SchedContext_AI.thy index 159d0c9452..ff678e179a 100644 --- a/proof/invariant-abstract/SchedContext_AI.thy +++ b/proof/invariant-abstract/SchedContext_AI.thy @@ -1358,17 +1358,6 @@ lemma sched_context_bind_tcb_invs[wp]: dest!: symreftype_inverse' split: if_splits) done -lemma maybe_sched_context_bind_tcb_invs[wp]: - "\invs and (\s. tcb_at tcb s \ (bound_sc_tcb_at (\x. x \ Some sc) tcb s \ - ex_nonz_cap_to sc s \ ex_nonz_cap_to tcb s - \ sc_tcb_sc_at ((=) None) sc s \ bound_sc_tcb_at ((=) None) tcb s))\ - maybe_sched_context_bind_tcb sc tcb - \\rv. invs\" - unfolding maybe_sched_context_bind_tcb_def - apply (wpsimp simp: get_tcb_obj_ref_def wp: thread_get_wp) - apply (fastforce simp: pred_tcb_at_def obj_at_def is_tcb) - done - lemma sched_context_unbind_valid_replies[wp]: "tcb_release_remove tcb_ptr \ valid_replies_pred P \" by (wpsimp simp: tcb_release_remove_def) @@ -1734,12 +1723,6 @@ lemma maybe_sched_context_unbind_tcb_lift: unfolding maybe_sched_context_unbind_tcb_def by (wpsimp wp: A hoare_drop_imps) -lemma maybe_sched_context_bind_tcb_lift: - assumes A: "sched_context_bind_tcb sc_ptr tcb_ptr \P\" - shows "maybe_sched_context_bind_tcb sc_ptr tcb_ptr \P\" - unfolding maybe_sched_context_bind_tcb_def - by (wpsimp wp: A hoare_drop_imps) - (* sched_context_yield_to is moved to the start of SchedContextInv_AI because it needs to be after Ipc_AI *) diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy index a26c274651..d06f919731 100644 --- a/proof/invariant-abstract/Tcb_AI.thy +++ b/proof/invariant-abstract/Tcb_AI.thy @@ -1245,12 +1245,8 @@ lemma decode_set_sched_params_wf[wp]: apply (rule conjI; clarsimp) apply (clarsimp simp: obj_at_def is_tcb pred_tcb_at_def is_cap_simps sc_tcb_sc_at_def sc_at_ppred_def) - apply (rule conjI, fastforce) - apply (subgoal_tac "excaps ! Suc 0 \ set excaps") - prefer 2 - apply fastforce - apply (cases "excaps ! Suc 0") - apply (clarsimp) + apply (prop_tac "excaps ! Suc 0 \ set excaps", fastforce) + apply (cases "excaps ! Suc 0"; fastforce) done end @@ -1865,7 +1861,7 @@ lemma set_priority_bound_sc_tcb_at[wp]: by (wpsimp simp: wp: hoare_drop_imps) crunch cancel_all_ipc - for bound_sc_tcb_at[wp]: "bound_sc_tcb_at P target" + for bound_sc_tcb_at[wp]: "\s. Q (bound_sc_tcb_at P target s)" (wp: crunch_wps) lemma cap_delete_fh_lift: diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy index 9e9f282f04..ea7151f707 100644 --- a/proof/refine/RISCV64/Tcb_R.thy +++ b/proof/refine/RISCV64/Tcb_R.thy @@ -2086,13 +2086,7 @@ lemma monadic_rewrite_bind_unbind: | Some x \ sched_context_unbind_tcb x | Some (Some sc_ptr) \ when (y \ Some sc_ptr) $ sched_context_bind_tcb sc_ptr t od)" - apply (case_tac sc_opt; clarsimp) - apply (clarsimp simp: monadic_rewrite_def bind_def get_tcb_obj_ref_def thread_get_def - gets_the_def get_tcb_def gets_def get_def obj_at_def is_tcb_def) - apply (case_tac ko; clarsimp simp: return_def) - apply (case_tac a; clarsimp simp: maybeM_def maybe_sched_context_unbind_tcb_def - maybe_sched_context_bind_tcb_def monadic_rewrite_def) - done +oops defs tcs_cross_asrt1_def: "tcs_cross_asrt1 t sc_opt \ @@ -2158,22 +2152,24 @@ lemma tc_corres_sched: apply (rule_tac P=\ and P'=\ in corres_option_split; clarsimp) apply wpfix apply (rule setPriority) - apply (simp add: bind_assoc[symmetric]) apply (rule corres_split_nor) - apply (rule monadic_rewrite_corres_l[OF monadic_rewrite_bind_unbind]) - apply (rule corres_split_eqr) - apply (simp only: mapTCBPtr_threadGet get_tcb_obj_ref_def) - apply (rule threadGet_corres, clarsimp simp: tcb_relation_def) - apply (rule_tac P=\ and P'=\ in corres_option_split; clarsimp) - apply (rule corres_option_split; clarsimp?) - apply (rule_tac P=\ and P'=\ in corres_option_split; clarsimp) + apply (rule_tac P=\ and P'=\ in corres_option_split; clarsimp) + apply (rule corres_option_split) + apply clarsimp + apply (clarsimp simp: maybe_sched_context_unbind_tcb_def) + apply (rule corres_split[OF get_tcb_obj_ref_corres[where r="(=)"]]) + apply (clarsimp simp: tcb_relation_def) + apply (clarsimp simp: maybeM_def) + apply (rule corres_option_split[where P=\]; clarsimp?) apply (rule schedContextUnbindTCB_corres') - apply (rule corres_when[OF _ schedContextBindTCB_corres], fastforce) - apply (wp get_tcb_obj_ref_wp) - apply (wpsimp wp: getTCB_wp simp: mapTCBPtr_def) - apply (clarsimp simp: returnOk_def) - apply (rule_tac P=\ in hoare_TrueI) - apply (rule hoare_TrueI) + apply (wp get_tcb_obj_ref_wp) + apply (wpsimp wp: threadGet_wp) + apply (rule schedContextBindTCB_corres) + apply (rule corres_returnOk_eq_same) + apply simp + apply wpsimp + apply wpsimp + apply (wpsimp wp: getTCB_wp) apply (rule_tac Q'="\_ s. invs s \ valid_machine_time s \ valid_sched s \ simple_sched_action s \ current_time_bounded s \ tcb_at t s \ ex_nonz_cap_to t s \ @@ -2198,7 +2194,7 @@ lemma tc_corres_sched: in hoare_strengthen_post[rotated], fastforce split: option.split) apply (wpsimp wp: setP_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) apply clarsimp - apply (prop_tac "ct_active s \ ct_released s", erule conjunct1) + apply (prop_tac "einvs s \ ct_active s \ ct_released s", erule conjunct1) apply simp apply clarsimp \ \the following is unified with one of the guard schematics\ @@ -2209,7 +2205,7 @@ lemma tc_corres_sched: apply (fastforce elim: ready_qs_runnable_cross ct_active_cross split: option.splits) apply (clarsimp simp: tcs_cross_asrt2_def) apply (intro conjI) - apply (fastforce elim: ready_qs_runnable_cross) + apply (fastforce intro!: ready_qs_runnable_cross invs_psp_aligned) apply (fastforce elim: ct_active_cross) apply (prop_tac "cur_tcb s", fastforce) apply (frule cur_tcb_cross) @@ -2217,24 +2213,30 @@ lemma tc_corres_sched: apply fastforce apply fastforce apply (fastforce elim: ct_released_cross_weak[simplified]) - apply (rule_tac Q'="\_. invs" in hoare_post_add) - apply (clarsimp simp: invs_cur case_option_If2 if_fun_split - cong: conj_cong imp_cong split del: if_split) + apply ((wpsimp wp: hoare_vcg_all_lift hoare_vcg_const_imp_lift hoare_case_option_wp + | strengthen invs_psp_aligned invs_distinct invs_sym_refs)+)[1] + apply (rule_tac Q'="\_. invs and valid_sched and tcb_at t" in hoare_post_imp) + apply (clarsimp split: option.splits) + apply (frule invs_sym_refs) + apply (frule sym_ref_tcb_sc) + apply (fastforce simp: obj_at_def) + apply fastforce + apply (clarsimp simp: pred_tcb_at_def sc_at_ppred_def obj_at_def) + apply (wpsimp wp: setMCPriority_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) + apply ((wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_all_lift + | strengthen invs_psp_aligned invs_distinct invs_sym_refs)+)[1] apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_const_imp_lift) - apply (rule_tac Q'="\_. invs'" in hoare_post_add) - apply (clarsimp simp: case_option_If2 if_fun_split - cong: conj_cong imp_cong split del: if_split) - apply (rule_tac f="ksCurThread" in hoare_lift_Pf3) - apply (wpsimp wp: setMCPriority_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) - apply wpsimp + apply (wpsimp wp: setMCPriority_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) apply (rule_tac Q'="\_ s. einvs s \ valid_machine_time s \ simple_sched_action s \ tcb_at t s - \ ex_nonz_cap_to t s \ ct_active s \ ct_released s - \ ct_not_in_release_q s \ current_time_bounded s \ - (\scp. sc_opt = Some (Some scp) \ ex_nonz_cap_to scp s \ - sc_tcb_sc_at ((=) None) scp s \ - bound_sc_tcb_at ((=) None) t s)" - and E'="\_. \" in hoare_strengthen_postE[rotated], fastforce split: option.splits, simp) - apply (rule hoare_vcg_conj_elimE) + \ ex_nonz_cap_to t s \ ct_active s \ ct_released s + \ ct_not_in_release_q s \ current_time_bounded s + \ (\scp. sc_opt = Some (Some scp) + \ ex_nonz_cap_to scp s \ sc_tcb_sc_at ((=) None) scp s + \ bound_sc_tcb_at ((=) None) t s)" + and E'="\_. \" in hoare_strengthen_postE[rotated]) + apply (fastforce dest: invs_sym_refs sym_ref_tcb_sc + simp: obj_at_def pred_tcb_at_def sc_at_ppred_def + split: option.splits) apply wp apply (wp install_tcb_cap_invs install_tcb_cap_ex_nonz_cap_to install_tcb_cap_ct_active hoare_vcg_all_lift hoare_weak_lift_imp @@ -2250,9 +2252,20 @@ lemma tc_corres_sched: apply (prop_tac "(not ep_at t) s") apply (clarsimp simp: pred_neg_def obj_at_def is_tcb_def is_ep_def) apply (clarsimp split: Structures_A.kernel_object.splits) - apply (fastforce simp: tcb_cap_valid_def pred_tcb_at_def pred_neg_def - sc_at_ppred_def obj_at_def is_ep_def is_tcb_def - elim: cte_wp_at_weakenE dest: tcb_ep_slot_cte_wp_ats) + apply (clarsimp simp: pred_neg_def) + apply (intro conjI) + apply (fastforce simp: obj_at_def is_tcb_def + elim: cte_wp_at_weakenE dest: tcb_ep_slot_cte_wp_ats) + subgoal + by (fastforce simp: tcb_cap_valid_def pred_tcb_at_def pred_neg_def + sc_at_ppred_def obj_at_def is_ep_def is_tcb_def + elim: cte_wp_at_weakenE dest: tcb_ep_slot_cte_wp_ats) + subgoal + by (fastforce simp: tcb_cap_valid_def pred_tcb_at_def pred_neg_def + sc_at_ppred_def obj_at_def is_ep_def is_tcb_def + elim: cte_wp_at_weakenE dest: tcb_ep_slot_cte_wp_ats) + apply fastforce + subgoal by (fastforce simp: pred_tcb_at_def is_ep_def is_tcb_def sc_at_ppred_def obj_at_def) apply (clarsimp simp: tcs_cross_asrt1_def) apply (intro conjI impI allI; clarsimp?) apply (clarsimp simp: tcb_at_cte_at'_3) @@ -2301,37 +2314,70 @@ lemma tc_caps_invs': fastforce simp: isValidFaultHandler_def isCap_simps isValidVTableRoot_def) done -lemma schedContextBindTCB_invs': - "\\s. invs' s \ ex_nonz_cap_to' tcbPtr s \ ex_nonz_cap_to' scPtr s \ - bound_sc_tcb_at' (\sc. sc = None) tcbPtr s \ obj_at' (\sc. scTCB sc = None) scPtr s\ +lemma schedContextBindTCB_valid_objs'[wp]: + "\valid_objs' and pspace_aligned' and pspace_distinct' and pspace_bounded' and tcb_at' tcbPtr\ + schedContextBindTCB scPtr tcbPtr + \\_. valid_objs'\" + unfolding schedContextBindTCB_def + apply (wpsimp wp: isSchedulable_wp hoare_drop_imps) + apply (frule (1) sc_ko_at_valid_objs_valid_sc') + apply (clarsimp simp: valid_sched_context'_def refillSize_def valid_sched_context_size'_def + scBits_simps objBits_simps) + done + +crunch schedContextBindTCB + for sym_heap_sched_pointers[wp]: sym_heap_sched_pointers + and valid_sched_pointers[wp]: valid_sched_pointers + and untyped_ranges_zero'[wp]: untyped_ranges_zero' + (wp: crunch_wps threadSet_sched_pointers threadSet_valid_sched_pointers threadSet_urz + simp: crunch_simps + ignore: threadSet) + +lemma postpone_if_live_then_nonz_cap'[wp]: + "\if_live_then_nonz_cap' and pspace_aligned' and pspace_distinct' and pspace_bounded' + and valid_objs' and sym_heap_sched_pointers and valid_sched_pointers\ + postpone scPtr + \\_. if_live_then_nonz_cap'\" + unfolding postpone_def + by wpsimp + +lemma schedContextResume_if_live_then_nonz_cap'[wp]: + "\if_live_then_nonz_cap' and pspace_aligned' and pspace_distinct' and pspace_bounded' + and valid_objs' and sym_heap_sched_pointers and valid_sched_pointers\ + schedContextResume scPtr + \\_. if_live_then_nonz_cap'\" + unfolding schedContextResume_def + by (wpsimp wp: isSchedulable_wp) + +lemma schedContextBindTCB_if_live_then_nonz_cap'[wp]: + "\if_live_then_nonz_cap' and ex_nonz_cap_to' scPtr and ex_nonz_cap_to' tcbPtr + and sc_at' scPtr and tcb_at' tcbPtr + and pspace_aligned' and pspace_distinct' and pspace_bounded' and valid_objs' + and sym_heap_sched_pointers and valid_sched_pointers\ + schedContextBindTCB scPtr tcbPtr + \\_. if_live_then_nonz_cap'\" + unfolding schedContextBindTCB_def + apply (wpsimp wp: tcbSchedContext_update_Nothing_if_live_then_nonz_cap' + threadSet_iflive' threadSet_cap_to threadSet_sched_pointers + threadSet_valid_sched_pointers isSchedulable_wp hoare_drop_imps + simp: tcbSchedContext_update_update_tcb_cte_cases) + apply (frule (1) sc_ko_at_valid_objs_valid_sc') + apply (clarsimp simp: valid_sched_context'_def refillSize_def valid_sched_context_size'_def + scBits_simps objBits_simps) + done + +crunch schedContextBindTCB + for valid_mdb'[wp]: valid_mdb' + and if_unsafe_then_cap'[wp]: if_unsafe_then_cap' + (wp: crunch_wps valid_mdb'_lift threadSet_ifunsafe'T + simp: tcbSchedContext_update_update_tcb_cte_cases crunch_simps) + +lemma schedContextBindTCB_invs'[wp]: + "\invs' and ex_nonz_cap_to' tcbPtr and ex_nonz_cap_to' scPtr and sc_at' scPtr and tcb_at' tcbPtr\ schedContextBindTCB scPtr tcbPtr \\_. invs'\" - apply (simp add: schedContextBindTCB_def) - 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 (wp (once) hoare_drop_imps) - apply (wp hoare_vcg_imp_lift') - apply (wp hoare_drop_imps) - apply (wpsimp wp: hoare_vcg_imp_lift' simp: ifCondRefillUnblockCheck_def) - apply (rule_tac Q'="\_ s. invs' s" in hoare_strengthen_post[rotated], simp) - apply (simp add: invs'_def valid_pspace'_def valid_dom_schedule'_def) - apply (wp threadSet_valid_objs' threadSet_mdb' threadSet_iflive' - threadSet_cap_to threadSet_ifunsafe'T threadSet_ctes_ofT - untyped_ranges_zero_lift valid_irq_node_lift - valid_irq_handlers_lift'' hoare_vcg_const_imp_lift hoare_vcg_imp_lift' - threadSet_valid_replies' threadSet_valid_sched_pointers threadSet_tcbInReleaseQueue - sym_heap_sched_pointers_lift threadSet_tcbSchedNexts_of threadSet_tcbSchedPrevs_of - threadSet_tcbQueued - | clarsimp simp: tcb_cte_cases_def cteCaps_of_def cteSizeBits_def)+ - apply (clarsimp simp: invs'_def valid_pspace'_def valid_dom_schedule'_def) - by (fastforce simp: pred_tcb_at'_def obj_at'_def - objBits_def objBitsKO_def valid_tcb'_def tcb_cte_cases_def comp_def - valid_obj'_def valid_sched_context'_def valid_sched_context_size'_def - inQ_def cteCaps_of_def cteSizeBits_def refillSize_def - elim: ps_clear_domE split: if_splits) + apply (simp add: invs'_def valid_pspace'_def valid_dom_schedule'_def) + by (wpsimp wp: valid_irq_node_lift valid_irq_handlers_lift'' simp: o_def) lemma threadSetPriority_bound_sc_tcb_at' [wp]: "threadSetPriority tptr prio \\s. Q (bound_sc_tcb_at' P t s)\" @@ -2401,37 +2447,26 @@ lemma tc_sched_invs': \\_. invs'\" apply (simp add: invokeTCB_def) apply (wpsimp wp: schedContextUnbindTCB_invs' schedContextBindTCB_invs') - apply (wpsimp wp: getTCB_wp simp: mapTCBPtr_def) - apply (rule_tac Q'="\rv s. invs' s \ ex_nonz_cap_to' t s \ - (sc_opt = Some None \ - bound_sc_tcb_at' (\sc. sc \ Some idle_sc_ptr) t s) \ - (\x. sc_opt = Some (Some x) \ - ex_nonz_cap_to' x s \ obj_at' (\sc. scTCB sc = None) x s \ - bound_sc_tcb_at' (\sc. sc = None) t s \ - bound_sc_tcb_at' bound (ksCurThread s) s)" - in hoare_strengthen_post[rotated]) - apply (fastforce simp: pred_tcb_at'_def obj_at'_def projectKOs) - apply (rule hoare_lift_Pf3[where f=ksCurThread]) - apply (wpsimp wp: setP_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) + apply (rule_tac Q'="\rv s. invs' s \ ex_nonz_cap_to' t s \ tcb_at' t s \ + (\scPtr. sc_opt = Some (Some scPtr) \ + ex_nonz_cap_to' scPtr s \ sc_at' scPtr s)" + in hoare_strengthen_post[rotated]) + apply (fastforce simp: pred_tcb_at'_def obj_at'_def projectKOs) + apply (rule hoare_lift_Pf3[where f=ksCurThread]) + apply (wpsimp wp: setP_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) + apply wpsimp apply wpsimp - apply wpsimp - apply (clarsimp simp: tcs_cross_asrt2_def) - apply (wp (once) hoare_drop_imps) - apply (wpsimp wp: setMCPriority_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) - apply (wpsimp wp: installTCBCap_invs' installTCBCap_fh_ex_nonz_cap_to' - installTCBCap_fh_bound_sc_tcb_at' installTCBCap_fh_sc_tcb_sc_at' - hoare_vcg_all_lift hoare_vcg_ball_lift2 hoare_vcg_const_imp_lift) - apply (wpsimp simp: stateAssertE_def)+ - apply (clarsimp cong: conj_cong) - apply (subgoal_tac "sc_opt = Some None \ bound_sc_tcb_at' (\a. a \ Some idle_sc_ptr) t s") - apply (fastforce simp: tcs_cross_asrt1_def comp_def isValidFaultHandler_def - isCap_simps pred_tcb_at'_def obj_at'_def projectKOs) - apply (clarsimp simp: invs'_def valid_idle'_def - pred_tcb_at'_def obj_at'_def tcs_cross_asrt1_def valid_idle'_asrt_def) - apply (frule_tac p=t and ko="ko :: tcb" for ko in sym_refs_ko_atD'[rotated]) - apply (auto simp: ko_wp_at'_def obj_at'_def projectKOs valid_idle'_def tcb_bound_refs'_def - dest!: global'_no_ex_cap) - done + apply (clarsimp simp: tcs_cross_asrt2_def) + apply (wp (once) hoare_drop_imps) + apply (wpsimp wp: setMCPriority_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) + apply (wpsimp wp: installTCBCap_invs' installTCBCap_fh_ex_nonz_cap_to' + installTCBCap_fh_bound_sc_tcb_at' installTCBCap_fh_sc_tcb_sc_at' + hoare_vcg_all_lift hoare_vcg_ball_lift2 hoare_vcg_const_imp_lift) + apply (wpsimp simp: stateAssertE_def)+ + by (intro conjI impI allI; + clarsimp simp: invs'_def valid_idle'_def isCap_simps isCap_defs + pred_tcb_at'_def obj_at'_def tcs_cross_asrt1_def valid_idle'_asrt_def + o_def isValidFaultHandler_def ko_wp_at'_def tcb_bound_refs'_def) lemma setSchedulerAction_invs'[wp]: "\invs' and sch_act_wf sa\ @@ -2805,16 +2840,17 @@ lemma decodeSetSchedParams_wf: \ s \' fst x \ (\y \ zobj_refs' (fst x). ex_nonz_cap_to' y s))\ decodeSetSchedParams args (ThreadCap t) slot extras \tcb_inv_wf'\,-" + supply if_split[split del] unfolding decodeSetSchedParams_def scReleased_def refillReady_def scActive_def isBlocked_def apply (cases args; cases extras; clarsimp; (solves \wpsimp wp: checkPrio_inv\)?) apply (clarsimp split: list.splits; safe; (solves \wpsimp wp: checkPrio_inv\)?) apply (clarsimp simp: validE_R_def) apply (rule bindE_wp_fwd_skip, wpsimp wp: checkPrio_inv) apply (rule bindE_wp[OF _ checkPrio_lt_ct_weak'[unfolded validE_R_def]])+ - apply (wpsimp wp: checkPrio_lt_ct_weak gts_wp' threadGet_wp split_del: if_split) - apply (clarsimp simp: maxPriority_def numPriorities_def pred_tcb_at'_def obj_at'_def) - using max_word_max [of \UCAST(64 \ 8) x\ for x] - apply (auto simp: max_word_mask numeral_eq_Suc mask_Suc) + apply (wp gts_wp' hoare_vcg_if_lift2 threadGet_wp | wpc | simp)+ + apply (clarsimp simp: maxPriority_def numPriorities_def pred_tcb_at'_def) + using max_word_max[of \UCAST(64 \ 8) x\ for x] + apply (auto simp: max_word_mask numeral_eq_Suc mask_Suc split: if_splits) done (* FIXME RT: There's probably a way to avoid this using cap.case_eq_if and corres_if, but it @@ -2853,6 +2889,7 @@ lemma decodeSetSchedParams_corres: (invs' and (\s. s \' cap' \ (\x \ set extras'. s \' (fst x)))) (decode_set_sched_params args cap slot extras) (decodeSetSchedParams args cap' slot' extras')" + supply if_split[split del] apply (clarsimp simp: is_cap_simps) apply (simp add: decode_set_sched_params_def decodeSetSchedParams_def decode_update_sc_def check_handler_ep_def unlessE_whenE) @@ -2899,12 +2936,11 @@ lemma decodeSetSchedParams_corres: apply (fastforce simp: valid_cap_def) apply (clarsimp simp: valid_cap_simps') apply normalise_obj_at' - apply (intro exI impI conjI allI) - apply (clarsimp simp: obj_at'_def ko_wp_at'_def) - apply (rename_tac obj) - apply (case_tac obj; clarsimp) - apply (erule invs_valid_objs') - apply (clarsimp simp: obj_at'_def) + apply (frule invs_valid_objs') + apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') + apply (clarsimp simp: obj_at'_def ko_wp_at'_def split: kernel_object.splits) + apply (rename_tac obj) + apply (case_tac obj; clarsimp) done lemma checkValidIPCBuffer_corres: @@ -3482,8 +3518,26 @@ lemma decodeTCBInvocation_corres: elim!: list_all2_mono) done +lemma decodeSetSchedParams_inv: + "decodeSetSchedParams args cap slot extras \P\" + unfolding decodeSetSchedParams_def + apply (cases args; cases extras; clarsimp) + apply wpsimp + apply wpsimp + apply (clarsimp split: list.splits; safe; wpsimp) + apply (clarsimp split: list.splits) + apply (intro conjI impI allI) + apply wpsimp + apply wpsimp + apply wpsimp + apply forward_inv_step + apply (forward_inv_step wp: checkPrio_inv) + apply (forward_inv_step wp: checkPrio_inv) + apply forward_inv_step + by (wp scReleased_inv hoare_vcg_if_lift2 hoare_drop_imps checkPrio_inv | simp | wpc)+ + crunch decodeTCBInvocation - for inv[wp]: P + for inv[wp]: P (simp: crunch_simps wp: crunch_wps) lemma real_cte_at_not_tcb_at': diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy index 7e4b4c7ef8..32872ba37b 100644 --- a/spec/abstract/Decode_A.thy +++ b/spec/abstract/Decode_A.thy @@ -316,28 +316,27 @@ where (tc_new_croot space) (tc_new_vroot space) None odE" -definition - decode_update_sc :: "cap \ cslot_ptr \ cap \ (obj_ref option,'z::state_ext) se_monad" -where +definition decode_update_sc :: + "cap \ cslot_ptr \ cap \ (obj_ref option option, 'z::state_ext) se_monad" where "decode_update_sc cap slot sc_cap \ (case sc_cap of NullCap \ doE tcb_ptr \ returnOk $ obj_ref_of cap; ct_ptr \ liftE $ gets cur_thread; whenE (tcb_ptr = ct_ptr) $ throwError IllegalOperation; - returnOk None + returnOk $ Some None odE | SchedContextCap _ _ \ doE tcb_ptr \ returnOk $ obj_ref_of cap; sc_ptr \ returnOk $ obj_ref_of sc_cap; sc_ptr' \ liftE $ get_tcb_obj_ref tcb_sched_context tcb_ptr; - whenE (sc_ptr' \ None) $ throwError IllegalOperation; + whenE (sc_ptr' \ None \ sc_ptr' \ Some sc_ptr) $ throwError IllegalOperation; sc \ liftE $ get_sched_context sc_ptr; whenE (sc_tcb sc \ None) $ throwError IllegalOperation; blocked \ liftE $ is_blocked tcb_ptr; released \ liftE $ get_sc_released sc_ptr; whenE (blocked \ \released) $ throwError IllegalOperation; - returnOk $ Some sc_ptr + returnOk $ if sc_ptr' = Some sc_ptr then None else Some (Some sc_ptr) odE | _ \ throwError (InvalidCapability 2))" @@ -416,9 +415,9 @@ where returnOk (SetTLSBase (obj_ref_of cap) (ucast (args ! 0))) odE" -definition - decode_set_sched_params :: "data list \ cap \ cslot_ptr \ (cap \ cslot_ptr) list \ (tcb_invocation,'z::state_ext) se_monad" -where +definition decode_set_sched_params :: + "data list \ cap \ cslot_ptr \ (cap \ cslot_ptr) list \ (tcb_invocation,'z::state_ext) se_monad" + where "decode_set_sched_params args cap slot extra_caps \ doE whenE (length args < 2) $ throwError TruncatedMessage; whenE (length extra_caps < 3) $ throwError TruncatedMessage; @@ -432,11 +431,11 @@ where | _ \ throwError (InvalidCapability 1); check_prio (args ! 0) auth_tcb; check_prio (args ! 1) auth_tcb; - sc \ decode_update_sc cap slot sc_cap; + sc_ptr_opt_opt \ decode_update_sc cap slot sc_cap; fh \ check_handler_ep 3 fh_arg; returnOk $ ThreadControlSched (obj_ref_of cap) slot (Some fh) - (Some (new_mcp, auth_tcb)) (Some (new_prio, auth_tcb)) - (Some sc) + (Some (new_mcp, auth_tcb)) (Some (new_prio, auth_tcb)) + sc_ptr_opt_opt odE" definition diff --git a/spec/abstract/SchedContext_A.thy b/spec/abstract/SchedContext_A.thy index 2e09b413d9..cec5241bee 100644 --- a/spec/abstract/SchedContext_A.thy +++ b/spec/abstract/SchedContext_A.thy @@ -392,14 +392,6 @@ where od od" -definition - maybe_sched_context_bind_tcb :: "obj_ref \ obj_ref \ (unit, 'z::state_ext) s_monad" -where - "maybe_sched_context_bind_tcb sc_ptr tcb_ptr = do - sc' \ get_tcb_obj_ref tcb_sched_context tcb_ptr; - when (sc' \ Some sc_ptr) $ sched_context_bind_tcb sc_ptr tcb_ptr - od" - definition sched_context_set_inactive :: "obj_ref \ (unit, 'z::state_ext) s_monad" where diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy index 8842788f8e..013c0c27a6 100644 --- a/spec/abstract/Tcb_A.thy +++ b/spec/abstract/Tcb_A.thy @@ -189,7 +189,7 @@ where liftE $ maybeM (\(prio, _). set_priority target prio) priority; liftE $ maybeM (\scopt. case scopt of None \ maybe_sched_context_unbind_tcb target - | Some sc_ptr \ maybe_sched_context_bind_tcb sc_ptr target) sc; + | Some sc_ptr \ sched_context_bind_tcb sc_ptr target) sc; returnOk [] odE" diff --git a/spec/haskell/src/SEL4/Object/TCB.lhs b/spec/haskell/src/SEL4/Object/TCB.lhs index 8a357d8385..a03f5e3920 100644 --- a/spec/haskell/src/SEL4/Object/TCB.lhs +++ b/spec/haskell/src/SEL4/Object/TCB.lhs @@ -265,20 +265,20 @@ The "SetSchedParams" call sets both the priority and the MCP in a single call. > tcbPtr <- case cap of > ThreadCap { capTCBPtr = tcbPtr } -> return tcbPtr > _ -> throw $ InvalidCapability 1 -> scPtr <- case scCap of +> scPtrOptOpt <- case scCap of > SchedContextCap { capSchedContextPtr = scPtr } -> do > tcbSc <- withoutFailure $ threadGet tcbSchedContext tcbPtr -> when (tcbSc /= Nothing) $ throw IllegalOperation +> when (tcbSc /= Nothing && tcbSc /= Just scPtr) $ throw IllegalOperation > sc <- withoutFailure $ getSchedContext scPtr > when (scTCB sc /= Nothing) $ throw IllegalOperation > blocked <- withoutFailure $ isBlocked tcbPtr > released <- withoutFailure $ scReleased scPtr > when (blocked && not released) $ throw IllegalOperation -> return $ Just scPtr +> return $ if tcbSc == Just scPtr then Nothing else Just (Just scPtr) > NullCap -> do > curTcbPtr <- withoutFailure getCurThread > when (tcbPtr == curTcbPtr) $ throw IllegalOperation -> return Nothing +> return $ Just Nothing > _ -> throw $ InvalidCapability 2 > when (not $ isValidFaultHandler fhCap) $ throw $ InvalidCapability 3 > return $ ThreadControlSched { @@ -287,7 +287,7 @@ The "SetSchedParams" call sets both the priority and the MCP in a single call. > tcSchedFaultHandler = Just (fhCap, fhSlot), > tcSchedMCPriority = Just (fromIntegral newMCP, authTCB), > tcSchedPriority = Just (fromIntegral newPrio, authTCB), -> tcSchedSchedContext = Just scPtr } +> tcSchedSchedContext = scPtrOptOpt } > decodeSetSchedParams _ _ _ _ = throw TruncatedMessage \subsubsection{The Set IPC Buffer Call} @@ -505,9 +505,9 @@ The use of "checkCapAt" addresses a corner case in which the only capability to > installThreadBuffer target slot buffer > return [] -> invokeTCB (ThreadControlSched target slot faultHandler mcPriority priority sc) +> invokeTCB (ThreadControlSched target slot faultHandler mcPriority priority scPtrOptOpt) > = do -> stateAssert (tcs_cross_asrt1 target sc) +> stateAssert (tcs_cross_asrt1 target scPtrOptOpt) > "Assert some conditions that hold in the abstract at this point" > stateAssert valid_idle'_asrt > "Assert that `valid_idle' s` holds" @@ -519,14 +519,14 @@ The use of "checkCapAt" addresses a corner case in which the only capability to > "Assert some conditions that hold in the abstract at this point" > let priority' = mapMaybe fst priority > maybe (return ()) (setPriority target) priority' -> targetScOpt <- mapTCBPtr target tcbSchedContext -> case sc of +> case scPtrOptOpt of > Nothing -> return () -> Just Nothing -> case targetScOpt of -> Nothing -> return () -> Just targetSc -> schedContextUnbindTCB targetSc -> Just (Just scPtr) -> -> when (sc /= Just targetScOpt) $ schedContextBindTCB scPtr target +> Just Nothing -> do +> targetScOpt <- threadGet tcbSchedContext target +> case targetScOpt of +> Nothing -> return () +> Just targetSc -> schedContextUnbindTCB targetSc +> Just (Just scPtr) -> schedContextBindTCB scPtr target > return [] \subsubsection{Register State}