diff --git a/proof/crefine/RISCV64/IpcCancel_C.thy b/proof/crefine/RISCV64/IpcCancel_C.thy index d1c311fdf3..567f1b5588 100644 --- a/proof/crefine/RISCV64/IpcCancel_C.thy +++ b/proof/crefine/RISCV64/IpcCancel_C.thy @@ -1877,7 +1877,7 @@ lemma rescheduleRequired_ccorres: "ccorres dc xfdc ((\s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct') - UNIV [] + UNIV hs rescheduleRequired (Call rescheduleRequired_'proc)" supply if_split[split del] apply cinit diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index 1f80932177..52392b3cc6 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -5009,11 +5009,101 @@ lemma reply_push_ccorres: (replyPush callerPtr calleePtr replyPtr canDonate) (Call reply_push_'proc)" sorry (* FIXME RT: reply_push_ccorres *) +(* Note that valid_objs' can be removed from the Haskell guard by asserting valid_objs' within + schedContextDonate *) lemma schedContext_donate_ccorres: "ccorres dc xfdc - \ (\\sc = Ptr callerPtr\ \ \\to = tcb_ptr_to_ctcb_ptr tcbPtr\) [] + (sc_at' scPtr and tcb_at' tcbPtr and valid_objs' and no_0_obj' + and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct') + (\\sc = Ptr scPtr\ \ \\to = tcb_ptr_to_ctcb_ptr tcbPtr\) [] (schedContextDonate scPtr tcbPtr) (Call schedContext_donate_'proc)" -sorry (* FIXME RT: schedContext_donate_ccorres *) + (is "ccorres _ _ ?abs _ _ _ _") + apply (cinit lift: sc_' to_') + apply (rule ccorres_pre_getObject_sc, rename_tac sc) + apply (rule ccorres_move_c_guard_sc) + apply (rule_tac xf'=from_' + and val="option_to_ctcb_ptr (scTCB sc)" + and R="ko_at' sc scPtr" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply clarsimp + apply (frule (1) obj_at_cslift_sc) + apply (clarsimp simp: csched_context_relation_def typ_heap_simps) + apply ceqv + apply (clarsimp simp: when_def) + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply (rule_tac Q="no_0_obj' and ko_at' sc scPtr and valid_objs'" + and Q'="\s'. from_' s' = option_to_ctcb_ptr (scTCB sc)" + in ccorres_cond_both') + apply (fastforce dest: tcb_at_not_NULL sc_ko_at_valid_objs_valid_sc' + simp: option_to_ctcb_ptr_def valid_sched_context'_def + split: option.splits) + apply (rule ccorres_rhs_assoc)+ + apply (ctac add: tcbSchedDequeue_ccorres) + apply (ctac add: tcbReleaseRemove_ccorres) + apply (rule ccorres_move_c_guard_tcb) + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply (rule_tac R="{s'. from_' s' = option_to_ctcb_ptr (scTCB sc)}" + and P'="valid_objs' and no_0_obj' and ko_at' sc scPtr" + in threadSet_ccorres_lemma4[where P=\]) + apply vcg + subgoal + by (fastforce intro!: rf_sr_tcb_update_no_queue_gen2 + simp: typ_heap_simps' option_to_ctcb_ptr_def tcb_cte_cases_def + cteSizeBits_def ctcb_relation_def) + apply ceqv + apply (rule ccorres_pre_getCurThread) + apply (rule ccorres_pre_getSchedulerAction) + apply (rule_tac Q="\s. action = ksSchedulerAction s \ cur = ksCurThread s + \ valid_objs' s \ no_0_obj' s \ ko_at' sc scPtr s" + and Q'="\s'. from_' s' = option_to_ctcb_ptr (scTCB sc)" + in ccorres_cond_both') + apply clarsimp + apply (prop_tac "tcb_at' (the (scTCB sc)) s") + apply (fastforce dest!: sc_ko_at_valid_objs_valid_sc' + simp: valid_sched_context'_def) + subgoal + by (force dest: tcb_at_not_NULL tcb_at_1 + simp: rf_sr_def cstate_relation_def Let_def option_to_ctcb_ptr_def + cscheduler_action_relation_def + split: scheduler_action.splits) + apply (ctac add: rescheduleRequired_ccorres) + apply (rule ccorres_return_Skip) + apply (rule_tac Q'="\_. ?abs and ko_at' sc scPtr" in hoare_post_imp) + apply clarsimp + apply wpsimp + apply vcg + apply wpsimp + apply (vcg exspec=tcbReleaseRemove_modifies) + apply wpsimp + apply (vcg exspec=tcbSchedDequeue_modifies) + apply (rule ccorres_return_Skip) + apply ceqv + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply (rule updateSchedContext_ccorres_lemma2[where P=\]) + apply vcg + apply simp + apply (fastforce intro: rf_sr_sc_update_no_refill_buffer_update2 + refill_buffer_relation_sc_no_refills_update + simp: typ_heap_simps' csched_context_relation_def option_to_ctcb_ptr_def) + apply ceqv + apply (rule threadSet_ccorres_lemma2[where P=\]) + apply vcg + subgoal + by (fastforce intro!: rf_sr_tcb_update_no_queue_gen2 + simp: typ_heap_simps' tcb_cte_cases_def cteSizeBits_def ctcb_relation_def) + apply wpsimp + apply vcg + apply (wpsimp wp: hoare_drop_imps) + apply (vcg exspec=tcbSchedDequeue_modifies + exspec=tcbReleaseRemove_modifies + exspec=rescheduleRequired_modifies) + apply vcg + apply normalise_obj_at' + apply (frule (1) sc_ko_at_valid_objs_valid_sc') + apply (clarsimp simp: valid_sched_context'_def option_to_ctcb_ptr_def split: option.splits) + done lemma sendIPC_ccorres [corres]: "ccorres dc xfdc (invs' and st_tcb_at' simple' thread diff --git a/proof/crefine/RISCV64/IsolatedThreadAction.thy b/proof/crefine/RISCV64/IsolatedThreadAction.thy index bef8be547f..8e7892a042 100644 --- a/proof/crefine/RISCV64/IsolatedThreadAction.thy +++ b/proof/crefine/RISCV64/IsolatedThreadAction.thy @@ -920,7 +920,7 @@ lemma tcbReleaseRemove_tcbPriority[wp]: lemma schedContextDonate_tcbPriority[wp]: "schedContextDonate scPtr tcbPtr \obj_at' (\tcb. P (tcbPriority tcb)) t\" - apply (simp add: schedContextDonate_def) + apply (simp add: schedContextDonate_def updateSchedContext_def) by (wpsimp wp: hoare_drop_imps) lemma asUser_obj_at_unchangedT: diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index 9b321d418f..049f0e4c57 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -6178,35 +6178,6 @@ lemma bindScReply_valid_idle': unfolding bindScReply_def by (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_all_lift set_reply'.obj_at') -lemma replyPush_valid_idle': - "\valid_idle' - and valid_pspace' - and (\s. callerPtr \ ksIdleThread s) - and sym_heap_tcbSCs\ - replyPush callerPtr calleePtr replyPtr canDonate - \\_. valid_idle'\" - apply (simp only: replyPush_def) - supply if_split [split del] - apply wpsimp - apply (wpsimp wp: schedContextDonate_valid_idle' bindScReply_valid_idle')+ - apply (wpsimp wp: hoare_vcg_if_lift2 hoare_vcg_imp_lift') - apply (wpsimp wp: hoare_vcg_if_lift2 hoare_vcg_imp_lift') - apply (wpsimp wp: threadGet_wp)+ - apply (clarsimp simp: tcb_at'_ex_eq_all valid_pspace'_def) - apply (subgoal_tac "\kob. valid_reply' kob s \ valid_reply' (replyTCB_update (\_. Some callerPtr) kob) s") - apply (subgoal_tac "calleePtr \ idle_thread_ptr", simp) - apply (subgoal_tac "y \ idle_sc_ptr", simp) - apply (erule (3) not_idle_scTCB) - apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') - apply (clarsimp simp: valid_tcb'_def) - apply (frule (2) not_idle_tcbSC[where p=callerPtr]) - apply (clarsimp simp: valid_idle'_def) - apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def) - apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def) - apply (clarsimp simp: valid_idle'_def idle_tcb'_def obj_at'_real_def ko_wp_at'_def) - apply (clarsimp simp: valid_reply'_def) - done - lemma replyPush_untyped_ranges_zero'[wp]: "replyPush callerPtr calleePtr replyPtr canDonate \untyped_ranges_zero'\" apply (clarsimp simp: untyped_ranges_zero_inv_null_filter_cteCaps_of) @@ -6724,8 +6695,7 @@ lemma si_invs'_helper2: od) \\b s. invs' s \ tcb_at' d s \ ex_nonz_cap_to' d s \ st_tcb_at' (Not \ is_BlockedOnReply) d s\" - apply (wpsimp wp: ex_nonz_cap_to_pres' schedContextDonate_invs' replyPush_invs' - replyPush_valid_idle' sts_invs_minor' schedContextDonate_valid_idle' + apply (wpsimp wp: ex_nonz_cap_to_pres' schedContextDonate_invs' replyPush_invs' sts_invs_minor' replyPush_st_tcb_at'_not_caller sts_st_tcb' threadGet_wp) apply (frule_tac P'="(\st'. \rptr. st' \ BlockedOnReply rptr)" in pred_tcb'_weakenE) apply (clarsimp simp: is_BlockedOnReply_def) diff --git a/proof/refine/RISCV64/KHeap_R.thy b/proof/refine/RISCV64/KHeap_R.thy index e1efe240eb..08b9475127 100644 --- a/proof/refine/RISCV64/KHeap_R.thy +++ b/proof/refine/RISCV64/KHeap_R.thy @@ -4900,6 +4900,12 @@ lemma setSchedContext_scReplies_of: apply (erule back_subst[where P=P], rule ext) by (clarsimp simp: opt_map_def) +lemma updateSchedContext_scReplies_of: + "(\sc. scReply (f sc) = scReply sc) \ updateSchedContext scPtr f \\s. P' (scReplies_of s)\" + apply (wpsimp simp: updateSchedContext_def wp: setSchedContext_scReplies_of) + apply (auto elim!: rsubst[where P=P'] simp: opt_map_def obj_at'_def) + done + lemma getObject_tcb_wp: "\\s. tcb_at' p s \ (\t::tcb. ko_at' t p s \ Q t s)\ getObject p \Q\" by (clarsimp simp: getObject_def valid_def in_monad diff --git a/proof/refine/RISCV64/SchedContext_R.thy b/proof/refine/RISCV64/SchedContext_R.thy index 22e86bcd0e..df9fc1b4eb 100644 --- a/proof/refine/RISCV64/SchedContext_R.thy +++ b/proof/refine/RISCV64/SchedContext_R.thy @@ -584,6 +584,9 @@ crunch schedContextDonate global_interpretation schedContextDonate: typ_at_all_props' "schedContextDonate scPtr tcbPtr" by typ_at_props' +global_interpretation updateSchedContext: typ_at_all_props' "updateSchedContext scPtr f" + by typ_at_props' + crunch schedContextDonate for aligned'[wp]: "pspace_aligned'" and distinct'[wp]:"pspace_distinct'" @@ -625,6 +628,16 @@ lemma tcbSchedContext_update_None_valid_objs'[wp]: apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def cteSizeBits_def) done +lemma updateSchedContext_valid_objs'_stTCB_update_Just[wp]: + "\valid_objs' and sc_at' scPtr and tcb_at' tcbPtr\ + updateSchedContext scPtr (scTCB_update (\_. Just tcbPtr)) + \\_. valid_objs'\" + apply wpsimp + by (clarsimp simp: opt_pred_def opt_map_def valid_obj'_def + valid_sched_context'_def valid_sched_context_size'_def + objBits_def objBitsKO_def refillSize_def obj_at'_def + split: if_splits) + lemma schedContextDonate_valid_objs': "\valid_objs' and tcb_at' tcbPtr and sym_heap_sched_pointers and valid_sched_pointers @@ -632,46 +645,19 @@ lemma schedContextDonate_valid_objs': schedContextDonate scPtr tcbPtr \\_. valid_objs'\" unfolding schedContextDonate_def - apply (wpsimp wp: hoare_vcg_all_lift hoare_drop_imps) - by (fastforce dest: sc_ko_at_valid_objs_valid_sc' - simp: valid_sched_context'_def valid_sched_context_size'_def - sc_size_bounds_def objBits_def objBitsKO_def refillSize_def) + apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_disj_lift) + by fastforce lemma schedContextDonate_list_refs_of_replies' [wp]: "schedContextDonate scPtr tcbPtr \\s. P (list_refs_of_replies' s)\" - unfolding schedContextDonate_def + unfolding schedContextDonate_def updateSchedContext_def by (wpsimp simp: comp_def | rule hoare_strengthen_post[where Q'="\_ s. P (list_refs_of_replies' s)"])+ -lemma schedContextDonate_valid_idle': - "\\s. valid_idle' s \ tcbPtr \ idle_thread_ptr \ - obj_at' (\sc. scTCB sc \ Some idle_thread_ptr) scPtr s\ - schedContextDonate scPtr tcbPtr - \\_. valid_idle'\" - apply (simp only: schedContextDonate_def) - apply (wp threadSet_idle' setSchedContext_valid_idle') - apply (rule_tac Q'="\_ s. tcbPtr \ ksIdleThread s" in hoare_strengthen_post; wpsimp) - apply (rule_tac Q'="\_ s. valid_idle' s \ scPtr \ idle_sc_ptr \ tcbPtr \ ksIdleThread s" - in hoare_strengthen_post; wpsimp) - apply (wpsimp wp: threadSet_idle' hoare_drop_imps threadSet_idle') - apply (rule_tac Q'="\_ s. valid_idle' s \ scPtr \ idle_sc_ptr \ - tcbPtr \ ksIdleThread s \ from \ ksIdleThread s" - in hoare_strengthen_post) - apply wpsimp+ - apply (auto simp: obj_at'_def valid_idle'_def) - done - lemma schedContextDonate_bound_tcb_sc_at[wp]: "\\\ schedContextDonate scPtr tcbPtr \\_. obj_at' (\a. \y. scTCB a = Some y) scPtr\" - unfolding schedContextDonate_def + unfolding schedContextDonate_def updateSchedContext_def by (wpsimp wp: set_sc'.obj_at') -lemma updateSchedContext_obj_at'[wp]: - "\sc'. objBits sc' = objBits (f' sc'::sched_context) \ - updateSchedContext scp f' \\s. P (sc_at' p s)\" - apply (wpsimp simp: updateSchedContext_def wp: set_sc'.set_wp) - apply (clarsimp simp: obj_at'_def ps_clear_upd objBits_simps) - done - (* corres rules for updateRefillHd / updateRefillTl *) (* using the abstract side size *) diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index f634ef8b9c..81d9ad5583 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -106,9 +106,6 @@ global_interpretation refillNew: typ_at_all_props' "refillNew scPtr maxRefills b global_interpretation refillUpdate: typ_at_all_props' "refillUpdate scPtr newPeriod newBudget newMaxRefills" by typ_at_props' -global_interpretation updateSchedContext: typ_at_all_props' "updateSchedContext scPtr f" - by typ_at_props' - context begin interpretation Arch . (*FIXME: arch_split*) lemma findM_awesome': @@ -5255,7 +5252,7 @@ lemma schedContextDonate_if_live_then_nonz_cap': \ pspace_aligned' s \ pspace_distinct' s \ pspace_bounded' s\ schedContextDonate scPtr tcbPtr \\_. if_live_then_nonz_cap'\" - unfolding schedContextDonate_def + unfolding schedContextDonate_def updateSchedContext_def by (wpsimp wp: threadSet_iflive'T setSchedContext_iflive' hoare_vcg_all_lift threadSet_cap_to' simp: conj_ac cong: conj_cong | wp hoare_drop_imps @@ -5268,8 +5265,6 @@ crunch schedContextDonate (wp: crunch_wps threadSet_sched_pointers threadSet_valid_sched_pointers hoare_vcg_all_lift simp: crunch_simps) -(* `obj_at' (\x. scTCB x \ Some idle_thread_ptr) scPtr s` is - needed because sometimes sym_refs doesn't hold in its entirety here. *) lemma schedContextDonate_invs': "\\s. invs' s \ bound_sc_tcb_at' ((=) None) tcbPtr s \ ex_nonz_cap_to' scPtr s \ ex_nonz_cap_to' tcbPtr s\ @@ -5369,7 +5364,7 @@ lemma schedContextDonate_corres: apply (rule_tac r'=sched_act_relation in corres_split) apply (rule getSchedulerAction_corres) apply (rule corres_when) - apply (case_tac rv; clarsimp simp: sched_act_relation_def sc_relation_def) + apply (case_tac rv; fastforce simp: sched_act_relation_def sc_relation_def) apply (rule rescheduleRequired_corres_weak) apply wpsimp apply wpsimp @@ -5389,7 +5384,7 @@ lemma schedContextDonate_corres: hoare_vcg_all_lift hoare_vcg_imp_lift') apply (wpsimp wp: hoare_vcg_all_lift) apply (rule corres_split - [OF update_sc_no_reply_stack_update_ko_at'_corres + [OF updateSchedContext_no_stack_update_corres [where f'="scTCB_update (\_. Some thread)"]]) apply (clarsimp simp: sc_relation_def refillSize_def) apply clarsimp diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 1a7c2074a8..4e125b6dc2 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -2306,7 +2306,7 @@ lemma cteInsert_sane[wp]: crunch setExtraBadge, transferCaps, handleFaultReply, doIPCTransfer for sch_act_sane [wp]: sch_act_sane - (wp: crunch_wps simp: crunch_simps) + (wp: crunch_wps sch_act_sane_lift simp: crunch_simps) lemma handleHypervisorFault_corres: "corres dc (einvs and st_tcb_at active thread and ex_nonz_cap_to thread diff --git a/spec/haskell/src/SEL4/Object/SchedContext.lhs b/spec/haskell/src/SEL4/Object/SchedContext.lhs index ea3711294f..776736ccc8 100644 --- a/spec/haskell/src/SEL4/Object/SchedContext.lhs +++ b/spec/haskell/src/SEL4/Object/SchedContext.lhs @@ -664,10 +664,9 @@ This module uses the C preprocessor to select a target architecture. > threadSet (\tcb -> tcb { tcbSchedContext = Nothing }) from > cur <- getCurThread > action <- getSchedulerAction -> case action of -> SwitchToThread candidate -> when (candidate == from || from == cur) rescheduleRequired -> _ -> when (from == cur) rescheduleRequired -> setSchedContext scPtr (sc { scTCB = Just tcbPtr }) +> when (from == cur || action == SwitchToThread from) +> rescheduleRequired +> updateSchedContext scPtr (\sc -> sc { scTCB = Just tcbPtr }) > threadSet (\tcb -> tcb { tcbSchedContext = Just scPtr }) tcbPtr > invokeSchedControlConfigureFlags :: SchedControlInvocation -> Kernel ()