Skip to content

Commit

Permalink
rt crefine: address PR comments squash
Browse files Browse the repository at this point in the history 
Signed-off-by: Michael McInerney <[email protected]>
  • Loading branch information
@michaelmcinerney
michaelmcinerney committed Sep 10, 2024
1 parent fda6c62 commit 341c6bb
Show file tree
Hide file tree
Showing 3 changed files with 64 additions and 54 deletions.
81 changes: 36 additions & 45 deletions proof/crefine/RISCV64/Finalise_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ declare if_split [split del]
definition
"option_map2 f m = option_map f \<circ> m"

lemma thread_state_ptr_set_tcbQueued_tcb_fields:
lemma thread_state_ptr_set_tcbQueued_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. s \<Turnstile>\<^sub>c (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C''] :: tcb_C ptr)\<rbrace>
Call thread_state_ptr_set_tcbQueued_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
Expand All @@ -55,7 +55,7 @@ lemma thread_state_ptr_set_tcbQueued_tcb_fields:
split: if_splits\<close>)
done

lemma thread_state_ptr_set_tsType_tcb_fields:
lemma thread_state_ptr_set_tsType_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. s \<Turnstile>\<^sub>c (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C''] :: tcb_C ptr)\<rbrace>
Call thread_state_ptr_set_tsType_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
Expand All @@ -75,7 +75,7 @@ lemma thread_state_ptr_set_tsType_tcb_fields:
split: if_splits\<close>)
done

lemma tcb_queue_prepend_tcb_fields:
lemma tcb_queue_prepend_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
Call tcb_queue_prepend_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
Expand All @@ -88,7 +88,7 @@ lemma tcb_queue_prepend_tcb_fields:
split: if_splits)
done

lemma addToBitmap_tcb_fields:
lemma addToBitmap_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
Call addToBitmap_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
Expand All @@ -100,7 +100,7 @@ lemma addToBitmap_tcb_fields:
apply clarsimp
done

lemma ready_queues_index_tcb_fields:
lemma ready_queues_index_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
Call ready_queues_index_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
Expand All @@ -113,7 +113,7 @@ lemma ready_queues_index_tcb_fields:
apply clarsimp
done

lemma tcbSchedEnqueue_tcb_fields:
lemma tcbSchedEnqueue_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. True\<rbrace>
Call tcbSchedEnqueue_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
Expand All @@ -122,14 +122,14 @@ lemma tcbSchedEnqueue_tcb_fields:
\<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)}"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (rule allI, rule conseqPre)
apply (vcg exspec=thread_state_ptr_set_tcbQueued_tcb_fields
exspec=tcb_queue_prepend_tcb_fields
exspec=addToBitmap_tcb_fields
exspec=ready_queues_index_tcb_fields)
apply (vcg exspec=thread_state_ptr_set_tcbQueued_spec_tcb_fields
exspec=tcb_queue_prepend_spec_tcb_fields
exspec=addToBitmap_spec_tcb_fields
exspec=ready_queues_index_spec_tcb_fields)
apply simp
done

lemma isSchedulable_tcb_fields:
lemma isSchedulable_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
Call isSchedulable_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
Expand All @@ -141,45 +141,45 @@ lemma isSchedulable_tcb_fields:
apply clarsimp
done

lemma rescheduleRequired_tcb_fields:
lemma rescheduleRequired_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
Call rescheduleRequired_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
\<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)
\<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s)
\<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)}"
apply (rule allI, rule conseqPre)
apply (vcg exspec=tcbSchedEnqueue_tcb_fields exspec=isSchedulable_tcb_fields)
apply (vcg exspec=tcbSchedEnqueue_spec_tcb_fields exspec=isSchedulable_spec_tcb_fields)
apply clarsimp
done

lemma possibleSwitchTo_tcb_fields:
lemma possibleSwitchTo_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
Call possibleSwitchTo_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
\<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)
\<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s)
\<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)}"
apply (rule allI, rule conseqPre)
apply (vcg exspec=rescheduleRequired_tcb_fields exspec=tcbSchedEnqueue_tcb_fields)
apply (vcg exspec=rescheduleRequired_spec_tcb_fields exspec=tcbSchedEnqueue_spec_tcb_fields)
apply clarsimp
done

lemma setThreadState_tcb_fields:
lemma setThreadState_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
Call setThreadState_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
\<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)
\<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s)
\<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)}"
apply (rule allI, rule conseqPre)
apply (vcg exspec=rescheduleRequired_tcb_fields
exspec=thread_state_ptr_set_tsType_tcb_fields
exspec=isSchedulable_tcb_fields)
apply (vcg exspec=rescheduleRequired_spec_tcb_fields
exspec=thread_state_ptr_set_tsType_spec_tcb_fields
exspec=isSchedulable_spec_tcb_fields)
apply clarsimp
done

lemma refill_head_overlapping_tcb_fields:
lemma refill_head_overlapping_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
Call refill_head_overlapping_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
Expand All @@ -191,7 +191,7 @@ lemma refill_head_overlapping_tcb_fields:
apply clarsimp
done

lemma refill_pop_head_tcb_fields:
lemma refill_pop_head_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
Call refill_pop_head_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
Expand All @@ -203,56 +203,47 @@ lemma refill_pop_head_tcb_fields:
apply (clarsimp simp: typ_heap_simps)
done

lemma merge_overlapping_head_refill_tcb_fields:
lemma merge_overlapping_head_refill_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
Call merge_overlapping_head_refill_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
\<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)
\<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s)
\<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)}"
apply (rule allI, rule conseqPre)
apply (vcg exspec=refill_pop_head_tcb_fields exspec=refill_head_modifies
apply (vcg exspec=refill_pop_head_spec_tcb_fields exspec=refill_head_modifies
exspec=refill_index_modifies)
apply (clarsimp simp: typ_heap_simps)
done

lemma refill_unblock_check_tcb_fields:
lemma refill_unblock_check_spec_tcb_fields:
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
Call refill_unblock_check_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
\<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)
\<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s)
\<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)}"
(is "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} ?f ({s'. ?post s s'})")
apply (rule allI, rule conseqPre)
apply vcg_step
apply vcg_step
apply vcg_step
apply vcg_step
apply vcg_step
apply vcg_step
apply (rule HoarePartial.SeqSwap)
apply (rule_tac I="{t. ?post t s}" in HoarePartial.reannotateWhileNoGuard)
apply (vcg exspec=merge_overlapping_head_refill_tcb_fields
exspec=refill_head_overlapping_tcb_fields)
apply fastforce
apply fastforce
apply (vcg exspec=refill_head_overlapping_tcb_fields)
apply vcg
apply (rule order_refl)
apply vcg
by (clarsimp simp: typ_heap_simps)
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (clarsimp simp: whileAnno_def)
apply (rule_tac I1="{t. ?post t s}" in subst[OF whileAnno_def])
apply (vcg exspec=merge_overlapping_head_refill_spec_tcb_fields
exspec=refill_head_overlapping_spec_tcb_fields)
subgoal by (clarsimp simp: option_map2_def typ_heap_simps split: if_splits)
apply fastforce
apply fastforce
done

lemma restart_thread_if_no_fault_tcb_fields:
lemma restart_thread_if_no_fault_spec_tcb_fields:
"\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s}
Call restart_thread_if_no_fault_'proc
{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
\<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)
\<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s)
\<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)}"
apply (rule allI, rule conseqPre)
apply (vcg exspec=possibleSwitchTo_tcb_fields exspec=setThreadState_tcb_fields
exspec=refill_unblock_check_tcb_fields)
apply (vcg exspec=possibleSwitchTo_spec_tcb_fields exspec=setThreadState_spec_tcb_fields
exspec=refill_unblock_check_spec_tcb_fields)
apply clarsimp
done

Expand Down
14 changes: 5 additions & 9 deletions proof/crefine/RISCV64/Recycle_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -840,15 +840,14 @@ lemma restart_thread_if_no_fault_ccorres:
apply (simp add: if_to_top_of_bind)
apply (rule ccorres_if_lhs)
apply (clarsimp simp: bind_assoc, rename_tac scPtr)
apply (wpfix add: option.sel)
apply wpfix
apply (rule ccorres_pre_getObject_sc, rename_tac sc)
apply (rule ccorres_pre_getCurSc, rename_tac cur_sc)
apply (rule_tac xf'="ret__unsigned_long_'"
and val="from_bool (scSporadic sc)"
and R="obj_at' (\<lambda>tcb. tcbSchedContext tcb = Some scPtr) t and ko_at' sc scPtr
and no_0_obj'"
and R'=UNIV
in ccorres_symb_exec_r_known_rv)
in ccorres_symb_exec_r_known_rv[where R'=UNIV])
apply (rule conseqPre, vcg)
apply normalise_obj_at'
apply (frule (1) obj_at_cslift_tcb)
Expand Down Expand Up @@ -879,8 +878,7 @@ lemma restart_thread_if_no_fault_ccorres:
apply (rule_tac xf'="ret__unsigned_long_'"
and val="from_bool False"
and R="obj_at' (\<lambda>tcb. tcbSchedContext tcb = None) t"
and R'=UNIV
in ccorres_symb_exec_r_known_rv)
in ccorres_symb_exec_r_known_rv[where R'=UNIV])
apply (rule conseqPre, vcg)
apply clarsimp
apply (frule (1) obj_at_cslift_tcb)
Expand All @@ -898,8 +896,7 @@ lemma restart_thread_if_no_fault_ccorres:
apply wpsimp
apply (vcg exspec=setThreadState_modifies)
apply (ctac add: setThreadState_ccorres)
apply (fastforce simp: mask_def[where n=4] ThreadState_defs typ_heap_simps ctcb_relation_def
guard_is_UNIV_def from_bool_def)
apply (fastforce simp: typ_heap_simps ctcb_relation_def guard_is_UNIV_def from_bool_def)
apply fastforce
done

Expand Down Expand Up @@ -1148,7 +1145,7 @@ lemma cancelBadgedSends_ccorres:
sts_sch_act sts_valid_objs'
setThreadState_state_refs_of' threadGet_wp hoare_vcg_all_lift
| wp (once) hoare_drop_imps)+
apply (vcg exspec=restart_thread_if_no_fault_tcb_fields)
apply (vcg exspec=restart_thread_if_no_fault_spec_tcb_fields)
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_symb_exec_r2)
apply (drule_tac x="x @ [a]" in spec, simp)
Expand All @@ -1164,7 +1161,6 @@ lemma cancelBadgedSends_ccorres:
apply (clarsimp simp: typ_heap_simps st_tcb_at'_def)
apply (drule(1) obj_at_cslift_tcb)
apply (clarsimp simp: ctcb_relation_blocking_ipc_badge)

apply (rule context_conjI)
apply (clarsimp simp: tcb_queue_relation'_def)
apply (erule iffD2[OF ep_queue_relation_shift[rule_format], rotated -1])
Expand Down
23 changes: 23 additions & 0 deletions proof/crefine/RISCV64/Wellformed_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -598,6 +598,29 @@ abbreviation(input)
where
"prioInvalid == seL4_InvalidPrio"

(* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
lemma
shows ThreadState_Restart_mask[simp]:
"(scast ThreadState_Restart :: machine_word) && mask 4 = scast ThreadState_Restart"
and ThreadState_Inactive_mask[simp]:
"(scast ThreadState_Inactive :: machine_word) && mask 4 = scast ThreadState_Inactive"
and ThreadState_Running_mask[simp]:
"(scast ThreadState_Running :: machine_word) && mask 4 = scast ThreadState_Running"
and ThreadState_BlockedOnReceive_mask[simp]:
"(scast ThreadState_BlockedOnReceive :: machine_word) && mask 4
= scast ThreadState_BlockedOnReceive"
and ThreadState_BlockedOnSend_mask[simp]:
"(scast ThreadState_BlockedOnSend :: machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
and ThreadState_BlockedOnReply_mask[simp]:
"(scast ThreadState_BlockedOnReply :: machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
and ThreadState_BlockedOnNotification_mask[simp]:
"(scast ThreadState_BlockedOnNotification :: machine_word) && mask 4
= scast ThreadState_BlockedOnNotification"
and ThreadState_IdleThreadState_mask[simp]:
"(scast ThreadState_IdleThreadState :: machine_word) && mask 4 = scast ThreadState_IdleThreadState"
by (simp add: ThreadState_defs mask_def)+


(* generic lemmas with arch-specific consequences *)

schematic_goal size_gpRegisters:
Expand Down

0 comments on commit 341c6bb

Please sign in to comment.