diff --git a/proof/crefine/RISCV64/Arch_C.thy b/proof/crefine/RISCV64/Arch_C.thy index 23e0cdcc2e..c0e6f68de8 100644 --- a/proof/crefine/RISCV64/Arch_C.thy +++ b/proof/crefine/RISCV64/Arch_C.thy @@ -1087,7 +1087,7 @@ lemma decodeRISCVPageTableInvocation_ccorres: apply (clarsimp simp: ct_in_state'_def isCap_simps valid_tcb_state'_def) apply (case_tac v1; clarsimp) (* is PT mapped *) apply (auto simp: ct_in_state'_def isCap_simps valid_tcb_state'_def valid_cap'_def - wellformed_mapdata'_def sch_act_wf_def sch_act_simple_def + wellformed_mapdata'_def weak_sch_act_wf_def sch_act_simple_def elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread') done apply (rule conjI) @@ -1102,7 +1102,7 @@ lemma decodeRISCVPageTableInvocation_ccorres: slotcap_in_mem_def dest!: ctes_of_valid') by (auto simp: ct_in_state'_def pred_tcb_at' mask_def valid_tcb_state'_def valid_cap'_def wellformed_acap'_def wellformed_mapdata'_def - sch_act_wf_def sch_act_simple_def + weak_sch_act_wf_def sch_act_simple_def elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')[1] apply (rule conjI) @@ -2105,7 +2105,7 @@ lemma decodeRISCVFrameInvocation_ccorres: subgoal by (auto simp: ct_in_state'_def pred_tcb_at' mask_def valid_tcb_state'_def valid_cap'_def wellformed_acap'_def wellformed_mapdata'_def - sch_act_wf_def sch_act_simple_def + weak_sch_act_wf_def sch_act_simple_def elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread') (* RISCVPageUnMap, Haskell side *) @@ -2113,7 +2113,7 @@ lemma decodeRISCVFrameInvocation_ccorres: subgoal by (auto simp: isCap_simps comp_def ct_in_state'_def pred_tcb_at' mask_def valid_tcb_state'_def valid_cap'_def wellformed_acap'_def wellformed_mapdata'_def - sch_act_wf_def sch_act_simple_def + weak_sch_act_wf_def sch_act_simple_def elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread') (* C side of precondition satisfaction *) @@ -2847,6 +2847,10 @@ lemma decodeRISCVMMUInvocation_ccorres: apply (rule conjI; clarsimp)+ apply (rule conjI, erule ctes_of_valid', clarsimp) apply (intro conjI) + apply fastforce + apply fastforce + apply fastforce + apply fastforce apply fastforce apply (fastforce elim!: pred_tcb'_weakenE) apply (clarsimp simp: excaps_in_mem_def slotcap_in_mem_def) @@ -2864,6 +2868,10 @@ lemma decodeRISCVMMUInvocation_ccorres: apply (clarsimp simp: isCap_simps valid_tcb_state'_def) apply (frule invs_arch_state', clarsimp) apply (intro conjI) + apply (fastforce simp: ct_in_state'_def elim!: pred_tcb'_weakenE) + apply fastforce + apply fastforce + apply fastforce apply (fastforce simp: ct_in_state'_def elim!: pred_tcb'_weakenE) apply (fastforce simp: ct_in_state'_def elim!: pred_tcb'_weakenE) apply (cases extraCaps; simp) diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy index d7866f37a7..6110bdc7f7 100644 --- a/proof/crefine/RISCV64/Finalise_C.thy +++ b/proof/crefine/RISCV64/Finalise_C.thy @@ -1173,17 +1173,18 @@ lemma tcb_queue_relation2_cong: context kernel_m begin -lemma setThreadState_ccorres_valid_queues'_simple: +lemma setThreadState_ccorres_simple: "ccorres dc xfdc - (tcb_at' thread) - ({s'. (\cl fl. cthread_state_relation_lifted st (cl\tsType_CL := ts_' s' && mask 4\, fl))} - \ {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) [] + (\s. tcb_at' thread s \ sch_act_simple s \ no_0_obj' s + \ weak_sch_act_wf (ksSchedulerAction s) s) + (\\cl fl. cthread_state_relation_lifted st (cl\tsType_CL := \ts && mask 4\, fl)\ + \ \\tptr = tcb_ptr_to_ctcb_ptr thread\) [] (setThreadState st thread) (Call setThreadState_'proc)" apply (cinit lift: tptr_' cong add: call_ignore_cong) - apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres) - apply (ctac add: scheduleTCB_ccorres_valid_queues'_simple) - apply wpsimp - apply (clarsimp simp: weak_sch_act_wf_def) + apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres) + apply (ctac add: scheduleTCB_ccorres_simple) + apply (wpsimp wp: threadSet_valid_objs') + apply clarsimp done lemma updateRestartPC_ccorres: @@ -1401,23 +1402,27 @@ lemma active_runnable': crunches updateRestartPC for no_0_obj'[wp]: no_0_obj' + and weak_sch_act_wf[wp]: "\s. weak_sch_act_wf (ksSchedulerAction s) s" (wp: crunch_wps) lemma suspend_ccorres: assumes cteDeleteOne_ccorres: - "\w slot. ccorres dc xfdc - (invs' and cte_wp_at' (\ct. w = -1 \ cteCap ct = NullCap - \ (\cap'. ccap_relation (cteCap ct) cap' \ cap_get_tag cap' = w)) slot) - ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w} + "\w slot. + ccorres dc xfdc + (invs' + and cte_wp_at' (\ct. w = -1 \ cteCap ct = NullCap + \ (\cap'. ccap_relation (cteCap ct) cap' \ cap_get_tag cap' = w)) slot) + ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w} \ {s. slot_' s = Ptr slot}) [] (cteDeleteOne slot) (Call cteDeleteOne_'proc)" shows "ccorres dc xfdc - (invs' and tcb_at' thread and (\s. thread \ ksIdleThread s)) - (UNIV \ {s. target_' s = tcb_ptr_to_ctcb_ptr thread}) [] - (suspend thread) (Call suspend_'proc)" + (invs' and sch_act_simple and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and tcb_at' thread + and (\s. thread \ ksIdleThread s)) + \\target = tcb_ptr_to_ctcb_ptr thread\ [] + (suspend thread) (Call suspend_'proc)" apply (cinit lift: target_') - apply (rule ccorres_stateAssert) + apply (rule ccorres_stateAssert) apply (ctac(no_vcg) add: cancelIPC_ccorres1 [OF cteDeleteOne_ccorres]) apply (rule getThreadState_ccorres_foo) apply (rename_tac threadState) @@ -1444,7 +1449,7 @@ lemma suspend_ccorres: apply (ctac (no_vcg) add: updateRestartPC_ccorres) apply (rule ccorres_return_Skip) apply ceqv - apply (ctac(no_vcg) add: setThreadState_ccorres_valid_queues'_simple) + apply (ctac(no_vcg) add: setThreadState_ccorres_simple) apply (ctac (no_vcg) add: tcbSchedDequeue_ccorres) apply (ctac (no_vcg) add: tcbReleaseRemove_ccorres) apply (ctac (no_vcg) add: schedContext_cancelYieldTo_ccorres) @@ -1454,10 +1459,12 @@ lemma suspend_ccorres: apply clarsimp apply (rule conseqPre, vcg) apply (rule subset_refl) - apply (rule_tac Q="\_. invs' and tcb_at' thread" in hoare_post_imp) + apply (rule_tac Q="\_ s. invs' s \ tcb_at' thread s \ sch_act_simple s + \ weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp) apply fastforce apply (wpsimp wp: hoare_vcg_all_lift) - by (auto simp: ThreadState_defs)[1] + apply (auto simp: ThreadState_defs) + done lemma cap_to_H_NTFNCap_tag: "\ cap_to_H cap = NotificationCap word1 word2 a b; diff --git a/proof/crefine/RISCV64/Interrupt_C.thy b/proof/crefine/RISCV64/Interrupt_C.thy index 7691d34f89..950c642fbb 100644 --- a/proof/crefine/RISCV64/Interrupt_C.thy +++ b/proof/crefine/RISCV64/Interrupt_C.thy @@ -250,13 +250,13 @@ lemma decodeIRQHandlerInvocation_ccorres: apply (rule ccorres_alternative2) apply (rule ccorres_return_CE, simp+)[1] apply (wp sts_invs_minor')+ - apply (rule ccorres_equals_throwError) - apply (fastforce simp: invocationCatch_def throwError_bind - split: gen_invocation_labels.split) - apply (simp add: ccorres_cond_iffs cong: StateSpace.state.fold_congs globals.fold_congs) - apply (rule syscall_error_throwError_ccorres_n) - apply (simp add: syscall_error_to_H_cases) - apply simp + apply (rule ccorres_equals_throwError) + apply (fastforce simp: invocationCatch_def throwError_bind + split: gen_invocation_labels.split) + apply (simp add: ccorres_cond_iffs cong: StateSpace.state.fold_congs globals.fold_congs) + apply (rule syscall_error_throwError_ccorres_n) + apply (simp add: syscall_error_to_H_cases) + apply simp apply (clarsimp simp: Collect_const_mem) apply (clarsimp simp: invs_valid_objs' ct_in_state'_def @@ -270,16 +270,18 @@ lemma decodeIRQHandlerInvocation_ccorres: slotcap_in_mem_def valid_tcb_state'_def dest!: interpret_excaps_eq split: bool.splits) apply (intro conjI impI allI) - apply (clarsimp simp: cte_wp_at_ctes_of neq_Nil_conv sysargs_rel_def n_msgRegisters_def - excaps_map_def excaps_in_mem_def word_less_nat_alt hd_conv_nth - slotcap_in_mem_def valid_tcb_state'_def - dest!: interpret_excaps_eq split: bool.splits)+ - apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')[6] + apply (clarsimp simp: cte_wp_at_ctes_of neq_Nil_conv sysargs_rel_def n_msgRegisters_def + excaps_map_def excaps_in_mem_def word_less_nat_alt hd_conv_nth + slotcap_in_mem_def valid_tcb_state'_def + dest!: interpret_excaps_eq split: bool.splits)+ + apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')[6] + apply fastforce + apply fastforce apply (drule ctes_of_valid') apply fastforce apply (clarsimp simp add:valid_cap_simps' RISCV64.maxIRQ_def) apply (erule order.trans,simp) - apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid') + apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid') done declare mask_of_mask[simp] diff --git a/proof/crefine/RISCV64/Invoke_C.thy b/proof/crefine/RISCV64/Invoke_C.thy index 27da132eda..42d02b63ab 100644 --- a/proof/crefine/RISCV64/Invoke_C.thy +++ b/proof/crefine/RISCV64/Invoke_C.thy @@ -40,9 +40,12 @@ lemma cap_case_ThreadCap2: by (simp add: isCap_simps split: capability.split) +crunches tcbSchedEnqueue + for weak_sch_act_wf[wp]: "\s. weak_sch_act_wf (ksSchedulerAction s) s" + lemma setDomain_ccorres: "ccorres dc xfdc - (invs' and tcb_at' t and (\s. d \ maxDomain)) + (invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and tcb_at' t and (\s. d \ maxDomain)) (UNIV \ {s. tptr_' s = tcb_ptr_to_ctcb_ptr t} \ {s. dom_' s = ucast d}) [] (setDomain t d) (Call setDomain_'proc)" apply (rule ccorres_gen_asm) @@ -75,12 +78,14 @@ lemma setDomain_ccorres: apply (simp add: guard_is_UNIV_def) apply simp apply wp - apply (rule_tac Q="\rv'. invs' and tcb_at' t and (\s. curThread = ksCurThread s)" + apply (rule_tac Q="\rv'. invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s) + and tcb_at' t and (\s. curThread = ksCurThread s)" in hoare_strengthen_post) apply (wpsimp wp: isSchedulable_wp) apply (fastforce simp: valid_pspace_valid_objs' weak_sch_act_wf_def split: if_splits) - apply (rule_tac Q="\_. invs' and tcb_at' t and (\s. curThread = ksCurThread s)" + apply (rule_tac Q="\_. invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s) + and tcb_at' t and (\s. curThread = ksCurThread s)" in hoare_strengthen_post) apply (wpsimp wp: threadSet_tcbDomain_update_invs' hoare_vcg_imp_lift' threadSet_isSchedulable_bool)+ diff --git a/proof/crefine/RISCV64/IpcCancel_C.thy b/proof/crefine/RISCV64/IpcCancel_C.thy index cbd8de3438..fb13e637e1 100644 --- a/proof/crefine/RISCV64/IpcCancel_C.thy +++ b/proof/crefine/RISCV64/IpcCancel_C.thy @@ -313,18 +313,22 @@ lemma ko_at_obj_congD': apply simp done -lemma threadGet_vcg_corres_P: - assumes c: "\x. \\. \\ {s. (\, s) \ rf_sr - \ tcb_at' thread \ \ P \ - \ (\tcb. ko_at' tcb thread \ \ (\tcb'. - x = f tcb \ cslift s (tcb_ptr_to_ctcb_ptr thread) = Some tcb' - \ ctcb_relation tcb tcb'))} c {s. (\, s) \ rf_sr \ r x (xf s)}" - shows "ccorres r xf P UNIV hs (threadGet f thread) c" +lemma threadGet_vcg_corres_P_P': + assumes c: + "\x. \\. \ \ {s. (\, s) \ rf_sr + \ tcb_at' thread \ \ P \ \ s \ P' + \ (\tcb. ko_at' tcb thread \ + \ (\tcb'. x = f tcb + \ cslift s (tcb_ptr_to_ctcb_ptr thread) = Some tcb' + \ ctcb_relation tcb tcb'))} + c + {s. (\, s) \ rf_sr \ r x (xf s)}" + shows "ccorres r xf P P' hs (threadGet f thread) c" apply (rule ccorres_add_return2) apply (rule ccorres_guard_imp2) apply (rule ccorres_pre_threadGet) - apply (rule_tac P = "\\. \tcb. ko_at' tcb thread \ \ x = f tcb \ P \" - and P' = UNIV in ccorres_from_vcg) + apply (rule_tac P="\s. \tcb. ko_at' tcb thread s \ x = f tcb \ P s" and P'=P' + in ccorres_from_vcg) apply (simp add: return_def) apply (rule allI, rule conseqPre) apply (rule spec [OF c]) @@ -341,6 +345,8 @@ lemma threadGet_vcg_corres_P: apply fastforce done +lemmas threadGet_vcg_corres_P = threadGet_vcg_corres_P_P'[where P'=UNIV, simplified] + lemmas threadGet_vcg_corres = threadGet_vcg_corres_P[where P=\] lemma threadGet_specs_corres: @@ -1769,44 +1775,160 @@ lemma tcb_at_1: apply (clarsimp simp add: is_aligned_def ctcb_size_bits_def) done +crunch (empty_fail) empty_fail[wp]: inReleaseQueue, isSchedulable + lemma isSchedulable_ccorres [corres]: "ccorres (\r r'. r = to_bool r') ret__unsigned_long_' - (tcb_at' tcbPtr) (UNIV \ {s. thread_' s = tcb_ptr_to_ctcb_ptr tcbPtr}) [] - (isSchedulable tcbPtr) (Call isSchedulable_'proc)" -sorry (* FIXME RT: isSchedulable_ccorres *) + (tcb_at' tcbPtr and no_0_obj') \\thread = tcb_ptr_to_ctcb_ptr tcbPtr\ [] + (isSchedulable tcbPtr) (Call isSchedulable_'proc)" + supply Collect_const[simp del] + if_split[split del] + apply (cinit lift: thread_') + apply (ctac add: isRunnable_ccorres) + apply (rename_tac runnable) + apply csymbr + apply (rule ccorres_pre_threadGet) + apply clarsimp + apply (rule_tac P="to_bool runnable" in ccorres_cases; clarsimp simp: to_bool_def) + apply ccorres_rewrite + apply (rule ccorres_move_c_guard_tcb) + apply (rule ccorres_stateAssert) + apply (rule_tac xf'=ret__int_' + and val="from_bool (scPtrOpt \ None)" + and R="\s. obj_at' (\tcb. tcbSchedContext tcb = scPtrOpt) tcbPtr s + \ valid_tcbs' s \ no_0_obj' s" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply normalise_obj_at' + apply (frule (1) ko_at'_valid_tcbs'_valid_tcb') + apply (frule (1) obj_at_cslift_tcb) + subgoal + by (fastforce simp: from_bool_def ctcb_relation_def typ_heap_simps valid_tcb'_def + split: if_splits bool.splits) + apply ceqv + apply (rule ccorres_cond_seq) + apply ccorres_rewrite + apply (subst if_swap) + apply (rule_tac P="scPtrOpt = None" in ccorres_cases; clarsimp) + apply ccorres_rewrite + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond_false) + apply ccorres_rewrite + apply (fastforce intro: ccorres_return_C') + apply ccorres_rewrite + apply (rule ccorres_rhs_assoc) + apply (rule ccorres_move_c_guard_tcb) + apply wpfix + apply (ctac add: sc_active_ccorres) + apply csymbr + apply clarsimp + apply (rename_tac active) + apply (rule_tac P="to_bool active" in ccorres_cases; clarsimp) + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond_true) + apply (rule ccorres_rhs_assoc) + apply (rule ccorres_move_c_guard_tcb) + apply (clarsimp simp: inReleaseQueue_def) + apply (rule_tac r'="\rv rv'. rv = to_bool rv'" and xf'="ret__unsigned_longlong_'" + in ccorres_split_nothrow) + apply (rule threadGet_vcg_corres) + apply (rule allI, rule conseqPre, vcg) + apply clarsimp + apply (drule obj_at_ko_at', clarsimp) + apply (drule spec, drule (1) mp, clarsimp) + apply (clarsimp simp: typ_heap_simps ctcb_relation_def) + apply ceqv + apply csymbr + apply (fastforce intro: ccorres_return_C') + apply wpsimp + apply (vcg exspec=thread_state_get_tcbInReleaseQueue_modifies) + apply (clarsimp simp: to_bool_def) + apply ccorres_rewrite + apply (rule ccorres_symb_exec_l') + apply (fastforce intro: ccorres_return_C') + apply wpsimp+ + apply (vcg expsec=sc_active_modifies) + apply vcg + apply ccorres_rewrite + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond_false) + apply ccorres_rewrite + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond_false) + apply ccorres_rewrite + apply (rule ccorres_stateAssert) + apply (rule ccorres_if_lhs) + apply (fastforce intro: ccorres_return_C) + apply clarsimp + apply (rule ccorres_symb_exec_l') + apply (rule ccorres_symb_exec_l') + apply (fastforce intro: ccorres_return_C') + apply wpsimp+ + apply (vcg exspec=isRunnable_modifies) + apply normalise_obj_at' + apply (frule (1) obj_at_cslift_tcb) + by (fastforce simp: valid_tcbs'_asrt_def obj_at'_def to_bool_def typ_heap_simps ctcb_relation_def + split: if_splits) lemma rescheduleRequired_ccorres: - "ccorres dc xfdc valid_objs' UNIV [] rescheduleRequired (Call rescheduleRequired_'proc)" -sorry (* FIXME RT: 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 [] + rescheduleRequired (Call rescheduleRequired_'proc)" + supply if_split[split del] apply cinit - apply (rule ccorres_symb_exec_l) - apply (rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc]) - apply (simp add: scheduler_action_case_switch_to_if - cong: if_weak_cong split del: if_split) - apply (rule_tac R="\s. action = ksSchedulerAction s \ weak_sch_act_wf action s" - in ccorres_cond) - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - cscheduler_action_relation_def) - subgoal by (clarsimp simp: weak_sch_act_wf_def tcb_at_1 tcb_at_not_NULL - split: scheduler_action.split_asm dest!: pred_tcb_at') - apply (ctac add: tcbSchedEnqueue_ccorres) - apply (rule ccorres_return_Skip) + apply (rule ccorres_pre_getSchedulerAction) + apply (rule ccorres_rhs_assoc2)+ + apply (rule_tac xf'=xfdc in ccorres_split_nothrow) + apply (subst scheduler_action_case_switch_to_if) + apply (rule ccorres_rhs_assoc) + apply (rule_tac val="from_bool (\target. action = SwitchToThread target)" + and xf'=ret__int_' + and R="\s. (\target. ksSchedulerAction s = action) + \ weak_sch_act_wf (ksSchedulerAction s) s" + in ccorres_symb_exec_r_known_rv) + apply vcg + apply clarsimp + apply (frule rf_sr_sched_action_relation) + subgoal + by (clarsimp simp: cscheduler_action_relation_def weak_sch_act_wf_def tcb_at_1 + tcb_at_not_NULL + dest!: pred_tcb_at' split: scheduler_action.splits) apply ceqv - apply (rule ccorres_from_vcg[where P=\ and P'=UNIV]) - apply (rule allI, rule conseqPre, vcg) - apply (clarsimp simp: setSchedulerAction_def simpler_modify_def) - subgoal by (clarsimp simp: rf_sr_def cstate_relation_def Let_def - cscheduler_action_relation_def - carch_state_relation_def cmachine_state_relation_def) - apply wp - apply (simp add: guard_is_UNIV_def) - apply wp+ - apply (simp add: getSchedulerAction_def) - apply (clarsimp simp: weak_sch_act_wf_def rf_sr_def cstate_relation_def - Let_def cscheduler_action_relation_def) - by (auto simp: tcb_at_not_NULL tcb_at_1 - tcb_at_not_NULL[THEN not_sym] tcb_at_1[THEN not_sym] - split: scheduler_action.split_asm) *) + apply (rule ccorres_cond_seq) + apply (clarsimp simp: when_def true_def) + apply (simp flip: Collect_const) + apply (rule ccorres_cond_both'[where Q=\ and Q'=\ and xf=xfdc]) + apply fastforce + apply (rule ccorres_rhs_assoc) + apply (ctac add: isSchedulable_ccorres) + apply csymbr + apply (clarsimp simp: when_def true_def) + apply (rule ccorres_cond[where R=\ ]) + apply (clarsimp simp: to_bool_def split: if_split) + apply (ctac add: tcbSchedEnqueue_ccorres) + apply (rule ccorres_return_Skip) + apply (wpsimp wp: isSchedulable_wp) + apply (vcg exspec=isSchedulable_modifies) + apply (clarsimp simp: to_bool_def) + apply (rule ccorres_cond_false) + apply (rule ccorres_return_Skip') + apply vcg + apply ceqv + apply (rule ccorres_from_vcg[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: setSchedulerAction_def simpler_modify_def) + apply (frule rf_sr_sched_action_relation) + subgoal + by (clarsimp simp: cscheduler_action_relation_def rf_sr_def cstate_relation_def + carch_state_relation_def cmachine_state_relation_def) + apply wpsimp + apply (vcg exspec=isSchedulable_modifies exspec=tcbSchedEnqueue_modifies) + apply (fastforce simp: cscheduler_action_relation_def weak_sch_act_wf_def + dest: rf_sr_sched_action_relation) + done lemma getReadyQueuesL1Bitmap_sp: "\\s. P s \ d \ maxDomain \ @@ -2074,299 +2196,297 @@ lemma getCurDomain_maxDom_ccorres_dom_': rf_sr_ksCurDomain) done -lemma thread_state_get_tcbInReleaseQueue_ccorres: - "ccorres (\rv rv'. rv = to_bool rv') ret_' - (tcb_at' tcbPtr) - \\thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr tcbPtr\[''tcbState_C''])\ - hs - (inReleaseQueue tcbPtr) (Call thread_state_get_tcbInReleaseQueue_'proc)" -sorry (* FIXME RT: thread_state_get_tcbInReleaseQueue_ccorres *) - lemma threadGet_get_obj_at'_has_domain: "\ tcb_at' t \ threadGet tcbDomain t \\rv. obj_at' (\tcb. rv = tcbDomain tcb) t\" by (wp threadGet_obj_at') (simp add: obj_at'_def) lemma possibleSwitchTo_ccorres: - shows "ccorres dc xfdc - ((\s. ksCurDomain s \ maxDomain) and valid_objs') - ({s. target_' s = tcb_ptr_to_ctcb_ptr t} - \ UNIV) [] - (possibleSwitchTo t ) - (Call possibleSwitchTo_'proc)" - supply if_split [split del] - supply Collect_const [simp del] + ((\s. weak_sch_act_wf (ksSchedulerAction s) s) + and tcb_at' t and (\s. ksCurDomain s \ maxDomain) + and valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct') + \\target = tcb_ptr_to_ctcb_ptr t\ [] + (possibleSwitchTo t ) (Call possibleSwitchTo_'proc)" + supply if_split[split del] + supply Collect_const[simp del] + supply dc_simp[simp del] supply prio_and_dom_limit_helpers[simp] (* FIXME: these should likely be in simpset for CRefine, or even in general *) supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] ccorres_IF_True[simp] if_cong[cong] apply (cinit lift: target_') -sorry (* FIXME RT: possibleSwitchTo_ccorres *) (* apply (rule ccorres_move_c_guard_tcb) - apply (rule ccorres_pre_curDomain, rename_tac curDom) - apply (rule ccorres_symb_exec_l3[OF _ threadGet_inv _ empty_fail_threadGet], rename_tac targetDom) - apply (rule ccorres_symb_exec_l3[OF _ gsa_wp _ empty_fail_getSchedulerAction], rename_tac sact) - apply (rule_tac C'="{s. targetDom \ curDom}" - and Q="\s. curDom = ksCurDomain s \ obj_at' (\tcb. targetDom = tcbDomain tcb) t s" - and Q'=UNIV in ccorres_rewrite_cond_sr) + apply (rule ccorres_pre_threadGet, rename_tac scOpt) + apply (rule_tac val="from_bool (\scPtr. scOpt = Some scPtr)" + and xf'=ret__int_' + and R="tcb_at' t and bound_sc_tcb_at' ((=) scOpt) t and valid_objs' and no_0_obj'" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply clarsimp + apply (frule (1) obj_at_cslift_tcb) + apply normalise_obj_at' + apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') subgoal + by (fastforce simp: typ_heap_simps ctcb_relation_def option_to_ptr_def option_to_0_def + valid_tcb'_def + split: option.splits) + apply ceqv + apply (rule_tac r'="\rv rv'. rv' = from_bool ((\scPtr. scOpt = Some scPtr) \ \ rv)" + and xf'=ret__int_' + and P'="\\ret__int = from_bool (\scPtr. scOpt = Some scPtr)\" + in ccorres_split_nothrow) + apply (clarsimp simp: inReleaseQueue_def) + apply (rule threadGet_vcg_corres_P_P') + apply (rule allI, rule conseqPre, vcg) apply clarsimp - apply (drule obj_at_ko_at', clarsimp simp: rf_sr_ksCurDomain) - apply (frule (1) obj_at_cslift_tcb, clarsimp simp: typ_heap_simps') - apply (drule ctcb_relation_unat_tcbDomain_C) - apply unat_arith + apply (drule obj_at_ko_at') + apply (clarsimp simp: typ_heap_simps ctcb_relation_def obj_at'_def to_bool_def) + apply ceqv + apply (clarsimp simp: when_def) + apply (rule_tac R=\ in ccorres_cond) apply fastforce - done - apply (rule ccorres_cond2[where R=\], simp) - apply (ctac add: tcbSchedEnqueue_ccorres) - apply (rule_tac R="\s. sact = ksSchedulerAction s \ weak_sch_act_wf (ksSchedulerAction s) s" - in ccorres_cond) - apply (fastforce dest!: rf_sr_sched_action_relation pred_tcb_at' tcb_at_not_NULL - simp: cscheduler_action_relation_def weak_sch_act_wf_def - split: scheduler_action.splits) - apply (ctac add: rescheduleRequired_ccorres) + apply (rule ccorres_pre_curDomain, rename_tac curDomain) + apply (rule ccorres_pre_threadGet, rename_tac targetDomain) + apply (rule ccorres_pre_getSchedulerAction, rename_tac action) + apply (rule ccorres_move_c_guard_tcb) + apply (rule_tac Q="\s. obj_at' (\tcb. tcbDomain tcb = targetDomain) t s + \ ksCurDomain s = curDomain" + and Q'=\ + in ccorres_cond_both') + apply clarsimp + apply (frule (1) obj_at_cslift_tcb) + apply (frule rf_sr_ksCurDomain) + apply (fastforce simp: ctcb_relation_def typ_heap_simps obj_at'_def) apply (ctac add: tcbSchedEnqueue_ccorres) - apply wp - apply (vcg exspec=rescheduleRequired_modifies) - apply (rule ccorres_setSchedulerAction, simp add: cscheduler_action_relation_def) - apply clarsimp - apply wp - apply clarsimp - apply (wp hoare_drop_imps threadGet_get_obj_at'_has_domain) - apply (clarsimp simp: pred_tcb_at') - done *) + apply (rule_tac Q="\s. ksSchedulerAction s = action \ weak_sch_act_wf action s" + and Q'=\ + in ccorres_cond_both') + apply clarsimp + apply (frule rf_sr_sched_action_relation) + apply (clarsimp simp: cscheduler_action_relation_def weak_sch_act_wf_def pred_tcb_at'_def + intro!: tcb_at_not_NULL + split: scheduler_action.splits) + apply (fastforce simp: obj_at'_def) + apply (ctac add: rescheduleRequired_ccorres) + apply (ctac add: tcbSchedEnqueue_ccorres) + apply (wpsimp wp: hoare_vcg_all_lift) + apply (vcg exspec=rescheduleRequired_modifies) + apply (rule ccorres_setSchedulerAction, simp add: cscheduler_action_relation_def) + apply (rule ccorres_return_Skip) + apply (wpsimp wp: inReleaseQueue_wp) + apply vcg + apply vcg + apply (fastforce simp: typ_heap_simps obj_at'_def pred_tcb_at'_def) + done -lemma scheduleTCB_ccorres': +lemma scheduleTCB_ccorres: "ccorres dc xfdc - (tcb_at' thread and valid_objs') - (UNIV \ {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) - [] - (scheduleTCB thread) - (Call scheduleTCB_'proc)" -sorry (* FIXME RT: scheduleTCB_ccorres' *) -(* - apply (cinit' lift: tptr_') - apply (rule ccorres_rhs_assoc2)+ - apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) - defer + ((\s. weak_sch_act_wf (ksSchedulerAction s) s) + and tcb_at' thread and valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct') + \\tptr = tcb_ptr_to_ctcb_ptr thread\ [] + (scheduleTCB thread) (Call scheduleTCB_'proc)" + supply Collect_const[simp del] + if_split[split del] + apply (cinit lift: tptr_') + apply (rule ccorres_pre_getCurThread, rename_tac curThread) + apply (rule_tac val="from_bool (thread = curThread)" + and xf'=ret__int_' + and R="\s. ksCurThread s = curThread" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (fastforce dest: rf_sr_ksCurThread simp: from_bool_def split: bool.splits) + apply ceqv + apply (rule ccorres_pre_getSchedulerAction, rename_tac action) + apply (rule ccorres_cond_seq) + apply (rule_tac P="thread = curThread" in ccorres_cases; clarsimp) + apply ccorres_rewrite + apply (rule_tac val="from_bool (action = ResumeCurrentThread)" + and xf'=ret__int_' + and R="\s. ksSchedulerAction s = action \ weak_sch_act_wf action s" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (fastforce dest: rf_sr_sched_action_relation + simp: cscheduler_action_relation_def weak_sch_act_wf_def false_def + intro!: tcb_at_not_NULL + split: scheduler_action.splits) apply ceqv - apply (unfold split_def)[1] - apply (rule ccorres_when[where R=\]) - apply (intro allI impI) - apply (unfold mem_simps)[1] - apply assumption - apply (ctac add: rescheduleRequired_ccorres) - prefer 4 - apply (rule ccorres_symb_exec_l) - apply (rule ccorres_pre_getCurThread) - apply (rule ccorres_symb_exec_l) - apply (rule_tac P="\s. st_tcb_at' (\st. runnable' st = runnable) thread s - \ curThread = ksCurThread s - \ action = ksSchedulerAction s - \ (\t. ksSchedulerAction s = SwitchToThread t \ tcb_at' t s)" - and P'=UNIV in ccorres_from_vcg) - apply (rule allI, rule conseqPre, vcg) - apply (clarsimp simp: return_def split del: if_split) - apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread) - apply (rule conjI) - apply (clarsimp simp: st_tcb_at'_def) - apply (drule (1) obj_at_cslift_tcb) - apply (clarsimp simp: typ_heap_simps) - apply (subgoal_tac "ksSchedulerAction \ = ResumeCurrentThread") - apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def) - apply (case_tac "tcbState ko", simp_all add: ThreadState_defs)[1] - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - cscheduler_action_relation_def tcb_at_not_NULL - split: scheduler_action.split_asm) - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - cscheduler_action_relation_def) - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - cscheduler_action_relation_def) - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - cscheduler_action_relation_def tcb_at_not_NULL - split: scheduler_action.split_asm) - apply wp+ - apply (simp add: isRunnable_def isStopped_def) - apply (simp add: guard_is_UNIV_def) + apply (rule ccorres_cond_seq) + apply (rule_tac P="action = ResumeCurrentThread" in ccorres_cases; clarsimp) + apply ccorres_rewrite + apply (rule ccorres_rhs_assoc) + apply (ctac (no_vcg) add: isSchedulable_ccorres) + apply csymbr + apply (clarsimp simp: when_def) + apply (rule ccorres_cond[where R=\]) + apply (fastforce simp: to_bool_def) + apply (ctac (no_vcg) add: rescheduleRequired_ccorres) + apply (rule ccorres_return_Skip) + apply (wpsimp wp: isSchedulable_wp) + apply ccorres_rewrite + apply (rule ccorres_cond_false) + apply (rule ccorres_symb_exec_l') + apply (rule ccorres_return_Skip) + apply wpsimp+ + apply vcg + apply ccorres_rewrite + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond_false) + apply ccorres_rewrite + apply (rule ccorres_cond_false) + apply (rule ccorres_symb_exec_l') + apply (rule ccorres_return_Skip) + apply wpsimp+ + apply vcg apply clarsimp - apply (clarsimp simp: st_tcb_at'_def obj_at'_def weak_sch_act_wf_def) - done *) - -lemma scheduleTCB_ccorres_valid_queues'_pre: - "ccorresG rf_sr \ dc xfdc - (tcb_at' thread and valid_objs') - (UNIV \ \\tptr = tcb_ptr_to_ctcb_ptr thread\) [] - (scheduleTCB thread) - (Call scheduleTCB_'proc)" - by (fastforce intro: scheduleTCB_ccorres' ccorres_guard_imp) - -lemmas scheduleTCB_ccorres_valid_queues' - = scheduleTCB_ccorres_valid_queues'_pre[unfolded bind_assoc return_bind split_conv] + done -lemma rescheduleRequired_ccorres_valid_queues'_simple: - "ccorresG rf_sr \ dc xfdc sch_act_simple UNIV [] +lemma rescheduleRequired_ccorres_simple: + "ccorres dc xfdc sch_act_simple UNIV [] rescheduleRequired (Call rescheduleRequired_'proc)" -sorry (* FIXME RT: rescheduleRequired_ccorres_valid_queues'_simple *) (* apply cinit - apply (rule ccorres_symb_exec_l) - apply (rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc]) - apply (simp add: scheduler_action_case_switch_to_if - cong: if_weak_cong split del: if_split) - apply (rule_tac R="\s. action = ksSchedulerAction s \ sch_act_simple s" - in ccorres_cond) - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - cscheduler_action_relation_def) - apply (clarsimp simp: weak_sch_act_wf_def tcb_at_1 tcb_at_not_NULL - split: scheduler_action.split_asm dest!: st_tcb_strg'[rule_format]) - apply (ctac add: tcbSchedEnqueue_ccorres) - apply (rule ccorres_return_Skip) - apply ceqv - apply (rule ccorres_from_vcg[where P=\ and P'=UNIV]) - apply (rule allI, rule conseqPre, vcg) - apply (clarsimp simp: setSchedulerAction_def simpler_modify_def) - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - cscheduler_action_relation_def - carch_state_relation_def cmachine_state_relation_def - ) - apply wp - apply (simp add: guard_is_UNIV_def) - apply wp+ - apply (simp add: getSchedulerAction_def) - apply (clarsimp simp: weak_sch_act_wf_def rf_sr_def cstate_relation_def - Let_def cscheduler_action_relation_def) - by (auto simp: tcb_at_not_NULL tcb_at_1 - tcb_at_not_NULL[THEN not_sym] tcb_at_1[THEN not_sym] - split: scheduler_action.split_asm) *) - -lemma scheduleTCB_ccorres_valid_queues'_pre_simple: - "ccorresG rf_sr \ dc xfdc - (tcb_at' thread) - (UNIV \ \\tptr = tcb_ptr_to_ctcb_ptr thread\) [] - (scheduleTCB thread) - (Call scheduleTCB_'proc)" -sorry (* FIXME RT: scheduleTCB_ccorres_valid_queues'_pre_simple *) (* - apply (cinit' lift: tptr_' simp del: word_neq_0_conv) + apply (rule ccorres_pre_getSchedulerAction) apply (rule ccorres_rhs_assoc2)+ - apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) - defer + apply (rule_tac xf'=xfdc in ccorres_split_nothrow) + apply (subst scheduler_action_case_switch_to_if) + apply (rule ccorres_rhs_assoc) + apply (rule_tac val=0 + and xf'=ret__int_' + and R=sch_act_simple + in ccorres_symb_exec_r_known_rv) + apply vcg + subgoal + by (fastforce dest: rf_sr_sched_action_relation + simp: cscheduler_action_relation_def split: scheduler_action.splits) + apply ceqv + apply (rule ccorres_cond_seq) + apply (rule_tac R="\s. ksSchedulerAction s = action \ sch_act_simple s" in ccorres_cond) + apply (clarsimp simp: sch_act_simple_def) + apply (rule ccorres_empty) + apply ccorres_rewrite + apply (rule ccorres_cond_false) + apply (rule ccorres_return_Skip) + apply vcg + apply ceqv + apply (rule ccorres_setSchedulerAction, simp add: cscheduler_action_relation_def) + apply wpsimp + apply (vcg exspec=isSchedulable_modifies exspec=tcbSchedEnqueue_modifies) + apply fastforce + done + +lemma scheduleTCB_ccorres_simple: + "ccorres dc xfdc + ((\s. weak_sch_act_wf (ksSchedulerAction s) s) + and tcb_at' thread and sch_act_simple and no_0_obj') + \\tptr = tcb_ptr_to_ctcb_ptr thread\ [] + (scheduleTCB thread) (Call scheduleTCB_'proc)" + supply Collect_const[simp del] + if_split[split del] + apply (cinit lift: tptr_') + apply (rule ccorres_pre_getCurThread, rename_tac curThread) + apply (rule_tac val="from_bool (thread = curThread)" + and xf'=ret__int_' + and R="\s. ksCurThread s = curThread" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (fastforce dest: rf_sr_ksCurThread simp: from_bool_def split: bool.splits) + apply ceqv + apply (rule ccorres_pre_getSchedulerAction, rename_tac action) + apply (rule ccorres_cond_seq) + apply (rule_tac P="thread = curThread" in ccorres_cases; clarsimp) + apply ccorres_rewrite + apply (rule_tac val="from_bool (action = ResumeCurrentThread)" + and xf'=ret__int_' + and R="\s. ksSchedulerAction s = action \ weak_sch_act_wf action s" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (fastforce dest: rf_sr_sched_action_relation + simp: cscheduler_action_relation_def weak_sch_act_wf_def false_def + intro!: tcb_at_not_NULL + split: scheduler_action.splits) apply ceqv - apply (unfold split_def)[1] - apply (rule ccorres_when[where R=\]) - apply (intro allI impI) - apply (unfold mem_simps)[1] - apply assumption - apply (ctac add: rescheduleRequired_ccorres_valid_queues'_simple) - prefer 4 - apply (rule ccorres_symb_exec_l) - apply (rule ccorres_pre_getCurThread) - apply (rule ccorres_symb_exec_l) - apply (rule_tac P="\s. st_tcb_at' (\st. runnable' st = runnable) thread s - \ curThread = ksCurThread s - \ action = ksSchedulerAction s - \ sch_act_simple s" - and P'=UNIV in ccorres_from_vcg) - apply (rule allI, rule conseqPre, vcg) - apply (clarsimp simp: return_def if_1_0_0 split del: if_split) - apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread) - apply (rule conjI) - apply (clarsimp simp: st_tcb_at'_def) - apply (drule (1) obj_at_cslift_tcb) - apply (clarsimp simp: typ_heap_simps) - apply (subgoal_tac "ksSchedulerAction \ = ResumeCurrentThread") - apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def) - apply (case_tac "tcbState ko", simp_all add: ThreadState_defs)[1] - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - cscheduler_action_relation_def - tcb_at_not_NULL - split: scheduler_action.split_asm) - apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def - cscheduler_action_relation_def) - apply wp+ - apply (simp add: isRunnable_def isStopped_def) - apply (simp add: guard_is_UNIV_def) + apply (rule ccorres_cond_seq) + apply (rule_tac P="action = ResumeCurrentThread" in ccorres_cases; clarsimp) + apply ccorres_rewrite + apply (rule ccorres_rhs_assoc) + apply (ctac (no_vcg) add: isSchedulable_ccorres) + apply csymbr + apply (clarsimp simp: when_def) + apply (rule ccorres_cond[where R=\]) + apply (fastforce simp: to_bool_def) + apply (ctac (no_vcg) add: rescheduleRequired_ccorres_simple) + apply (rule ccorres_return_Skip) + apply (wpsimp wp: isSchedulable_wp) + apply ccorres_rewrite + apply (rule ccorres_cond_false) + apply (rule ccorres_symb_exec_l') + apply (rule ccorres_return_Skip) + apply wpsimp+ + apply vcg + apply ccorres_rewrite + apply (rule ccorres_cond_seq) + apply (rule ccorres_cond_false) + apply ccorres_rewrite + apply (rule ccorres_cond_false) + apply (rule ccorres_symb_exec_l') + apply (rule ccorres_return_Skip) + apply wpsimp+ + apply vcg apply clarsimp - apply (clarsimp simp: st_tcb_at'_def obj_at'_def valid_queues'_def) - done *) - -lemmas scheduleTCB_ccorres_valid_queues'_simple - = scheduleTCB_ccorres_valid_queues'_pre_simple[unfolded bind_assoc return_bind split_conv] - -lemmas scheduleTCB_ccorres[corres] - = scheduleTCB_ccorres'[unfolded bind_assoc return_bind split_conv] - -lemma threadSet_weak_sch_act_wf_runnable': - "\ \s. (ksSchedulerAction s = SwitchToThread thread \ runnable' st) \ weak_sch_act_wf (ksSchedulerAction s) s \ - threadSet (tcbState_update (\_. st)) thread - \ \rv s. weak_sch_act_wf (ksSchedulerAction s) s \" - apply (simp add: weak_sch_act_wf_def) - apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift threadSet_pred_tcb_at_state - threadSet_tcbDomain_triv) - apply simp - apply (clarsimp) -done + done lemma setThreadState_ccorres[corres]: "ccorres dc xfdc - (\s. tcb_at' thread s \ valid_objs' s \ valid_tcb_state' st s) - ({s'. (\cl fl. cthread_state_relation_lifted st (cl\tsType_CL := ts_' s' && mask 4\, fl))} - \ {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) hs + (\s. tcb_at' thread s \ valid_objs' s \ valid_tcb_state' st s + \ weak_sch_act_wf (ksSchedulerAction s) s \ no_0_obj' s + \ pspace_aligned' s \ pspace_distinct' s) + (\\cl fl. cthread_state_relation_lifted st (cl\tsType_CL := \ts && mask 4\, fl)\ + \ \\tptr = tcb_ptr_to_ctcb_ptr thread\) hs (setThreadState st thread) (Call setThreadState_'proc)" apply (cinit lift: tptr_' cong add: call_ignore_cong) apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres) apply (ctac add: scheduleTCB_ccorres) - apply (wp threadSet_weak_sch_act_wf_runnable' - threadSet_valid_objs') - by (clarsimp simp: weak_sch_act_wf_def valid_tcb'_tcbState_update) - -lemma setThreadState_ccorres_valid_queues': - "ccorres dc xfdc - (\s. tcb_at' thread s \ valid_objs' s \ valid_tcb_state' st s) - ({s'. (\cl fl. cthread_state_relation_lifted st (cl\tsType_CL := ts_' s' && mask 4\, fl))} - \ {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) [] - (setThreadState st thread) (Call setThreadState_'proc)" - apply (cinit lift: tptr_' cong add: call_ignore_cong) - apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres) - apply (ctac add: scheduleTCB_ccorres_valid_queues') - apply (wp threadSet_weak_sch_act_wf_runnable' threadSet_valid_objs') - by (clarsimp simp: valid_tcb'_def tcb_cte_cases_def cteSizeBits_def) + apply (wp threadSet_valid_objs') + apply (clarsimp simp: weak_sch_act_wf_def valid_tcb'_tcbState_update) + done lemma simp_list_case_return: "(case x of [] \ return e | y # ys \ return f) = return (if x = [] then e else f)" by (clarsimp split: list.splits) -lemma cancelSignal_ccorres [corres]: - "ccorres dc xfdc - (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) - (UNIV \ {s. threadPtr_' s = tcb_ptr_to_ctcb_ptr thread} \ {s. ntfnPtr_' s = Ptr ntfn}) - [] (cancelSignal thread ntfn) (Call cancelSignal_'proc)" - apply (cinit lift: threadPtr_' ntfnPtr_' simp add: Let_def list_case_return cong add: call_ignore_cong) +lemma cancelSignal_ccorres[corres]: + "ccorres dc xfdc + (invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s) + and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) + (\\threadPtr = tcb_ptr_to_ctcb_ptr thread\ \ \\ntfnPtr = ntfn_Ptr ntfn\) [] + (cancelSignal thread ntfn) (Call cancelSignal_'proc)" + supply if_split[split del] + apply (cinit lift: threadPtr_' ntfnPtr_') apply (unfold fun_app_def) apply (simp only: simp_list_case_return return_bind ccorres_seq_skip) -sorry (* FIXME RT: cancelSignal_ccorres *) (* + apply (rule ccorres_stateAssert)+ apply (rule ccorres_pre_getNotification) apply (rule ccorres_assert) - apply (rule ccorres_rhs_assoc2) - apply (rule ccorres_rhs_assoc2) - apply (rule ccorres_rhs_assoc2) + apply (rule ccorres_rhs_assoc2)+ apply (ctac (no_vcg) add: cancelSignal_ccorres_helper) - apply (ctac add: setThreadState_ccorres_valid_queues') - apply ((wp setNotification_nosch hoare_vcg_all_lift set_ntfn_valid_objs' | simp add: valid_tcb_state'_def split del: if_split)+)[1] - apply (simp add: ThreadState_defs) - apply (rule conjI, clarsimp, rule conjI, clarsimp) - apply (frule (1) ko_at_valid_ntfn'[OF _ invs_valid_objs']) - subgoal by ((auto simp: obj_at'_def projectKOs st_tcb_at'_def invs'_def valid_state'_def - isTS_defs cte_wp_at_ctes_of - cthread_state_relation_def sch_act_wf_weak valid_ntfn'_def - | clarsimp simp: eq_commute)+) - apply (clarsimp) - apply (frule (1) ko_at_valid_ntfn'[OF _ invs_valid_objs']) - apply (frule (2) ntfn_blocked_in_queueD) - by (auto simp: obj_at'_def projectKOs st_tcb_at'_def invs'_def valid_state'_def - isTS_defs cte_wp_at_ctes_of valid_ntfn'_def - cthread_state_relation_def sch_act_wf_weak isWaitingNtfn_def - split: ntfn.splits option.splits - | clarsimp simp: eq_commute - | drule_tac x=thread in bspec)+ *) + apply (ctac add: setThreadState_ccorres) + apply (wp hoare_vcg_all_lift set_ntfn_valid_objs') + apply (simp add: "StrictC'_thread_state_defs") + apply clarsimp + apply (frule st_tcb_strg'[rule_format]) + apply (frule invs_valid_objs') + apply (clarsimp simp: sym_refs_asrt_def) + apply (rule conjI) + apply (frule (1) ntfn_ko_at_valid_objs_valid_ntfn') + apply (fastforce dest!: ntfn_blocked_in_queueD simp: valid_ntfn'_def isWaitingNtfn_def + split: ntfn.splits option.splits if_splits) + apply (clarsimp simp: weak_sch_act_wf_def st_tcb_at'_def obj_at'_def) + apply (case_tac" tcbState obj"; fastforce) + done (* FIXME: MOVE *) lemma ccorres_pre_getEndpoint [ccorres_pre]: @@ -2815,13 +2935,14 @@ sorry (* FIXME RT: reply_remove_ccorres *) lemma cancelIPC_ccorres1: assumes cteDeleteOne_ccorres: "\w slot. ccorres dc xfdc - (invs' and cte_wp_at' (\ct. w = -1 \ cteCap ct = NullCap + (invs' + and cte_wp_at' (\ct. w = -1 \ cteCap ct = NullCap \ (\cap'. ccap_relation (cteCap ct) cap' \ cap_get_tag cap' = w)) slot) ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w} \ {s. slot_' s = Ptr slot}) [] (cteDeleteOne slot) (Call cteDeleteOne_'proc)" shows - "ccorres dc xfdc (tcb_at' thread and invs') + "ccorres dc xfdc (tcb_at' thread and invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) (UNIV \ {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) [] (cancelIPC thread) (Call cancelIPC_'proc)" apply (cinit lift: tptr_' simp: Let_def cong: call_ignore_cong) diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index 002a44f6cd..2aa72f1165 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -4596,7 +4596,8 @@ lemma sendIPC_dequeue_ccorres_helper: lemma sendIPC_block_ccorres_helper: "ccorres dc xfdc (tcb_at' thread and valid_objs' and pspace_canonical' and sch_act_not thread and ep_at' epptr and - (\s. sch_act_wf (ksSchedulerAction s) s) and + (\s. sch_act_wf (ksSchedulerAction s) s) and no_0_obj' and + pspace_aligned' and pspace_distinct' and K (bos = ThreadState_BlockedOnSend \ epptr' = epptr \ badge' = badge \ cg = from_bool canGrant \ cgr = from_bool canGrantReply @@ -4654,8 +4655,8 @@ lemma sendIPC_block_ccorres_helper: split: bool.split) apply ceqv apply clarsimp - apply ctac - apply (wp threadSet_weak_sch_act_wf_runnable' threadSet_valid_objs') + apply (ctac add: scheduleTCB_ccorres) + apply (wp threadSet_valid_objs') apply (clarsimp simp: guard_is_UNIV_def) apply (clarsimp simp: sch_act_wf_weak valid_tcb'_def valid_tcb_state'_def tcb_cte_cases_def cteSizeBits_def) @@ -6333,6 +6334,7 @@ lemma receiveSignal_block_ccorres_helper: "ccorres dc xfdc (tcb_at' thread and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr and pspace_canonical' and (\s. sch_act_wf (ksSchedulerAction s) s) and + no_0_obj' and pspace_aligned' and pspace_distinct' and K (ntfnptr = ntfnptr && ~~ mask 4)) UNIV hs (setThreadState (Structures_H.thread_state.BlockedOnNotification @@ -6367,8 +6369,8 @@ lemma receiveSignal_block_ccorres_helper: apply (clarsimp simp: canonical_address_sign_extended sign_extended_iff_sign_extend) apply ceqv apply clarsimp - apply ctac - apply (wp hoare_vcg_all_lift threadSet_valid_objs' threadSet_weak_sch_act_wf_runnable') + apply (ctac add: scheduleTCB_ccorres) + apply (wp hoare_vcg_all_lift threadSet_valid_objs') apply (clarsimp simp: guard_is_UNIV_def) apply (auto simp: weak_sch_act_wf_def valid_tcb'_def tcb_cte_cases_def valid_tcb_state'_def obj_at'_is_canonical cteSizeBits_def) diff --git a/proof/crefine/RISCV64/Schedule_C.thy b/proof/crefine/RISCV64/Schedule_C.thy index f8b13bc7b6..4df6637ea4 100644 --- a/proof/crefine/RISCV64/Schedule_C.thy +++ b/proof/crefine/RISCV64/Schedule_C.thy @@ -514,6 +514,8 @@ lemma refill_size_length_scRefills_helper: simp: refillSizeBytes_def word_bits_def) done +crunch (empty_fail) empty_fail[wp]: getSchedContext + lemma refill_size_ccorres: "ccorres (\rv rv'. rv = unat rv') ret__unsigned_long_' (sc_at' scPtr and valid_objs' and valid_refills' scPtr) \\sc = Ptr scPtr\ [] diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy index 247713b59b..dd1ff4e115 100644 --- a/proof/crefine/RISCV64/Tcb_C.thy +++ b/proof/crefine/RISCV64/Tcb_C.thy @@ -1226,14 +1226,15 @@ crunches suspend lemma invokeTCB_CopyRegisters_ccorres: "ccorres (cintr \ (\rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') - (invs' and tcb_at' destn and tcb_at' source - and ex_nonz_cap_to' destn and ex_nonz_cap_to' source) - (UNIV \ {s. dest___ptr_to_struct_tcb_C_' s = tcb_ptr_to_ctcb_ptr destn} - \ {s. tcb_src_' s = tcb_ptr_to_ctcb_ptr source} - \ {s. to_bool (resumeTarget_' s) = resume} - \ {s. to_bool (suspendSource_' s) = susp} - \ {s. to_bool (transferFrame_' s) = frames} - \ {s. to_bool (transferInteger_' s) = ints}) [] + (invs' and sch_act_simple and (\s. weak_sch_act_wf (ksSchedulerAction s) s) + and tcb_at' destn and tcb_at' source + and ex_nonz_cap_to' destn and ex_nonz_cap_to' source) + (\\dest = tcb_ptr_to_ctcb_ptr destn\ + \ \\tcb_src = tcb_ptr_to_ctcb_ptr source\ + \ \to_bool \resumeTarget = resume\ + \ \to_bool \suspendSource = susp\ + \ \to_bool \transferFrame = frames\ + \ \to_bool \transferInteger = ints\) [] (invokeTCB (CopyRegisters destn source susp resume frames ints arch)) (Call invokeTCB_CopyRegisters_'proc)" apply (cinit lift: dest___ptr_to_struct_tcb_C_' tcb_src_' resumeTarget_' @@ -1317,16 +1318,17 @@ lemma invokeTCB_CopyRegisters_ccorres: apply (simp add: pred_conj_def guard_is_UNIV_def cong: if_cong | wp mapM_x_wp_inv hoare_drop_imp)+ apply clarsimp - apply (rule_tac Q="\rv. invs' and tcb_at' destn" + apply (rule_tac Q="\_. invs' and tcb_at' destn + and (\s. weak_sch_act_wf (ksSchedulerAction s) s)" in hoare_strengthen_post[rotated]) apply (fastforce simp: sch_act_wf_weak) apply (wpsimp wp: hoare_drop_imp restart_invs')+ apply (clarsimp simp add: guard_is_UNIV_def) apply (wp hoare_drop_imp hoare_vcg_if_lift)+ apply simp - apply (rule_tac Q="\rv. invs' and tcb_at' destn and ex_nonz_cap_to' destn" + apply (rule_tac Q="\rv. invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and tcb_at' destn and ex_nonz_cap_to' destn" in hoare_strengthen_post[rotated]) - apply (fastforce intro: global'_no_ex_cap) + apply (fastforce dest: global'_no_ex_cap) apply (wpsimp wp: hoare_drop_imp)+ apply (clarsimp simp add: guard_is_UNIV_def) apply (clarsimp simp: invs_valid_objs' @@ -1776,8 +1778,9 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]: lemma invokeTCB_Suspend_ccorres: "ccorres (cintr \ (\rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') - (invs' and tcb_at' t and ex_nonz_cap_to' t) - {s. thread_' s = tcb_ptr_to_ctcb_ptr t} [] + (invs' and sch_act_simple and (\s. weak_sch_act_wf (ksSchedulerAction s) s) + and tcb_at' t and ex_nonz_cap_to' t) + \\thread = tcb_ptr_to_ctcb_ptr t\ [] (invokeTCB (Suspend t)) (Call invokeTCB_Suspend_'proc)" apply (cinit lift: thread_') apply (simp add: liftE_def return_returnOk) @@ -1856,6 +1859,9 @@ lemma asUser_valid_ipc_buffer_ptr': "\ valid_ipc_buffer_ptr' p \ asUser t m \ \rv s. valid_ipc_buffer_ptr' p s \" by (simp add: valid_ipc_buffer_ptr'_def, wp, auto simp: valid_ipc_buffer_ptr'_def) +crunches setMessageInfo, storeWordUser + for weak_sch_act_wf[wp]: "\s. weak_sch_act_wf (ksSchedulerAction s) s" + lemma invokeTCB_ReadRegisters_ccorres: notes nat_min_simps [simp del] @@ -2186,7 +2192,7 @@ shows apply (clarsimp simp: ThreadState_defs mask_def) apply (rule mapM_x_wp') apply (rule hoare_pre) - apply (wpsimp wp: sch_act_wf_lift tcb_in_cur_domain'_lift) + apply (wpsimp wp: weak_sch_act_wf_lift tcb_in_cur_domain'_lift) apply fastforce apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem) apply (simp add: message_info_to_H_def) @@ -2254,7 +2260,8 @@ shows apply wp apply (simp add: Collect_const_mem ThreadState_defs mask_def) apply vcg - apply (rule_tac Q="\_. invs' and st_tcb_at' ((=) Restart) thread and tcb_at' target" + apply (rule_tac Q="\_. invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s) + and st_tcb_at' ((=) Restart) thread and tcb_at' target" in hoare_post_imp) apply (clarsimp simp: pred_tcb_at') apply (auto elim!: pred_tcb'_weakenE)[1] diff --git a/proof/refine/RISCV64/InterruptAcc_R.thy b/proof/refine/RISCV64/InterruptAcc_R.thy index d79fa73135..ad53540791 100644 --- a/proof/refine/RISCV64/InterruptAcc_R.thy +++ b/proof/refine/RISCV64/InterruptAcc_R.thy @@ -284,14 +284,6 @@ lemma get_sc_active_sp: apply (clarsimp simp: obj_at_def active_sc_def) done -lemma scActive_sp: - "\P\ - scActive scPtr - \\rv s. P s \ (\sc. ko_at' sc scPtr s \ rv = (0 < scRefillMax sc))\" - apply wpsimp - 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" @@ -306,9 +298,6 @@ 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: diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy index ce2277e47a..19bbd05119 100644 --- a/proof/refine/RISCV64/IpcCancel_R.thy +++ b/proof/refine/RISCV64/IpcCancel_R.thy @@ -360,13 +360,14 @@ lemma blocked_cancelIPC_corres: lemma cancelSignal_corres: "corres dc - (invs and valid_ready_qs and st_tcb_at ((=) (Structures_A.BlockedOnNotification ntfn)) t) - (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) t) - (cancel_signal t ntfn) - (cancelSignal t ntfn)" + (invs and valid_ready_qs and st_tcb_at ((=) (Structures_A.BlockedOnNotification ntfn)) t) + (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) t) + (cancel_signal t ntfn) (cancelSignal t ntfn)" apply add_sym_refs apply add_ready_qs_runnable apply (simp add: cancel_signal_def cancelSignal_def Let_def) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (clarsimp simp: sym_refs_asrt_def) apply (rule corres_stateAssert_add_assertion[rotated]) apply clarsimp apply (rule corres_guard_imp) @@ -1775,7 +1776,7 @@ lemma cancelSignal_invs': done show ?thesis apply (simp add: cancelSignal_def invs'_def Let_def valid_dom_schedule'_def) - apply (rule bind_wp[OF _ stateAssert_sp]) + apply (intro bind_wp[OF _ stateAssert_sp]) apply (wp valid_irq_node_lift sts_sch_act' irqs_masked_lift hoare_vcg_all_lift [OF set_ntfn'.ksReadyQueues] setThreadState_ct_not_inQ NTFNSN set_ntfn'.get_wp @@ -1996,10 +1997,8 @@ lemma cancelIPC_st_tcb_at: done lemma weak_sch_act_wf_lift_linear: - "\ \t. \\s. sa s \ SwitchToThread t\ f \\rv s. sa s \ SwitchToThread t\; - \t. \st_tcb_at' runnable' t\ f \\rv. st_tcb_at' runnable' t\; - \t. \tcb_in_cur_domain' t\ f \\rv. tcb_in_cur_domain' t\ \ - \ \\s. weak_sch_act_wf (sa s) s\ f \\rv s. weak_sch_act_wf (sa s) s\" + "\ \t. f \\s. sa s \ SwitchToThread t\; \t. f \tcb_at' t\ \ + \ f \\s. weak_sch_act_wf (sa s) s\" apply (simp only: weak_sch_act_wf_def imp_conv_disj) apply (intro hoare_vcg_all_lift hoare_vcg_disj_lift hoare_vcg_conj_lift) apply simp_all @@ -2069,17 +2068,12 @@ lemma setObject_ntfn_sa_unchanged[wp]: done lemma setNotification_weak_sch_act_wf[wp]: - "\\s. weak_sch_act_wf (ksSchedulerAction s) s\ - setNotification ntfnptr ntfn - \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" - apply (wp hoare_vcg_all_lift hoare_convert_imp hoare_vcg_conj_lift - | simp add: weak_sch_act_wf_def st_tcb_at'_def tcb_in_cur_domain'_def)+ - apply wps - apply (wpsimp simp: o_def)+ - done + "setNotification ntfnptr ntfn \\s. weak_sch_act_wf (ksSchedulerAction s) s\" + by (wpsimp wp: hoare_vcg_all_lift hoare_convert_imp hoare_vcg_conj_lift + simp: weak_sch_act_wf_def)+ lemmas ipccancel_weak_sch_act_wfs - = weak_sch_act_wf_lift[OF _ setCTE_pred_tcb_at'] + = weak_sch_act_wf_lift[OF _ setCTE.typ_at_lifts_all'(1)] (* prevents wp from splitting on the when; stronger technique than hoare_when_weak_wp FIXME: possible to replace with hoare_when_weak_wp? @@ -2802,47 +2796,11 @@ lemma ep'_Idle_case_helper: "(case ep of IdleEP \ a | _ \ b) = (if (ep = IdleEP) then a else b)" by (cases ep, simp_all) -lemma rescheduleRequired_notresume: - "\\s. ksSchedulerAction s \ ResumeCurrentThread\ - rescheduleRequired \\_ s. ksSchedulerAction s = ChooseNewThread\" - proof - - have ssa: "\\\ setSchedulerAction ChooseNewThread - \\_ s. ksSchedulerAction s = ChooseNewThread\" - by (simp add: setSchedulerAction_def | wp)+ - show ?thesis - by (simp add: rescheduleRequired_def, wp ssa) - qed - -lemma setThreadState_ResumeCurrentThread_imp_notct[wp]: - "\\s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\ - setThreadState st t - \\_ s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\" - (is "\?PRE\ _ \_\") -proof - - have nrct: - "\\s. ksSchedulerAction s \ ResumeCurrentThread\ - rescheduleRequired - \\_ s. ksSchedulerAction s \ ResumeCurrentThread\" - by (rule hoare_strengthen_post [OF rescheduleRequired_notresume], simp) - show ?thesis - apply (simp add: setThreadState_def scheduleTCB_def) - apply (wpsimp wp: hoare_vcg_imp_lift [OF nrct] isSchedulable_wp hoare_vcg_if_lift2) - apply (rule_tac Q="\_. ?PRE" in hoare_post_imp) - apply clarsimp - apply (rule hoare_convert_imp [OF threadSet.ksSchedulerAction threadSet.ct]) - apply assumption - done -qed - lemma replyUnlink_valid_irq_node'[wp]: "replyUnlink r t \\ s. valid_irq_node' (irq_node' s) s\" unfolding replyUnlink_def by (wpsimp wp: valid_irq_node_lift gts_wp') -lemma weak_sch_act_wf_D1: - "weak_sch_act_wf sa s \ (\t. sa = SwitchToThread t \ st_tcb_at' runnable' t s)" - by (simp add: weak_sch_act_wf_def) - lemma updateSchedContext_valid_pspace'[wp]: "\valid_pspace' and (\s. \sc. (valid_sched_context' sc s \ valid_sched_context' (f sc) s) @@ -2970,7 +2928,7 @@ lemma cancel_all_invs'_helper: hoare_vcg_const_Ball_lift sts_st_tcb' possibleSwitchTo_sch_act_not_other) apply (wpsimp wp: valid_irq_node_lift hoare_vcg_const_Ball_lift sts_st_tcb' sts_sch_act' - split: if_splits | strengthen weak_sch_act_wf_D1)+ + split: if_splits) apply (wp hoare_drop_imp) apply (wpsimp wp: hoare_vcg_const_Ball_lift hoare_vcg_all_lift gts_wp' hoare_vcg_imp_lift replyUnlink_valid_objs' replyUnlink_st_tcb_at' @@ -3079,7 +3037,7 @@ lemma ct_not_in_ntfnQueue: lemma sch_act_wf_weak[elim!]: "sch_act_wf sa s \ weak_sch_act_wf sa s" - by (case_tac sa, (simp add: weak_sch_act_wf_def)+) + by (case_tac sa, (fastforce simp: weak_sch_act_wf_def st_tcb_at'_def obj_at'_def)+) crunches setEndpoint, setNotification for sym_heap_sched_pointers[wp]: sym_heap_sched_pointers diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index dce4d16a6b..9f00194b12 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -1865,48 +1865,10 @@ crunches unbindMaybeNotification, schedContextMaybeUnbindNtfn, isFinalCapability for sch_act_not[wp]: "sch_act_not t" (wp: crunch_wps simp: crunch_simps) -crunches replyRemove, replyRemoveTCB +crunches replyRemove, replyRemoveTCB, cancelSignal, cancelIPC, replyClear, cteDeleteOne for weak_sch_act_wf[wp]: "\s. weak_sch_act_wf (ksSchedulerAction s) s" (simp: crunch_simps wp: crunch_wps) -lemma cancelSignal_weak_sch_act_wf[wp]: - "\\s. weak_sch_act_wf (ksSchedulerAction s) s \ sch_act_not threadPtr s\ - cancelSignal threadPtr ntfnPtr - \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" - unfolding cancelSignal_def Let_def - by (wpsimp wp: gts_wp' | wp (once) hoare_drop_imp)+ - -lemma cancelIPC_weak_sch_act_wf[wp]: - "\\s. weak_sch_act_wf (ksSchedulerAction s) s \ sch_act_not tptr s\ - cancelIPC tptr - \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" - unfolding cancelIPC_def blockedCancelIPC_def Let_def getBlockingObject_def - apply (wpsimp wp: gts_wp' threadSet_weak_sch_act_wf hoare_vcg_all_lift - | wp (once) hoare_drop_imps)+ - done - -lemma replyClear_weak_sch_act_wf[wp]: - "\\s. weak_sch_act_wf (ksSchedulerAction s) s\ - replyClear rptr tptr - \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" - unfolding replyClear_def - apply (wpsimp wp: gts_wp' simp: pred_tcb_at'_eq_commute) - apply (auto simp: pred_tcb_at'_def obj_at'_def weak_sch_act_wf_def) - done - -crunches finaliseCapTrue_standin - for weak_sch_act_wf[wp]: "\s. weak_sch_act_wf (ksSchedulerAction s) s" - (simp: crunch_simps wp: crunch_wps) - -lemma cteDeleteOne_weak_sch_act[wp]: - "\\s. weak_sch_act_wf (ksSchedulerAction s) s\ - cteDeleteOne sl - \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" - apply (simp add: cteDeleteOne_def unless_def) - apply (wp hoare_drop_imps finaliseCapTrue_standin_cur' isFinalCapability_cur' - | simp add: split_def)+ - done - context begin interpretation Arch . (*FIXME: arch_split*) crunches handleFaultReply @@ -4598,51 +4560,6 @@ crunches cleanReply for schedulerAction[wp]: "\s. P (ksSchedulerAction s)" (simp: crunch_simps) -lemma replyUnlink_ResumeCurrentThread_imp_notct[wp]: - "\\s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\ - replyUnlink a b - \\_ s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\" - apply (clarsimp simp: replyUnlink_def updateReply_def) - apply (wpsimp wp: set_reply'.set_wp gts_wp') - done - -lemma replyRemoveTCB_ResumeCurrentThread_imp_notct[wp]: - "\\s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\ - replyRemoveTCB tptr - \\_ s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\" - apply (clarsimp simp: replyRemoveTCB_def) - apply (rule bind_wp_fwd_skip, solves \wpsimp wp: getEndpoint_wp\)+ - apply (rule bind_wp_fwd_skip) - apply (clarsimp simp: when_def) - apply (intro conjI impI) - apply (wpsimp wp: set_sc'.set_wp set_reply'.set_wp hoare_vcg_imp_lift')+ - done - -lemma cancelSignal_ResumeCurrentThread_imp_notct[wp]: - "cancelSignal t ntfn \\s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\" - (is "\?PRE t'\ _ \_\") - apply (simp add: cancelSignal_def) - apply wp[1] - apply (wp hoare_convert_imp)+ - apply (rule_tac P="\s. ksSchedulerAction s \ ResumeCurrentThread" - in hoare_weaken_pre) - apply (wpc) - apply (wp | simp)+ - apply (wpc, wp+) - apply (rule_tac Q="\_. ?PRE t'" in hoare_post_imp, clarsimp) - apply (wpsimp wp: stateAssert_wp)+ - done - -lemma blockedCancelIPC_ResumeCurrentThread_imp_notct[wp]: - "blockedCancelIPC a b c \\s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\" - unfolding blockedCancelIPC_def getBlockingObject_def - apply (wpsimp wp: hoare_vcg_imp_lift' getEndpoint_wp) - done - -crunches cancelIPC - for ResumeCurrentThread_imp_notct[wp]: "\s. ksSchedulerAction s = ResumeCurrentThread - \ ksCurThread s \ t" - lemma tcbEPFindIndex_wp: "\\s. (\i j. 0 \ i \ i \ Suc sz \ (\tcb tcba. ko_at' tcb tptr s \ ko_at' tcba (queue ! j) s \ diff --git a/proof/refine/RISCV64/Reply_R.thy b/proof/refine/RISCV64/Reply_R.thy index d36c2713ae..bb8f187381 100644 --- a/proof/refine/RISCV64/Reply_R.thy +++ b/proof/refine/RISCV64/Reply_R.thy @@ -593,7 +593,7 @@ lemma replyUnlink_weak_sch_act_wf[wp]: "replyUnlink r t \\s. weak_sch_act_wf (ksSchedulerAction s) s\" apply (simp only: replyUnlink_def liftM_def) apply (wpsimp wp: sts_sch_act' gts_wp') - by (fastforce simp: replyUnlink_assertion_def st_tcb_at'_def obj_at'_def weak_sch_act_wf_def) + done lemma replyRemoveTCB_sch_act_wf: "replyRemoveTCB tptr \\s. sch_act_wf (ksSchedulerAction s) s\" diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index ef6fdf712a..756ef3d148 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -2673,32 +2673,22 @@ lemma rescheduleRequired_sch_act_sane[wp]: crunch sch_act_sane[wp]: setThreadState, setBoundNotification "sch_act_sane" (simp: crunch_simps wp: crunch_wps) -lemma weak_sch_act_wf_at_cross: +lemma weak_sch_act_wf_cross: assumes sr: "(s,s') \ state_relation" assumes aligned: "pspace_aligned s" assumes distinct: "pspace_distinct s" - assumes t: "valid_sched_action s" + assumes t: "weak_valid_sched_action s" shows "weak_sch_act_wf (ksSchedulerAction s') s'" using assms - apply (clarsimp simp: valid_sched_action_def weak_valid_sched_action_def weak_sch_act_wf_def) + apply (clarsimp simp: weak_valid_sched_action_def weak_sch_act_wf_def) apply (frule state_relation_sched_act_relation) apply (rename_tac t) apply (drule_tac x=t in spec) apply (prop_tac "scheduler_action s = switch_thread t") - apply (metis sched_act_relation.simps Structures_A.scheduler_action.exhaust - scheduler_action.simps) - apply (intro conjI impI) - apply (rule st_tcb_at_runnable_cross; fastforce?) - apply (clarsimp simp: vs_all_heap_simps pred_tcb_at_def obj_at_def) - apply (clarsimp simp: switch_in_cur_domain_def in_cur_domain_def etcb_at_def vs_all_heap_simps) - apply (prop_tac "tcb_at t s") - apply (clarsimp simp: obj_at_def is_tcb_def) - apply (frule state_relation_pspace_relation) - apply (frule (3) tcb_at_cross) - apply (clarsimp simp: tcb_in_cur_domain'_def obj_at'_def) - apply (frule curdomain_relation) - apply (frule (2) pspace_relation_tcb_domain_priority) - apply simp + subgoal + by (metis sched_act_relation.simps Structures_A.scheduler_action.exhaust + scheduler_action.simps) + apply (auto simp: obj_at_def is_tcb_def vs_all_heap_simps intro: tcb_at_cross) done lemma tcb_sched_enqueue_in_correct_ready_q[wp]: @@ -3347,6 +3337,14 @@ lemma threadGet_wp': apply (wp getObject_tcb_wp) done +crunches setEndpoint, setReply, setNotification + for weak_sch_act_wf[wp]: "\s. weak_sch_act_wf (ksSchedulerAction s) s" + (wp: weak_sch_act_wf_lift) + +crunches restart, suspend + for weak_sch_act_wf[wp]: "\s. weak_sch_act_wf (ksSchedulerAction s) s" + (wp: crunch_wps simp: crunch_simps) + lemma setNextInterrupt_corres: "corres dc ((\s. active_sc_tcb_at (cur_thread s) s) and (\s. \t \ set (release_queue s). active_sc_tcb_at t s) @@ -3633,14 +3631,6 @@ lemma no_fail_getRefillHead[wp]: apply (erule no_ofailD[OF no_ofail_readRefillHead]) done -lemma no_ofail_readScActive[wp]: - "no_ofail (sc_at' scPtr) (readScActive scPtr)" - unfolding readScActive_def readSchedContext_def - by (wpsimp wp_del: ovalid_readObject) - -lemmas no_fail_scActive[wp] = - no_ofail_gets_the[OF no_ofail_readScActive, simplified scActive_def[symmetric]] - lemma no_fail_refillPopHead[wp]: "no_fail (sc_at' scPtr) (refillPopHead scPtr)" by (wpsimp simp: refillPopHead_def obj_at'_def opt_map_def opt_pred_def objBits_simps @@ -5028,22 +5018,19 @@ lemma schedule_corres: apply fastforce apply (wpsimp wp: awaken_invs') apply (corresKsimp corres: awaken_corres) - apply (fastforce intro: weak_sch_act_wf_at_cross dest: valid_sched_valid_ready_qs - simp: invs_def valid_state_def) + apply (fastforce dest: valid_sched_valid_ready_qs simp: invs_def valid_state_def) apply (rule corres_split_skip) apply (wpsimp wp: hoare_vcg_imp_lift' cur_sc_active_lift) apply wpsimp apply (corresKsimp corres: checkDomainTime_corres) - apply (fastforce intro: weak_sch_act_wf_at_cross dest: valid_sched_valid_ready_qs - simp: invs_def valid_state_def) + apply (fastforce dest: valid_sched_valid_ready_qs simp: invs_def valid_state_def) apply (rule corres_underlying_split[rotated 2, OF gets_sp getCurThread_sp]) apply corresKsimp apply clarsimp apply (rename_tac curThread) apply (rule corres_underlying_split[rotated 2, OF is_schedulable_sp' isSchedulable_sp]) apply (corresKsimp corres: isSchedulable_corres) - apply (fastforce intro: weak_sch_act_wf_at_cross - simp: invs_def valid_state_def state_relation_def cur_tcb_def) + apply (fastforce simp: invs_def valid_state_def state_relation_def cur_tcb_def) apply (rule corres_underlying_split[rotated 2, OF gets_sp getSchedulerAction_sp]) apply (corresKsimp corres: getSchedulerAction_corres) diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy index 808b276a3e..0e61a34924 100644 --- a/proof/refine/RISCV64/TcbAcc_R.thy +++ b/proof/refine/RISCV64/TcbAcc_R.thy @@ -2586,10 +2586,8 @@ lemma tcbSchedEnqueue_corres: by (auto dest!: hd_in_set simp: inQ_def in_opt_pred opt_map_def fun_upd_apply split: if_splits option.splits) -definition - weak_sch_act_wf :: "scheduler_action \ kernel_state \ bool" -where - "weak_sch_act_wf sa = (\s. \t. sa = SwitchToThread t \ st_tcb_at' runnable' t s \ tcb_in_cur_domain' t s)" +definition weak_sch_act_wf :: "scheduler_action \ kernel_state \ bool" where + "weak_sch_act_wf sa s \ \t. sa = SwitchToThread t \ tcb_at' t s" lemma weak_sch_act_wf_updates[simp]: "\f. weak_sch_act_wf sa (ksDomainTime_update f s) = weak_sch_act_wf sa s" @@ -2703,36 +2701,94 @@ lemma isRunnable_corres: apply (clarsimp simp: obj_at'_weaken) done +lemma scActive_sp: + "\P\ scActive scPtr \\rv s. P s \ (\sc. ko_at' sc scPtr s \ rv = (0 < scRefillMax sc))\" + apply wpsimp + apply (clarsimp simp: obj_at'_def) + done + +lemma pspace_relation_sc_relation: + "\pspace_relation (kheap s) (ksPSpace s'); kheap s ptr = Some (Structures_A.SchedContext sc n); + ksPSpace s' ptr = Some (KOSchedContext sc')\ + \ sc_relation sc n sc'" + apply (clarsimp simp: pspace_relation_def) + apply (drule_tac x=ptr in bspec) + apply (fastforce simp: obj_at_def) + apply (clarsimp simp: obj_at_def obj_at'_def split: if_splits) + done + +lemma no_ofail_readScActive[wp]: + "no_ofail (sc_at' scPtr) (readScActive scPtr)" + unfolding readScActive_def readSchedContext_def + by (wpsimp wp_del: ovalid_readObject) + +lemmas no_fail_scActive[wp] = + no_ofail_gets_the[OF no_ofail_readScActive, simplified scActive_def[symmetric]] + +crunches inReleaseQueue + for inv[wp]: P + +defs sc_at'_asrt_def: + "sc_at'_asrt \ \scPtr s. sc_at' scPtr s" + +lemma ko_at'_valid_tcbs'_valid_tcb': + "\ko_at' ko ptr s; valid_tcbs' s\ \ valid_tcb' ko s" + by (fastforce simp: valid_tcbs'_def obj_at'_def) + +defs valid_tcbs'_asrt_def: + "valid_tcbs'_asrt \ valid_tcbs'" + lemma isSchedulable_corres: "corres (=) - (valid_tcbs and pspace_aligned and pspace_distinct and tcb_at t) - valid_tcbs' - (is_schedulable t) - (isSchedulable t)" + (valid_tcbs and pspace_aligned and pspace_distinct and tcb_at t) valid_tcbs' + (is_schedulable t) (isSchedulable t)" apply (rule corres_cross_add_guard[where Q'="tcb_at' t"]) apply (fastforce intro: tcb_at_cross) - unfolding is_schedulable_def isSchedulable_def fun_app_def - apply (rule corres_guard_imp) - apply (rule corres_split[OF getObject_TCB_corres]) - apply (rename_tac tcb_abs tcb_conc) - apply (rule corres_if[OF _ corres_return_eq_same]) - apply (clarsimp simp: tcb_relation_def Option.is_none_def) - apply simp - apply (rule corres_split[OF get_sc_corres[THEN equify]]) - apply (clarsimp simp: tcb_relation_def) - apply (rename_tac sc_abs sc_conc) - apply (rule corres_split[OF isRunnable_corres]) - apply assumption - apply (rule corres_split[OF inReleaseQueue_corres]) - apply (clarsimp simp: sc_relation_def active_sc_def) - apply blast - apply wp+ - apply (wpsimp simp: pred_conj_def - wp: hoare_vcg_if_lift2 getObject_tcb_wp) - apply (clarsimp simp: pred_conj_def) - apply (frule (1) valid_tcbs_valid_tcb) - apply (fastforce simp: valid_tcb_def valid_bound_obj_def obj_at_def split: option.splits) - apply (fastforce simp: valid_tcbs'_def valid_tcb'_def obj_at'_def) + apply (clarsimp simp: is_schedulable_def isSchedulable_def Option.is_none_def) + apply (rule corres_symb_exec_l[OF _ _ gets_the_sp]) + apply (rule corres_symb_exec_r[OF _ isRunnable_sp]) + apply (rule corres_symb_exec_r[OF _ threadGet_sp]) + apply (rule corres_stateAssert_add_assertion) + apply (rule corres_if_strong') + apply clarsimp + apply normalise_obj_at' + apply (frule state_relation_pspace_relation) + apply (frule pspace_relation_tcb_relation) + apply (fastforce dest: get_tcb_ko_atD simp: obj_at_def) + apply (fastforce simp: obj_at'_def) + apply (clarsimp simp: tcb_relation_def) + apply corres + apply clarsimp + apply (rule corres_symb_exec_l[OF _ _ get_sched_context_sp]) + apply (rule corres_symb_exec_r[OF _ scActive_sp]) + apply (rule corres_symb_exec_l[OF _ _ gets_sp]) + apply (rule corres_symb_exec_r[OF _ inReleaseQueue_sp]) + apply clarsimp + apply normalise_obj_at' + apply (frule state_relation_pspace_relation) + apply (frule pspace_relation_tcb_relation[where ptr=t]) + apply (fastforce dest: get_tcb_ko_atD simp: tcb_at_def obj_at_def) + apply (fastforce simp: obj_at'_def) + apply (rule conj_cong) + apply (clarsimp simp: tcb_relation_def) + apply (case_tac "tcb_state tcb"; clarsimp) + apply (rule conj_cong) + apply (force dest!: pspace_relation_sc_relation + simp: obj_at_def obj_at'_def active_sc_def + tcb_relation_def sc_relation_def) + apply (drule state_relation_release_queue_relation) + apply (clarsimp simp: release_queue_relation_def list_queue_relation_def + in_queue_2_def obj_at'_def opt_pred_def opt_map_def + split: option.splits) + apply wpsimp+ + apply (fastforce simp: valid_tcbs'_def valid_tcb'_def obj_at'_def) + apply (rule get_sched_context_exs_valid) + apply (fastforce dest!: get_tcb_SomeD intro: sc_atD1 + simp: valid_tcbs_def obj_at_def valid_tcb_def) + apply wpsimp + apply (fastforce dest!: get_tcb_SomeD intro: sc_atD1 + simp: valid_tcbs_def obj_at_def valid_tcb_def) + apply (wpsimp simp: tcb_at_def valid_tcbs'_asrt_def)+ done lemma get_simple_ko_exs_valid: @@ -2748,19 +2804,40 @@ lemmas get_reply_exs_valid[wp] = lemmas get_endpoint_exs_valid[wp] = get_simple_ko_exs_valid[where C=kernel_object.Endpoint, simplified] -lemma inReleaseQueue_inv[wp]: - "inReleaseQueue t \P\" - by (simp add: inReleaseQueue_def | wp gts_inv')+ - lemma conjunct_rewrite: "P = P' \ Q = Q' \ R = R' \ (P \ Q \ R) = (P' \ Q' \ R')" by simp +definition isScActive :: "machine_word \ kernel_state \ bool" where + "isScActive scPtr s' \ pred_map (\sc. 0 < scRefillMax sc) (scs_of' s') scPtr" + +abbreviation ct_isSchedulable :: "kernel_state \ bool" where + "ct_isSchedulable \ ct_active' + and (\s. pred_map (\tcb. \ tcbInReleaseQueue tcb) (tcbs_of' s) (ksCurThread s)) + and (\s. pred_map (\scPtr. isScActive scPtr s) (tcbSCs_of s) (ksCurThread s))" + +definition isSchedulable_bool :: "machine_word \ kernel_state \ bool" where + "isSchedulable_bool tcbPtr s' + \ pred_map (\tcb. runnable' (tcbState tcb) \ \ tcbInReleaseQueue tcb) (tcbs_of' s') tcbPtr + \ pred_map (\scPtr. isScActive scPtr s') (tcbSCs_of s') tcbPtr" + +lemma isSchedulable_wp: + "\\s. \t. isSchedulable_bool tcbPtr s = t \ tcb_at' tcbPtr s \ P t s\ isSchedulable tcbPtr \P\" + apply (clarsimp simp: isSchedulable_def) + apply (wpsimp simp: hoare_vcg_if_lift2 obj_at_def is_tcb inReleaseQueue_def + wp: threadGet_wp getTCB_wp) + apply (fastforce elim: rsubst2[where P=P] + simp: isSchedulable_bool_def isScActive_def obj_at'_def + pred_tcb_at'_def pred_map_simps in_opt_map_eq) + done + +lemma isSchedulable_sp: + "\P\ isSchedulable tcbPtr \\rv. (\s. rv = isSchedulable_bool tcbPtr s) and P\" + by (wpsimp wp: isSchedulable_wp) + lemma isSchedulable_inv[wp]: "isSchedulable tcbPtr \P\" - apply (clarsimp simp: isSchedulable_def inReleaseQueue_def) - apply (rule bind_wp[OF _ getObject_tcb_inv]) - by (wpsimp wp: inReleaseQueue_inv) + by (wpsimp wp: isSchedulable_wp) \ \In sched_context_donate, weak_valid_sched_action does not propagate backwards over the statement where from_tptr's sched context is set to None because it requires the thread associated with a @@ -2865,14 +2942,29 @@ lemma rescheduleRequired_corres_simple: done lemma weak_sch_act_wf_lift: - assumes pre: "\P. \\s. P (sa s)\ f \\rv s. P (sa s)\" - "\t. \st_tcb_at' runnable' t\ f \\rv. st_tcb_at' runnable' t\" - "\t. \tcb_in_cur_domain' t\ f \\rv. tcb_in_cur_domain' t\" - shows "\\s. weak_sch_act_wf (sa s) s\ f \\rv s. weak_sch_act_wf (sa s) s\" + assumes pre: "\P. f \\s. P (sa s)\" + "\t. f \tcb_at' t\" + shows "f \\s. weak_sch_act_wf (sa s) s\" apply (simp only: weak_sch_act_wf_def imp_conv_disj) apply (intro hoare_vcg_all_lift hoare_vcg_conj_lift hoare_vcg_disj_lift pre | simp)+ done +crunches tcbSchedEnqueue + for weak_sch_act_wf[wp]: "\s. weak_sch_act_wf (ksSchedulerAction s) s" + (wp: weak_sch_act_wf_lift) + +lemma rescheduleRequired_weak_sch_act_wf[wp]: + "\\\ + rescheduleRequired + \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" + by (wp | simp add: rescheduleRequired_def setSchedulerAction_def weak_sch_act_wf_def)+ + +lemma possibleSwitchTo_weak_sch_act_wf[wp]: + "possibleSwitchTo target \\s. weak_sch_act_wf (ksSchedulerAction s) s\" + unfolding possibleSwitchTo_def + apply (wpsimp wp: threadGet_wp inReleaseQueue_wp simp: setSchedulerAction_def) + by (fastforce simp: weak_sch_act_wf_def obj_at'_def ps_clear_def) + lemma asUser_weak_sch_act_wf[wp]: "\\s. weak_sch_act_wf (ksSchedulerAction s) s\ asUser t m \\rv s. weak_sch_act_wf (ksSchedulerAction s) s\" @@ -2897,8 +2989,8 @@ lemma threadSet_tcbDomain_triv: apply (wp threadSet_obj_at'_strongish getObject_tcb_wp | simp add: assms)+ done -lemmas threadSet_weak_sch_act_wf - = weak_sch_act_wf_lift[OF threadSet.ksSchedulerAction threadSet_pred_tcb_no_state threadSet_tcbDomain_triv, simplified] +lemmas threadSet_weak_sch_act_wf[wp] + = weak_sch_act_wf_lift[OF threadSet.ksSchedulerAction threadSet_tcb_at', simplified] lemma removeFromBitmap_nosch[wp]: "\\s. P (ksSchedulerAction s)\ removeFromBitmap d p \\rv s. P (ksSchedulerAction s)\" @@ -3038,33 +3130,6 @@ lemma setObject_tcbState_update_corres: apply (fastforce simp: inQ_def)+ done -definition isScActive :: "machine_word \ kernel_state \ bool" where - "isScActive scPtr s' \ pred_map (\sc. 0 < scRefillMax sc) (scs_of' s') scPtr" - -abbreviation ct_isSchedulable :: "kernel_state \ bool" where - "ct_isSchedulable \ ct_active' - and (\s. pred_map (\tcb. \ tcbInReleaseQueue tcb) (tcbs_of' s) (ksCurThread s)) - and (\s. pred_map (\scPtr. isScActive scPtr s) (tcbSCs_of s) (ksCurThread s))" - -definition isSchedulable_bool :: "machine_word \ kernel_state \ bool" where - "isSchedulable_bool tcbPtr s' - \ pred_map (\tcb. runnable' (tcbState tcb) \ \ tcbInReleaseQueue tcb) (tcbs_of' s') tcbPtr - \ pred_map (\scPtr. isScActive scPtr s') (tcbSCs_of s') tcbPtr" - -lemma isSchedulable_wp: - "\\s. \t. isSchedulable_bool tcbPtr s = t \ tcb_at' tcbPtr s \ P t s\ isSchedulable tcbPtr \P\" - apply (clarsimp simp: isSchedulable_def) - apply (wpsimp simp: hoare_vcg_if_lift2 obj_at_def is_tcb inReleaseQueue_def - wp: threadGet_wp getTCB_wp) - apply (fastforce elim: rsubst2[where P=P] - simp: isSchedulable_bool_def isScActive_def obj_at'_def - pred_tcb_at'_def pred_map_simps in_opt_map_eq) - done - -lemma isSchedulable_sp: - "\P\ isSchedulable tcbPtr \\rv. (\s. rv = isSchedulable_bool tcbPtr s) and P\" - by (wpsimp wp: isSchedulable_wp) - lemma scheduleTCB_corres: "corres dc (valid_tcbs and weak_valid_sched_action and pspace_aligned and pspace_distinct @@ -3490,23 +3555,10 @@ lemma rescheduleRequired_sch_act'[wp]: \\rv s. sch_act_wf (ksSchedulerAction s) s\" by (wpsimp simp: rescheduleRequired_def wp: isSchedulable_wp) -lemma rescheduleRequired_weak_sch_act_wf[wp]: - "\\\ - rescheduleRequired - \\rv s. weak_sch_act_wf (ksSchedulerAction s) s\" - apply (simp add: rescheduleRequired_def setSchedulerAction_def) - apply (wp hoare_TrueI | simp add: weak_sch_act_wf_def)+ - done - lemma sts_weak_sch_act_wf[wp]: - "\\s. weak_sch_act_wf (ksSchedulerAction s) s - \ (ksSchedulerAction s = SwitchToThread t \ runnable' st)\ - setThreadState st t - \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" + "setThreadState st t \\s. weak_sch_act_wf (ksSchedulerAction s) s\" unfolding setThreadState_def scheduleTCB_def apply (wpsimp wp: hoare_vcg_if_lift2 hoare_vcg_imp_lift hoare_vcg_all_lift - threadSet_pred_tcb_at_state threadSet_tcbDomain_triv - isSchedulable_inv hoare_pre_cont[where f="isSchedulable x" and P="\rv _. rv" for x] hoare_pre_cont[where f="isSchedulable x" and P="\rv _. \rv" for x] simp: weak_sch_act_wf_def) @@ -3931,10 +3983,6 @@ lemma setQueue_sets_queue[wp]: crunches setQueue for ksReleaseQueue[wp]: "\s. P (ksReleaseQueue s)" -lemma ko_at'_valid_tcbs'_valid_tcb': - "\ko_at' ko ptr s; valid_tcbs' s\ \ valid_tcb' ko s" - by (fastforce simp: valid_tcbs'_def obj_at'_def) - lemma tcbSchedEnqueue_tcbInReleaseQueue[wp]: "tcbSchedEnqueue tcbPtr \\s. P (tcbInReleaseQueue |< tcbs_of' s)\" apply (clarsimp simp: tcbSchedEnqueue_def tcbQueuePrepend_def unless_def when_def setQueue_def) diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy index 107b7eff07..c267813ea4 100644 --- a/proof/refine/RISCV64/Tcb_R.thy +++ b/proof/refine/RISCV64/Tcb_R.thy @@ -373,38 +373,6 @@ lemma invokeTCB_WriteRegisters_corres: apply (fastforce dest: valid_sched_valid_ready_qs) done -lemma tcbSchedDequeue_ResumeCurrentThread_imp_notct[wp]: - "\\s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\ - tcbSchedDequeue t - \\rv s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\" - by (wp hoare_convert_imp) - -lemma updateRestartPC_ResumeCurrentThread_imp_notct[wp]: - "\\s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\ - updateRestartPC t - \\rv s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\" - unfolding updateRestartPC_def - apply (wp hoare_convert_imp) - done - -lemma schedContextCancelYieldTo_ResumeCurrentThread_imp_notct[wp]: - "\\s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\ - schedContextCancelYieldTo t - \\rv s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\" - by (wp hoare_convert_imp) - -lemma tcbReleaseRemove_ResumeCurrentThread_imp_notct[wp]: - "\\s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\ - tcbReleaseRemove t - \\rv s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\" - by (wp hoare_convert_imp) - -lemma suspend_ResumeCurrentThread_imp_notct[wp]: - "\\s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\ - suspend t - \\rv s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\" - by (wpsimp simp: suspend_def wp_del: getThreadState_only_state_wp) - lemma invokeTCB_CopyRegisters_corres: "corres (dc \ (=)) (einvs and simple_sched_action and tcb_at dest and tcb_at src and ex_nonz_cap_to src and diff --git a/spec/design/skel/KernelStateData_H.thy b/spec/design/skel/KernelStateData_H.thy index 6a77d406f3..b67579130b 100644 --- a/spec/design/skel/KernelStateData_H.thy +++ b/spec/design/skel/KernelStateData_H.thy @@ -100,7 +100,7 @@ where return r od" -#INCLUDE_HASKELL SEL4/Model/StateData.lhs decls_only ONLY capHasProperty sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tc_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt -#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 +#INCLUDE_HASKELL SEL4/Model/StateData.lhs decls_only ONLY capHasProperty sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tc_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt +#INCLUDE_HASKELL SEL4/Model/StateData.lhs NOT doMachineOp KernelState ReadyQueue ReleaseQueue ReaderM Kernel KernelR getsJust assert stateAssert funOfM condition whileLoop findM funArray newKernelState capHasProperty ifM whenM whileM andM orM sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tc_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt end diff --git a/spec/haskell/src/SEL4/Kernel/Thread.lhs b/spec/haskell/src/SEL4/Kernel/Thread.lhs index b495dfa8ac..93a4392bf3 100644 --- a/spec/haskell/src/SEL4/Kernel/Thread.lhs +++ b/spec/haskell/src/SEL4/Kernel/Thread.lhs @@ -111,14 +111,16 @@ runnable; this is to prevent it being inserted in the scheduler queue. > isSchedulable :: PPtr TCB -> Kernel Bool > isSchedulable tcbPtr = do -> tcb <- getObject tcbPtr -> if tcbSchedContext tcb == Nothing +> runnable <- isRunnable tcbPtr +> scPtrOpt <- threadGet tcbSchedContext tcbPtr +> stateAssert valid_tcbs'_asrt "valid_tcbs' holds" +> if scPtrOpt == Nothing > then return False > else do -> sc <- getSchedContext $ fromJust $ tcbSchedContext tcb -> runnable <- isRunnable tcbPtr +> let scPtr = fromJust scPtrOpt +> active <- scActive scPtr > inReleaseQ <- inReleaseQueue tcbPtr -> return $! runnable && scRefillMax sc > 0 && not inReleaseQ +> return $ runnable && active && not inReleaseQ \subsubsection{Suspending a Thread} diff --git a/spec/haskell/src/SEL4/Model/StateData.lhs b/spec/haskell/src/SEL4/Model/StateData.lhs index 28c3b4f388..589bcd7972 100644 --- a/spec/haskell/src/SEL4/Model/StateData.lhs +++ b/spec/haskell/src/SEL4/Model/StateData.lhs @@ -521,3 +521,8 @@ 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 + +An assert that will say that valid_tcbs' holds + +> valid_tcbs'_asrt :: KernelState -> Bool +> valid_tcbs'_asrt _ = True diff --git a/spec/haskell/src/SEL4/Object/Notification.lhs b/spec/haskell/src/SEL4/Object/Notification.lhs index 8f85386d6c..524d14bf4c 100644 --- a/spec/haskell/src/SEL4/Object/Notification.lhs +++ b/spec/haskell/src/SEL4/Object/Notification.lhs @@ -178,6 +178,8 @@ The following function will remove the given thread from the queue of the notifi > cancelSignal :: PPtr TCB -> PPtr Notification -> Kernel () > cancelSignal threadPtr ntfnPtr = do +> stateAssert sym_refs_asrt +> "Assert that `sym_refs (state_refs_of' s)` holds" > stateAssert ready_qs_runnable > "Threads in the ready queues are runnable'" > ntfn <- getNotification ntfnPtr