diff --git a/proof/invariant-abstract/AInvs.thy b/proof/invariant-abstract/AInvs.thy index 5df6ff4184..9bbaca463d 100644 --- a/proof/invariant-abstract/AInvs.thy +++ b/proof/invariant-abstract/AInvs.thy @@ -428,7 +428,6 @@ lemma invoke_tcb_schact_is_rct_imp_cur_sc_active: apply (intro conjI impI) apply (clarsimp simp: maybe_sched_context_unbind_tcb_def) apply (wpsimp wp: thread_get_wp simp: get_tcb_obj_ref_def) - apply (clarsimp simp: maybe_sched_context_bind_tcb_def) apply (wpsimp wp: hoare_vcg_imp_lift' cur_sc_active_lift) apply wpsimp apply (rename_tac t ntfn) @@ -875,10 +874,7 @@ lemma invoke_tcb_schact_is_rct_imp_ct_not_in_release_q: apply (clarsimp split: option.splits) apply (intro conjI) apply (wpsimp wp: hoare_drop_imps) - apply (clarsimp simp: maybe_sched_context_bind_tcb_def bind_assoc) - apply (wpsimp wp: sched_context_bind_tcb_schact_is_rct_imp_ct_not_in_release_q hoare_vcg_if_lift2) - apply (wpsimp wp: hoare_drop_imps) - apply wpsimp + apply (wpsimp wp: sched_context_bind_tcb_schact_is_rct_imp_ct_not_in_release_q) apply (clarsimp simp: pred_tcb_at_def obj_at_def) done @@ -1667,7 +1663,7 @@ lemma install_tcb_frame_cap_schact_is_rct_imp_ct_activatable: apply (fastforce simp: ct_in_state_def pred_tcb_at_def obj_at_def get_tcb_def) done -crunch set_priority, maybe_sched_context_unbind_tcb, maybe_sched_context_bind_tcb +crunch set_priority, maybe_sched_context_unbind_tcb, sched_context_bind_tcb for ct_in_state[wp]: "ct_in_state P" (wp: crunch_wps) @@ -1716,7 +1712,7 @@ lemma invoke_tcb_schact_is_rct_imp_ct_activatable: apply (wpsimp wp: install_tcb_cap_schact_is_rct_imp_ct_activatable) apply (fastforce simp: ct_in_state_def pred_tcb_at_def obj_at_def) apply (rule bindE_wp_fwd_skip, solves \wpsimp wp: hoare_vcg_imp_lift'\)+ - apply (wpsimp wp: hoare_vcg_imp_lift') + apply (wpsimp wp: hoare_vcg_imp_lift' sched_context_bind_tcb_ct_in_state) apply wpsimp apply (fastforce simp: ct_in_state_def pred_tcb_at_def obj_at_def) apply wpsimp diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index 79f069d9ae..24fdd4d55f 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -7633,12 +7633,12 @@ crunch if_cond_refill_unblock_check (wp: crunch_wps) lemma sched_context_bind_tcb_valid_sched: - "\\s. valid_sched s \ simple_sched_action s \ current_time_bounded s - \ pred_map_eq None (tcb_scps_of s) tcbptr - \ not_cur_thread tcbptr s \ sc_not_in_release_q scptr s - \ sched_context_donate_ipc_queues_precond tcbptr scptr s\ + "\\s. valid_sched s \ simple_sched_action s \ bound_sc_tcb_at ((=) None) tcbptr s + \ not_cur_thread tcbptr s + \ sched_context_donate_ipc_queues_precond tcbptr scptr s \current_time_bounded s + \ sc_not_in_release_q scptr s\ sched_context_bind_tcb scptr tcbptr - \\y. valid_sched\" + \\_. valid_sched\" supply if_split[split del] apply (clarsimp simp: sched_context_bind_tcb_def) apply (wpsimp wp: is_schedulable_wp' reschedule_valid_sched_const) @@ -7675,20 +7675,10 @@ lemma sched_context_bind_tcb_valid_sched: simp: valid_sched_def) apply (subst op_equal[symmetric]) apply (wpsimp wp: ssc_bound_sc_tcb_at) - apply (clarsimp simp: valid_sched_def cong: conj_cong) - apply (fastforce simp: in_queues_2_def valid_release_q_def vs_all_heap_simps in_queue_2_def - dest!: valid_ready_qs_no_sc_not_queued) - done - -lemma maybe_sched_context_bind_tcb_valid_sched: - "\\s. valid_sched s \ simple_sched_action s \ bound_sc_tcb_at ((=) None) tcbptr s \ not_cur_thread tcbptr s - \ sched_context_donate_ipc_queues_precond tcbptr scptr s \ current_time_bounded s - \ sc_not_in_release_q scptr s\ - maybe_sched_context_bind_tcb scptr tcbptr - \\y. valid_sched\" - unfolding maybe_sched_context_bind_tcb_def - apply (wpsimp wp: sched_context_bind_tcb_valid_sched get_tcb_obj_ref_wp) - by (auto simp: obj_at_kh_kheap_simps vs_all_heap_simps split: if_splits) + apply (clarsimp simp: valid_sched_def tcb_at_kh_simps(4) cong: conj_cong) + apply (drule valid_ready_qs_no_sc_not_queued[where ref=tcbptr]) + apply (fastforce simp: pred_map_eq_def) + by (fastforce simp: in_queues_2_def valid_release_q_def vs_all_heap_simps in_queue_2_def) context DetSchedSchedule_AI_det_ext begin @@ -7892,8 +7882,8 @@ crunch cancel_all_ipc context DetSchedSchedule_AI begin crunch restart, install_tcb_frame_cap, install_tcb_cap, maybe_sched_context_unbind_tcb, - maybe_sched_context_bind_tcb, bind_notification, invoke_sched_context, - invoke_sched_control_configure_flags + sched_context_bind_tcb, bind_notification, invoke_sched_context, + invoke_sched_control_configure_flags for current_time_bounded[wp]: "current_time_bounded :: 'state_ext state \ _" (wp: crunch_wps check_cap_inv simp: crunch_simps) @@ -8095,14 +8085,14 @@ lemma tcs_valid_sched: and tcb_inv_wf (ThreadControlSched target slot fault_handler mcp priority sc) and (\s. heap_refs_inv (tcb_scps_of s) (sc_tcbs_of s)) and ct_active and ct_released and ct_not_in_release_q\ - invoke_tcb (ThreadControlSched target slot fault_handler mcp priority sc) - \\rv. valid_sched :: det_state \ _\" + invoke_tcb (ThreadControlSched target slot fault_handler mcp priority sc) + \\_ s :: det_state. valid_sched s\" supply if_split[split del] apply (simp add: split_def cong: option.case_cong) apply (wp maybeM_wp_drop_None) \ \bind/unbind sched context\ apply (clarsimp cong: conj_cong) - apply (wpsimp wp: maybe_sched_context_bind_tcb_valid_sched + apply (wpsimp wp: sched_context_bind_tcb_valid_sched maybe_sched_context_unbind_tcb_valid_sched, assumption) apply (strengthen not_cur_thread_2_simps) \ \set priority\ @@ -8120,20 +8110,22 @@ lemma tcs_valid_sched: apply (rule valid_validE_R) apply ((wpsimp wp: hoare_vcg_all_lift install_tcb_cap_ct_active hoare_vcg_imp_lift install_tcb_cap_timeout_faulted_tcb_at - split: if_split - | rule valid_validE, wps)+)[1] + split: if_split + | rule valid_validE, wps)+)[1] \ \resolve using preconditions\ apply (clarsimp, frule tcb_at_invs, frule valid_sched_active_scs_valid) apply (prop_tac "active_scs_valid s \ released_ipc_queues s", fastforce) - apply (clarsimp simp: obj_at_def is_tcb) - apply (clarsimp simp: tcb_at_kh_simps[symmetric] - pred_tcb_at_def obj_at_def sc_at_released_kh_simps released_sc_at_def - split: option.splits cong: conj_cong; - intro conjI; (erule disjE)?; - clarsimp dest!: active_scs_validE - simp: ipc_queued_thread_state_def2 sc_tcb_sc_at_def obj_at_def - dest!: sym[of _ "tcb_sched_context _"]) - by (drule_tac tp=x in sym_ref_tcb_sc[OF invs_sym_refs], fastforce+)+ + apply (clarsimp simp: obj_at_def is_tcb pred_tcb_at_def released_sc_at_def + cong: conj_cong) + apply (prop_tac "\sc_ptr. sc = Some (Some sc_ptr) \ sc_not_in_release_q sc_ptr s") + apply (clarsimp simp: sc_tcb_sc_at_def obj_at_def vs_all_heap_simps) + apply (fastforce dest!: sym_ref_tcb_sc[OF invs_sym_refs]) + by (intro conjI; + clarsimp simp: sc_tcb_sc_at_def obj_at_def pred_map_simps(1) tcb_at_kh_simps(3) tcb_scps.Some; + intro conjI impI allI; + fastforce intro!: active_scs_validE + simp: ipc_queued_thread_state_def2 vs_all_heap_simps + sc_at_released_kh_simps tcb_at_kh_simps) end @@ -17319,8 +17311,8 @@ lemma tcc_cur_sc_chargeable: apply (all \clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\) by auto -crunch maybe_sched_context_unbind_tcb, maybe_sched_context_bind_tcb, set_priority - , bind_notification +crunch maybe_sched_context_unbind_tcb, sched_context_bind_tcb, set_priority, + bind_notification for scheduler_act_sane[wp]: scheduler_act_sane (wp: crunch_wps simp: crunch_simps) @@ -20388,8 +20380,8 @@ lemma rec_del_consumed_time_bounded[wp]: done crunch restart, install_tcb_frame_cap, install_tcb_cap, maybe_sched_context_unbind_tcb, - maybe_sched_context_bind_tcb, bind_notification, invoke_sched_context, - invoke_sched_control_configure_flags + sched_context_bind_tcb, bind_notification, invoke_sched_context, + invoke_sched_control_configure_flags for consumed_time_bounded[wp]: "consumed_time_bounded :: 'state_ext state \ _" (wp: crunch_wps check_cap_inv simp: crunch_simps) @@ -21065,7 +21057,7 @@ lemma restart_ct_not_blocked[wp]: apply (wpsimp wp: hoare_vcg_imp_lift' sts_ctis_neq cancel_ipc_ct_in_state get_tcb_obj_ref_wp gts_wp maybeM_inv) done -crunch maybe_sched_context_unbind_tcb, maybe_sched_context_bind_tcb +crunch maybe_sched_context_unbind_tcb, sched_context_bind_tcb for ct_not_blocked[wp]: "ct_not_blocked :: 'state_ext state \ _" (simp: crunch_simps wp: crunch_wps set_tcb_obj_ref_ct_in_state) @@ -21632,8 +21624,8 @@ crunch handle_interrupt check_cap_inv filterM_preserved simp: crunch_simps) -crunch do_reply_transfer, restart, maybe_sched_context_unbind_tcb, maybe_sched_context_bind_tcb, - set_priority, bind_notification +crunch do_reply_transfer, restart, maybe_sched_context_unbind_tcb, sched_context_bind_tcb, + set_priority, bind_notification for vmt[wp]: "(\s. P (last_machine_time_of s) (cur_time s)) :: det_state \ _" and pnt[wp]: "(\s. P (last_machine_time_of s) (time_state_of s)) :: det_state \ _" (wp: crunch_wps simp: crunch_simps) @@ -21816,8 +21808,7 @@ lemma sched_context_bind_tcb_cur_sc_more_than_ready[wp]: \cur_sc_more_than_ready\" unfolding sched_context_bind_tcb_def by wpsimp -crunch suspend, bind_notification, maybe_sched_context_unbind_tcb, - maybe_sched_context_bind_tcb +crunch suspend, bind_notification, maybe_sched_context_unbind_tcb, sched_context_bind_tcb for cur_sc_more_than_ready[wp]: cur_sc_more_than_ready (wp: crunch_wps hoare_vcg_if_lift2 simp: crunch_simps ignore: update_sched_context) @@ -22357,17 +22348,17 @@ lemma maybe_sched_context_unbind_tcb_cur_sc_offset_sufficient[wp]: apply wpsimp done -lemma maybe_sched_context_bind_tcb_cur_sc_offset_ready[wp]: - "maybe_sched_context_bind_tcb sc_ptr tcb_ptr +lemma sched_context_bind_tcb_cur_sc_offset_ready[wp]: + "sched_context_bind_tcb sc_ptr tcb_ptr \\s. cur_sc_active s \ cur_sc_offset_ready (consumed_time s) s\" - apply (clarsimp simp: maybe_sched_context_bind_tcb_def sched_context_bind_tcb_def) + apply (clarsimp simp: sched_context_bind_tcb_def) apply wpsimp done -lemma maybe_sched_context_bind_tcb_cur_sc_offset_sufficient[wp]: - "maybe_sched_context_bind_tcb sc_ptr tcb_ptr +lemma sched_context_bind_tcb_cur_sc_offset_sufficient[wp]: + "sched_context_bind_tcb sc_ptr tcb_ptr \\s. cur_sc_active s \ cur_sc_offset_sufficient (consumed_time s) s\" - apply (clarsimp simp: maybe_sched_context_bind_tcb_def sched_context_bind_tcb_def) + apply (clarsimp simp: sched_context_bind_tcb_def) apply wpsimp done @@ -24476,8 +24467,8 @@ lemma install_tcb_cap_release_q_not_blocked_on_reply[wp]: done crunch sched_context_yield_to, sched_context_bind_tcb, - cancel_badged_sends, restart, maybe_sched_context_unbind_tcb, maybe_sched_context_bind_tcb, - sched_context_bind_tcb, bind_notification, send_signal + cancel_badged_sends, restart, maybe_sched_context_unbind_tcb, sched_context_bind_tcb, + sched_context_bind_tcb, bind_notification, send_signal for cur_sc[wp]: "\s. P (cur_sc s)" (wp: crunch_wps check_cap_inv filterM_preserved simp: crunch_simps) @@ -24610,12 +24601,6 @@ lemma invoke_tcb_cur_sc_in_release_q_imp_zero_consumed[wp]: apply (case_tac sc_ptr_opt; clarsimp) apply (wpsimp wp: hoare_drop_imps) apply (clarsimp simp: cur_sc_in_release_q_imp_zero_consumed_def) - - apply (clarsimp simp: maybe_sched_context_bind_tcb_def) - apply (rule bind_wp[OF _ gsc_sp]) - apply (rule hoare_when_cases; (solves \wpsimp\)?) - apply wpsimp - apply (fastforce simp: cur_sc_in_release_q_imp_zero_consumed_def) apply wpsimp apply (fastforce simp: pred_tcb_at_def sc_at_pred_n_def obj_at_def vs_all_heap_simps pred_neg_def is_blocked_on_reply_def @@ -25521,14 +25506,7 @@ lemma sched_context_bind_tcb_released_if_bound[wp]: split: if_splits option.splits) done -lemma maybe_sched_context_bind_tcb_released_if_bound[wp]: - "\\s. released_if_bound_sc_tcb_at t s \ tcb_ptr \ t \ active_scs_valid s\ - maybe_sched_context_bind_tcb sc_ptr tcb_ptr - \\_. released_if_bound_sc_tcb_at t\" - unfolding maybe_sched_context_bind_tcb_def - by (wpsimp wp: hoare_drop_imp hoare_vcg_if_lift2) - -crunch install_tcb_frame_cap, maybe_sched_context_bind_tcb, maybe_sched_context_unbind_tcb +crunch install_tcb_frame_cap, sched_context_bind_tcb, maybe_sched_context_unbind_tcb for cur_thread[wp]: "\s. P (cur_thread s)" (wp: check_cap_inv crunch_wps) diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index e58794000f..8b4d506008 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -1759,7 +1759,7 @@ lemma reply_unlink_tcb_bound_sc_tcb_at[wp]: by (wpsimp wp: hoare_drop_imp) crunch blocked_cancel_ipc, cancel_signal, test_reschedule - for bound_sc_tcb_at[wp]: "bound_sc_tcb_at P t" + for bound_sc_tcb_at[wp]: "\s. Q (bound_sc_tcb_at P t s)" (wp: crunch_wps) lemma sched_context_cancel_yield_to_not_live0: diff --git a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy index d62e5b3c36..4ebb54baea 100644 --- a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy @@ -404,7 +404,8 @@ lemma tcs_invs[Tcb_AI_asms]: apply (intro conjI; intro allI impI) apply (clarsimp simp: pred_tcb_at_def obj_at_def is_tcb) apply (clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ) - apply (clarsimp simp: obj_at_def is_ep sc_at_pred_n_def) + apply (fastforce dest: invs_sym_refs sym_ref_sc_tcb + simp: obj_at_def is_ep sc_at_pred_n_def pred_tcb_at_def) apply clarsimp apply (drule bound_sc_tcb_at_idle_sc_idle_thread[rotated, rotated], clarsimp, clarsimp) apply (fastforce simp: invs_def valid_state_def sc_at_pred_n_def diff --git a/proof/invariant-abstract/SchedContext_AI.thy b/proof/invariant-abstract/SchedContext_AI.thy index 159d0c9452..ff678e179a 100644 --- a/proof/invariant-abstract/SchedContext_AI.thy +++ b/proof/invariant-abstract/SchedContext_AI.thy @@ -1358,17 +1358,6 @@ lemma sched_context_bind_tcb_invs[wp]: dest!: symreftype_inverse' split: if_splits) done -lemma maybe_sched_context_bind_tcb_invs[wp]: - "\invs and (\s. tcb_at tcb s \ (bound_sc_tcb_at (\x. x \ Some sc) tcb s \ - ex_nonz_cap_to sc s \ ex_nonz_cap_to tcb s - \ sc_tcb_sc_at ((=) None) sc s \ bound_sc_tcb_at ((=) None) tcb s))\ - maybe_sched_context_bind_tcb sc tcb - \\rv. invs\" - unfolding maybe_sched_context_bind_tcb_def - apply (wpsimp simp: get_tcb_obj_ref_def wp: thread_get_wp) - apply (fastforce simp: pred_tcb_at_def obj_at_def is_tcb) - done - lemma sched_context_unbind_valid_replies[wp]: "tcb_release_remove tcb_ptr \ valid_replies_pred P \" by (wpsimp simp: tcb_release_remove_def) @@ -1734,12 +1723,6 @@ lemma maybe_sched_context_unbind_tcb_lift: unfolding maybe_sched_context_unbind_tcb_def by (wpsimp wp: A hoare_drop_imps) -lemma maybe_sched_context_bind_tcb_lift: - assumes A: "sched_context_bind_tcb sc_ptr tcb_ptr \P\" - shows "maybe_sched_context_bind_tcb sc_ptr tcb_ptr \P\" - unfolding maybe_sched_context_bind_tcb_def - by (wpsimp wp: A hoare_drop_imps) - (* sched_context_yield_to is moved to the start of SchedContextInv_AI because it needs to be after Ipc_AI *) diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy index a26c274651..d06f919731 100644 --- a/proof/invariant-abstract/Tcb_AI.thy +++ b/proof/invariant-abstract/Tcb_AI.thy @@ -1245,12 +1245,8 @@ lemma decode_set_sched_params_wf[wp]: apply (rule conjI; clarsimp) apply (clarsimp simp: obj_at_def is_tcb pred_tcb_at_def is_cap_simps sc_tcb_sc_at_def sc_at_ppred_def) - apply (rule conjI, fastforce) - apply (subgoal_tac "excaps ! Suc 0 \ set excaps") - prefer 2 - apply fastforce - apply (cases "excaps ! Suc 0") - apply (clarsimp) + apply (prop_tac "excaps ! Suc 0 \ set excaps", fastforce) + apply (cases "excaps ! Suc 0"; fastforce) done end @@ -1865,7 +1861,7 @@ lemma set_priority_bound_sc_tcb_at[wp]: by (wpsimp simp: wp: hoare_drop_imps) crunch cancel_all_ipc - for bound_sc_tcb_at[wp]: "bound_sc_tcb_at P target" + for bound_sc_tcb_at[wp]: "\s. Q (bound_sc_tcb_at P target s)" (wp: crunch_wps) lemma cap_delete_fh_lift: diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy index 9e9f282f04..ea7151f707 100644 --- a/proof/refine/RISCV64/Tcb_R.thy +++ b/proof/refine/RISCV64/Tcb_R.thy @@ -2086,13 +2086,7 @@ lemma monadic_rewrite_bind_unbind: | Some x \ sched_context_unbind_tcb x | Some (Some sc_ptr) \ when (y \ Some sc_ptr) $ sched_context_bind_tcb sc_ptr t od)" - apply (case_tac sc_opt; clarsimp) - apply (clarsimp simp: monadic_rewrite_def bind_def get_tcb_obj_ref_def thread_get_def - gets_the_def get_tcb_def gets_def get_def obj_at_def is_tcb_def) - apply (case_tac ko; clarsimp simp: return_def) - apply (case_tac a; clarsimp simp: maybeM_def maybe_sched_context_unbind_tcb_def - maybe_sched_context_bind_tcb_def monadic_rewrite_def) - done +oops defs tcs_cross_asrt1_def: "tcs_cross_asrt1 t sc_opt \ @@ -2158,22 +2152,24 @@ lemma tc_corres_sched: apply (rule_tac P=\ and P'=\ in corres_option_split; clarsimp) apply wpfix apply (rule setPriority) - apply (simp add: bind_assoc[symmetric]) apply (rule corres_split_nor) - apply (rule monadic_rewrite_corres_l[OF monadic_rewrite_bind_unbind]) - apply (rule corres_split_eqr) - apply (simp only: mapTCBPtr_threadGet get_tcb_obj_ref_def) - apply (rule threadGet_corres, clarsimp simp: tcb_relation_def) - apply (rule_tac P=\ and P'=\ in corres_option_split; clarsimp) - apply (rule corres_option_split; clarsimp?) - apply (rule_tac P=\ and P'=\ in corres_option_split; clarsimp) + apply (rule_tac P=\ and P'=\ in corres_option_split; clarsimp) + apply (rule corres_option_split) + apply clarsimp + apply (clarsimp simp: maybe_sched_context_unbind_tcb_def) + apply (rule corres_split[OF get_tcb_obj_ref_corres[where r="(=)"]]) + apply (clarsimp simp: tcb_relation_def) + apply (clarsimp simp: maybeM_def) + apply (rule corres_option_split[where P=\]; clarsimp?) apply (rule schedContextUnbindTCB_corres') - apply (rule corres_when[OF _ schedContextBindTCB_corres], fastforce) - apply (wp get_tcb_obj_ref_wp) - apply (wpsimp wp: getTCB_wp simp: mapTCBPtr_def) - apply (clarsimp simp: returnOk_def) - apply (rule_tac P=\ in hoare_TrueI) - apply (rule hoare_TrueI) + apply (wp get_tcb_obj_ref_wp) + apply (wpsimp wp: threadGet_wp) + apply (rule schedContextBindTCB_corres) + apply (rule corres_returnOk_eq_same) + apply simp + apply wpsimp + apply wpsimp + apply (wpsimp wp: getTCB_wp) apply (rule_tac Q'="\_ s. invs s \ valid_machine_time s \ valid_sched s \ simple_sched_action s \ current_time_bounded s \ tcb_at t s \ ex_nonz_cap_to t s \ @@ -2198,7 +2194,7 @@ lemma tc_corres_sched: in hoare_strengthen_post[rotated], fastforce split: option.split) apply (wpsimp wp: setP_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) apply clarsimp - apply (prop_tac "ct_active s \ ct_released s", erule conjunct1) + apply (prop_tac "einvs s \ ct_active s \ ct_released s", erule conjunct1) apply simp apply clarsimp \ \the following is unified with one of the guard schematics\ @@ -2209,7 +2205,7 @@ lemma tc_corres_sched: apply (fastforce elim: ready_qs_runnable_cross ct_active_cross split: option.splits) apply (clarsimp simp: tcs_cross_asrt2_def) apply (intro conjI) - apply (fastforce elim: ready_qs_runnable_cross) + apply (fastforce intro!: ready_qs_runnable_cross invs_psp_aligned) apply (fastforce elim: ct_active_cross) apply (prop_tac "cur_tcb s", fastforce) apply (frule cur_tcb_cross) @@ -2217,24 +2213,30 @@ lemma tc_corres_sched: apply fastforce apply fastforce apply (fastforce elim: ct_released_cross_weak[simplified]) - apply (rule_tac Q'="\_. invs" in hoare_post_add) - apply (clarsimp simp: invs_cur case_option_If2 if_fun_split - cong: conj_cong imp_cong split del: if_split) + apply ((wpsimp wp: hoare_vcg_all_lift hoare_vcg_const_imp_lift hoare_case_option_wp + | strengthen invs_psp_aligned invs_distinct invs_sym_refs)+)[1] + apply (rule_tac Q'="\_. invs and valid_sched and tcb_at t" in hoare_post_imp) + apply (clarsimp split: option.splits) + apply (frule invs_sym_refs) + apply (frule sym_ref_tcb_sc) + apply (fastforce simp: obj_at_def) + apply fastforce + apply (clarsimp simp: pred_tcb_at_def sc_at_ppred_def obj_at_def) + apply (wpsimp wp: setMCPriority_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) + apply ((wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_all_lift + | strengthen invs_psp_aligned invs_distinct invs_sym_refs)+)[1] apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_const_imp_lift) - apply (rule_tac Q'="\_. invs'" in hoare_post_add) - apply (clarsimp simp: case_option_If2 if_fun_split - cong: conj_cong imp_cong split del: if_split) - apply (rule_tac f="ksCurThread" in hoare_lift_Pf3) - apply (wpsimp wp: setMCPriority_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) - apply wpsimp + apply (wpsimp wp: setMCPriority_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) apply (rule_tac Q'="\_ s. einvs s \ valid_machine_time s \ simple_sched_action s \ tcb_at t s - \ ex_nonz_cap_to t s \ ct_active s \ ct_released s - \ ct_not_in_release_q s \ current_time_bounded s \ - (\scp. sc_opt = Some (Some scp) \ ex_nonz_cap_to scp s \ - sc_tcb_sc_at ((=) None) scp s \ - bound_sc_tcb_at ((=) None) t s)" - and E'="\_. \" in hoare_strengthen_postE[rotated], fastforce split: option.splits, simp) - apply (rule hoare_vcg_conj_elimE) + \ ex_nonz_cap_to t s \ ct_active s \ ct_released s + \ ct_not_in_release_q s \ current_time_bounded s + \ (\scp. sc_opt = Some (Some scp) + \ ex_nonz_cap_to scp s \ sc_tcb_sc_at ((=) None) scp s + \ bound_sc_tcb_at ((=) None) t s)" + and E'="\_. \" in hoare_strengthen_postE[rotated]) + apply (fastforce dest: invs_sym_refs sym_ref_tcb_sc + simp: obj_at_def pred_tcb_at_def sc_at_ppred_def + split: option.splits) apply wp apply (wp install_tcb_cap_invs install_tcb_cap_ex_nonz_cap_to install_tcb_cap_ct_active hoare_vcg_all_lift hoare_weak_lift_imp @@ -2250,9 +2252,20 @@ lemma tc_corres_sched: apply (prop_tac "(not ep_at t) s") apply (clarsimp simp: pred_neg_def obj_at_def is_tcb_def is_ep_def) apply (clarsimp split: Structures_A.kernel_object.splits) - apply (fastforce simp: tcb_cap_valid_def pred_tcb_at_def pred_neg_def - sc_at_ppred_def obj_at_def is_ep_def is_tcb_def - elim: cte_wp_at_weakenE dest: tcb_ep_slot_cte_wp_ats) + apply (clarsimp simp: pred_neg_def) + apply (intro conjI) + apply (fastforce simp: obj_at_def is_tcb_def + elim: cte_wp_at_weakenE dest: tcb_ep_slot_cte_wp_ats) + subgoal + by (fastforce simp: tcb_cap_valid_def pred_tcb_at_def pred_neg_def + sc_at_ppred_def obj_at_def is_ep_def is_tcb_def + elim: cte_wp_at_weakenE dest: tcb_ep_slot_cte_wp_ats) + subgoal + by (fastforce simp: tcb_cap_valid_def pred_tcb_at_def pred_neg_def + sc_at_ppred_def obj_at_def is_ep_def is_tcb_def + elim: cte_wp_at_weakenE dest: tcb_ep_slot_cte_wp_ats) + apply fastforce + subgoal by (fastforce simp: pred_tcb_at_def is_ep_def is_tcb_def sc_at_ppred_def obj_at_def) apply (clarsimp simp: tcs_cross_asrt1_def) apply (intro conjI impI allI; clarsimp?) apply (clarsimp simp: tcb_at_cte_at'_3) @@ -2301,37 +2314,70 @@ lemma tc_caps_invs': fastforce simp: isValidFaultHandler_def isCap_simps isValidVTableRoot_def) done -lemma schedContextBindTCB_invs': - "\\s. invs' s \ ex_nonz_cap_to' tcbPtr s \ ex_nonz_cap_to' scPtr s \ - bound_sc_tcb_at' (\sc. sc = None) tcbPtr s \ obj_at' (\sc. scTCB sc = None) scPtr s\ +lemma schedContextBindTCB_valid_objs'[wp]: + "\valid_objs' and pspace_aligned' and pspace_distinct' and pspace_bounded' and tcb_at' tcbPtr\ + schedContextBindTCB scPtr tcbPtr + \\_. valid_objs'\" + unfolding schedContextBindTCB_def + apply (wpsimp wp: isSchedulable_wp hoare_drop_imps) + apply (frule (1) sc_ko_at_valid_objs_valid_sc') + apply (clarsimp simp: valid_sched_context'_def refillSize_def valid_sched_context_size'_def + scBits_simps objBits_simps) + done + +crunch schedContextBindTCB + for sym_heap_sched_pointers[wp]: sym_heap_sched_pointers + and valid_sched_pointers[wp]: valid_sched_pointers + and untyped_ranges_zero'[wp]: untyped_ranges_zero' + (wp: crunch_wps threadSet_sched_pointers threadSet_valid_sched_pointers threadSet_urz + simp: crunch_simps + ignore: threadSet) + +lemma postpone_if_live_then_nonz_cap'[wp]: + "\if_live_then_nonz_cap' and pspace_aligned' and pspace_distinct' and pspace_bounded' + and valid_objs' and sym_heap_sched_pointers and valid_sched_pointers\ + postpone scPtr + \\_. if_live_then_nonz_cap'\" + unfolding postpone_def + by wpsimp + +lemma schedContextResume_if_live_then_nonz_cap'[wp]: + "\if_live_then_nonz_cap' and pspace_aligned' and pspace_distinct' and pspace_bounded' + and valid_objs' and sym_heap_sched_pointers and valid_sched_pointers\ + schedContextResume scPtr + \\_. if_live_then_nonz_cap'\" + unfolding schedContextResume_def + by (wpsimp wp: isSchedulable_wp) + +lemma schedContextBindTCB_if_live_then_nonz_cap'[wp]: + "\if_live_then_nonz_cap' and ex_nonz_cap_to' scPtr and ex_nonz_cap_to' tcbPtr + and sc_at' scPtr and tcb_at' tcbPtr + and pspace_aligned' and pspace_distinct' and pspace_bounded' and valid_objs' + and sym_heap_sched_pointers and valid_sched_pointers\ + schedContextBindTCB scPtr tcbPtr + \\_. if_live_then_nonz_cap'\" + unfolding schedContextBindTCB_def + apply (wpsimp wp: tcbSchedContext_update_Nothing_if_live_then_nonz_cap' + threadSet_iflive' threadSet_cap_to threadSet_sched_pointers + threadSet_valid_sched_pointers isSchedulable_wp hoare_drop_imps + simp: tcbSchedContext_update_update_tcb_cte_cases) + apply (frule (1) sc_ko_at_valid_objs_valid_sc') + apply (clarsimp simp: valid_sched_context'_def refillSize_def valid_sched_context_size'_def + scBits_simps objBits_simps) + done + +crunch schedContextBindTCB + for valid_mdb'[wp]: valid_mdb' + and if_unsafe_then_cap'[wp]: if_unsafe_then_cap' + (wp: crunch_wps valid_mdb'_lift threadSet_ifunsafe'T + simp: tcbSchedContext_update_update_tcb_cte_cases crunch_simps) + +lemma schedContextBindTCB_invs'[wp]: + "\invs' and ex_nonz_cap_to' tcbPtr and ex_nonz_cap_to' scPtr and sc_at' scPtr and tcb_at' tcbPtr\ schedContextBindTCB scPtr tcbPtr \\_. invs'\" - apply (simp add: schedContextBindTCB_def) - apply (subst bind_assoc[symmetric, where m="threadSet _ _"]) - apply (rule bind_wp)+ - apply wpsimp - apply (wpsimp wp: isSchedulable_wp) - apply (clarsimp simp: isSchedulable_bool_runnableE) - apply (wp (once) hoare_drop_imps) - apply (wp hoare_vcg_imp_lift') - apply (wp hoare_drop_imps) - apply (wpsimp wp: hoare_vcg_imp_lift' simp: ifCondRefillUnblockCheck_def) - apply (rule_tac Q'="\_ s. invs' s" in hoare_strengthen_post[rotated], simp) - apply (simp add: invs'_def valid_pspace'_def valid_dom_schedule'_def) - apply (wp threadSet_valid_objs' threadSet_mdb' threadSet_iflive' - threadSet_cap_to threadSet_ifunsafe'T threadSet_ctes_ofT - untyped_ranges_zero_lift valid_irq_node_lift - valid_irq_handlers_lift'' hoare_vcg_const_imp_lift hoare_vcg_imp_lift' - threadSet_valid_replies' threadSet_valid_sched_pointers threadSet_tcbInReleaseQueue - sym_heap_sched_pointers_lift threadSet_tcbSchedNexts_of threadSet_tcbSchedPrevs_of - threadSet_tcbQueued - | clarsimp simp: tcb_cte_cases_def cteCaps_of_def cteSizeBits_def)+ - apply (clarsimp simp: invs'_def valid_pspace'_def valid_dom_schedule'_def) - by (fastforce simp: pred_tcb_at'_def obj_at'_def - objBits_def objBitsKO_def valid_tcb'_def tcb_cte_cases_def comp_def - valid_obj'_def valid_sched_context'_def valid_sched_context_size'_def - inQ_def cteCaps_of_def cteSizeBits_def refillSize_def - elim: ps_clear_domE split: if_splits) + apply (simp add: invs'_def valid_pspace'_def valid_dom_schedule'_def) + by (wpsimp wp: valid_irq_node_lift valid_irq_handlers_lift'' simp: o_def) lemma threadSetPriority_bound_sc_tcb_at' [wp]: "threadSetPriority tptr prio \\s. Q (bound_sc_tcb_at' P t s)\" @@ -2401,37 +2447,26 @@ lemma tc_sched_invs': \\_. invs'\" apply (simp add: invokeTCB_def) apply (wpsimp wp: schedContextUnbindTCB_invs' schedContextBindTCB_invs') - apply (wpsimp wp: getTCB_wp simp: mapTCBPtr_def) - apply (rule_tac Q'="\rv s. invs' s \ ex_nonz_cap_to' t s \ - (sc_opt = Some None \ - bound_sc_tcb_at' (\sc. sc \ Some idle_sc_ptr) t s) \ - (\x. sc_opt = Some (Some x) \ - ex_nonz_cap_to' x s \ obj_at' (\sc. scTCB sc = None) x s \ - bound_sc_tcb_at' (\sc. sc = None) t s \ - bound_sc_tcb_at' bound (ksCurThread s) s)" - in hoare_strengthen_post[rotated]) - apply (fastforce simp: pred_tcb_at'_def obj_at'_def projectKOs) - apply (rule hoare_lift_Pf3[where f=ksCurThread]) - apply (wpsimp wp: setP_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) + apply (rule_tac Q'="\rv s. invs' s \ ex_nonz_cap_to' t s \ tcb_at' t s \ + (\scPtr. sc_opt = Some (Some scPtr) \ + ex_nonz_cap_to' scPtr s \ sc_at' scPtr s)" + in hoare_strengthen_post[rotated]) + apply (fastforce simp: pred_tcb_at'_def obj_at'_def projectKOs) + apply (rule hoare_lift_Pf3[where f=ksCurThread]) + apply (wpsimp wp: setP_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) + apply wpsimp apply wpsimp - apply wpsimp - apply (clarsimp simp: tcs_cross_asrt2_def) - apply (wp (once) hoare_drop_imps) - apply (wpsimp wp: setMCPriority_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) - apply (wpsimp wp: installTCBCap_invs' installTCBCap_fh_ex_nonz_cap_to' - installTCBCap_fh_bound_sc_tcb_at' installTCBCap_fh_sc_tcb_sc_at' - hoare_vcg_all_lift hoare_vcg_ball_lift2 hoare_vcg_const_imp_lift) - apply (wpsimp simp: stateAssertE_def)+ - apply (clarsimp cong: conj_cong) - apply (subgoal_tac "sc_opt = Some None \ bound_sc_tcb_at' (\a. a \ Some idle_sc_ptr) t s") - apply (fastforce simp: tcs_cross_asrt1_def comp_def isValidFaultHandler_def - isCap_simps pred_tcb_at'_def obj_at'_def projectKOs) - apply (clarsimp simp: invs'_def valid_idle'_def - pred_tcb_at'_def obj_at'_def tcs_cross_asrt1_def valid_idle'_asrt_def) - apply (frule_tac p=t and ko="ko :: tcb" for ko in sym_refs_ko_atD'[rotated]) - apply (auto simp: ko_wp_at'_def obj_at'_def projectKOs valid_idle'_def tcb_bound_refs'_def - dest!: global'_no_ex_cap) - done + apply (clarsimp simp: tcs_cross_asrt2_def) + apply (wp (once) hoare_drop_imps) + apply (wpsimp wp: setMCPriority_invs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) + apply (wpsimp wp: installTCBCap_invs' installTCBCap_fh_ex_nonz_cap_to' + installTCBCap_fh_bound_sc_tcb_at' installTCBCap_fh_sc_tcb_sc_at' + hoare_vcg_all_lift hoare_vcg_ball_lift2 hoare_vcg_const_imp_lift) + apply (wpsimp simp: stateAssertE_def)+ + by (intro conjI impI allI; + clarsimp simp: invs'_def valid_idle'_def isCap_simps isCap_defs + pred_tcb_at'_def obj_at'_def tcs_cross_asrt1_def valid_idle'_asrt_def + o_def isValidFaultHandler_def ko_wp_at'_def tcb_bound_refs'_def) lemma setSchedulerAction_invs'[wp]: "\invs' and sch_act_wf sa\ @@ -2805,16 +2840,17 @@ lemma decodeSetSchedParams_wf: \ s \' fst x \ (\y \ zobj_refs' (fst x). ex_nonz_cap_to' y s))\ decodeSetSchedParams args (ThreadCap t) slot extras \tcb_inv_wf'\,-" + supply if_split[split del] unfolding decodeSetSchedParams_def scReleased_def refillReady_def scActive_def isBlocked_def apply (cases args; cases extras; clarsimp; (solves \wpsimp wp: checkPrio_inv\)?) apply (clarsimp split: list.splits; safe; (solves \wpsimp wp: checkPrio_inv\)?) apply (clarsimp simp: validE_R_def) apply (rule bindE_wp_fwd_skip, wpsimp wp: checkPrio_inv) apply (rule bindE_wp[OF _ checkPrio_lt_ct_weak'[unfolded validE_R_def]])+ - apply (wpsimp wp: checkPrio_lt_ct_weak gts_wp' threadGet_wp split_del: if_split) - apply (clarsimp simp: maxPriority_def numPriorities_def pred_tcb_at'_def obj_at'_def) - using max_word_max [of \UCAST(64 \ 8) x\ for x] - apply (auto simp: max_word_mask numeral_eq_Suc mask_Suc) + apply (wp gts_wp' hoare_vcg_if_lift2 threadGet_wp | wpc | simp)+ + apply (clarsimp simp: maxPriority_def numPriorities_def pred_tcb_at'_def) + using max_word_max[of \UCAST(64 \ 8) x\ for x] + apply (auto simp: max_word_mask numeral_eq_Suc mask_Suc split: if_splits) done (* FIXME RT: There's probably a way to avoid this using cap.case_eq_if and corres_if, but it @@ -2853,6 +2889,7 @@ lemma decodeSetSchedParams_corres: (invs' and (\s. s \' cap' \ (\x \ set extras'. s \' (fst x)))) (decode_set_sched_params args cap slot extras) (decodeSetSchedParams args cap' slot' extras')" + supply if_split[split del] apply (clarsimp simp: is_cap_simps) apply (simp add: decode_set_sched_params_def decodeSetSchedParams_def decode_update_sc_def check_handler_ep_def unlessE_whenE) @@ -2899,12 +2936,11 @@ lemma decodeSetSchedParams_corres: apply (fastforce simp: valid_cap_def) apply (clarsimp simp: valid_cap_simps') apply normalise_obj_at' - apply (intro exI impI conjI allI) - apply (clarsimp simp: obj_at'_def ko_wp_at'_def) - apply (rename_tac obj) - apply (case_tac obj; clarsimp) - apply (erule invs_valid_objs') - apply (clarsimp simp: obj_at'_def) + apply (frule invs_valid_objs') + apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') + apply (clarsimp simp: obj_at'_def ko_wp_at'_def split: kernel_object.splits) + apply (rename_tac obj) + apply (case_tac obj; clarsimp) done lemma checkValidIPCBuffer_corres: @@ -3482,8 +3518,26 @@ lemma decodeTCBInvocation_corres: elim!: list_all2_mono) done +lemma decodeSetSchedParams_inv: + "decodeSetSchedParams args cap slot extras \P\" + unfolding decodeSetSchedParams_def + apply (cases args; cases extras; clarsimp) + apply wpsimp + apply wpsimp + apply (clarsimp split: list.splits; safe; wpsimp) + apply (clarsimp split: list.splits) + apply (intro conjI impI allI) + apply wpsimp + apply wpsimp + apply wpsimp + apply forward_inv_step + apply (forward_inv_step wp: checkPrio_inv) + apply (forward_inv_step wp: checkPrio_inv) + apply forward_inv_step + by (wp scReleased_inv hoare_vcg_if_lift2 hoare_drop_imps checkPrio_inv | simp | wpc)+ + crunch decodeTCBInvocation - for inv[wp]: P + for inv[wp]: P (simp: crunch_simps wp: crunch_wps) lemma real_cte_at_not_tcb_at': diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy index 7e4b4c7ef8..32872ba37b 100644 --- a/spec/abstract/Decode_A.thy +++ b/spec/abstract/Decode_A.thy @@ -316,28 +316,27 @@ where (tc_new_croot space) (tc_new_vroot space) None odE" -definition - decode_update_sc :: "cap \ cslot_ptr \ cap \ (obj_ref option,'z::state_ext) se_monad" -where +definition decode_update_sc :: + "cap \ cslot_ptr \ cap \ (obj_ref option option, 'z::state_ext) se_monad" where "decode_update_sc cap slot sc_cap \ (case sc_cap of NullCap \ doE tcb_ptr \ returnOk $ obj_ref_of cap; ct_ptr \ liftE $ gets cur_thread; whenE (tcb_ptr = ct_ptr) $ throwError IllegalOperation; - returnOk None + returnOk $ Some None odE | SchedContextCap _ _ \ doE tcb_ptr \ returnOk $ obj_ref_of cap; sc_ptr \ returnOk $ obj_ref_of sc_cap; sc_ptr' \ liftE $ get_tcb_obj_ref tcb_sched_context tcb_ptr; - whenE (sc_ptr' \ None) $ throwError IllegalOperation; + whenE (sc_ptr' \ None \ sc_ptr' \ Some sc_ptr) $ throwError IllegalOperation; sc \ liftE $ get_sched_context sc_ptr; whenE (sc_tcb sc \ None) $ throwError IllegalOperation; blocked \ liftE $ is_blocked tcb_ptr; released \ liftE $ get_sc_released sc_ptr; whenE (blocked \ \released) $ throwError IllegalOperation; - returnOk $ Some sc_ptr + returnOk $ if sc_ptr' = Some sc_ptr then None else Some (Some sc_ptr) odE | _ \ throwError (InvalidCapability 2))" @@ -416,9 +415,9 @@ where returnOk (SetTLSBase (obj_ref_of cap) (ucast (args ! 0))) odE" -definition - decode_set_sched_params :: "data list \ cap \ cslot_ptr \ (cap \ cslot_ptr) list \ (tcb_invocation,'z::state_ext) se_monad" -where +definition decode_set_sched_params :: + "data list \ cap \ cslot_ptr \ (cap \ cslot_ptr) list \ (tcb_invocation,'z::state_ext) se_monad" + where "decode_set_sched_params args cap slot extra_caps \ doE whenE (length args < 2) $ throwError TruncatedMessage; whenE (length extra_caps < 3) $ throwError TruncatedMessage; @@ -432,11 +431,11 @@ where | _ \ throwError (InvalidCapability 1); check_prio (args ! 0) auth_tcb; check_prio (args ! 1) auth_tcb; - sc \ decode_update_sc cap slot sc_cap; + sc_ptr_opt_opt \ decode_update_sc cap slot sc_cap; fh \ check_handler_ep 3 fh_arg; returnOk $ ThreadControlSched (obj_ref_of cap) slot (Some fh) - (Some (new_mcp, auth_tcb)) (Some (new_prio, auth_tcb)) - (Some sc) + (Some (new_mcp, auth_tcb)) (Some (new_prio, auth_tcb)) + sc_ptr_opt_opt odE" definition diff --git a/spec/abstract/SchedContext_A.thy b/spec/abstract/SchedContext_A.thy index 2e09b413d9..cec5241bee 100644 --- a/spec/abstract/SchedContext_A.thy +++ b/spec/abstract/SchedContext_A.thy @@ -392,14 +392,6 @@ where od od" -definition - maybe_sched_context_bind_tcb :: "obj_ref \ obj_ref \ (unit, 'z::state_ext) s_monad" -where - "maybe_sched_context_bind_tcb sc_ptr tcb_ptr = do - sc' \ get_tcb_obj_ref tcb_sched_context tcb_ptr; - when (sc' \ Some sc_ptr) $ sched_context_bind_tcb sc_ptr tcb_ptr - od" - definition sched_context_set_inactive :: "obj_ref \ (unit, 'z::state_ext) s_monad" where diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy index 8842788f8e..013c0c27a6 100644 --- a/spec/abstract/Tcb_A.thy +++ b/spec/abstract/Tcb_A.thy @@ -189,7 +189,7 @@ where liftE $ maybeM (\(prio, _). set_priority target prio) priority; liftE $ maybeM (\scopt. case scopt of None \ maybe_sched_context_unbind_tcb target - | Some sc_ptr \ maybe_sched_context_bind_tcb sc_ptr target) sc; + | Some sc_ptr \ sched_context_bind_tcb sc_ptr target) sc; returnOk [] odE" diff --git a/spec/haskell/src/SEL4/Object/TCB.lhs b/spec/haskell/src/SEL4/Object/TCB.lhs index 8a357d8385..a03f5e3920 100644 --- a/spec/haskell/src/SEL4/Object/TCB.lhs +++ b/spec/haskell/src/SEL4/Object/TCB.lhs @@ -265,20 +265,20 @@ The "SetSchedParams" call sets both the priority and the MCP in a single call. > tcbPtr <- case cap of > ThreadCap { capTCBPtr = tcbPtr } -> return tcbPtr > _ -> throw $ InvalidCapability 1 -> scPtr <- case scCap of +> scPtrOptOpt <- case scCap of > SchedContextCap { capSchedContextPtr = scPtr } -> do > tcbSc <- withoutFailure $ threadGet tcbSchedContext tcbPtr -> when (tcbSc /= Nothing) $ throw IllegalOperation +> when (tcbSc /= Nothing && tcbSc /= Just scPtr) $ throw IllegalOperation > sc <- withoutFailure $ getSchedContext scPtr > when (scTCB sc /= Nothing) $ throw IllegalOperation > blocked <- withoutFailure $ isBlocked tcbPtr > released <- withoutFailure $ scReleased scPtr > when (blocked && not released) $ throw IllegalOperation -> return $ Just scPtr +> return $ if tcbSc == Just scPtr then Nothing else Just (Just scPtr) > NullCap -> do > curTcbPtr <- withoutFailure getCurThread > when (tcbPtr == curTcbPtr) $ throw IllegalOperation -> return Nothing +> return $ Just Nothing > _ -> throw $ InvalidCapability 2 > when (not $ isValidFaultHandler fhCap) $ throw $ InvalidCapability 3 > return $ ThreadControlSched { @@ -287,7 +287,7 @@ The "SetSchedParams" call sets both the priority and the MCP in a single call. > tcSchedFaultHandler = Just (fhCap, fhSlot), > tcSchedMCPriority = Just (fromIntegral newMCP, authTCB), > tcSchedPriority = Just (fromIntegral newPrio, authTCB), -> tcSchedSchedContext = Just scPtr } +> tcSchedSchedContext = scPtrOptOpt } > decodeSetSchedParams _ _ _ _ = throw TruncatedMessage \subsubsection{The Set IPC Buffer Call} @@ -505,9 +505,9 @@ The use of "checkCapAt" addresses a corner case in which the only capability to > installThreadBuffer target slot buffer > return [] -> invokeTCB (ThreadControlSched target slot faultHandler mcPriority priority sc) +> invokeTCB (ThreadControlSched target slot faultHandler mcPriority priority scPtrOptOpt) > = do -> stateAssert (tcs_cross_asrt1 target sc) +> stateAssert (tcs_cross_asrt1 target scPtrOptOpt) > "Assert some conditions that hold in the abstract at this point" > stateAssert valid_idle'_asrt > "Assert that `valid_idle' s` holds" @@ -519,14 +519,14 @@ The use of "checkCapAt" addresses a corner case in which the only capability to > "Assert some conditions that hold in the abstract at this point" > let priority' = mapMaybe fst priority > maybe (return ()) (setPriority target) priority' -> targetScOpt <- mapTCBPtr target tcbSchedContext -> case sc of +> case scPtrOptOpt of > Nothing -> return () -> Just Nothing -> case targetScOpt of -> Nothing -> return () -> Just targetSc -> schedContextUnbindTCB targetSc -> Just (Just scPtr) -> -> when (sc /= Just targetScOpt) $ schedContextBindTCB scPtr target +> Just Nothing -> do +> targetScOpt <- threadGet tcbSchedContext target +> case targetScOpt of +> Nothing -> return () +> Just targetSc -> schedContextUnbindTCB targetSc +> Just (Just scPtr) -> schedContextBindTCB scPtr target > return [] \subsubsection{Register State}