From da19275f4100d2d1903582911c59ab3e6ee13ecc Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 12 Jun 2024 15:09:29 +0930 Subject: [PATCH] rt spec+proof: prove preemptionPoint_ccorres This also adjusts the ASpec and Haskell definitions of preemption_point/preemptionPoint to more closely align with the C. Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/SyscallArgs_C.thy | 191 ++++++++++++++---- .../DetSchedSchedule_AI.thy | 30 +-- proof/invariant-abstract/Deterministic_AI.thy | 2 +- proof/invariant-abstract/Syscall_AI.thy | 1 + proof/refine/RISCV64/InterruptAcc_R.thy | 167 ++++++++------- proof/refine/RISCV64/Schedule_R.thy | 13 +- proof/refine/RISCV64/Untyped_R.thy | 1 + spec/abstract/KHeap_A.thy | 12 +- spec/design/skel/KernelStateData_H.thy | 4 +- spec/haskell/src/SEL4/Model/StateData.lhs | 5 + spec/haskell/src/SEL4/Object/SchedContext.lhs | 5 +- 11 files changed, 278 insertions(+), 153 deletions(-) diff --git a/proof/crefine/RISCV64/SyscallArgs_C.thy b/proof/crefine/RISCV64/SyscallArgs_C.thy index 9cd3faae86..ac0b96baea 100644 --- a/proof/crefine/RISCV64/SyscallArgs_C.thy +++ b/proof/crefine/RISCV64/SyscallArgs_C.thy @@ -473,29 +473,53 @@ lemma refill_capacity_ccorres: done lemma refill_sufficient_ccorres: - "ccorres dc xfdc - \ (\\sc = Ptr scPtr\ \ \\usage = usage\) [] + "ccorres (\rv rv'. rv = to_bool rv') ret__unsigned_long_' + (active_sc_at' scPtr and valid_objs' and no_0_obj') (\\sc = Ptr scPtr\ \ \\usage = usage\) [] (getRefillSufficient scPtr usage) (Call refill_sufficient_'proc)" -sorry (* FIXME RT: refill_sufficient_ccorres *) + apply (cinit simp: readRefillSufficient_def getRefillCapacity_def[symmetric]) + apply (ctac add: refill_capacity_ccorres) + apply csymbr + apply (fastforce intro: ccorres_return_C) + apply wpsimp + apply (vcg exspec=refill_capacity_modifies) + apply wpsimp + apply (clarsimp simp: minBudget_def split: if_splits) + done lemma isCurDomainExpired_ccorres: - "ccorres dc xfdc \ UNIV [] isCurDomainExpired (Call isCurDomainExpired_'proc)" -sorry (* FIXME RT: isCurDomainExpired_ccorres *) + "ccorres (\rv rv'. rv = to_bool rv') ret__unsigned_long_' \ UNIV [] + isCurDomainExpired (Call isCurDomainExpired_'proc)" + apply cinit + apply (rule ccorres_pre_getDomainTime) + apply (rule ccorres_return_C) + apply clarsimp + apply fastforce + apply fastforce + apply (clarsimp simp: to_bool_def numDomains_sge_1_simp split: if_splits) + done + +crunches updateTimeStamp, setWorkUnits + for obj_at'[wp]: "\s. P (obj_at' Q ptr s)" + and active_sc_at'[wp]: "active_sc_at' scPtr" + and valid_objs'[wp]: valid_objs' + and no_0_obj'[wp]: no_0_obj' + and ksCurSc[wp]: "\s. P (ksCurSc s)" + (simp: active_sc_at'_def) + +crunch (empty_fail) empty_fail[wp]: + scActive, getRefillSufficient, getConsumedTime, isCurDomainExpired, getCurSc lemma preemptionPoint_ccorres: - "ccorres (cintr \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') - invs' UNIV [] - preemptionPoint (Call preemptionPoint_'proc)" + "ccorres (cintr \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') invs' UNIV [] + preemptionPoint (Call preemptionPoint_'proc)" + supply Collect_const[simp del] apply (cinit simp: Kernel_Config.workUnitsLimit_def whenE_def) apply (rule ccorres_liftE_Seq) - apply (rule ccorres_split_nothrow - [where P=\ and P'=UNIV and r'=dc and xf'=xfdc]) + apply (rule ccorres_split_nothrow[where P=\ and P'=UNIV and r'=dc and xf'=xfdc]) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) - apply (clarsimp simp: modifyWorkUnits_def simpler_modify_def) - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - carch_state_relation_def - cmachine_state_relation_def) + apply (clarsimp simp: modifyWorkUnits_def simpler_modify_def rf_sr_def cstate_relation_def + Let_def carch_state_relation_def cmachine_state_relation_def) apply ceqv apply (rule ccorres_liftE_Seq) apply (rule ccorres_pre_getWorkUnits) @@ -503,37 +527,134 @@ lemma preemptionPoint_ccorres: apply (rule_tac R="\s. rv = ksWorkUnitsCompleted s" in ccorres_cond2) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) prefer 2 - apply simp - apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (simp add: returnOk_def return_def) apply (rule ccorres_liftE_Seq) apply (rule ccorres_rhs_assoc)+ - apply (rule ccorres_split_nothrow - [where P=\ and P'=UNIV and r'=dc and xf'=xfdc]) + apply (rule ccorres_split_nothrow[where P=\ and P'=UNIV and r'=dc and xf'=xfdc]) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) - apply (thin_tac "P" for P)+ - apply (clarsimp simp: setWorkUnits_def simpler_modify_def) - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - carch_state_relation_def - cmachine_state_relation_def) + apply (clarsimp simp: setWorkUnits_def simpler_modify_def rf_sr_def cstate_relation_def + Let_def carch_state_relation_def cmachine_state_relation_def) apply ceqv apply (rule ccorres_liftE_Seq) -sorry (* FIXME RT: preemptionPoint_corres *) (* - apply (ctac (no_vcg) add: isIRQPending_ccorres) - apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) - apply (rule allI, rule conseqPre, vcg) - apply (simp add: from_bool_0 whenE_def returnOk_def throwError_def - return_def split: option.splits) - apply (clarsimp simp: cintr_def exception_defs) - apply wp+ + apply (ctac (no_vcg) add: updateTimestamp_ccorres) + apply (rule ccorres_liftE_Seq) + apply (ctac (no_vcg) add: isIRQPending_ccorres) + apply csymbr + apply clarsimp + apply (rename_tac irq_opt) + apply (rule_tac P="irq_opt \ None" in ccorres_cases; clarsimp) + apply ccorres_rewrite + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_symb_exec_l') + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_symb_exec_l') + apply (clarsimp simp: stateAssertE_def) + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_stateAssert) + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_symb_exec_l') + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_symb_exec_l') + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond_true) + apply ccorres_rewrite + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond_true) + apply ccorres_rewrite + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (simp add: throwError_def return_def cintr_def exception_defs) + apply (clarsimp simp: andM_def ifM_def) + apply wpsimp+ + apply (rule ccorres_cond_seq) + apply ccorres_rewrite + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_rhs_assoc) + apply (ctac (no_vcg) add: isCurDomainExpired_ccorres, rename_tac domExp) + apply csymbr + apply (rule ccorres_cond_seq) + apply clarsimp + apply (rule_tac P="to_bool domExp" in ccorres_cases; clarsimp simp: to_bool_def) + apply ccorres_rewrite + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_pre_getCurSc) + apply (clarsimp simp: stateAssertE_def) + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_stateAssert) + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond_true) + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_symb_exec_l') + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_symb_exec_l') + apply ccorres_rewrite + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (simp add: throwError_def return_def cintr_def exception_defs) + apply (clarsimp simp: andM_def ifM_def) + apply wpsimp+ + apply ccorres_rewrite + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_pre_getCurSc) + apply (clarsimp simp: stateAssertE_def) + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_stateAssert) + apply (rule ccorres_liftE_Seq) + apply (rule ccorres_pre_getConsumedTime) + apply (rule ccorres_liftE_Seq) + apply ccorres_rewrite + apply (rule ccorres_rhs_assoc) + apply (rule_tac r'="\rv rv'. rv = to_bool rv'" and xf'=ret__int_' + in ccorres_split_nothrow_novcg) + apply (clarsimp simp: andM_def ifM_def bind_assoc) + apply (rule ccorres_rhs_assoc) + apply (ctac add: sc_active_ccorres) + apply csymbr + apply (rule ccorres_cond[where R=\]) + apply (fastforce simp: to_bool_def) + apply (rule ccorres_add_return2) + apply (ctac add: refill_sufficient_ccorres) + apply (rule ccorres_return[where R=\ and R'=UNIV]) + apply vcg + apply (fastforce simp: to_bool_def) + apply wpsimp + apply clarsimp + apply (vcg exspec=refill_sufficient_modifies) + apply (rule ccorres_return_Skip') + apply wpsimp + apply (clarsimp simp: to_bool_def) + apply (vcg exspec=sc_active_modifies) + apply ceqv + apply clarsimp + apply csymbr + apply clarsimp + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond[where R=\]) + apply (fastforce simp: to_bool_def) + apply ccorres_rewrite + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (simp add: throwError_def return_def cintr_def exception_defs) + apply ccorres_rewrite + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (simp add: throwError_def returnOk_def return_def cintr_def exception_defs) + apply wpsimp + apply (clarsimp simp: guard_is_UNIV_def) + apply (rule_tac Q="\_. valid_objs' and no_0_obj'" in hoare_post_imp) + apply (clarsimp simp: active_sc_at'_def obj_at'_def) + apply wpsimp + apply (wpsimp wp: hoare_drop_imps) + apply wpsimp + apply wpsimp apply vcg - apply (unfold modifyWorkUnits_def)[1] - apply wp + apply (wpsimp simp: modifyWorkUnits_def) apply vcg - apply simp - done *) + apply (fastforce simp: sc_at'_asrt_def) + done definition "invocationCatch thread isBlocking isCall canDonate inject diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index 384881c1b3..bf85f4f563 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -20335,12 +20335,6 @@ lemma reset_untyped_cap_consumed_time_bounded[wp]: apply (wpsimp wp: mapME_x_wp_inv)+ done -lemma preemption_point_current_time_bounded[wp]: - "preemption_point \current_time_bounded :: 'state_ext state \ _\" - apply (clarsimp simp: preemption_point_def) - apply (wpsimp wp: OR_choiceE_weak_wp hoare_drop_imps update_time_stamp_current_time_bounded) - done - lemma reset_untyped_cap_current_time_bounded[wp]: "reset_untyped_cap slot \current_time_bounded :: 'state_ext state \ _\" apply (clarsimp simp: reset_untyped_cap_def) @@ -21890,23 +21884,21 @@ crunches update_work_units, reset_work_units (simp: is_cur_domain_expired_def) lemma preemption_point_cur_sc_offset_sufficient[wp]: - "\\s :: det_state. (cur_sc_active s \ cur_sc_offset_sufficient (consumed_time s) s)\ + "\\s :: det_state. cur_sc_active s \ cur_sc_offset_sufficient (consumed_time s) s\ preemption_point - \\_ s. (cur_sc_active s \ cur_sc_offset_sufficient (consumed_time s) s)\, -" - apply (clarsimp simp: preemption_point_def) - apply (clarsimp simp: validE_R_def) - apply (rule bindE_wp_fwd_skip, wpsimp) - apply (clarsimp simp: validE_R_def[symmetric]) + \\_ s. cur_sc_active s \ cur_sc_offset_sufficient (consumed_time s) s\, -" + unfolding preemption_point_def + apply forward_inv_step apply (rule OR_choiceE_E_weak_wp) - apply (rule alternativeE_R_wp[where P=Q and P'=Q for Q, simplified pred_conj_def, simplified] - ; (solves wpsimp)?) - apply (clarsimp simp: validE_R_def) - apply (rule bindE_wp_fwd_skip, wpsimp) + apply (rule alternativeE_R_wp[where P=Q and P'=Q for Q, simplified pred_conj_def, simplified]; + (solves wpsimp)?) + apply forward_inv_step apply (clarsimp simp: validE_R_def) apply (rule_tac Q'="\\" in bindE_wp) - apply (rule bindE_wp_fwd_skip, wpsimp) - apply wpsimp - apply (clarsimp simp: obj_at_def vs_all_heap_simps) + apply forward_inv_step \ \step over the do_machine_op\ + apply (wpsimp wp: hoare_vcg_all_lift) + apply (fastforce dest: read_sc_refill_sufficient_SomeD read_sched_context_SomeD + simp: obj_at_def vs_all_heap_simps ) apply wpsimp done diff --git a/proof/invariant-abstract/Deterministic_AI.thy b/proof/invariant-abstract/Deterministic_AI.thy index f6ac0f4cbf..b3101a959b 100644 --- a/proof/invariant-abstract/Deterministic_AI.thy +++ b/proof/invariant-abstract/Deterministic_AI.thy @@ -3976,7 +3976,7 @@ lemma preemption_point_inv': apply (clarsimp simp: preemption_point_def) apply (wpsimp simp: reset_work_units_def update_work_units_def wp: OR_choiceE_weak_wp update_time_stamp_wp hoare_drop_imps - hoare_vcg_all_lift) + hoare_vcg_all_lift hoare_vcg_if_lift2) done locale Deterministic_AI_1 = diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index 430e79da9b..85b6d1ac8e 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -1314,6 +1314,7 @@ crunches preemption_point and cte_wp_at[wp]: "cte_wp_at P p" and cur_sc_tcb[wp]: cur_sc_tcb and invs[wp]: invs + and scheduler_action[wp]: "\s. P (scheduler_action s)" (rule: preemption_point_inv simp: cur_sc_tcb_def ignore_del: preemption_point) lemma update_time_stamp_ct_schedulable[wp]: diff --git a/proof/refine/RISCV64/InterruptAcc_R.thy b/proof/refine/RISCV64/InterruptAcc_R.thy index c5e9e36bf8..d79fa73135 100644 --- a/proof/refine/RISCV64/InterruptAcc_R.thy +++ b/proof/refine/RISCV64/InterruptAcc_R.thy @@ -18,8 +18,15 @@ lemma getIRQSlot_corres: ucast_nat_def shiftl_t2n) done +crunches modifyWorkUnits + for typ_at'[wp]: "\s. P (typ_at' T p s)" + and sc_at'_n[wp]: "\s. P (sc_at'_n n p s)" + context begin interpretation Arch . (*FIXME: arch_split*) +global_interpretation modifyWorkUnits: typ_at_all_props' "modifyWorkUnits f" + by typ_at_props' + lemma setIRQState_corres: "irq_state_relation state state' \ corres dc \ \ (set_irq_state state irq) (setIRQState state' irq)" @@ -285,24 +292,42 @@ lemma scActive_sp: apply (clarsimp simp: obj_at'_def) done +crunches updateTimeStamp, setWorkUnits, isCurDomainExpired + for ksPSpace[wp]: "\s. P (ksPSpace s)" + and active_sc_at'[wp]: "active_sc_at' scPtr" + and valid_objs'[wp]: valid_objs' + and no_0_obj'[wp]: no_0_obj' + and ksCurSc[wp]: "\s. P (ksCurSc s)" + and scs_of'[wp]: "\s. P (scs_of' s)" + (simp: active_sc_at'_def crunch_simps getDomainTime_def setDomainTime_def setConsumedTime_def + setCurTime_def) + +crunches update_time_stamp + for kheap[wp]: "\s. P (kheap s)" + (simp: crunch_simps) + +defs sc_at'_asrt_def: + "sc_at'_asrt \ \scPtr s. sc_at' scPtr s" + +crunch (no_fail) no_fail[wp]: getCurSc + lemma preemptionPoint_corres: "corres (dc \ dc) - (\s. valid_objs s \ cur_sc_tcb s \ pspace_aligned s \ pspace_distinct s - \ active_scs_valid s \ valid_machine_time s) - valid_objs' - preemption_point - preemptionPoint" + (valid_objs and cur_sc_tcb and pspace_aligned and pspace_distinct and active_scs_valid) + valid_objs' + preemption_point preemptionPoint" (is "corres _ ?abs ?conc _ _") supply if_split[split del] apply (simp add: preemption_point_def preemptionPoint_def) apply (rule corres_splitEE_skip; corresKsimp corres: update_work_units_corres - simp: update_work_units_def) - apply (clarsimp simp: bindE_def liftE_def) - apply (rule_tac Q'="\rv s. rv = ksWorkUnitsCompleted s \ ?conc s" in corres_symb_exec_r[rotated]) + simp: update_work_units_def) + apply (subst liftE_bindE[where a=getWorkUnits]) + apply (rule_tac Q'="\rv s. rv = ksWorkUnitsCompleted s \ ?conc s" + in corres_symb_exec_r[rotated]) apply (wpsimp simp: getWorkUnits_def)+ apply (rename_tac work_units) - apply (clarsimp simp: OR_choiceE_def whenE_def work_units_limit_reached_def bindE_def liftE_def) + apply (clarsimp simp: OR_choiceE_def whenE_def work_units_limit_reached_def liftE_bindE) apply (rule_tac Q="\rv s. rv = s \ ?abs s" in corres_symb_exec_l[rotated]) apply wpsimp+ apply (rename_tac ex) @@ -313,63 +338,56 @@ lemma preemptionPoint_corres: apply simp apply (rule_tac Q="\rv s. \rv'' t. rv = (rv'', s) \ rv'' = (workUnitsLimit \ work_units) \ ?abs s" in corres_symb_exec_l[rotated]) - apply (clarsimp simp: select_f_def mk_ef_def bind_def gets_def exs_valid_def get_def return_def - wrap_ext_bool_det_ext_ext_def) + apply (clarsimp simp: select_f_def mk_ef_def bind_def gets_def exs_valid_def get_def + return_def wrap_ext_bool_det_ext_ext_def) apply wpsimp - apply (clarsimp simp: select_f_def mk_ef_def bind_def gets_def get_def return_def - work_units_limit_def wrap_ext_bool_det_ext_ext_def Kernel_Config.workUnitsLimit_def) + apply (clarsimp simp: mk_ef_def bind_def gets_def get_def return_def work_units_limit_def + wrap_ext_bool_det_ext_ext_def Kernel_Config.workUnitsLimit_def) apply wpsimp - apply (clarsimp simp: select_f_def mk_ef_def bind_def gets_def exs_valid_def get_def return_def - work_units_limit_def wrap_ext_bool_det_ext_ext_def Kernel_Config.workUnitsLimit_def) + apply (clarsimp simp: mk_ef_def bind_def gets_def get_def return_def + wrap_ext_bool_det_ext_ext_def) apply (case_tac rv; clarsimp) - apply (rename_tac bool state) - apply (rule_tac F="bool = (workUnitsLimit \ work_units) \ ?abs state" in corres_req) - apply simp - apply (rule corres_guard_imp) - apply (rule corres_if3) - apply clarsimp - apply (rule_tac P="?abs" and P'="?conc" in corres_inst) - apply (rule corres_split_skip) - apply (wpsimp simp: reset_work_units_def) - apply (wpsimp simp: setWorkUnits_def) - apply (corresKsimp corres: setWorkUnits_corres) - apply (rule corres_split_skip) - apply wpsimp - apply wpsimp - apply (corresKsimp corres: updateTimeStamp_corres) - apply (rule corres_split_skip) - apply (wpsimp simp: cur_sc_tcb_def) - apply wpsimp - apply (corresKsimp corres: corres_machine_op) - apply (rule corres_underlying_split[rotated 2, OF gets_sp getCurSc_sp]) - apply (corresKsimp corres: getCurSc_corres) - apply (rule corres_underlying_split[rotated 2, OF gets_sp getConsumedTime_sp]) - apply (corresKsimp corres: getConsumedTime_corres) - apply (clarsimp simp: andM_def ifM_def bind_assoc) - apply (rule corres_underlying_split[rotated 2, OF get_sc_active_sp scActive_sp]) - apply (corresKsimp corres: scActive_corres) - apply (fastforce dest: valid_objs_valid_sched_context_size - simp: cur_sc_tcb_def obj_at_def is_sc_obj_def sc_at_pred_n_def) - apply (clarsimp split: if_split) - apply (intro conjI impI) - apply (rule corres_guard_imp) - apply (rule corres_split[OF getRefillSufficient_corres]; simp) - apply (rule corres_split[OF isCurDomainExpired_corres]) - apply (clarsimp simp: returnOk_def - split: if_split) - apply wpsimp - apply (wpsimp simp: isCurDomainExpired_def)+ - apply (prop_tac "is_active_sc (cur_sc s) s") - apply (clarsimp simp: obj_at_def vs_all_heap_simps active_sc_def) - apply (frule (1) active_scs_validE) - apply (clarsimp simp: obj_at_def is_sc_obj_def sc_at_pred_n_def vs_all_heap_simps - active_sc_def sc_valid_refills_def rr_valid_refills_def - split: if_splits) - apply simp - apply corresKsimp - apply (fastforce intro: corres_returnOkTT) - apply (clarsimp split: if_split) - apply (clarsimp split: if_split) + apply (rule corres_if_strong') + apply clarsimp + apply (rule corres_guard_imp) + apply (rule corres_split[OF setWorkUnits_corres]) + apply (rule corres_split[OF updateTimeStamp_corres]) + apply (rule corres_split[OF corres_machine_op]) + apply corres + apply (rule corres_split[OF isCurDomainExpired_corres]) + apply (rule corres_split[OF getCurSc_corres], clarsimp, rename_tac csc) + apply (clarsimp simp: stateAssertE_def) + apply (subst liftE_bindE) + apply (rule_tac P'="\s. csc = cur_sc s \ sc_at csc s" in corres_stateAssert_implied) + apply (rule corres_split[OF getConsumedTime_corres]) + apply (clarsimp simp: andM_def ifM_def bind_assoc) + apply (rule corres_split[OF scActive_corres], rule refl, rename_tac active) + apply clarsimp + apply (rule_tac R=active in corres_cases'; clarsimp) + apply (rule_tac R="\\" and R'="\\" in corres_split) + apply (rule corres_gets_the_gets) + apply (simp flip: get_sc_refill_sufficient_def) + apply (rule getRefillSufficient_corres, simp) + apply (fastforce intro: corres_returnOkTT split: if_splits) + apply wpsimp+ + apply (rule_tac Q="\\" and P'=\ in corres_symb_exec_l) + apply fastforce + apply wpsimp+ + apply (fastforce intro!: sc_at_cross simp: sc_at'_asrt_def) + apply wpsimp + apply (rule_tac Q="\_. valid_objs'" in hoare_post_imp) + apply fastforce + apply wpsimp+ + apply (rule_tac Q="\_ s. sc_at (cur_sc s) s \ pspace_aligned s \ pspace_distinct s + \ valid_objs s \ active_scs_valid s" + in hoare_post_imp) + apply (fastforce intro!: valid_refills_nonempty_refills active_scs_validE + simp: vs_all_heap_simps) + apply ((wpsimp | wps)+)[1] + apply (wpsimp simp: reset_work_units_def)+ + apply (fastforce intro!: cur_sc_tcb_sc_at_cur_sc) + apply clarsimp + apply (corres corres: corres_returnOkTT) done lemma updateTimeStamp_inv: @@ -391,6 +409,11 @@ lemma updateTimeStamp_inv: apply (fastforce simp: update_time_stamp_independent_A_def domain_time_independent_H_def) done +lemma getDomainTime_wp[wp]: + "\\s. P (ksDomainTime s) s \ getDomainTime \ P \" + unfolding getDomainTime_def + by wp + lemma preemptionPoint_inv: assumes "(\f s. P (ksWorkUnitsCompleted_update f s) = P s)" "irq_state_independent_H P" @@ -400,21 +423,9 @@ lemma preemptionPoint_inv: "domain_time_independent_H P" shows "preemptionPoint \P\" using assms - apply (simp add: preemptionPoint_def setWorkUnits_def getWorkUnits_def modifyWorkUnits_def - setConsumedTime_def setCurTime_def) - apply (rule validE_valid) - apply (rule bindE_wp_fwd_skip, solves wpsimp)+ - apply (clarsimp simp: whenE_def) - apply (intro conjI impI; (solves wpsimp)?) - apply (rule bindE_wp_fwd_skip, solves wpsimp)+ - apply (rename_tac preempt) - apply (case_tac preempt; clarsimp) - apply (rule bindE_wp_fwd_skip) - apply (wpsimp wp: updateTimeStamp_inv) - apply (rule bindE_wp_fwd_skip, solves wpsimp)+ - apply (wpsimp wp: getRefills_wp hoare_drop_imps - simp: isCurDomainExpired_def getDomainTime_def refillSufficient_def) - done + apply (simp add: preemptionPoint_def setWorkUnits_def getWorkUnits_def modifyWorkUnits_def) + by (wpsimp simp: isCurDomainExpired_def stateAssertE_def + wp: getDomainTime_wp updateTimeStamp_inv hoare_drop_imps) lemma ct_in_state_machine_state_independent[intro!, simp]: "ct_in_state P (machine_state_update f s) = ct_in_state P s" diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index 3d8c6a471a..ef6fdf712a 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -1710,9 +1710,9 @@ lemma setSchedulerAction_invs': (* not in wp set, clobbered by ssa_wp *) lemma scheduleChooseNewThread_corres: "corres dc - (\s. invs s \ valid_ready_qs s \ ready_or_release s \ scheduler_action s = choose_new_thread) - (\s. invs' s \ ksSchedulerAction s = ChooseNewThread) - schedule_choose_new_thread scheduleChooseNewThread" + (\s. invs s \ valid_ready_qs s \ ready_or_release s \ scheduler_action s = choose_new_thread) + (\s. invs' s \ ksSchedulerAction s = ChooseNewThread) + schedule_choose_new_thread scheduleChooseNewThread" apply (clarsimp simp: schedule_choose_new_thread_def scheduleChooseNewThread_def) apply (rule corres_stateAssert_ignore) apply (fastforce intro: ksReadyQueues_asrt_cross) @@ -1720,8 +1720,7 @@ lemma scheduleChooseNewThread_corres: apply (rule corres_split[OF getDomainTime_corres], clarsimp) apply (rule corres_split[OF scheduleChooseNewThread_fragment_corres, simplified bind_assoc]) apply (rule setSchedulerAction_corres) - apply (wp | simp)+ - apply (wp | simp add: getDomainTime_def)+ + apply wpsimp+ done lemma ssa_ct_not_inQ: @@ -1735,10 +1734,6 @@ lemma ssa_invs': apply (clarsimp simp: invs'_def valid_irq_node'_def valid_dom_schedule'_def) done -lemma getDomainTime_wp[wp]: "\\s. P (ksDomainTime s) s \ getDomainTime \ P \" - unfolding getDomainTime_def - by wp - lemma switchToThread_ct_not_queued_2: "\invs' and tcb_at' t\ switchToThread t \\rv s. obj_at' (Not \ tcbQueued) (ksCurThread s) s\" (is "\_\ _ \\_. ?POST\") diff --git a/proof/refine/RISCV64/Untyped_R.thy b/proof/refine/RISCV64/Untyped_R.thy index f5e352664a..35c454e174 100644 --- a/proof/refine/RISCV64/Untyped_R.thy +++ b/proof/refine/RISCV64/Untyped_R.thy @@ -1417,6 +1417,7 @@ crunches set_cap, set_cdt for domain_index[wp]: "\s. P (domain_index s)" and reprogram_timer[wp]: "\s. P (reprogram_timer s)" (wp: crunch_wps) + crunches updateMDB, updateNewFreeIndex, setCTE for rdyq_projs[wp]: "\s. P (ksReadyQueues s) (tcbSchedNexts_of s) (tcbSchedPrevs_of s) (\d p. inQ d p |< tcbs_of' s)" diff --git a/spec/abstract/KHeap_A.thy b/spec/abstract/KHeap_A.thy index 1036afba38..69f72edcf3 100644 --- a/spec/abstract/KHeap_A.thy +++ b/spec/abstract/KHeap_A.thy @@ -650,21 +650,19 @@ where else modify (\s. s\ domain_time := domain_time - consumed \) od" -definition - preemption_point :: "(unit,'z::state_ext) p_monad" -where +definition preemption_point :: "(unit,'z::state_ext) p_monad" where "preemption_point \ doE liftE $ do_extended_op update_work_units; OR_choiceE work_units_limit_reached (doE liftE $ do_extended_op reset_work_units; liftE $ update_time_stamp; irq_opt \ liftE $ do_machine_op (getActiveIRQ True); + exp \ liftE $ gets is_cur_domain_expired; cur_sc \ liftE $ gets cur_sc; consumed \ liftE $ gets consumed_time; - test \ liftE $ andM (get_sc_active cur_sc) - (get_sc_refill_sufficient cur_sc consumed); - exp \ liftE $ gets is_cur_domain_expired; - whenE (\test \ exp \ irq_opt \ None) $ throwError () + active \ liftE $ get_sc_active cur_sc; + sufficient \ liftE $ gets $ read_sc_refill_sufficient cur_sc consumed; + whenE ((irq_opt \ None) \ exp \ \ (active \ sufficient = Some True)) (throwError ()) odE) (returnOk ()) odE" diff --git a/spec/design/skel/KernelStateData_H.thy b/spec/design/skel/KernelStateData_H.thy index b7764d7d15..6a77d406f3 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 -#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 +#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 +#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 end diff --git a/spec/haskell/src/SEL4/Model/StateData.lhs b/spec/haskell/src/SEL4/Model/StateData.lhs index 9aa7fc18ef..28c3b4f388 100644 --- a/spec/haskell/src/SEL4/Model/StateData.lhs +++ b/spec/haskell/src/SEL4/Model/StateData.lhs @@ -516,3 +516,8 @@ An assert that will say that the idle thread is not in a ready queue > idleThreadNotQueued :: KernelState -> Bool > idleThreadNotQueued _ = True + +An assert that will say that there is a scheduling context at the given pointer + +> sc_at'_asrt :: PPtr SchedContext -> KernelState -> Bool +> sc_at'_asrt _ _ = True diff --git a/spec/haskell/src/SEL4/Object/SchedContext.lhs b/spec/haskell/src/SEL4/Object/SchedContext.lhs index adb3c7c805..d36482fe7e 100644 --- a/spec/haskell/src/SEL4/Object/SchedContext.lhs +++ b/spec/haskell/src/SEL4/Object/SchedContext.lhs @@ -867,10 +867,11 @@ In preemptible code, the kernel may explicitly mark a preemption point with the > withoutPreemption $ setWorkUnits 0 > withoutPreemption $ updateTimeStamp > preempt <- withoutPreemption $ doMachineOp (getActiveIRQ True) +> domExp <- withoutPreemption $ isCurDomainExpired > csc <- withoutPreemption $ getCurSc +> stateAssert (sc_at'_asrt csc) "there is a scheduling context at ksCurSc" > consumed <- withoutPreemption $ getConsumedTime > test <- withoutPreemption $ andM (scActive csc) (getRefillSufficient csc consumed) -> domExp <- withoutPreemption $ isCurDomainExpired -> if (not test || domExp || isJust preempt) +> if (isJust preempt || domExp || not test) > then throwError () > else return ()