From f90f11e3152af79688529aa2878b3be5502d0f2b Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Fri, 15 Jul 2022 16:21:09 +0930 Subject: [PATCH] rt riscv refine: add release_q_runnable_asrt to deleteObjects Signed-off-by: Michael McInerney --- proof/refine/RISCV64/Detype_R.thy | 14 ++++++++------ proof/refine/RISCV64/KHeap_R.thy | 19 +++++++++++++++++++ proof/refine/RISCV64/TcbAcc_R.thy | 12 ------------ 3 files changed, 27 insertions(+), 18 deletions(-) diff --git a/proof/refine/RISCV64/Detype_R.thy b/proof/refine/RISCV64/Detype_R.thy index c672d78fae..6457ad785d 100644 --- a/proof/refine/RISCV64/Detype_R.thy +++ b/proof/refine/RISCV64/Detype_R.thy @@ -109,6 +109,9 @@ defs cNodePartialOverlap_def: \ (\ mask_range p (cte_level_bits + n) \ {p. inRange p} \ \ mask_range p (cte_level_bits + n) \ {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: @@ -116,6 +119,7 @@ lemma deleteObjects_def2: 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 \ mask_range ptr bits)) []; @@ -149,6 +153,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); @@ -843,19 +848,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/RISCV64/KHeap_R.thy b/proof/refine/RISCV64/KHeap_R.thy index 9662afe8df..52dd49453e 100644 --- a/proof/refine/RISCV64/KHeap_R.thy +++ b/proof/refine/RISCV64/KHeap_R.thy @@ -5005,6 +5005,18 @@ 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.\ @@ -5037,6 +5049,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/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy index d89f20b218..fa1e3191ad 100644 --- a/proof/refine/RISCV64/TcbAcc_R.thy +++ b/proof/refine/RISCV64/TcbAcc_R.thy @@ -4565,18 +4565,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'