Skip to content

Commit

Permalink
spec+proof: use linked lists in the design spec
Browse files Browse the repository at this point in the history 
This models the ready queues in the design spec as linked lists
via the tcbSchedNext and tcbSchedPrev pointers of a TCB, as in the C.

Library functions to update these linked lists are introduced, and used
to perform all functions which modify the ready queues.

Refinement between the linked lists and the Isabelle lists in the
abstract spec is handled via the predicate `heap_ls`.

`invs'` has been significantly modified, with the introduction of
`valid_sched_pointers` and `sym_heap_sched_pointers`. The various
invariants related to the bitmaps have been collected in the invariant
`valid_bitmaps`.

This includes a major revision to Orphanage, which now uses the
tcbQueued field of a TCB to indicate a thread's membership in a
ready queue, rather than the previous formulation which used
membership in the set of the Isabelle list.

Co-authored-by: Rafal Kolanski <[email protected]>
Co-authored-by: Gerwin Klein <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
  • Loading branch information
@michaelmcinerney @Xaphiosis @lsf37
3 people committed May 23, 2024
1 parent eb3db4b commit d869bb5
Show file tree
Hide file tree
Showing 267 changed files with 39,421 additions and 37,135 deletions.
183 changes: 126 additions & 57 deletions proof/crefine/AARCH64/ADT_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,8 +82,8 @@ lemma Basic_sem_eq:

lemma setTCBContext_C_corres:
"\<lbrakk> ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t \<rbrakk> \<Longrightarrow>
corres_underlying rf_sr nf nf' dc (pspace_domain_valid and tcb_at' t) \<top>
(threadSet (\<lambda>tcb. tcb \<lparr> tcbArch := atcbContextSet tc (tcbArch tcb)\<rparr>) t) (setTCBContext_C tc' t')"
corres_underlying rf_sr nf nf' dc (pspace_domain_valid and tcb_at' t) \<top>
(threadSet (\<lambda>tcb. tcb \<lparr> tcbArch := atcbContextSet tc (tcbArch tcb)\<rparr>) t) (setTCBContext_C tc' t')"
apply (simp add: setTCBContext_C_def exec_C_def Basic_sem_eq corres_underlying_def)
apply clarsimp
apply (simp add: threadSet_def bind_assoc split_def exec_gets)
Expand Down Expand Up @@ -112,8 +112,6 @@ lemma setTCBContext_C_corres:
apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def
cvariable_relation_upd_const ko_at_projectKO_opt cteSizeBits_def)
apply (simp add: cep_relations_drop_fun_upd)
apply (apply_conjunct \<open>match conclusion in \<open>cready_queues_relation _ _ _\<close> \<Rightarrow>
\<open>erule cready_queues_relation_not_queue_ptrs; rule ext; simp split: if_split\<close>\<close>)
apply (drule ko_at_projectKO_opt)
apply (erule (2) cmap_relation_upd_relI)
apply (simp add: ctcb_relation_def carch_tcb_relation_def)
Expand Down Expand Up @@ -648,25 +646,51 @@ lemma tcb_queue_rel'_unique:
apply (erule(2) tcb_queue_rel_unique)
done

definition
cready_queues_to_H
:: "(tcb_C ptr \<rightharpoonup> tcb_C) \<Rightarrow> (tcb_queue_C[num_tcb_queues]) \<Rightarrow> word8 \<times> word8 \<Rightarrow> machine_word list"

definition tcb_queue_C_to_tcb_queue :: "tcb_queue_C \<Rightarrow> tcb_queue" where
"tcb_queue_C_to_tcb_queue q \<equiv>
TcbQueue (if head_C q = NULL then None else Some (ctcb_ptr_to_tcb_ptr (head_C q)))
(if end_C q = NULL then None else Some (ctcb_ptr_to_tcb_ptr (end_C q)))"

definition cready_queues_to_H ::
"tcb_queue_C[num_tcb_queues] \<Rightarrow> (domain \<times> priority \<Rightarrow> ready_queue)"
where
"cready_queues_to_H h_tcb cs \<equiv> \<lambda>(qdom, prio). if ucast minDom \<le> qdom \<and> qdom \<le> ucast maxDom
\<and> ucast seL4_MinPrio \<le> prio \<and> prio \<le> ucast seL4_MaxPrio
then THE aq. let cqueue = index cs (cready_queues_index_to_C qdom prio)
in sched_queue_relation' h_tcb aq (head_C cqueue) (StateRelation_C.end_C cqueue)
else []"
"cready_queues_to_H cs \<equiv>
\<lambda>(qdom, prio).
if qdom \<le> maxDomain \<and> prio \<le> maxPriority
then let cqueue = index cs (cready_queues_index_to_C qdom prio)
in tcb_queue_C_to_tcb_queue cqueue
else TcbQueue None None"

lemma cready_queues_to_H_correct:
"cready_queues_relation (clift s) cs as \<Longrightarrow>
cready_queues_to_H (clift s) cs = as"
apply (clarsimp simp: cready_queues_to_H_def cready_queues_relation_def
fun_eq_iff)
apply (rule the_equality)
apply simp
apply (clarsimp simp: Let_def)
apply (rule_tac hp="clift s" in tcb_queue_rel'_unique, simp_all add: lift_t_NULL)
"\<lbrakk>cready_queues_relation (ksReadyQueues s) (ksReadyQueues_' ch);
no_0_obj' s; ksReadyQueues_asrt s; pspace_aligned' s; pspace_distinct' s\<rbrakk>
\<Longrightarrow> cready_queues_to_H (ksReadyQueues_' ch) = ksReadyQueues s"
apply (clarsimp simp: cready_queues_to_H_def cready_queues_relation_def Let_def)
apply (clarsimp simp: fun_eq_iff)
apply (rename_tac d p)
apply (drule_tac x=d in spec)
apply (drule_tac x=p in spec)
apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def)
apply (drule_tac x=d in spec)
apply (drule_tac x=p in spec)
apply clarsimp
apply (frule (3) obj_at'_tcbQueueHead_ksReadyQueues)
apply (frule (3) obj_at'_tcbQueueEnd_ksReadyQueues)
apply (frule tcbQueueHead_iff_tcbQueueEnd)
apply (rule conjI)
apply (clarsimp simp: tcb_queue_C_to_tcb_queue_def ctcb_queue_relation_def option_to_ctcb_ptr_def)
apply (case_tac "tcbQueueHead (ksReadyQueues s (d, p)) = None")
apply (clarsimp simp: tcb_queue.expand)
apply clarsimp
apply (rename_tac queue_head queue_end)
apply (prop_tac "tcb_at' queue_head s", fastforce simp: tcbQueueEmpty_def obj_at'_def)
apply (prop_tac "tcb_at' queue_end s", fastforce simp: tcbQueueEmpty_def obj_at'_def)
apply (drule tcb_at_not_NULL)+
apply (fastforce simp: tcb_queue.expand kernel.ctcb_ptr_to_ctcb_ptr)
apply (clarsimp simp: tcbQueueEmpty_def ctcb_queue_relation_def option_to_ctcb_ptr_def
split: option.splits;
metis tcb_queue.exhaust_sel word_not_le)
done

(* showing that cpspace_relation is actually unique >>>*)
Expand Down Expand Up @@ -820,17 +844,20 @@ lemma cthread_state_rel_imp_eq:
apply (cases y, simp_all add: ThreadState_defs)+
done

lemma ksPSpace_valid_objs_tcbBoundNotification_nonzero:
"\<exists>s. ksPSpace s = ah \<and> no_0_obj' s \<and> valid_objs' s
\<Longrightarrow> map_to_tcbs ah p = Some tcb \<Longrightarrow> tcbBoundNotification tcb \<noteq> Some 0"
lemma map_to_tcbs_Some_refs_nonzero:
"\<lbrakk>map_to_tcbs (ksPSpace s) p = Some tcb; no_0_obj' s; valid_objs' s\<rbrakk>
\<Longrightarrow> tcbBoundNotification tcb \<noteq> Some 0
\<and> tcbSchedPrev tcb \<noteq> Some 0
\<and> tcbSchedNext tcb \<noteq> Some 0"
supply word_neq_0_conv[simp del]
apply (clarsimp simp: map_comp_def split: option.splits)
apply (erule(1) valid_objsE')
apply (clarsimp simp: valid_obj'_def valid_tcb'_def)
apply (erule (1) valid_objsE')
apply (fastforce simp: valid_obj'_def valid_tcb'_def)
done

lemma ksPSpace_valid_objs_atcbVCPUPtr_nonzero:
"\<exists>s. ksPSpace s = ah \<and> no_0_obj' s \<and> valid_objs' s
\<Longrightarrow> map_to_tcbs ah p = Some tcb \<Longrightarrow> atcbVCPUPtr (tcbArch tcb) \<noteq> Some 0"
"\<lbrakk> no_0_obj' s; valid_objs' s \<rbrakk> \<Longrightarrow>
map_to_tcbs (ksPSpace s) p = Some tcb \<Longrightarrow> atcbVCPUPtr (tcbArch tcb) \<noteq> Some 0"
apply (clarsimp simp: map_comp_def split: option.splits)
apply (erule(1) valid_objsE')
apply (clarsimp simp: valid_obj'_def valid_tcb'_def valid_arch_tcb'_def)
Expand All @@ -855,36 +882,77 @@ lemma carch_tcb_relation_imp_eq:
apply (case_tac vcpuptr2 ; simp)
done

lemma tcb_ptr_to_ctcb_ptr_inj:
"tcb_ptr_to_ctcb_ptr x = tcb_ptr_to_ctcb_ptr y \<Longrightarrow> x = y"
by (auto simp: tcb_ptr_to_ctcb_ptr_def ctcb_offset_def)

lemma
assumes "pspace_aligned' as" "pspace_distinct' as" "valid_tcb' atcb as"
shows tcb_at'_tcbBoundNotification:
"bound (tcbBoundNotification atcb) \<longrightarrow> ntfn_at' (the (tcbBoundNotification atcb)) as"
and tcb_at'_tcbSchedPrev:
"tcbSchedPrev atcb \<noteq> None \<longrightarrow> tcb_at' (the (tcbSchedPrev atcb)) as"
and tcb_at'_tcbSchedNext:
"tcbSchedNext atcb \<noteq> None \<longrightarrow> tcb_at' (the (tcbSchedNext atcb)) as"
using assms
by (clarsimp simp: valid_tcb'_def obj_at'_def)+

lemma cpspace_tcb_relation_unique:
assumes tcbs: "cpspace_tcb_relation ah ch" "cpspace_tcb_relation ah' ch"
and vs: "\<exists>s. ksPSpace s = ah \<and> no_0_obj' s \<and> valid_objs' s"
and vs': "\<exists>s. ksPSpace s = ah' \<and> no_0_obj' s \<and> valid_objs' s"
assumes ctes: " \<forall>tcb tcb'. (\<exists>p. map_to_tcbs ah p = Some tcb \<and>
map_to_tcbs ah' p = Some tcb') \<longrightarrow>
(\<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb)"
shows "map_to_tcbs ah' = map_to_tcbs ah"
assumes tcbs: "cpspace_tcb_relation (ksPSpace as) ch" "cpspace_tcb_relation (ksPSpace as') ch"
assumes vs: "no_0_obj' as" "valid_objs' as"
assumes vs': "no_0_obj' as'" "valid_objs' as'"
assumes ad: "pspace_aligned' as" "pspace_distinct' as"
assumes ad': "pspace_aligned' as'" "pspace_distinct' as'"
assumes ctes: "\<forall>tcb tcb'. (\<exists>p. map_to_tcbs (ksPSpace as) p = Some tcb \<and>
map_to_tcbs (ksPSpace as') p = Some tcb') \<longrightarrow>
(\<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb)"
shows "map_to_tcbs (ksPSpace as') = map_to_tcbs (ksPSpace as)"
using tcbs(2) tcbs(1)
apply (clarsimp simp add: cmap_relation_def)
apply (drule inj_image_inv[OF inj_tcb_ptr_to_ctcb_ptr])+
apply (simp add: tcb_ptr_to_ctcb_ptr_def[abs_def] ctcb_offset_def)
apply (rule ext)
apply (case_tac "x:dom (map_to_tcbs ah)")
apply (case_tac "x \<in> dom (map_to_tcbs (ksPSpace as))")
apply (drule bspec, assumption)+
apply (simp add: dom_def Collect_eq, drule_tac x=x in spec)
apply clarsimp
apply (rename_tac p x y)
apply (cut_tac ctes)
apply (drule_tac x=x in spec, drule_tac x=y in spec, erule impE, fastforce)
apply (frule ksPSpace_valid_objs_tcbBoundNotification_nonzero[OF vs])
apply (frule ksPSpace_valid_objs_tcbBoundNotification_nonzero[OF vs'])
apply (frule map_to_tcbs_Some_refs_nonzero[OF _ vs])
apply (frule map_to_tcbs_Some_refs_nonzero[OF _ vs'])
apply (frule ksPSpace_valid_objs_atcbVCPUPtr_nonzero[OF vs])
apply (frule ksPSpace_valid_objs_atcbVCPUPtr_nonzero[OF vs'])
apply (rename_tac atcb atcb')
apply (prop_tac "valid_tcb' atcb as")
apply (fastforce intro: vs ad map_to_ko_atI tcb_ko_at_valid_objs_valid_tcb')
apply (prop_tac "valid_tcb' atcb' as'")
apply (fastforce intro: vs' ad' map_to_ko_atI tcb_ko_at_valid_objs_valid_tcb')
apply (frule tcb_at'_tcbSchedPrev[OF ad])
apply (frule tcb_at'_tcbSchedPrev[OF ad'])
apply (frule tcb_at'_tcbSchedNext[OF ad])
apply (frule tcb_at'_tcbSchedNext[OF ad'])
apply (thin_tac "map_to_tcbs x y = Some z" for x y z)+
apply (case_tac x, case_tac y, case_tac "the (clift ch (tcb_Ptr (p+0x400)))")
apply (case_tac "the (clift ch (tcb_Ptr (p + 2 ^ ctcb_size_bits)))")
apply (clarsimp simp: ctcb_relation_def ran_tcb_cte_cases)
apply (clarsimp simp: option_to_ptr_def option_to_0_def split: option.splits)
apply (auto simp: cfault_rel_imp_eq cthread_state_rel_imp_eq carch_tcb_relation_imp_eq
ccontext_relation_imp_eq up_ucast_inj_eq ctcb_size_bits_def)
apply (clarsimp simp: option_to_ctcb_ptr_def option_to_ptr_def option_to_0_def)
apply (rule tcb.expand)
apply clarsimp
apply (intro conjI)
apply (simp add: cthread_state_rel_imp_eq)
apply (simp add: cfault_rel_imp_eq)
apply (case_tac "tcbBoundNotification atcb'", case_tac "tcbBoundNotification atcb"; clarsimp)
apply (clarsimp split: option.splits)
apply (case_tac "tcbSchedPrev atcb'"; case_tac "tcbSchedPrev atcb"; clarsimp)
apply (force dest!: tcb_at_not_NULL)
apply (force dest!: tcb_at_not_NULL)
apply (force simp: tcb_ptr_to_ctcb_ptr_inj)
apply (case_tac "tcbSchedNext atcb'"; case_tac "tcbSchedNext atcb"; clarsimp)
apply (force dest!: tcb_at_not_NULL)
apply (force dest!: tcb_at_not_NULL)
apply (force simp: tcb_ptr_to_ctcb_ptr_inj)
apply (clarsimp simp: carch_tcb_relation_imp_eq)
apply auto
done

lemma tcb_queue_rel_clift_unique:
Expand Down Expand Up @@ -916,10 +984,6 @@ lemma is_aligned_no_overflow_0:
abbreviation
"is_aligned_opt x n \<equiv> case x of None \<Rightarrow> True | Some y \<Rightarrow> is_aligned y n"

lemma tcb_ptr_to_ctcb_ptr_inj:
"tcb_ptr_to_ctcb_ptr x = tcb_ptr_to_ctcb_ptr y \<Longrightarrow> x = y"
by (auto simp: tcb_ptr_to_ctcb_ptr_def ctcb_offset_def)

lemma option_to_ctcb_ptr_inj:
"\<lbrakk> is_aligned_opt a tcbBlockSizeBits; is_aligned_opt b tcbBlockSizeBits \<rbrakk>
\<Longrightarrow> (option_to_ctcb_ptr a = option_to_ctcb_ptr b) = (a = b)"
Expand Down Expand Up @@ -1218,8 +1282,8 @@ proof -
apply (rule valid_objs'_aligned_vcpuTCB [OF valid_objs])
apply (rule valid_objs'_aligned_vcpuTCB [OF valid_objs'])
apply (drule (1) cpspace_tcb_relation_unique)
apply (fastforce intro: no_0_objs no_0_objs' valid_objs valid_objs')
apply (fastforce intro: no_0_objs no_0_objs' valid_objs valid_objs')
apply (fastforce intro: no_0_objs no_0_objs' valid_objs valid_objs')+
apply (fastforce intro: aligned distinct aligned' distinct')+
apply (intro allI impI,elim exE conjE)
apply (rule_tac p=p in map_to_ctes_tcb_ctes, assumption)
apply (frule (1) map_to_ko_atI[OF _ aligned distinct])
Expand Down Expand Up @@ -1427,7 +1491,7 @@ where
ksDomSchedule = cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule,
ksCurDomain = ucast (ksCurDomain_' s),
ksDomainTime = ksDomainTime_' s,
ksReadyQueues = cready_queues_to_H (clift (t_hrs_' s)) (ksReadyQueues_' s),
ksReadyQueues = cready_queues_to_H (ksReadyQueues_' s),
ksReadyQueuesL1Bitmap = cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' s),
ksReadyQueuesL2Bitmap = cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' s),
ksCurThread = ctcb_ptr_to_tcb_ptr (ksCurThread_' s),
Expand All @@ -1449,27 +1513,27 @@ lemma trivial_eq_conj: "B = C \<Longrightarrow> (A \<and> B) = (A \<and> C)"
lemma cstate_to_H_correct:
assumes valid: "valid_state' as"
assumes cstate_rel: "cstate_relation as cs"
assumes rdyqs: "ksReadyQueues_asrt as"
shows "cstate_to_H cs = as \<lparr>ksMachineState:= observable_memory (ksMachineState as) (user_mem' as)\<rparr>"
apply (subgoal_tac "cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)")
apply (rule kernel_state.equality, simp_all add: cstate_to_H_def)
apply (rule cstate_to_pspace_H_correct)
apply (rule cstate_to_pspace_H_correct)
using valid
apply (simp add: valid_state'_def)
using cstate_rel valid
apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def
observable_memory_def valid_state'_def
valid_pspace'_def)
observable_memory_def valid_state'_def valid_pspace'_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def prod_eq_iff)
using cstate_rel
apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def prod_eq_iff)
using valid cstate_rel
apply (rule mk_gsUntypedZeroRanges_correct)
subgoal
using cstate_rel
by (fastforce simp: cstate_relation_def cpspace_relation_def
Let_def ghost_size_rel_def unat_eq_0
split: if_split)
using cstate_rel
by (fastforce simp: cstate_relation_def cpspace_relation_def
Let_def ghost_size_rel_def unat_eq_0
split: if_split)
using valid cstate_rel
apply (rule cDomScheduleIdx_to_H_correct)
using cstate_rel
Expand All @@ -1483,8 +1547,13 @@ lemma cstate_to_H_correct:
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
apply (rule cready_queues_to_H_correct)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel rdyqs
apply (fastforce intro!: cready_queues_to_H_correct
simp: cstate_relation_def Let_def)
using valid apply (fastforce simp: valid_state'_def)
using rdyqs apply fastforce
using valid apply (fastforce simp: valid_state'_def)
using valid apply (fastforce simp: valid_state'_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
Expand Down
9 changes: 0 additions & 9 deletions proof/crefine/AARCH64/ArchMove_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -292,9 +292,6 @@ lemma asUser_getRegister_discarded:
return_def fail_def stateAssert_def)
done

crunches Arch.switchToThread
for valid_queues'[wp]: valid_queues'
(simp: crunch_simps wp: hoare_drop_imps crunch_wps getASID_wp)
crunches switchToIdleThread
for ksCurDomain[wp]: "\<lambda>s. P (ksCurDomain s)"

Expand All @@ -312,10 +309,6 @@ lemma updateASIDPoolEntry_valid_pspace'[wp]:
unfolding updateASIDPoolEntry_def valid_pspace'_def getPoolPtr_def
by (wpsimp wp: getASID_wp)

crunches switchToIdleThread, switchToThread
for valid_pspace'[wp]: valid_pspace'
(simp: whenE_def crunch_simps wp: crunch_wps hoare_drop_imps)

lemma getMessageInfo_less_4:
"\<lbrace>\<top>\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. msgExtraCaps rv < 4\<rbrace>"
including no_pre
Expand Down Expand Up @@ -454,8 +447,6 @@ lemma ko_at_vcpu_at'D:
crunch pred_tcb_at'2[wp]: doMachineOp "\<lambda>s. P (pred_tcb_at' a b p s)"
(simp: crunch_simps)

crunch valid_queues'[wp]: readVCPUReg "\<lambda>s. valid_queues s"

crunch valid_objs'[wp]: readVCPUReg "\<lambda>s. valid_objs' s"

crunch sch_act_wf'[wp]: readVCPUReg "\<lambda>s. P (sch_act_wf (ksSchedulerAction s) s)"
Expand Down
Loading

0 comments on commit d869bb5

Please sign in to comment.