From 5f1eb8b0a1bf18ec08fca771ba14468ded0d6913 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Fri, 15 Jul 2022 16:23:35 +0930 Subject: [PATCH] rt arm refine: add release_q_runnable_asrt to deleteObjects Signed-off-by: Michael McInerney --- proof/refine/ARM/Detype_R.thy | 15 +++++++++------ proof/refine/ARM/KHeap_R.thy | 20 ++++++++++++++++++++ proof/refine/ARM/PageTableDuplicates.thy | 17 +++++++---------- proof/refine/ARM/TcbAcc_R.thy | 12 ------------ 4 files changed, 36 insertions(+), 28 deletions(-) diff --git a/proof/refine/ARM/Detype_R.thy b/proof/refine/ARM/Detype_R.thy index 01a90014da..1112f3f134 100644 --- a/proof/refine/ARM/Detype_R.thy +++ b/proof/refine/ARM/Detype_R.thy @@ -106,12 +106,17 @@ defs cNodePartialOverlap_def: \ (\ {p .. p + 2 ^ (cte_level_bits + n) - 1} \ {p. inRange p} \ \ {p .. p + 2 ^ (cte_level_bits + n) - 1} \ {p. \ inRange p}))" +defs release_q_runnable_asrt_def: + "release_q_runnable_asrt \ + \s. \p. p \ set (ksReleaseQueue s) \ obj_at' (runnable' \ tcbState) p s" + (* FIXME: move *) lemma deleteObjects_def2: "is_aligned ptr bits \ deleteObjects ptr bits = do stateAssert sym_refs_asrt []; stateAssert valid_idle'_asrt []; + stateAssert release_q_runnable_asrt []; stateAssert (deletionIsSafe ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ {ptr .. ptr + 2 ^ bits - 1})) []; @@ -145,6 +150,7 @@ lemma deleteObjects_def3: do stateAssert sym_refs_asrt []; stateAssert valid_idle'_asrt []; + stateAssert release_q_runnable_asrt []; assert (is_aligned ptr bits); stateAssert (deletionIsSafe ptr bits) []; doMachineOp (freeMemory ptr bits); @@ -887,19 +893,16 @@ lemma deleteObjects_corres: \ s' \' (UntypedCap d base magnitude idx)) (delete_objects base magnitude) (deleteObjects base magnitude)" (is "_ \ _ \ corres _ _ ?conc_guard _ _") - apply (rule corres_cross_over_guard - [where Q="?conc_guard - and (\s'. \p. p \ set (ksReleaseQueue s') - \ obj_at' (runnable' \ tcbState) p s')"]) - apply (simp add: pred_conj_def) - apply (erule ksReleaseQueue_runnable_thread_state; fastforce?) apply add_sym_refs apply add_valid_idle' + apply add_release_q_runnable apply (simp add: deleteObjects_def2) apply (rule corres_stateAssert_add_assertion[rotated]) apply (clarsimp simp: sym_refs_asrt_def) apply (rule corres_stateAssert_add_assertion[rotated]) apply (clarsimp simp: valid_idle'_asrt_def) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (clarsimp simp: release_q_runnable_asrt_def) apply (rule corres_stateAssert_add_assertion) prefer 2 apply clarsimp diff --git a/proof/refine/ARM/KHeap_R.thy b/proof/refine/ARM/KHeap_R.thy index b420ecdc48..f5ad5085c0 100644 --- a/proof/refine/ARM/KHeap_R.thy +++ b/proof/refine/ARM/KHeap_R.thy @@ -5089,6 +5089,19 @@ lemma is_active_sc'2_cross: active_sc_def opt_map_red StateRelation.is_active_sc'_def) done +lemma release_q_runnable_cross: + "\(s,s') \ state_relation; valid_release_q s; pspace_aligned s; pspace_distinct s\ \ + \p. p \ set (ksReleaseQueue s') \ obj_at' (runnable' \ tcbState) p s'" + apply (frule state_relation_release_queue_relation) + apply (clarsimp simp: valid_release_q_def obj_at'_def release_queue_relation_def) + apply (drule_tac x=p in bspec, blast) + apply (clarsimp simp: vs_all_heap_simps) + apply (frule_tac t=p in st_tcb_at_coerce_concrete[rotated, where P=runnable], simp, simp) + apply (clarsimp simp: pred_tcb_at_def obj_at_def) + apply (clarsimp simp: pred_tcb_at'_def obj_at'_def sts_rel_runnable) + done + + \ \Some methods to add invariants to the concrete guard of a corres proof. Often used for properties that are asserted to hold in the Haskell definition.\ @@ -5121,6 +5134,13 @@ method add_ready_qs_runnable = (frule valid_sched_valid_ready_qs)?, (frule invs_psp_aligned)?, (frule invs_distinct)?, fastforce dest: ready_qs_runnable_cross +method add_release_q_runnable = + rule_tac Q="\s'. \p. p \ set (ksReleaseQueue s') \ obj_at' (runnable' \ tcbState) p s'" + in corres_cross_add_guard, + (simp only: pred_conj_def)?, + (frule valid_sched_valid_release_q)?, (frule invs_psp_aligned)?, (frule invs_distinct)?, + fastforce dest: release_q_runnable_cross + method add_valid_replies for rptr uses simp = rule_tac Q="\s. valid_replies'_sc_asrt rptr s" in corres_cross_add_guard, fastforce elim: valid_replies_sc_cross simp: simp diff --git a/proof/refine/ARM/PageTableDuplicates.thy b/proof/refine/ARM/PageTableDuplicates.thy index cceb7a8d81..58a2a2c828 100644 --- a/proof/refine/ARM/PageTableDuplicates.thy +++ b/proof/refine/ARM/PageTableDuplicates.thy @@ -1323,19 +1323,16 @@ lemma valid_duplicates_deleteObjects_helper: done lemma deleteObjects_valid_duplicates'[wp]: - notes [simp del] = atLeastAtMost_simps + notes [simp del] = atLeastAtMost_simps shows - "\(\s. vs_valid_duplicates' (ksPSpace s)) and - K (is_aligned ptr sz) - \ deleteObjects ptr sz - \\r s. vs_valid_duplicates' (ksPSpace s)\" + "\(\s. vs_valid_duplicates' (ksPSpace s)) and K (is_aligned ptr sz)\ + deleteObjects ptr sz + \\_ s. vs_valid_duplicates' (ksPSpace s)\" apply (rule hoare_gen_asm) apply (clarsimp simp: deleteObjects_def2) - apply (rule hoare_seq_ext_skip, wpsimp) - apply (rule hoare_seq_ext_skip, wpsimp) - apply (wp hoare_drop_imps|simp)+ - apply clarsimp - apply (simp add:deletionIsSafe_def) + apply (intro hoare_seq_ext[OF _ stateAssert_sp]) + apply (wpsimp wp: hoare_drop_imps) + apply (clarsimp simp: deletionIsSafe_def) apply (erule valid_duplicates_deleteObjects_helper) apply fastforce apply simp diff --git a/proof/refine/ARM/TcbAcc_R.thy b/proof/refine/ARM/TcbAcc_R.thy index 3a75ac6999..00b6320d6f 100644 --- a/proof/refine/ARM/TcbAcc_R.thy +++ b/proof/refine/ARM/TcbAcc_R.thy @@ -4561,18 +4561,6 @@ lemma tcbReleaseRemove_pred_tcb_at'[wp]: crunches tcbReleaseRemove for weak_sch_act_wf[wp]: "\s. weak_sch_act_wf (ksSchedulerAction s) s" -lemma ksReleaseQueue_runnable_thread_state: - "\(s,s') \ state_relation; valid_release_q s; pspace_aligned s; pspace_distinct s\ - \ \p. p \ set (ksReleaseQueue s') \ obj_at' (runnable' \ tcbState) p s'" - apply (frule state_relation_release_queue_relation) - apply (clarsimp simp: valid_release_q_def obj_at'_def release_queue_relation_def) - apply (drule_tac x=p in bspec, blast) - apply (clarsimp simp: vs_all_heap_simps) - apply (frule_tac t=p in st_tcb_at_coerce_concrete[rotated, where P=runnable], simp, simp) - apply (clarsimp simp: pred_tcb_at_def obj_at_def) - apply (clarsimp simp: pred_tcb_at'_def obj_at'_def sts_rel_runnable) - done - lemma sts_st_tcb': "\if t = t' then K (P st) else st_tcb_at' P t\ setThreadState st t'