diff --git a/proof/capDL-api/Kernel_DP.thy b/proof/capDL-api/Kernel_DP.thy index 83118e25f..99b8f5df4 100644 --- a/proof/capDL-api/Kernel_DP.thy +++ b/proof/capDL-api/Kernel_DP.thy @@ -133,7 +133,7 @@ where cdl_intent_error = False, cdl_intent_cap = tcb_cap, cdl_intent_extras = [], - cdl_intent_recv_slot = None\ False" + cdl_intent_recv_slot = None\ True" definition seL4_TCB_WriteRegisters :: "cdl_cptr \ bool \ word8 \ word32 \ cdl_raw_usercontext \ bool u_monad" where diff --git a/proof/capDL-api/TCB_DP.thy b/proof/capDL-api/TCB_DP.thy index 0cbfb6ef2..9f9d862cc 100644 --- a/proof/capDL-api/TCB_DP.thy +++ b/proof/capDL-api/TCB_DP.thy @@ -19,6 +19,35 @@ lemma reset_cap_asid_reset_mem_mapping: "reset_cap_asid (reset_mem_mapping cap) = reset_cap_asid cap" by (clarsimp simp: reset_cap_asid_def cap_type_def split:cdl_cap.splits) +lemma ipc_cancel_return: + "\< (tcb, tcb_pending_op_slot) \c NullCap \* (\_. True) > and R \ipc_cancel tcb\\_. R\" + apply (clarsimp simp:ipc_cancel_def) + apply wp + apply (rule_tac P = "cap = NullCap" in hoare_gen_asm) + apply (wp | simp)+ + apply clarsimp + apply (drule opt_cap_sep_imp) + apply (clarsimp simp:reset_cap_asid_simps2) + done + +lemma restart_null_wp: + "\ < (tcb,tcb_pending_op_slot) \c NullCap + \* (tcb, tcb_replycap_slot) \c- + \* R > \ + restart tcb + \\_. < (tcb,tcb_pending_op_slot) \c RestartCap + \* (tcb, tcb_replycap_slot) \c (MasterReplyCap tcb) \* R > \" + apply (clarsimp simp:restart_def) + apply (wp set_cap_wp[sep_wand_wp]) + apply (rule hoare_post_imp[OF _ ipc_cancel_return]) + apply (assumption) + apply (wp get_cap_wp) + apply (frule opt_cap_sep_imp) + apply (clarsimp dest!:reset_cap_asid_simps2) + apply (rule conjI) + apply sep_solve + apply sep_solve + done lemma restart_wp: "cap = RunningCap \ cap = RestartCap \ @@ -1321,7 +1350,8 @@ shows cnode_id = cap_object cnode_cap \ \ \ \ root_tcb_id \f root_tcb \* (root_tcb_id, tcb_pending_op_slot) \c RunningCap - \* (cap_object tcb_cap, tcb_pending_op_slot) \c - + \* (cap_object tcb_cap, tcb_pending_op_slot) \c NullCap + \* (cap_object tcb_cap, tcb_replycap_slot) \c - \* (root_tcb_id, tcb_cspace_slot) \c cnode_cap \* cap_object cnode_cap \f CNode (empty_cnode root_size) \* (cap_object cnode_cap, offset tcb_ref root_size) \c tcb_cap @@ -1330,6 +1360,7 @@ shows \\_. \ root_tcb_id \f root_tcb \* (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* (cap_object tcb_cap, tcb_pending_op_slot) \c RestartCap + \* (cap_object tcb_cap, tcb_replycap_slot) \c MasterReplyCap (cap_object tcb_cap) \* (root_tcb_id, tcb_cspace_slot) \c cnode_cap \* cap_object cnode_cap \f CNode (empty_cnode root_size) \* (cap_object cnode_cap, offset tcb_ref root_size) \c tcb_cap @@ -1339,38 +1370,35 @@ shows apply (rule hoare_pre) apply (wp do_kernel_op_pull_back) apply (rule hoare_post_imp[OF _ call_kernel_with_intent_allow_error_helper - [where check = False,simplified]]) - apply clarsimp - apply (case_tac r,(clarsimp,assumption)+)[1] + [where check = True,simplified]]) + apply simp apply fastforce apply (rule hoare_strengthen_post[OF set_cap_wp]) apply (sep_select 2,sep_cancel) apply wp[4] apply (rule_tac P= " iv = (InvokeTcb $ Resume (cap_object tcb_cap))" in hoare_gen_asmEx) - apply (clarsimp simp:invoke_tcb_def) -sorry (* ipc_cancel - apply (wp restart_cdl_current_thread[where cap = NullCap] - restart_cdl_current_domain[where cap = NullCap]) - apply (rule_tac R1="root_tcb_id \f Tcb cdl_tcb_ext + apply (clarsimp simp:invoke_tcb_def) + apply (wp restart_cdl_current_thread[where cap = NullCap] + restart_cdl_current_domain[where cap = NullCap]) + apply (rule_tac R1="root_tcb_id \f Tcb cdl_tcb_ext \* (root_tcb_id, tcb_pending_op_slot) \c RestartCap \* ?Q" in - hoare_post_imp[OF _ restart_wp[where cap = RestartCap ]]) - apply (rule conjI,sep_solve) - apply (rule sep_any_imp_c'_conj) - apply sep_cancel - apply sep_cancel - apply simp - apply wp + hoare_post_imp[OF _ restart_null_wp]) + apply (rule conjI,sep_solve) + apply (rule sep_any_imp_c'_conj) + apply sep_cancel + apply sep_cancel + apply simp apply (simp add:is_pending_cap_def conj_ac) apply (wp set_cap_wp hoare_vcg_conj_lift) - apply (rule_tac R1 ="(cap_object tcb_cap, tcb_pending_op_slot) \c RestartCap \* (\_. True)" + apply (rule_tac R1 ="(cap_object tcb_cap, tcb_pending_op_slot) \c NullCap \* (\_. True)" in hoare_post_imp[OF _ set_cap_wp]) apply sep_cancel apply simp apply (rule_tac R1="root_tcb_id \f Tcb cdl_tcb_ext \* ?Q" in hoare_post_imp[OF _ set_cap_wp]) + apply (sep_select 4,sep_cancel) apply (sep_select 3,sep_cancel) - apply (sep_select 2,sep_cancel) apply (rule_tac P = "c = TcbCap (cap_object tcb_cap) " in hoare_gen_asmEx) apply (simp add: decode_invocation_def @@ -1413,6 +1441,5 @@ sorry (* ipc_cancel apply sep_solve done -*) end diff --git a/proof/drefine/Tcb_DR.thy b/proof/drefine/Tcb_DR.thy index 969ffde36..5a894e73e 100644 --- a/proof/drefine/Tcb_DR.thy +++ b/proof/drefine/Tcb_DR.thy @@ -533,7 +533,6 @@ lemma restart_corres: apply (rule dcorres_rhs_noop_below_True[OF dcorres_rhs_noop_below_True]) apply (rule switch_if_required_to_dcorres) apply (rule tcb_sched_action_dcorres) - apply (rule corres_alternate1) apply (rule dcorres_set_thread_state_Restart2[unfolded tcb_pending_op_slot_def]) apply wp apply (simp add:not_idle_thread_def) diff --git a/spec/capDL/Tcb_D.thy b/spec/capDL/Tcb_D.thy index e86d9b6ea..841b334fc 100644 --- a/spec/capDL/Tcb_D.thy +++ b/spec/capDL/Tcb_D.thy @@ -201,7 +201,7 @@ where (do CSpace_D.ipc_cancel target_tcb; KHeap_D.set_cap (target_tcb,tcb_replycap_slot) (cdl_cap.MasterReplyCap target_tcb); - KHeap_D.set_cap (target_tcb,tcb_pending_op_slot) (cdl_cap.RestartCap) \ return () + KHeap_D.set_cap (target_tcb,tcb_pending_op_slot) (cdl_cap.RestartCap) od) od"