adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

arm refine: define valid_idle' directly, without using itcb 

- introduces idle_tcb' defined using tcb fields
- backport from MCS

Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
This commit is contained in:
Miki Tanaka 2021-04-09 16:55:36 +10:00 committed by Miki Tanaka
parent de7c2f7605
commit d054484474
11 changed files with 90 additions and 55 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
proof/refine/ARM/CSpace_R.thy
View File

@ -2786,7 +2786,10 @@ lemma setCTE_idle [wp]:
"\<lbrace>valid_idle'\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
apply (simp add: valid_idle'_def)
apply (rule hoare_lift_Pf [where f="ksIdleThread"])
apply (wp setCTE_pred_tcb_at')+
apply (intro hoare_vcg_conj_lift; (solves \<open>wpsimp\<close>)?)
apply (clarsimp simp: setCTE_def)
apply (rule setObject_cte_obj_at_tcb'[where P="idle_tcb'", simplified])
apply wpsimp
done
crunch it[wp]: getCTE "\<lambda>s. P (ksIdleThread s)"
@ -2796,7 +2799,7 @@ lemma updateMDB_idle'[wp]:
apply (clarsimp simp add: updateMDB_def)
apply (rule hoare_pre)
apply (wp | simp add: valid_idle'_def)+
done
by fastforce
lemma updateCap_idle':
"\<lbrace>valid_idle'\<rbrace> updateCap p c \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"

27
proof/refine/ARM/Invariants_H.thy
View File

@ -965,12 +965,27 @@ where
abbreviation
"sch_act_not t \<equiv> \<lambda>s. ksSchedulerAction s \<noteq> SwitchToThread t"
abbreviation "idle_tcb_at' \<equiv> pred_tcb_at' (\<lambda>t. (itcbState t, itcbBoundNotification t))"
definition
idle_tcb'_2 :: "Structures_H.thread_state \<times> machine_word option
\<Rightarrow> bool"
where
"idle_tcb'_2 \<equiv> \<lambda>(st, ntfn_opt). (idle' st \<and> ntfn_opt = None)"
abbreviation
"idle_tcb' tcb \<equiv> idle_tcb'_2 (tcbState tcb, tcbBoundNotification tcb)"
lemmas idle_tcb'_def = idle_tcb'_2_def
definition
valid_idle' :: "kernel_state \<Rightarrow> bool"
where
"valid_idle' \<equiv> \<lambda>s. idle_tcb_at' (\<lambda>p. idle' (fst p) \<and> snd p = None) (ksIdleThread s) s"
"valid_idle' \<equiv>
\<lambda>s. obj_at' idle_tcb' (ksIdleThread s) s
\<and> idle_thread_ptr = ksIdleThread s"
lemma valid_idle'_tcb_at':
"valid_idle' s \<Longrightarrow> obj_at' idle_tcb' (ksIdleThread s) s"
by (clarsimp simp: valid_idle'_def)
definition
valid_irq_node' :: "word32 \<Rightarrow> kernel_state \<Rightarrow> bool"
@ -1692,7 +1707,7 @@ lemma valid_pspaceE' [elim]:
lemma idle'_no_refs:
"valid_idle' s \<Longrightarrow> state_refs_of' s (ksIdleThread s) = {}"
by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def tcb_ntfn_is_bound'_def
projectKO_eq project_inject state_refs_of'_def)
projectKO_eq project_inject state_refs_of'_def idle_tcb'_def)
lemma idle'_not_queued':
"\<lbrakk>valid_idle' s; sym_refs (state_refs_of' s);
@ -1817,7 +1832,7 @@ lemma valid_idle'_pspace_itI[elim]:
"\<lbrakk> valid_idle' s; ksPSpace s = ksPSpace s'; ksIdleThread s = ksIdleThread s' \<rbrakk>
\<Longrightarrow> valid_idle' s'"
apply (clarsimp simp: valid_idle'_def ex_nonz_cap_to'_def)
apply (erule pred_tcb_at'_pspaceI, assumption)
apply (erule obj_at'_pspaceI, assumption)
done
lemma obj_at'_weaken:
@ -3129,10 +3144,6 @@ lemma not_pred_tcb_at'_strengthen:
"pred_tcb_at' f (Not \<circ> P) p s \<Longrightarrow> \<not> pred_tcb_at' f P p s"
by (clarsimp simp: pred_tcb_at'_def obj_at'_def)
lemma idle_tcb_at'_split:
"idle_tcb_at' (\<lambda>p. P (fst p) \<and> Q (snd p)) t s \<Longrightarrow> st_tcb_at' P t s \<and> bound_tcb_at' Q t s"
by (clarsimp simp: pred_tcb_at'_def dest!: obj_at'_conj_distrib)
lemma valid_queues_no_bitmap_def':
"valid_queues_no_bitmap =
(\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)).

4
proof/refine/ARM/IpcCancel_R.thy
View File

@ -859,7 +859,7 @@ proof -
apply (rule hoare_strengthen_post [OF get_ep_sp'])
apply (clarsimp simp: pred_tcb_at' fun_upd_def[symmetric] conj_comms
split del: if_split cong: if_cong)
apply (rule conjI, clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs)
apply (rule conjI, clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def)
apply (frule obj_at_valid_objs', clarsimp)
apply (clarsimp simp: projectKOs valid_obj'_def)
apply (rule conjI)
@ -2546,7 +2546,7 @@ lemma cancelBadgedSends_filterM_helper':
apply (intro conjI)
apply (clarsimp simp: valid_pspace'_def valid_tcb'_def elim!: valid_objs_valid_tcbE dest!: st_tcb_ex_cap'')
apply (fastforce dest!: st_tcb_ex_cap'')
apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def)
apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def)
apply (erule delta_sym_refs)
apply (fastforce elim!: obj_atE'
simp: state_refs_of'_def projectKOs tcb_bound_refs'_def

4
proof/refine/ARM/Ipc_R.thy
View File

@ -2977,7 +2977,7 @@ lemma sai_invs'[wp]:
apply (clarsimp simp: valid_obj'_def valid_ntfn'_def
split: list.splits)
apply (clarsimp simp: invs'_def valid_state'_def)
apply (clarsimp simp: st_tcb_at_refs_of_rev' valid_idle'_def pred_tcb_at'_def
apply (clarsimp simp: st_tcb_at_refs_of_rev' valid_idle'_def pred_tcb_at'_def idle_tcb'_def
dest!: sym_refs_ko_atD' sym_refs_st_tcb_atD' sym_refs_obj_atD'
split: list.splits)
apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def)
@ -3575,7 +3575,7 @@ crunch cap_to'[wp]: doIPCTransfer "ex_nonz_cap_to' p"
lemma st_tcb_idle':
"\<lbrakk>valid_idle' s; st_tcb_at' P t s\<rbrakk> \<Longrightarrow>
(t = ksIdleThread s) \<longrightarrow> P IdleThreadState"
by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def)
by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def)
crunch idle'[wp]: getThreadCallerSlot "valid_idle'"
crunch idle'[wp]: getThreadReplySlot "valid_idle'"

27
proof/refine/ARM/KHeap_R.thy
View File

@ -1160,6 +1160,13 @@ lemma setObject_it[wp]:
apply (wp x | simp)+
done
\<comment>\<open>
`idle_tcb_ps val` asserts that `val` is a pspace_storable value
which corresponds to an idle TCB.
\<close>
definition idle_tcb_ps :: "('a :: pspace_storable) \<Rightarrow> bool" where
"idle_tcb_ps val \<equiv> (\<exists>tcb. projectKO_opt (injectKO val) = Some tcb \<and> idle_tcb' tcb)"
lemma setObject_idle':
fixes v :: "'a :: pspace_storable"
assumes R: "\<And>ko s x y n. (updateObject v ko ptr y n s)
@ -1170,12 +1177,9 @@ lemma setObject_idle':
\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> updateObject v p q n ko
\<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>"
shows "\<lbrace>\<lambda>s. valid_idle' s \<and>
(ptr = ksIdleThread s \<longrightarrow>
(\<exists>obj (val :: 'a). projectKO_opt (injectKO val) = Some obj
\<and> idle' (tcbState obj) \<and> tcbBoundNotification obj = None)
\<longrightarrow> (\<exists>obj. projectKO_opt (injectKO v) = Some obj \<and>
idle' (tcbState obj) \<and> tcbBoundNotification obj = None)) \<and>
P s\<rbrace>
(ptr = ksIdleThread s
\<longrightarrow> (\<exists>val :: 'a. idle_tcb_ps val)
\<longrightarrow> idle_tcb_ps v)\<rbrace>
setObject ptr v
\<lbrace>\<lambda>rv s. valid_idle' s\<rbrace>"
apply (simp add: valid_idle'_def pred_tcb_at'_def o_def)
@ -1184,8 +1188,7 @@ lemma setObject_idle':
apply (simp add: pred_tcb_at'_def obj_at'_real_def)
apply (rule setObject_ko_wp_at [OF R n m])
apply (wp z)
apply (clarsimp simp add: pred_tcb_at'_def obj_at'_real_def ko_wp_at'_def)
apply (drule_tac x=obj in spec, simp)
apply (clarsimp simp add: pred_tcb_at'_def obj_at'_real_def ko_wp_at'_def idle_tcb_ps_def)
apply (clarsimp simp add: project_inject)
apply (drule_tac x=obja in spec, simp)
done
@ -1717,9 +1720,9 @@ lemma setEndpoint_idle'[wp]:
setEndpoint p v
\<lbrace>\<lambda>_. valid_idle'\<rbrace>"
unfolding setEndpoint_def
apply (wp setObject_idle'[where P="\<top>"])
apply (wp setObject_idle')
apply (simp add: objBits_simps' updateObject_default_inv)+
apply (clarsimp simp: projectKOs)
apply (clarsimp simp: projectKOs idle_tcb_ps_def)
done
crunch it[wp]: setEndpoint "\<lambda>s. P (ksIdleThread s)"
@ -1855,9 +1858,9 @@ lemma setNotification_ifunsafe'[wp]:
lemma setNotification_idle'[wp]:
"\<lbrace>\<lambda>s. valid_idle' s\<rbrace> setNotification p v \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
unfolding setNotification_def
apply (wp setObject_idle'[where P="\<top>"])
apply (wp setObject_idle')
apply (simp add: objBits_simps' updateObject_default_inv)+
apply (clarsimp simp: projectKOs)
apply (clarsimp simp: projectKOs idle_tcb_ps_def)
done
crunch it[wp]: setNotification "\<lambda>s. P (ksIdleThread s)"

1
proof/refine/ARM/Retype_R.thy
View File

@ -4090,6 +4090,7 @@ lemma createObjects_idle':
apply (rule hoare_gen_asm)
apply (rule hoare_pre)
apply (clarsimp simp add: valid_idle'_def pred_tcb_at'_def)
apply (rule hoare_vcg_conj_lift)
apply (rule hoare_as_subst [OF createObjects'_it])
apply (wp createObjects_orig_obj_at'
createObjects_orig_cte_wp_at2'

14
proof/refine/ARM/Schedule_R.thy
View File

@ -764,7 +764,7 @@ lemma arch_switchToIdleThread_corres:
apply (simp add: arch_switch_to_idle_thread_def
ARM_H.switchToIdleThread_def)
apply (corressimp corres: getIdleThread_corres setVMRoot_corres[@lift_corres_args])
apply (clarsimp simp: valid_idle_def valid_idle'_def pred_tcb_at_def obj_at_def is_tcb)
apply (clarsimp simp: valid_idle_def valid_idle'_def pred_tcb_at_def obj_at_def is_tcb obj_at'_def)
done
lemma switchToIdleThread_corres:
@ -893,7 +893,7 @@ lemma idle'_not_tcbQueued':
shows "obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s"
proof -
from idle have stidle: "st_tcb_at' (Not \<circ> runnable') (ksIdleThread s) s"
by (clarsimp simp add: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs)
by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs idle_tcb'_def)
with vq vq' show ?thesis
by (rule valid_queues_not_runnable_not_queued)
@ -911,15 +911,17 @@ proof -
show ?thesis
apply (simp add: setCurThread_def)
apply wp
apply (clarsimp simp add: ct_not_inQ_ct idle'_activatable' idle'_not_tcbQueued'[simplified o_def]
apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def)
apply (frule (2) idle'_not_tcbQueued'[simplified o_def])
apply (clarsimp simp add: ct_not_inQ_ct idle'_activatable'
invs'_def cur_tcb'_def valid_state'_def valid_idle'_def
sch_act_wf ct_in_state'_def state_refs_of'_def
ps_clear_def valid_irq_node'_def
ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def
valid_queues_def bitmapQ_defs valid_queues_no_bitmap_def valid_queues'_def
all_invs_but_ct_idle_or_in_cur_domain'_def pred_tcb_at'_def
pred_tcb_at'_def
cong: option.case_cong)
apply (clarsimp simp: obj_at'_def projectKOs)
apply (clarsimp simp: obj_at'_def projectKOs idle_tcb'_def)
done
qed
@ -1988,7 +1990,7 @@ lemma switchToIdleThread_activatable_2[wp]:
ARM_H.switchToIdleThread_def)
apply (wp setCurThread_ct_in_state)
apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_idle'_def
pred_tcb_at'_def obj_at'_def)
pred_tcb_at'_def obj_at'_def idle_tcb'_def)
done
lemma switchToThread_tcb_in_cur_domain':

17
proof/refine/ARM/Syscall_R.thy
View File

@ -821,18 +821,17 @@ lemma doReply_invs[wp]:
in hoare_strengthen_post [rotated])
apply (clarsimp)
apply (rule conjI)
apply (clarsimp simp add: invs'_def valid_state'_def valid_idle'_def)
apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def)
apply (rule conjI)
apply clarsimp
apply clarsimp
apply (drule idle_tcb_at'_split, clarsimp, drule (1) st_tcb_at'_eqD, simp)
apply (clarsimp simp: obj_at'_def idle_tcb'_def pred_tcb_at'_def)
apply clarsimp
apply (rule conjI)
apply (clarsimp simp add: invs'_def valid_state'_def valid_idle'_def)
apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def)
apply (erule pred_tcb'_weakenE, clarsimp)
apply (rule conjI)
apply (clarsimp simp add: invs'_def valid_state'_def valid_idle'_def pred_tcb_at'_def
obj_at'_def)
apply (clarsimp simp : invs'_def valid_state'_def valid_idle'_def pred_tcb_at'_def
obj_at'_def idle_tcb'_def)
apply (rule conjI)
apply clarsimp
apply (frule invs'_not_runnable_not_queued)
@ -1142,7 +1141,7 @@ lemma get_mrs_length_rv[wp]:
lemma st_tcb_at_idle_thread':
"\<lbrakk> st_tcb_at' P (ksIdleThread s) s; valid_idle' s \<rbrakk>
\<Longrightarrow> P IdleThreadState"
by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def)
by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def)
crunch tcb_at'[wp]: replyFromKernel "tcb_at' t"
@ -1338,7 +1337,7 @@ lemma hinv_invs'[wp]:
apply (subgoal_tac "thread \<noteq> ksIdleThread s", simp_all)[1]
apply (fastforce elim!: pred_tcb'_weakenE st_tcb_ex_cap'')
apply (clarsimp simp: valid_idle'_def valid_state'_def
invs'_def pred_tcb_at'_def obj_at'_def)
invs'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def)
apply wp+
apply (rule_tac Q="\<lambda>rv'. invs' and valid_invocation' rv
and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
@ -2115,7 +2114,7 @@ proof
assume "ksCurThread s = ksIdleThread s"
with vi have "ct_in_state' idle' s"
unfolding ct_in_state'_def valid_idle'_def
by (clarsimp simp: pred_tcb_at'_def obj_at'_def)
by (clarsimp simp: pred_tcb_at'_def obj_at'_def idle_tcb'_def)
with cts show False
unfolding ct_in_state'_def

13
proof/refine/ARM/TcbAcc_R.thy
View File

@ -528,10 +528,10 @@ lemma setObject_tcb_idle':
(t = ksIdleThread s \<longrightarrow> idle' (tcbState v) \<and> tcbBoundNotification v = None)\<rbrace>
setObject t (v :: tcb) \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
apply (rule hoare_pre)
apply (rule_tac P="\<top>" in setObject_idle')
apply (rule setObject_idle')
apply (simp add: objBits_simps')+
apply (simp add: updateObject_default_inv)
apply (simp add: projectKOs)
apply (simp add: projectKOs idle_tcb_ps_def idle_tcb'_def)
done
lemma setObject_tcb_irq_node'[wp]:
@ -798,14 +798,13 @@ lemma threadSet_idle'T:
shows
"\<lbrace>\<lambda>s. valid_idle' s
\<and> (t = ksIdleThread s \<longrightarrow>
(\<forall>tcb. ko_at' tcb t s \<and> idle' (tcbState tcb) \<longrightarrow> idle' (tcbState (F tcb)))
\<and> (\<forall>tcb. ko_at' tcb t s \<and> tcbBoundNotification tcb = None \<longrightarrow> tcbBoundNotification (F tcb) = None))\<rbrace>
(\<forall>tcb. ko_at' tcb t s \<and> idle_tcb' tcb \<longrightarrow> idle_tcb' (F tcb)))\<rbrace>
threadSet F t
\<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
apply (simp add: threadSet_def)
apply (wp setObject_tcb_idle' getObject_tcb_wp)
apply (clarsimp simp: obj_at'_def projectKOs)
apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs)
apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs idle_tcb'_def)
done
lemmas threadSet_idle' =
@ -3646,7 +3645,7 @@ lemma sts_valid_idle'[wp]:
setThreadState ts t
\<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
apply (simp add: setThreadState_def)
apply (wp threadSet_idle', simp+)+
apply (wpsimp wp: threadSet_idle' simp: idle_tcb'_def)
done
lemma sbn_valid_idle'[wp]:
@ -3655,7 +3654,7 @@ lemma sbn_valid_idle'[wp]:
setBoundNotification ntfn t
\<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
apply (simp add: setBoundNotification_def)
apply (wp threadSet_idle', simp+)+
apply (wpsimp wp: threadSet_idle' simp: idle_tcb'_def)
done
lemma gts_sp':

2
proof/refine/ARM/Tcb_R.thy
View File

@ -120,7 +120,7 @@ lemma activate_invs':
in hoare_post_imp, clarsimp)
apply (wp sch_act_simple_lift)+
apply (clarsimp simp: valid_idle'_def invs'_def valid_state'_def
pred_tcb_at'_def obj_at'_def
pred_tcb_at'_def obj_at'_def idle_tcb'_def
elim!: pred_tcb'_weakenE)
apply (wp gts_st_tcb')+
apply (clarsimp simp: tcb_at_invs' ct_in_state'_def

29
proof/refine/ARM/VSpace_R.thy
View File

@ -2833,8 +2833,14 @@ lemma storePDE_ifunsafe [wp]:
lemma storePDE_idle [wp]:
"\<lbrace>valid_idle'\<rbrace> storePDE p pde \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
unfolding valid_idle'_def
by (rule hoare_lift_Pf [where f="ksIdleThread"]; wp)
apply (simp add: valid_idle'_def)
apply (rule hoare_lift_Pf [where f="ksIdleThread"])
apply (intro hoare_vcg_conj_lift; (solves \<open>wpsimp\<close>)?)
apply (clarsimp simp: storePDE_def)
apply (rule obj_at_setObject2[where P="idle_tcb'", simplified])
apply (clarsimp dest!: updateObject_default_result)
apply wpsimp
done
crunches storePDE
for arch'[wp]: "\<lambda>s. P (ksArchState s)"
@ -3020,8 +3026,14 @@ lemma storePTE_ifunsafe [wp]:
lemma storePTE_idle [wp]:
"\<lbrace>valid_idle'\<rbrace> storePTE p pte \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
unfolding valid_idle'_def
by (rule hoare_lift_Pf [where f="ksIdleThread"]; wp)
apply (simp add: valid_idle'_def)
apply (rule hoare_lift_Pf [where f="ksIdleThread"])
apply (intro hoare_vcg_conj_lift; (solves \<open>wpsimp\<close>)?)
apply (clarsimp simp: storePTE_def)
apply (rule obj_at_setObject2[where P="idle_tcb'", simplified])
apply (clarsimp dest!: updateObject_default_result)
apply wpsimp
done
crunches storePTE
for arch'[wp]: "\<lambda>s. P (ksArchState s)"
@ -3211,8 +3223,13 @@ lemma setASIDPool_it' [wp]:
lemma setASIDPool_idle [wp]:
"\<lbrace>valid_idle'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
unfolding valid_idle'_def
by (rule hoare_lift_Pf [where f="ksIdleThread"]; wp)
apply (simp add: valid_idle'_def)
apply (rule hoare_lift_Pf [where f="ksIdleThread"])
apply (intro hoare_vcg_conj_lift; (solves \<open>wpsimp\<close>)?)
apply (rule obj_at_setObject2[where P="idle_tcb'", simplified])
apply (clarsimp dest!: updateObject_default_result)
apply wpsimp
done
lemma setASIDPool_irq_states' [wp]:
"\<lbrace>valid_irq_states'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>"