dspec, drefine: fix for GrantReply (SELFOUR-6)
Nothing too exciting here, just duplicating the new GrantReply logic from ASpec and repairing the proofs.
This commit is contained in:
parent
4d4de9098b
commit
3758df05df
|
@ -332,20 +332,20 @@ lemma insert_cap_child_corres:
|
||||||
apply (clarsimp simp: caps_of_state_transform_opt_cap cte_wp_at_caps_of_state
|
apply (clarsimp simp: caps_of_state_transform_opt_cap cte_wp_at_caps_of_state
|
||||||
transform_cap_def)+
|
transform_cap_def)+
|
||||||
apply (clarsimp simp: valid_mdb_def cte_wp_at_cases dest!:invs_mdb)
|
apply (clarsimp simp: valid_mdb_def cte_wp_at_cases dest!:invs_mdb)
|
||||||
apply (case_tac "cdt s' child", safe intro!: mdb_cte_atI)
|
apply (case_tac "cdt s' child", safe intro!: mdb_cte_atI;
|
||||||
(* 121 subgoals *)
|
auto dest: mdb_cte_atD is_untyped_cap_eqD
|
||||||
by (auto dest: mdb_cte_atD is_untyped_cap_eqD
|
|
||||||
simp: valid_mdb_def swp_def cte_wp_at_caps_of_state not_idle_thread_def)
|
simp: valid_mdb_def swp_def cte_wp_at_caps_of_state not_idle_thread_def)
|
||||||
|
done
|
||||||
|
|
||||||
lemma reply_cap_insert_corres:
|
lemma reply_cap_insert_corres:
|
||||||
"sid \<noteq> did\<Longrightarrow>dcorres dc \<top>
|
"sid \<noteq> did\<Longrightarrow>dcorres dc \<top>
|
||||||
(valid_idle and not_idle_thread did and valid_mdb and st_tcb_at (\<lambda>r. \<not> inactive r \<and> \<not> idle r) sid
|
(valid_idle and not_idle_thread did and valid_mdb and st_tcb_at (\<lambda>r. \<not> inactive r \<and> \<not> idle r) sid
|
||||||
and valid_etcbs and tcb_at did and tcb_at sid and valid_objs)
|
and valid_etcbs and tcb_at did and tcb_at sid and valid_objs)
|
||||||
(insert_cap_child (cdl_cap.ReplyCap sid) (sid, tcb_replycap_slot)
|
(insert_cap_child (cdl_cap.ReplyCap sid rights) (sid, tcb_replycap_slot)
|
||||||
(did, tcb_caller_slot))
|
(did, tcb_caller_slot))
|
||||||
(cap_insert (cap.ReplyCap sid False) (sid,tcb_cnode_index 2) (did,tcb_cnode_index 3))"
|
(cap_insert (cap.ReplyCap sid False rights) (sid,tcb_cnode_index 2) (did,tcb_cnode_index 3))"
|
||||||
apply (rule corres_guard_imp)
|
apply (rule corres_guard_imp)
|
||||||
apply (rule insert_cap_child_corres [where cap = "cap.ReplyCap sid False"
|
apply (rule insert_cap_child_corres [where cap = "cap.ReplyCap sid False rights"
|
||||||
and src = "(sid, tcb_cnode_index 2)" and child = "(did, tcb_cnode_index 3)",
|
and src = "(sid, tcb_cnode_index 2)" and child = "(did, tcb_cnode_index 3)",
|
||||||
unfolded transform_cap_def transform_tcb_slot_simp
|
unfolded transform_cap_def transform_tcb_slot_simp
|
||||||
,simplified])
|
,simplified])
|
||||||
|
@ -493,10 +493,10 @@ crunch idle_thread[wp]: cap_move "\<lambda>s::'a::state_ext state. P (idle_threa
|
||||||
(wp: dxo_wp_weak)
|
(wp: dxo_wp_weak)
|
||||||
|
|
||||||
lemma cap_null_reply_case_If:
|
lemma cap_null_reply_case_If:
|
||||||
"(case cap of cap.ReplyCap t b \<Rightarrow> f t b | cap.NullCap \<Rightarrow> g | _ \<Rightarrow> h)
|
"(case cap of cap.ReplyCap t b R \<Rightarrow> f t b R | cap.NullCap \<Rightarrow> g | _ \<Rightarrow> h)
|
||||||
= (if cap = cap.NullCap then g
|
= (if cap = cap.NullCap then g
|
||||||
else if is_reply_cap cap \<or> is_master_reply_cap cap
|
else if is_reply_cap cap \<or> is_master_reply_cap cap
|
||||||
then f (obj_ref_of cap) (is_master_reply_cap cap)
|
then f (obj_ref_of cap) (is_master_reply_cap cap) (cap_rights cap)
|
||||||
else h)"
|
else h)"
|
||||||
by (simp add: is_reply_cap_def is_master_reply_cap_def split: cap.split)
|
by (simp add: is_reply_cap_def is_master_reply_cap_def split: cap.split)
|
||||||
|
|
||||||
|
@ -2323,7 +2323,7 @@ lemma lsfco_not_idle:
|
||||||
done
|
done
|
||||||
|
|
||||||
lemma cdl_right_UNIV:
|
lemma cdl_right_UNIV:
|
||||||
"UNIV = {Read, Write, Grant}"
|
"UNIV = {Read, Write, Grant, GrantReply}"
|
||||||
apply (rule set_eqI)
|
apply (rule set_eqI)
|
||||||
apply (case_tac x, auto)
|
apply (case_tac x, auto)
|
||||||
done
|
done
|
||||||
|
|
|
@ -36,17 +36,19 @@ lemma cte_wp_at_zombie_not_idle:
|
||||||
lemmas tcb_slots = Types_D.tcb_caller_slot_def Types_D.tcb_cspace_slot_def Types_D.tcb_ipcbuffer_slot_def
|
lemmas tcb_slots = Types_D.tcb_caller_slot_def Types_D.tcb_cspace_slot_def Types_D.tcb_ipcbuffer_slot_def
|
||||||
Types_D.tcb_pending_op_slot_def Types_D.tcb_replycap_slot_def Types_D.tcb_vspace_slot_def Types_D.tcb_boundntfn_slot_def
|
Types_D.tcb_pending_op_slot_def Types_D.tcb_replycap_slot_def Types_D.tcb_vspace_slot_def Types_D.tcb_boundntfn_slot_def
|
||||||
|
|
||||||
|
(* FIXME: MOVE *)
|
||||||
lemma tcb_cap_casesE:
|
lemma tcb_cap_casesE:
|
||||||
assumes cs: "tcb_cap_cases p = Some (gf, sf, restr)"
|
assumes cs: "tcb_cap_cases p = Some (gf, sf, restr)"
|
||||||
and rules: "\<lbrakk> p = tcb_cnode_index 0; gf = tcb_ctable; sf = tcb_ctable_update; restr = (\<lambda>_ _. \<top>) \<rbrakk> \<Longrightarrow> R"
|
and rules: "\<lbrakk> p = tcb_cnode_index 0; gf = tcb_ctable; sf = tcb_ctable_update; restr = (\<lambda>_ _. \<top>) \<rbrakk> \<Longrightarrow> R"
|
||||||
"\<lbrakk> p = tcb_cnode_index 1; gf = tcb_vtable; sf = tcb_vtable_update; restr = (\<lambda>_ _. \<top>) \<rbrakk> \<Longrightarrow> R"
|
"\<lbrakk> p = tcb_cnode_index 1; gf = tcb_vtable; sf = tcb_vtable_update;
|
||||||
"\<lbrakk> p = tcb_cnode_index 2; gf = tcb_reply; sf = tcb_reply_update; restr =
|
restr = (\<lambda>_ _. is_valid_vtable_root or ((=) cap.NullCap)) \<rbrakk> \<Longrightarrow> R"
|
||||||
(\<lambda>t st c.
|
"\<lbrakk> p = tcb_cnode_index 2; gf = tcb_reply; sf = tcb_reply_update;
|
||||||
(is_master_reply_cap c \<and> obj_ref_of c = t)
|
restr = (\<lambda>t st c. (is_master_reply_cap c \<and> obj_ref_of c = t
|
||||||
|
\<and> AllowGrant \<in> cap_rights c)
|
||||||
\<or> (halted st \<and> (c = cap.NullCap))) \<rbrakk> \<Longrightarrow> R"
|
\<or> (halted st \<and> (c = cap.NullCap))) \<rbrakk> \<Longrightarrow> R"
|
||||||
"\<lbrakk> p = tcb_cnode_index 3; gf = tcb_caller; sf = tcb_caller_update; restr =
|
"\<lbrakk> p = tcb_cnode_index 3; gf = tcb_caller; sf = tcb_caller_update;
|
||||||
(\<lambda>_ st. case st of
|
restr = (\<lambda>_ st. case st of
|
||||||
Structures_A.BlockedOnReceive e \<Rightarrow>
|
Structures_A.BlockedOnReceive e data \<Rightarrow>
|
||||||
((=) cap.NullCap)
|
((=) cap.NullCap)
|
||||||
| _ \<Rightarrow> is_reply_cap or ((=) cap.NullCap)) \<rbrakk> \<Longrightarrow> R"
|
| _ \<Rightarrow> is_reply_cap or ((=) cap.NullCap)) \<rbrakk> \<Longrightarrow> R"
|
||||||
"\<lbrakk> p = tcb_cnode_index 4; gf = tcb_ipcframe; sf = tcb_ipcframe_update; restr =
|
"\<lbrakk> p = tcb_cnode_index 4; gf = tcb_ipcframe; sf = tcb_ipcframe_update; restr =
|
||||||
|
@ -96,18 +98,20 @@ abbreviation
|
||||||
|
|
||||||
lemma tcb_cap_cases_slot_simps[simp]:
|
lemma tcb_cap_cases_slot_simps[simp]:
|
||||||
"tcb_cap_cases (tcb_cnode_index tcb_cspace_slot) = Some (tcb_ctable, tcb_ctable_update, (\<lambda>_ _. \<top>))"
|
"tcb_cap_cases (tcb_cnode_index tcb_cspace_slot) = Some (tcb_ctable, tcb_ctable_update, (\<lambda>_ _. \<top>))"
|
||||||
"tcb_cap_cases (tcb_cnode_index tcb_vspace_slot) = Some (tcb_vtable, tcb_vtable_update, (\<lambda>_ _. \<top>))"
|
"tcb_cap_cases (tcb_cnode_index tcb_vspace_slot) =
|
||||||
"tcb_cap_cases (tcb_cnode_index tcb_replycap_slot) = Some (tcb_reply, tcb_reply_update,
|
Some (tcb_vtable, tcb_vtable_update, (\<lambda>_ _. is_valid_vtable_root or ((=) cap.NullCap)))"
|
||||||
(\<lambda>t st c.
|
"tcb_cap_cases (tcb_cnode_index tcb_replycap_slot) =
|
||||||
(is_master_reply_cap c \<and> obj_ref_of c = t)
|
Some (tcb_reply, tcb_reply_update,
|
||||||
|
(\<lambda>t st c. (is_master_reply_cap c \<and> obj_ref_of c = t \<and> AllowGrant \<in> cap_rights c)
|
||||||
\<or> (halted st \<and> (c = cap.NullCap))))"
|
\<or> (halted st \<and> (c = cap.NullCap))))"
|
||||||
"tcb_cap_cases (tcb_cnode_index tcb_caller_slot) = Some (tcb_caller, tcb_caller_update,
|
"tcb_cap_cases (tcb_cnode_index tcb_caller_slot) =
|
||||||
|
Some (tcb_caller, tcb_caller_update,
|
||||||
(\<lambda>_ st. case st of
|
(\<lambda>_ st. case st of
|
||||||
Structures_A.BlockedOnReceive e \<Rightarrow>
|
Structures_A.BlockedOnReceive e data \<Rightarrow>
|
||||||
((=) cap.NullCap)
|
((=) cap.NullCap)
|
||||||
| _ \<Rightarrow> is_reply_cap or ((=) cap.NullCap)))"
|
| _ \<Rightarrow> is_reply_cap or ((=) cap.NullCap)))"
|
||||||
"tcb_cap_cases (tcb_cnode_index tcb_ipcbuffer_slot) = Some (tcb_ipcframe, tcb_ipcframe_update,
|
"tcb_cap_cases (tcb_cnode_index tcb_ipcbuffer_slot) =
|
||||||
(\<lambda>_ _. is_nondevice_page_cap or ((=) cap.NullCap)))"
|
Some (tcb_ipcframe, tcb_ipcframe_update, (\<lambda>_ _. is_nondevice_page_cap or ((=) cap.NullCap)))"
|
||||||
by (simp add: tcb_slots)+
|
by (simp add: tcb_slots)+
|
||||||
|
|
||||||
lemma opt_cap_tcb:
|
lemma opt_cap_tcb:
|
||||||
|
@ -189,7 +193,7 @@ definition
|
||||||
generates_pending :: "Structures_A.thread_state \<Rightarrow> bool"
|
generates_pending :: "Structures_A.thread_state \<Rightarrow> bool"
|
||||||
where
|
where
|
||||||
"generates_pending st \<equiv> case st of
|
"generates_pending st \<equiv> case st of
|
||||||
Structures_A.BlockedOnReceive ptr \<Rightarrow> True
|
Structures_A.BlockedOnReceive ptr payload \<Rightarrow> True
|
||||||
| Structures_A.BlockedOnSend ptr payload \<Rightarrow> True
|
| Structures_A.BlockedOnSend ptr payload \<Rightarrow> True
|
||||||
| Structures_A.BlockedOnReply \<Rightarrow> True
|
| Structures_A.BlockedOnReply \<Rightarrow> True
|
||||||
| Structures_A.BlockedOnNotification ptr \<Rightarrow> True
|
| Structures_A.BlockedOnNotification ptr \<Rightarrow> True
|
||||||
|
|
|
@ -400,12 +400,12 @@ lemma sts_gwp:
|
||||||
lemma block_thread_on_send_corres:
|
lemma block_thread_on_send_corres:
|
||||||
"dcorres dc \<top> (not_idle_thread thread and valid_etcbs)
|
"dcorres dc \<top> (not_idle_thread thread and valid_etcbs)
|
||||||
(KHeap_D.set_cap (thread, tcb_pending_op_slot)
|
(KHeap_D.set_cap (thread, tcb_pending_op_slot)
|
||||||
(PendingSyncSendCap epptr badge call can_grant
|
(PendingSyncSendCap epptr badge call can_grant can_grant_reply
|
||||||
False))
|
False))
|
||||||
(set_thread_state thread
|
(set_thread_state thread
|
||||||
(Structures_A.thread_state.BlockedOnSend epptr
|
(Structures_A.thread_state.BlockedOnSend epptr
|
||||||
\<lparr>sender_badge = badge, sender_can_grant = can_grant,
|
\<lparr>sender_badge = badge, sender_can_grant = can_grant,
|
||||||
sender_is_call = call\<rparr>))"
|
sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))"
|
||||||
apply (clarsimp simp:KHeap_D.set_cap_def set_thread_state_def)
|
apply (clarsimp simp:KHeap_D.set_cap_def set_thread_state_def)
|
||||||
apply (rule dcorres_gets_the, clarsimp)
|
apply (rule dcorres_gets_the, clarsimp)
|
||||||
apply (rule dcorres_rhs_noop_below_True[OF set_thread_state_ext_dcorres])
|
apply (rule dcorres_rhs_noop_below_True[OF set_thread_state_ext_dcorres])
|
||||||
|
@ -428,8 +428,9 @@ lemma block_thread_on_send_corres:
|
||||||
lemma block_thread_on_recv_corres:
|
lemma block_thread_on_recv_corres:
|
||||||
"dcorres dc \<top> (not_idle_thread thread and valid_etcbs)
|
"dcorres dc \<top> (not_idle_thread thread and valid_etcbs)
|
||||||
(KHeap_D.set_cap (thread, tcb_pending_op_slot)
|
(KHeap_D.set_cap (thread, tcb_pending_op_slot)
|
||||||
(PendingSyncRecvCap epptr False))
|
(PendingSyncRecvCap epptr False can_grant))
|
||||||
(set_thread_state thread (Structures_A.thread_state.BlockedOnReceive epptr))"
|
(set_thread_state thread
|
||||||
|
(Structures_A.thread_state.BlockedOnReceive epptr \<lparr>receiver_can_grant = can_grant\<rparr>))"
|
||||||
apply (clarsimp simp:KHeap_D.set_cap_def set_thread_state_def)
|
apply (clarsimp simp:KHeap_D.set_cap_def set_thread_state_def)
|
||||||
apply (rule dcorres_gets_the, clarsimp)
|
apply (rule dcorres_gets_the, clarsimp)
|
||||||
apply (rule dcorres_rhs_noop_below_True[OF set_thread_state_ext_dcorres])
|
apply (rule dcorres_rhs_noop_below_True[OF set_thread_state_ext_dcorres])
|
||||||
|
@ -973,29 +974,32 @@ lemma set_thread_state_block_on_send_corres:
|
||||||
"dcorres dc \<top>
|
"dcorres dc \<top>
|
||||||
(not_idle_thread thread and valid_etcbs)
|
(not_idle_thread thread and valid_etcbs)
|
||||||
(block_thread_on_ipc thread
|
(block_thread_on_ipc thread
|
||||||
(PendingSyncSendCap epptr badge call can_grant False))
|
(PendingSyncSendCap epptr badge call can_grant can_grant_reply False))
|
||||||
(set_thread_state thread
|
(set_thread_state thread
|
||||||
(Structures_A.thread_state.BlockedOnSend epptr
|
(Structures_A.thread_state.BlockedOnSend epptr
|
||||||
\<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_is_call = call\<rparr>))"
|
\<lparr>sender_badge = badge, sender_can_grant = can_grant,
|
||||||
|
sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))"
|
||||||
by (simp add:block_thread_on_ipc_def,rule block_thread_on_send_corres)
|
by (simp add:block_thread_on_ipc_def,rule block_thread_on_send_corres)
|
||||||
|
|
||||||
lemma set_thread_state_block_on_receive_corres:
|
lemma set_thread_state_block_on_receive_corres:
|
||||||
"dcorres dc \<top> (not_idle_thread thread and valid_etcbs)
|
"dcorres dc \<top> (not_idle_thread thread and valid_etcbs)
|
||||||
(block_thread_on_ipc thread (PendingSyncRecvCap epptr False))
|
(block_thread_on_ipc thread (PendingSyncRecvCap epptr False can_grant))
|
||||||
(set_thread_state thread (Structures_A.thread_state.BlockedOnReceive epptr))"
|
(set_thread_state thread
|
||||||
|
(Structures_A.thread_state.BlockedOnReceive epptr \<lparr>receiver_can_grant = can_grant\<rparr>))"
|
||||||
apply (simp add:block_thread_on_ipc_def)
|
apply (simp add:block_thread_on_ipc_def)
|
||||||
apply (rule block_thread_on_recv_corres)
|
apply (rule block_thread_on_recv_corres)
|
||||||
done
|
done
|
||||||
|
|
||||||
lemma corres_setup_caller_cap:
|
lemma corres_setup_caller_cap:
|
||||||
"sender \<noteq> receiver \<Longrightarrow> dcorres dc \<top>
|
"sender \<noteq> receiver \<Longrightarrow> dcorres dc \<top>
|
||||||
(valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver
|
(valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver
|
||||||
and st_tcb_at (Not\<circ> halted) sender and valid_objs and valid_etcbs)
|
and tcb_at sender and tcb_at receiver
|
||||||
(inject_reply_cap sender receiver)
|
and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs)
|
||||||
(setup_caller_cap sender receiver)"
|
(inject_reply_cap sender receiver can_grant)
|
||||||
|
(setup_caller_cap sender receiver can_grant)"
|
||||||
apply (rule dcorres_expand_pfx)
|
apply (rule dcorres_expand_pfx)
|
||||||
apply (rule corres_guard_imp)
|
apply (rule corres_guard_imp)
|
||||||
apply (simp add: inject_reply_cap_def setup_caller_cap_def)
|
apply (simp add: inject_reply_cap_def setup_caller_cap_def split del: if_split)
|
||||||
apply (rule corres_split[OF _ set_thread_state_corres])
|
apply (rule corres_split[OF _ set_thread_state_corres])
|
||||||
apply (rule reply_cap_insert_corres)
|
apply (rule reply_cap_insert_corres)
|
||||||
apply (simp add:not_idle_thread_def)+
|
apply (simp add:not_idle_thread_def)+
|
||||||
|
@ -1159,13 +1163,14 @@ definition
|
||||||
"dest_of xs \<equiv> case xs of [] \<Rightarrow> None | [r] \<Rightarrow> Some (transform_cslot_ptr r)"
|
"dest_of xs \<equiv> case xs of [] \<Rightarrow> None | [r] \<Rightarrow> Some (transform_cslot_ptr r)"
|
||||||
|
|
||||||
lemma update_cap_rights_cong:
|
lemma update_cap_rights_cong:
|
||||||
"\<lbrakk> is_ep_cap cap \<or> is_ntfn_cap cap \<or> is_arch_page_cap cap \<Longrightarrow> R = R' \<rbrakk> \<Longrightarrow>
|
"\<lbrakk> is_ep_cap cap \<or> is_ntfn_cap cap \<or> is_reply_cap cap \<or> is_arch_page_cap cap \<Longrightarrow> R = R' \<rbrakk> \<Longrightarrow>
|
||||||
transform_cap (cap_rights_update R' cap) = update_cap_rights R (transform_cap cap)"
|
transform_cap (cap_rights_update R' cap) = update_cap_rights R (transform_cap cap)"
|
||||||
by (clarsimp simp: cap_rights_update_def acap_rights_update_def update_cap_rights_def
|
by (clarsimp simp: is_reply_cap_def
|
||||||
|
cap_rights_update_def acap_rights_update_def update_cap_rights_def
|
||||||
split: cap.splits arch_cap.splits)
|
split: cap.splits arch_cap.splits)
|
||||||
|
|
||||||
lemma transform_cap_rights:
|
lemma transform_cap_rights:
|
||||||
"is_ep_cap cap \<or> is_ntfn_cap cap \<or> is_arch_page_cap cap
|
"is_ep_cap cap \<or> is_ntfn_cap cap \<or> is_reply_cap cap \<or> is_arch_page_cap cap
|
||||||
\<Longrightarrow> (Structures_A.cap_rights cap) = Types_D.cap_rights (transform_cap cap)"
|
\<Longrightarrow> (Structures_A.cap_rights cap) = Types_D.cap_rights (transform_cap cap)"
|
||||||
by (auto simp: is_cap_simps is_arch_page_cap_def Types_D.cap_rights_def transform_cap_def
|
by (auto simp: is_cap_simps is_arch_page_cap_def Types_D.cap_rights_def transform_cap_def
|
||||||
split: arch_cap.splits cap.splits)
|
split: arch_cap.splits cap.splits)
|
||||||
|
@ -1488,6 +1493,7 @@ lemma get_ipc_buffer_words_receive_slots:
|
||||||
apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric] word_of_int_hom_syms)
|
apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric] word_of_int_hom_syms)
|
||||||
done
|
done
|
||||||
|
|
||||||
|
(* FIXME: MOVE *)
|
||||||
lemma dcorres_return:
|
lemma dcorres_return:
|
||||||
"r a b \<Longrightarrow> dcorres (r) (\<lambda>_. True) (\<lambda>_. True) (return a) (return b)"
|
"r a b \<Longrightarrow> dcorres (r) (\<lambda>_. True) (\<lambda>_. True) (return a) (return b)"
|
||||||
by (clarsimp simp:return_def corres_underlying_def)
|
by (clarsimp simp:return_def corres_underlying_def)
|
||||||
|
@ -1586,11 +1592,10 @@ lemma get_receive_slot_dcorres:
|
||||||
apply (clarsimp simp: word_size word_bits_def)+
|
apply (clarsimp simp: word_size word_bits_def)+
|
||||||
apply (rule hoareE_TrueI)+
|
apply (rule hoareE_TrueI)+
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (rule hoare_post_impErr[OF hoareE_TrueI])
|
apply (rule hoare_post_impErr[OF hoareE_TrueI TrueI])
|
||||||
apply fastforce
|
|
||||||
apply simp
|
apply simp
|
||||||
apply (wp lsfco_not_idle | clarsimp)+
|
apply (wp lsfco_not_idle | clarsimp)+
|
||||||
apply fastforce
|
apply (rule conjI; rule TrueI)
|
||||||
apply (clarsimp simp:not_idle_thread_def)
|
apply (clarsimp simp:not_idle_thread_def)
|
||||||
apply fastforce
|
apply fastforce
|
||||||
apply (wp mapM_wp)
|
apply (wp mapM_wp)
|
||||||
|
@ -1944,7 +1949,7 @@ lemma corres_complete_ipc_transfer:
|
||||||
(valid_objs and pspace_aligned and valid_global_refs and pspace_distinct and valid_mdb
|
(valid_objs and pspace_aligned and valid_global_refs and pspace_distinct and valid_mdb
|
||||||
and (\<lambda>s. not_idle_thread (cur_thread s) s) and valid_irq_node
|
and (\<lambda>s. not_idle_thread (cur_thread s) s) and valid_irq_node
|
||||||
and valid_idle and not_idle_thread recv and not_idle_thread send and valid_etcbs)
|
and valid_idle and not_idle_thread recv and not_idle_thread send and valid_etcbs)
|
||||||
(Endpoint_D.do_ipc_transfer ep' send recv can_grant)
|
(Endpoint_D.do_ipc_transfer ep' send recv can_grant) (* FIXME argument order *)
|
||||||
(Ipc_A.do_ipc_transfer send ep badge can_grant recv)"
|
(Ipc_A.do_ipc_transfer send ep badge can_grant recv)"
|
||||||
apply (clarsimp simp: Endpoint_D.do_ipc_transfer_def Ipc_A.do_ipc_transfer_def)
|
apply (clarsimp simp: Endpoint_D.do_ipc_transfer_def Ipc_A.do_ipc_transfer_def)
|
||||||
apply (rule dcorres_expand_pfx)
|
apply (rule dcorres_expand_pfx)
|
||||||
|
@ -2236,11 +2241,12 @@ lemma do_reply_transfer_corres:
|
||||||
shows
|
shows
|
||||||
"slot' = transform_cslot_ptr slot \<Longrightarrow>
|
"slot' = transform_cslot_ptr slot \<Longrightarrow>
|
||||||
dcorres dc \<top>
|
dcorres dc \<top>
|
||||||
(invs and tcb_at recver and tcb_at sender and cte_wp_at ((=) (cap.ReplyCap recver False)) slot
|
(invs and tcb_at recver and tcb_at sender
|
||||||
|
and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap recver False R) slot
|
||||||
and (\<lambda>s. not_idle_thread (cur_thread s) s)
|
and (\<lambda>s. not_idle_thread (cur_thread s) s)
|
||||||
and not_idle_thread recver and not_idle_thread sender and valid_etcbs)
|
and not_idle_thread recver and not_idle_thread sender and valid_etcbs)
|
||||||
(Endpoint_D.do_reply_transfer sender recver slot')
|
(Endpoint_D.do_reply_transfer sender recver slot' can_grant)
|
||||||
(Ipc_A.do_reply_transfer sender recver slot)"
|
(Ipc_A.do_reply_transfer sender recver slot can_grant)"
|
||||||
apply (clarsimp simp:do_reply_transfer_def Endpoint_D.do_reply_transfer_def)
|
apply (clarsimp simp:do_reply_transfer_def Endpoint_D.do_reply_transfer_def)
|
||||||
apply (clarsimp simp:get_thread_state_def thread_get_def get_thread_fault_def)
|
apply (clarsimp simp:get_thread_state_def thread_get_def get_thread_fault_def)
|
||||||
apply (rule dcorres_absorb_gets_the)
|
apply (rule dcorres_absorb_gets_the)
|
||||||
|
@ -2296,12 +2302,13 @@ lemma do_reply_transfer_corres:
|
||||||
apply (rule conjI)
|
apply (rule conjI)
|
||||||
apply (case_tac slot)
|
apply (case_tac slot)
|
||||||
apply (clarsimp simp:invs_def not_idle_thread_def valid_state_def)
|
apply (clarsimp simp:invs_def not_idle_thread_def valid_state_def)
|
||||||
|
apply (clarsimp simp:cte_wp_at_caps_of_state)
|
||||||
apply (drule valid_idle_has_null_cap)
|
apply (drule valid_idle_has_null_cap)
|
||||||
apply assumption+
|
apply assumption+
|
||||||
apply (fastforce simp:valid_state_def cte_wp_at_caps_of_state)
|
apply (fastforce simp:valid_state_def)
|
||||||
apply simp
|
|
||||||
apply (rule emptyable_cte_wp_atD)
|
apply (rule emptyable_cte_wp_atD)
|
||||||
apply (simp add: is_master_reply_cap_def invs_def valid_state_def valid_pspace_def valid_idle_def)+
|
apply (fastforce simp:is_master_reply_cap_def invs_def
|
||||||
|
valid_state_def valid_pspace_def valid_idle_def)+
|
||||||
done
|
done
|
||||||
|
|
||||||
lemma set_endpoint_valid_irq_node[wp]:
|
lemma set_endpoint_valid_irq_node[wp]:
|
||||||
|
@ -2334,34 +2341,34 @@ lemma dcorres_if_rhs:
|
||||||
(* this is ugly and terrible, but pretty much recreates
|
(* this is ugly and terrible, but pretty much recreates
|
||||||
the old recv_sync_ipc_corres proof to avoid duplication *)
|
the old recv_sync_ipc_corres proof to avoid duplication *)
|
||||||
lemma dcorres_receive_sync:
|
lemma dcorres_receive_sync:
|
||||||
"\<lbrakk> ep_at word1 s; ko_at (kernel_object.Endpoint rv) word1 s; not_idle_thread thread s;
|
"\<lbrakk> ep_at ep s; ko_at (kernel_object.Endpoint rv) ep s; not_idle_thread thread s;
|
||||||
not_idle_thread (cur_thread s) s; st_tcb_at active thread s; valid_state s;
|
not_idle_thread (cur_thread s) s; st_tcb_at active thread s; valid_state s;
|
||||||
valid_etcbs s \<rbrakk> \<Longrightarrow>
|
valid_etcbs s \<rbrakk> \<Longrightarrow>
|
||||||
dcorres dc ((=) (transform s)) ((=) s)
|
dcorres dc ((=) (transform s)) ((=) s)
|
||||||
(receive_sync thread word1)
|
(receive_sync thread ep can_grant)
|
||||||
(case rv of
|
(case rv of
|
||||||
Structures_A.endpoint.IdleEP \<Rightarrow> (case is_blocking of
|
Structures_A.endpoint.IdleEP \<Rightarrow> (case is_blocking of
|
||||||
True \<Rightarrow> do set_thread_state thread
|
True \<Rightarrow> do set_thread_state thread
|
||||||
(Structures_A.thread_state.BlockedOnReceive word1);
|
(Structures_A.thread_state.BlockedOnReceive ep
|
||||||
set_endpoint word1 (Structures_A.endpoint.RecvEP [thread])
|
\<lparr>receiver_can_grant = can_grant\<rparr>);
|
||||||
|
set_endpoint ep (Structures_A.endpoint.RecvEP [thread])
|
||||||
od
|
od
|
||||||
| False \<Rightarrow> do_nbrecv_failed_transfer thread)
|
| False \<Rightarrow> do_nbrecv_failed_transfer thread)
|
||||||
| Structures_A.endpoint.SendEP q \<Rightarrow>
|
| Structures_A.endpoint.SendEP q \<Rightarrow>
|
||||||
do assert (q \<noteq> []);
|
do assert (q \<noteq> []);
|
||||||
queue \<leftarrow> return $ tl q;
|
queue \<leftarrow> return $ tl q;
|
||||||
sender \<leftarrow> return $ hd q;
|
sender \<leftarrow> return $ hd q;
|
||||||
set_endpoint word1 $
|
set_endpoint ep $
|
||||||
case queue of [] \<Rightarrow> Structures_A.endpoint.IdleEP
|
(case queue of [] \<Rightarrow> Structures_A.endpoint.IdleEP
|
||||||
| a # list \<Rightarrow> Structures_A.endpoint.SendEP queue;
|
| a # list \<Rightarrow> Structures_A.endpoint.SendEP queue);
|
||||||
sender_state \<leftarrow> get_thread_state sender;
|
sender_state \<leftarrow> get_thread_state sender;
|
||||||
data \<leftarrow> case sender_state of
|
payload \<leftarrow> case sender_state of
|
||||||
Structures_A.thread_state.BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
|
Structures_A.thread_state.BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
|
||||||
Ipc_A.do_ipc_transfer sender (Some word1) (sender_badge data)
|
Ipc_A.do_ipc_transfer sender (Some ep) (sender_badge payload)
|
||||||
(sender_can_grant data) thread;
|
(sender_can_grant payload) thread;
|
||||||
fault \<leftarrow> thread_get tcb_fault sender;
|
if sender_is_call payload
|
||||||
if sender_is_call data \<or> fault \<noteq> None
|
then if sender_can_grant payload \<or> sender_can_grant_reply payload
|
||||||
then if sender_can_grant data
|
then setup_caller_cap sender thread can_grant
|
||||||
then setup_caller_cap sender thread
|
|
||||||
else set_thread_state sender Structures_A.thread_state.Inactive
|
else set_thread_state sender Structures_A.thread_state.Inactive
|
||||||
else do set_thread_state sender Structures_A.thread_state.Running;
|
else do set_thread_state sender Structures_A.thread_state.Running;
|
||||||
do_extended_op (possible_switch_to sender)
|
do_extended_op (possible_switch_to sender)
|
||||||
|
@ -2369,8 +2376,9 @@ lemma dcorres_receive_sync:
|
||||||
od
|
od
|
||||||
| Structures_A.endpoint.RecvEP queue \<Rightarrow> (case is_blocking of
|
| Structures_A.endpoint.RecvEP queue \<Rightarrow> (case is_blocking of
|
||||||
True \<Rightarrow> do set_thread_state thread
|
True \<Rightarrow> do set_thread_state thread
|
||||||
(Structures_A.thread_state.BlockedOnReceive word1);
|
(Structures_A.thread_state.BlockedOnReceive ep
|
||||||
set_endpoint word1 (Structures_A.endpoint.RecvEP (queue @ [thread]))
|
\<lparr>receiver_can_grant = can_grant\<rparr>);
|
||||||
|
set_endpoint ep (Structures_A.endpoint.RecvEP (queue @ [thread]))
|
||||||
od
|
od
|
||||||
| False \<Rightarrow> do_nbrecv_failed_transfer thread))"
|
| False \<Rightarrow> do_nbrecv_failed_transfer thread))"
|
||||||
apply (clarsimp simp: receive_sync_def gets_def)
|
apply (clarsimp simp: receive_sync_def gets_def)
|
||||||
|
@ -2406,33 +2414,33 @@ lemma dcorres_receive_sync:
|
||||||
apply (rename_tac list)
|
apply (rename_tac list)
|
||||||
apply (drule_tac s = "set list" in sym)
|
apply (drule_tac s = "set list" in sym)
|
||||||
apply (rule conjI, clarsimp dest!: not_empty_list_not_empty_set)
|
apply (rule conjI, clarsimp dest!: not_empty_list_not_empty_set)
|
||||||
apply (clarsimp simp:neq_Nil_conv)
|
apply (clarsimp simp:neq_Nil_conv, rename_tac t ts)
|
||||||
apply (rule_tac P1="\<top>" and P'="(=) s" and x1 = y
|
apply (rule_tac P1="\<top>" and P'="(=) s" and x1 = t
|
||||||
in dcorres_absorb_pfx[OF select_pick_corres[OF dcorres_expand_pfx],rotated])
|
in dcorres_absorb_pfx[OF select_pick_corres[OF dcorres_expand_pfx],rotated])
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (drule_tac x1 = y in iffD2[OF eqset_imp_iff], simp)
|
apply (drule_tac x1 = t in iffD2[OF eqset_imp_iff], simp)
|
||||||
apply (clarsimp simp:ep_waiting_set_send_def get_thread_def bind_assoc gets_the_def gets_def)
|
apply (clarsimp simp:ep_waiting_set_send_def get_thread_def bind_assoc gets_the_def gets_def)
|
||||||
|
apply (rename_tac tcb payload)
|
||||||
apply (rule dcorres_absorb_get_l,clarsimp)
|
apply (rule dcorres_absorb_get_l,clarsimp)
|
||||||
apply (frule(1) valid_etcbs_tcb_etcb, clarsimp)
|
apply (frule(1) valid_etcbs_tcb_etcb, clarsimp)
|
||||||
apply (subst opt_object_tcb)
|
apply (subst opt_object_tcb)
|
||||||
apply (erule get_tcb_rev)
|
apply (erule get_tcb_rev)
|
||||||
apply (fastforce simp: get_etcb_def)
|
apply (fastforce simp: get_etcb_def)
|
||||||
apply (frule_tac a = y and list = "y # ys" in pending_thread_in_send_not_idle)
|
apply (frule_tac a = t and list = "t # ts" in pending_thread_in_send_not_idle)
|
||||||
apply ((simp add: valid_state_def insertI obj_at_def not_idle_thread_def )+)[4]
|
apply ((simp add: valid_state_def insertI obj_at_def not_idle_thread_def)+)[4]
|
||||||
apply (clarsimp simp: assert_opt_def transform_tcb_def infer_tcb_pending_op_def tcb_slots
|
apply (clarsimp simp: assert_opt_def transform_tcb_def infer_tcb_pending_op_def tcb_slots
|
||||||
split del: if_split)
|
split del: if_split)
|
||||||
apply (rule dcorres_symb_exec_r)
|
apply (rule dcorres_symb_exec_r)
|
||||||
apply (rule corres_symb_exec_r)
|
apply (rule corres_symb_exec_r)
|
||||||
apply (rule_tac F="sender_state = tcb_state t" in corres_gen_asm2)
|
apply (rule_tac F="sender_state = tcb_state tcb" in corres_gen_asm2)
|
||||||
apply (clarsimp dest!: get_tcb_SomeD simp: dc_def[symmetric]
|
apply (clarsimp dest!: get_tcb_SomeD simp: dc_def[symmetric]
|
||||||
split del: if_split split: if_split_asm)
|
split del: if_split split: if_split_asm)
|
||||||
apply (rule corres_guard_imp)
|
apply (rule corres_guard_imp)
|
||||||
apply (rule corres_split[OF _ corres_complete_ipc_transfer])
|
apply (rule corres_split[OF _ corres_complete_ipc_transfer])
|
||||||
prefer 2
|
prefer 2
|
||||||
apply simp
|
apply simp
|
||||||
apply (rule corres_symb_exec_r)
|
|
||||||
apply (rule dcorres_if_rhs)
|
apply (rule dcorres_if_rhs)
|
||||||
apply (rule dcorres_if_rhs)
|
apply (rule dcorres_if_rhs)
|
||||||
apply (simp add:dc_def[symmetric] when_def)
|
apply (simp add:dc_def[symmetric] when_def)
|
||||||
|
@ -2443,28 +2451,26 @@ lemma dcorres_receive_sync:
|
||||||
apply (rule corres_alternate1[OF corres_alternate2])
|
apply (rule corres_alternate1[OF corres_alternate2])
|
||||||
apply (rule dcorres_rhs_noop_below_True[OF possible_switch_to_dcorres])
|
apply (rule dcorres_rhs_noop_below_True[OF possible_switch_to_dcorres])
|
||||||
apply (rule set_thread_state_corres[unfolded tcb_slots])
|
apply (rule set_thread_state_corres[unfolded tcb_slots])
|
||||||
apply clarsimp
|
apply wp
|
||||||
apply (wp hoare_drop_imps)+
|
apply (wp hoare_drop_imps gts_st_tcb_at | simp add:not_idle_thread_def)+
|
||||||
apply clarsimp
|
|
||||||
apply (wp gts_st_tcb_at | simp add:not_idle_thread_def )+
|
|
||||||
apply (rule_tac Q="\<lambda>fault. valid_mdb and valid_objs and pspace_aligned
|
apply (rule_tac Q="\<lambda>fault. valid_mdb and valid_objs and pspace_aligned
|
||||||
and pspace_distinct and not_idle_thread y and not_idle_thread thread
|
and pspace_distinct and not_idle_thread t and not_idle_thread thread
|
||||||
and valid_idle and valid_irq_node and (\<lambda>s. cur_thread s \<noteq> idle_thread s)
|
and valid_idle and valid_irq_node and (\<lambda>s. cur_thread s \<noteq> idle_thread s)
|
||||||
and tcb_at y and tcb_at thread
|
and tcb_at t and tcb_at thread
|
||||||
and st_tcb_at (\<lambda>rv. rv = Structures_A.thread_state.BlockedOnSend word1 payload) y and valid_etcbs"
|
and st_tcb_at (\<lambda>rv. rv = Structures_A.thread_state.BlockedOnSend ep payload) t and valid_etcbs"
|
||||||
in hoare_strengthen_post[rotated])
|
in hoare_strengthen_post[rotated])
|
||||||
apply (clarsimp simp:not_idle_thread_def)
|
apply (clarsimp simp:not_idle_thread_def)
|
||||||
apply (clarsimp simp:st_tcb_at_def obj_at_def)
|
apply (clarsimp simp:st_tcb_at_def obj_at_def)
|
||||||
apply ((wp | clarsimp simp:not_idle_thread_def | wps )+)[1]
|
apply ((wp | clarsimp simp:not_idle_thread_def | wps )+)[1]
|
||||||
apply (frule_tac a = y and list = "y # ys" in pending_thread_in_send_not_idle)
|
apply (frule_tac a = t and list = "t # ts" in pending_thread_in_send_not_idle)
|
||||||
apply (clarsimp simp:valid_state_def insertI)+
|
apply (clarsimp simp:valid_state_def insertI)+
|
||||||
apply (simp add:obj_at_def not_idle_thread_def)+
|
apply (simp add:obj_at_def not_idle_thread_def)+
|
||||||
apply (clarsimp simp:valid_state_def st_tcb_at_def obj_at_def valid_pspace_def)
|
apply (clarsimp simp:valid_state_def st_tcb_at_def obj_at_def valid_pspace_def)
|
||||||
apply (drule valid_objs_valid_ep_simp)
|
apply (drule valid_objs_valid_ep_simp)
|
||||||
apply (simp add:is_ep_def)
|
apply (simp add:is_ep_def)
|
||||||
apply (clarsimp simp: valid_ep_def a_type_def
|
apply (clarsimp simp:valid_ep_def valid_simple_obj_def a_type_def
|
||||||
split: Structures_A.endpoint.splits list.splits)
|
split:Structures_A.endpoint.splits list.splits)
|
||||||
apply (clarsimp simp:valid_state_def valid_pspace_def a_type_def)+
|
apply (clarsimp simp:valid_state_def valid_pspace_def valid_simple_obj_def a_type_def)+
|
||||||
apply (rule dcorres_to_wp[where Q=\<top>,simplified])
|
apply (rule dcorres_to_wp[where Q=\<top>,simplified])
|
||||||
apply (rule corres_dummy_set_sync_ep)
|
apply (rule corres_dummy_set_sync_ep)
|
||||||
(* RecvEP *)
|
(* RecvEP *)
|
||||||
|
@ -2509,10 +2515,11 @@ lemma recv_sync_ipc_corres:
|
||||||
(ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s)
|
(ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s)
|
||||||
and st_tcb_at active thread
|
and st_tcb_at active thread
|
||||||
and valid_state and valid_etcbs)
|
and valid_state and valid_etcbs)
|
||||||
(Endpoint_D.receive_ipc tcb_id_receiver ep_id )
|
(Endpoint_D.receive_ipc tcb_id_receiver ep_id (Grant \<in> cap_rights ep_cap))
|
||||||
(Ipc_A.receive_ipc thread ep_cap is_blocking)"
|
(Ipc_A.receive_ipc thread ep_cap is_blocking)"
|
||||||
apply (clarsimp simp:corres_free_fail cap_ep_ptr_def Ipc_A.receive_ipc_def
|
apply (clarsimp simp:corres_free_fail cap_ep_ptr_def Ipc_A.receive_ipc_def
|
||||||
split:cap.splits Structures_A.endpoint.splits)
|
split:cap.splits Structures_A.endpoint.splits)
|
||||||
|
apply (rename_tac ep_badge ep_rights)
|
||||||
apply (rule dcorres_expand_pfx)
|
apply (rule dcorres_expand_pfx)
|
||||||
apply (rule_tac Q'="\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr" in corres_symb_exec_r)
|
apply (rule_tac Q'="\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr" in corres_symb_exec_r)
|
||||||
apply (simp add:Endpoint_D.receive_ipc_def get_bound_notification_def thread_get_def gets_the_def gets_def bind_assoc)
|
apply (simp add:Endpoint_D.receive_ipc_def get_bound_notification_def thread_get_def gets_the_def gets_def bind_assoc)
|
||||||
|
@ -2591,6 +2598,34 @@ lemma dcorres_dummy_set_pending_cap_Restart:
|
||||||
crunch pred_tcb[wp]: do_ipc_transfer "pred_tcb_at proj P t"
|
crunch pred_tcb[wp]: do_ipc_transfer "pred_tcb_at proj P t"
|
||||||
(wp: crunch_wps transfer_caps_loop_pres make_fault_message_inv simp: zipWithM_x_mapM)
|
(wp: crunch_wps transfer_caps_loop_pres make_fault_message_inv simp: zipWithM_x_mapM)
|
||||||
|
|
||||||
|
lemma dcorres_get_thread_state:
|
||||||
|
"dcorres (\<lambda>op ts. op = infer_tcb_pending_op t ts)
|
||||||
|
\<top>
|
||||||
|
(valid_etcbs and tcb_at t and not_idle_thread t)
|
||||||
|
(do tcb <- get_thread t; return (the (cdl_tcb_caps tcb tcb_pending_op_slot)) od)
|
||||||
|
(get_thread_state t)"
|
||||||
|
text \<open>Brute force proof. Trying to reuse @{thm thread_get_corres} doesn't
|
||||||
|
seem to work, because it expects to have concrete tcbs\<close>
|
||||||
|
apply (simp add: get_thread_state_def)
|
||||||
|
apply (monad_eq simp: corres_underlying_def Bex_def
|
||||||
|
get_thread_def opt_object_def
|
||||||
|
thread_get_def get_tcb_def
|
||||||
|
split: option.splits)
|
||||||
|
apply (rename_tac s ko tcb)
|
||||||
|
apply (case_tac ko; clarsimp)
|
||||||
|
text \<open>These two existential vars refer to the same transformed tcb.
|
||||||
|
We skip the first one and instantiate the second first\<close>
|
||||||
|
apply (rule exI)
|
||||||
|
apply (rule conjI)
|
||||||
|
apply (rule_tac x="transform_tcb (machine_state s) t tcb (the (get_etcb t s))" in exI)
|
||||||
|
apply (monad_eq simp: transform_tcb_def)
|
||||||
|
apply (rule conjI)
|
||||||
|
apply (fastforce simp: get_etcb_def cdl_objects_tcb not_idle_thread_def
|
||||||
|
dest: valid_etcbs_tcb_etcb)
|
||||||
|
apply (rule refl)
|
||||||
|
apply (clarsimp simp: infer_tcb_pending_op_def tcb_slot_defs)
|
||||||
|
done
|
||||||
|
|
||||||
lemma send_sync_ipc_corres:
|
lemma send_sync_ipc_corres:
|
||||||
"\<lbrakk>ep_id = epptr;tcb_id_sender= thread\<rbrakk> \<Longrightarrow>
|
"\<lbrakk>ep_id = epptr;tcb_id_sender= thread\<rbrakk> \<Longrightarrow>
|
||||||
dcorres dc
|
dcorres dc
|
||||||
|
@ -2598,9 +2633,10 @@ lemma send_sync_ipc_corres:
|
||||||
(not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s)
|
(not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s)
|
||||||
and st_tcb_at active thread
|
and st_tcb_at active thread
|
||||||
and valid_state and valid_etcbs)
|
and valid_state and valid_etcbs)
|
||||||
(Endpoint_D.send_ipc block call badge can_grant tcb_id_sender ep_id)
|
(Endpoint_D.send_ipc block call badge can_grant can_grant_reply tcb_id_sender ep_id)
|
||||||
(Ipc_A.send_ipc block call badge can_grant thread epptr)"
|
(Ipc_A.send_ipc block call badge can_grant can_grant_reply thread epptr)"
|
||||||
apply (clarsimp simp:gets_def Endpoint_D.send_ipc_def Ipc_A.send_ipc_def split del:if_split)
|
apply (clarsimp simp:gets_def Endpoint_D.send_ipc_def Ipc_A.send_ipc_def
|
||||||
|
split del:if_split)
|
||||||
apply (rule dcorres_absorb_get_l)
|
apply (rule dcorres_absorb_get_l)
|
||||||
apply (clarsimp split del:if_split)
|
apply (clarsimp split del:if_split)
|
||||||
apply (rule_tac Q' = "\<lambda>r. (=) s' and ko_at (kernel_object.Endpoint r) epptr" in corres_symb_exec_r[rotated])
|
apply (rule_tac Q' = "\<lambda>r. (=) s' and ko_at (kernel_object.Endpoint r) epptr" in corres_symb_exec_r[rotated])
|
||||||
|
@ -2651,36 +2687,36 @@ lemma send_sync_ipc_corres:
|
||||||
apply (subst when_def)+
|
apply (subst when_def)+
|
||||||
apply (rule corres_guard_imp)
|
apply (rule corres_guard_imp)
|
||||||
apply (rule dcorres_symb_exec_r)
|
apply (rule dcorres_symb_exec_r)
|
||||||
apply (rule corres_symb_exec_r)
|
apply (simp only: liftM_def)
|
||||||
apply (case_tac "recv_state"; simp add: corres_free_fail split del: if_split)
|
apply (rule corres_split[OF _ dcorres_get_thread_state])
|
||||||
|
apply (clarsimp, rename_tac recv_state')
|
||||||
|
apply (case_tac recv_state'; simp add: corres_free_fail split del: if_split)
|
||||||
apply (rule corres_split[OF _ corres_complete_ipc_transfer])
|
apply (rule corres_split[OF _ corres_complete_ipc_transfer])
|
||||||
apply (rule corres_split[OF _ set_thread_state_corres])
|
apply (rule corres_split[OF _ set_thread_state_corres])
|
||||||
apply (rule dcorres_rhs_noop_above[OF possible_switch_to_dcorres])
|
apply (rule dcorres_rhs_noop_above[OF possible_switch_to_dcorres])
|
||||||
apply (rule_tac corres_symb_exec_r)
|
|
||||||
apply (rule dcorres_if_rhs)
|
apply (rule dcorres_if_rhs)
|
||||||
apply (rule dcorres_if_rhs)
|
apply (rule dcorres_if_rhs)
|
||||||
apply (simp only:if_True)
|
apply (clarsimp simp only: if_True)
|
||||||
apply (rule corres_alternate1)+
|
apply (rule corres_alternate1)+
|
||||||
apply (rule corres_setup_caller_cap)
|
apply (rule corres_setup_caller_cap)
|
||||||
apply (clarsimp simp:ep_waiting_set_recv_def pred_tcb_at_def obj_at_def generates_pending_def)
|
apply (clarsimp simp:ep_waiting_set_recv_def pred_tcb_at_def obj_at_def generates_pending_def)
|
||||||
apply (rule corres_alternate1[OF corres_alternate2])
|
apply (rule corres_alternate1[OF corres_alternate2])
|
||||||
apply (rule set_thread_state_corres)
|
apply (rule set_thread_state_corres)
|
||||||
apply (rule corres_alternate2)
|
apply (rule corres_alternate2)
|
||||||
apply (rule corres_return_trivial )
|
apply (rule corres_return_trivial)
|
||||||
apply (clarsimp)
|
apply wp
|
||||||
apply (rule_tac Q="\<lambda>r. valid_mdb and valid_idle and valid_objs
|
apply (rule_tac Q="\<lambda>r. valid_mdb and valid_idle and valid_objs
|
||||||
and not_idle_thread thread and not_idle_thread y and tcb_at thread and tcb_at y
|
and not_idle_thread thread and not_idle_thread y and tcb_at thread and tcb_at y
|
||||||
and st_tcb_at runnable thread and valid_etcbs
|
and st_tcb_at runnable thread and valid_etcbs"
|
||||||
" in hoare_strengthen_post[rotated])
|
in hoare_strengthen_post[rotated])
|
||||||
apply (clarsimp simp:pred_tcb_at_def obj_at_def,
|
apply (clarsimp simp:pred_tcb_at_def obj_at_def,
|
||||||
simp split:Structures_A.thread_state.splits, fastforce)
|
simp split:Structures_A.thread_state.splits, fastforce)
|
||||||
apply ((wp sts_st_tcb_at' sts_st_tcb_at_neq |clarsimp simp add:not_idle_thread_def)+)
|
apply ((wp sts_st_tcb_at' sts_st_tcb_at_neq |clarsimp simp add:not_idle_thread_def)+)
|
||||||
apply (wp hoare_vcg_conj_lift)
|
apply (wp hoare_vcg_conj_lift)
|
||||||
apply (rule hoare_disjI1)
|
apply (rule hoare_disjI1)
|
||||||
apply (wp do_ipc_transfer_pred_tcb | wpc | simp)+
|
apply (wp do_ipc_transfer_pred_tcb | wpc | simp)+
|
||||||
apply (clarsimp simp:conj_comms not_idle_thread_def)+
|
apply (clarsimp simp:conj_comms not_idle_thread_def)
|
||||||
apply wp
|
apply (wp | wps)+
|
||||||
apply (wp|wps)+
|
|
||||||
apply (simp add:not_idle_thread_def)
|
apply (simp add:not_idle_thread_def)
|
||||||
apply (clarsimp simp:ep_waiting_set_recv_def obj_at_def st_tcb_at_def)+
|
apply (clarsimp simp:ep_waiting_set_recv_def obj_at_def st_tcb_at_def)+
|
||||||
apply (frule_tac a = "y" and list = "y # ys" in pending_thread_in_recv_not_idle)
|
apply (frule_tac a = "y" and list = "y # ys" in pending_thread_in_recv_not_idle)
|
||||||
|
|
|
@ -1429,7 +1429,7 @@ lemma fast_finalise_not_idle_thread[wp]:
|
||||||
lemma block_lift:
|
lemma block_lift:
|
||||||
"\<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; transform_tcb (machine_state b) word tcb_type etcb = Tcb cdl_tcb_type\<rbrakk>
|
"\<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; transform_tcb (machine_state b) word tcb_type etcb = Tcb cdl_tcb_type\<rbrakk>
|
||||||
\<Longrightarrow> is_thread_blocked_on_endpoint cdl_tcb_type ep = (case tcb_state tcb_type of
|
\<Longrightarrow> is_thread_blocked_on_endpoint cdl_tcb_type ep = (case tcb_state tcb_type of
|
||||||
Structures_A.thread_state.BlockedOnReceive p \<Rightarrow> ep = p
|
Structures_A.thread_state.BlockedOnReceive p _ \<Rightarrow> ep = p
|
||||||
| Structures_A.thread_state.BlockedOnSend p _ \<Rightarrow> ep = p
|
| Structures_A.thread_state.BlockedOnSend p _ \<Rightarrow> ep = p
|
||||||
| Structures_A.thread_state.BlockedOnNotification p \<Rightarrow> ep = p
|
| Structures_A.thread_state.BlockedOnNotification p \<Rightarrow> ep = p
|
||||||
| _ \<Rightarrow> False)"
|
| _ \<Rightarrow> False)"
|
||||||
|
@ -1451,18 +1451,22 @@ where "ntfn_waiting_set epptr s \<equiv>
|
||||||
definition none_is_waiting_ntfn :: "obj_ref \<Rightarrow> 'z::state_ext state\<Rightarrow>bool"
|
definition none_is_waiting_ntfn :: "obj_ref \<Rightarrow> 'z::state_ext state\<Rightarrow>bool"
|
||||||
where "none_is_waiting_ntfn epptr s \<equiv> (ntfn_waiting_set epptr s) = {}"
|
where "none_is_waiting_ntfn epptr s \<equiv> (ntfn_waiting_set epptr s) = {}"
|
||||||
|
|
||||||
definition ep_waiting_set_send :: "obj_ref\<Rightarrow> 'z::state_ext state\<Rightarrow>obj_ref set"
|
definition ep_waiting_set_send :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> obj_ref set"
|
||||||
where "ep_waiting_set_send epptr s \<equiv>
|
where "ep_waiting_set_send epptr s \<equiv>
|
||||||
{tcb. \<exists>t payload. ((kheap s tcb) = Some (TCB t))
|
{tcb. \<exists>t payload can_grant.
|
||||||
\<and> ((tcb_state t) = Structures_A.thread_state.BlockedOnSend epptr payload)}"
|
kheap s tcb = Some (TCB t)
|
||||||
|
\<and> tcb_state t = Structures_A.thread_state.BlockedOnSend epptr payload
|
||||||
|
\<and> can_grant = sender_can_grant payload}"
|
||||||
|
|
||||||
definition none_is_sending_ep:: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
|
definition none_is_sending_ep:: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
|
||||||
where "none_is_sending_ep epptr s \<equiv> (ep_waiting_set_send epptr s) = {}"
|
where "none_is_sending_ep epptr s \<equiv> (ep_waiting_set_send epptr s) = {}"
|
||||||
|
|
||||||
definition ep_waiting_set_recv :: "obj_ref\<Rightarrow> 'z::state_ext state\<Rightarrow>obj_ref set"
|
definition ep_waiting_set_recv :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> obj_ref set"
|
||||||
where "ep_waiting_set_recv epptr s \<equiv>
|
where "ep_waiting_set_recv epptr s \<equiv>
|
||||||
{tcb. \<exists>t. ((kheap s tcb) = Some (TCB t))
|
{tcb. \<exists>t payload can_grant.
|
||||||
\<and> ((tcb_state t) = Structures_A.thread_state.BlockedOnReceive epptr)}"
|
kheap s tcb = Some (TCB t)
|
||||||
|
\<and> tcb_state t = Structures_A.thread_state.BlockedOnReceive epptr payload
|
||||||
|
\<and> can_grant = receiver_can_grant payload}"
|
||||||
|
|
||||||
definition none_is_receiving_ep:: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
|
definition none_is_receiving_ep:: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
|
||||||
where "none_is_receiving_ep epptr s \<equiv> (ep_waiting_set_recv epptr s) = {}"
|
where "none_is_receiving_ep epptr s \<equiv> (ep_waiting_set_recv epptr s) = {}"
|
||||||
|
@ -1593,25 +1597,27 @@ lemma ntfn_not_waiting_ep_send:
|
||||||
"\<lbrakk> valid_objs s;kheap s epptr = Some (kernel_object.Notification ntfn) \<rbrakk>
|
"\<lbrakk> valid_objs s;kheap s epptr = Some (kernel_object.Notification ntfn) \<rbrakk>
|
||||||
\<Longrightarrow> ep_waiting_set_send epptr s = {}"
|
\<Longrightarrow> ep_waiting_set_send epptr s = {}"
|
||||||
apply (rule set_eqI)
|
apply (rule set_eqI)
|
||||||
apply (clarsimp simp:ep_waiting_set_send_def)
|
apply (clarsimp simp: ep_waiting_set_send_def)
|
||||||
apply (simp add:valid_objs_def)
|
apply (simp add: valid_objs_def)
|
||||||
apply (drule_tac x= x in bspec)
|
apply (rename_tac ptr t payload)
|
||||||
apply (clarsimp simp:dom_def)
|
apply (drule_tac x=ptr in bspec)
|
||||||
apply (clarsimp simp:valid_obj_def valid_tcb_def valid_tcb_state_def obj_at_def is_ep_def
|
apply (clarsimp simp: dom_def)
|
||||||
split:Structures_A.kernel_object.splits)
|
apply (clarsimp simp: valid_obj_def valid_tcb_def valid_tcb_state_def obj_at_def is_ep_def
|
||||||
done
|
split: Structures_A.kernel_object.splits)
|
||||||
|
done
|
||||||
|
|
||||||
lemma ntfn_not_waiting_ep_recv:
|
lemma ntfn_not_waiting_ep_recv:
|
||||||
"\<lbrakk> valid_objs s;kheap s epptr = Some (kernel_object.Notification ntfn) \<rbrakk>
|
"\<lbrakk> valid_objs s;kheap s epptr = Some (kernel_object.Notification ntfn) \<rbrakk>
|
||||||
\<Longrightarrow> ep_waiting_set_recv epptr s = {}"
|
\<Longrightarrow> ep_waiting_set_recv epptr s = {}"
|
||||||
apply (rule set_eqI)
|
apply (rule set_eqI)
|
||||||
apply (clarsimp simp:ep_waiting_set_recv_def)
|
apply (clarsimp simp: ep_waiting_set_recv_def)
|
||||||
apply (simp add:valid_objs_def)
|
apply (simp add: valid_objs_def)
|
||||||
apply (drule_tac x= x in bspec)
|
apply (rename_tac ptr t payload)
|
||||||
apply (clarsimp simp:dom_def)
|
apply (drule_tac x=ptr in bspec)
|
||||||
apply (clarsimp simp:valid_obj_def valid_tcb_def valid_tcb_state_def obj_at_def is_ep_def
|
apply (clarsimp simp: dom_def)
|
||||||
split:Structures_A.kernel_object.splits)
|
apply (clarsimp simp: valid_obj_def valid_tcb_def valid_tcb_state_def obj_at_def is_ep_def
|
||||||
done
|
split: Structures_A.kernel_object.splits)
|
||||||
|
done
|
||||||
|
|
||||||
lemma ep_not_waiting_ntfn:
|
lemma ep_not_waiting_ntfn:
|
||||||
"\<lbrakk> valid_objs s;kheap s epptr = Some (kernel_object.Endpoint ep) \<rbrakk>
|
"\<lbrakk> valid_objs s;kheap s epptr = Some (kernel_object.Endpoint ep) \<rbrakk>
|
||||||
|
@ -1624,7 +1630,6 @@ lemma ep_not_waiting_ntfn:
|
||||||
by (clarsimp simp:valid_obj_def valid_tcb_def valid_tcb_state_def obj_at_def is_ntfn_def
|
by (clarsimp simp:valid_obj_def valid_tcb_def valid_tcb_state_def obj_at_def is_ntfn_def
|
||||||
split:Structures_A.kernel_object.splits)
|
split:Structures_A.kernel_object.splits)
|
||||||
|
|
||||||
|
|
||||||
(* Following 2 lemmas is useful, it tells us that under certain condition, we can get valid_ep and valid_ntfn,
|
(* Following 2 lemmas is useful, it tells us that under certain condition, we can get valid_ep and valid_ntfn,
|
||||||
which helps us ruling out the idle thread and constract a map between the waiting list and waiting set
|
which helps us ruling out the idle thread and constract a map between the waiting list and waiting set
|
||||||
*)
|
*)
|
||||||
|
@ -1638,11 +1643,13 @@ lemma get_endpoint_pick:
|
||||||
apply (rule conjI)
|
apply (rule conjI)
|
||||||
apply (rule set_eqI)
|
apply (rule set_eqI)
|
||||||
apply (clarsimp simp:ep_waiting_set_send_def)
|
apply (clarsimp simp:ep_waiting_set_send_def)
|
||||||
apply (drule_tac x=x in spec)
|
apply (rename_tac ptr t payload)
|
||||||
|
apply (drule_tac x=ptr in spec)
|
||||||
apply (clarsimp simp: state_refs_of_def)
|
apply (clarsimp simp: state_refs_of_def)
|
||||||
apply (rule set_eqI)
|
apply (rule set_eqI)
|
||||||
apply (clarsimp simp:ep_waiting_set_recv_def)
|
apply (clarsimp simp:ep_waiting_set_recv_def)
|
||||||
apply (drule_tac x=x in spec)
|
apply (rename_tac ptr t payload)
|
||||||
|
apply (drule_tac x=ptr in spec)
|
||||||
apply (clarsimp simp:state_refs_of_def)
|
apply (clarsimp simp:state_refs_of_def)
|
||||||
apply (clarsimp simp:valid_state_def valid_pspace_def valid_objs_def)
|
apply (clarsimp simp:valid_state_def valid_pspace_def valid_objs_def)
|
||||||
apply (drule_tac x=epptr in bspec)
|
apply (drule_tac x=epptr in bspec)
|
||||||
|
@ -1652,7 +1659,8 @@ lemma get_endpoint_pick:
|
||||||
apply (rule sym)
|
apply (rule sym)
|
||||||
apply (rule antisym)
|
apply (rule antisym)
|
||||||
apply (clarsimp simp:ep_waiting_set_send_def sym_refs_def)
|
apply (clarsimp simp:ep_waiting_set_send_def sym_refs_def)
|
||||||
apply (drule_tac x = x in spec)
|
apply (rename_tac ptr t payload)
|
||||||
|
apply (drule_tac x=ptr in spec)
|
||||||
apply (clarsimp simp:state_refs_of_def)
|
apply (clarsimp simp:state_refs_of_def)
|
||||||
apply (clarsimp simp:ep_waiting_set_send_def sym_refs_def)
|
apply (clarsimp simp:ep_waiting_set_send_def sym_refs_def)
|
||||||
apply (drule_tac x= epptr in spec)
|
apply (drule_tac x= epptr in spec)
|
||||||
|
@ -1663,7 +1671,7 @@ lemma get_endpoint_pick:
|
||||||
apply (case_tac y)
|
apply (case_tac y)
|
||||||
apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def
|
apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def
|
||||||
split:Structures_A.kernel_object.splits)+
|
split:Structures_A.kernel_object.splits)+
|
||||||
apply (clarsimp simp:tcb_bound_refs_def2 split:Structures_A.thread_state.splits)
|
apply (force simp:tcb_bound_refs_def2 split:Structures_A.thread_state.splits)
|
||||||
apply (clarsimp simp:ep_waiting_set_send_def)
|
apply (clarsimp simp:ep_waiting_set_send_def)
|
||||||
apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def
|
apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def
|
||||||
split:Structures_A.kernel_object.splits)+
|
split:Structures_A.kernel_object.splits)+
|
||||||
|
@ -1677,7 +1685,8 @@ lemma get_endpoint_pick:
|
||||||
apply (clarsimp simp:none_is_receiving_ep_def)
|
apply (clarsimp simp:none_is_receiving_ep_def)
|
||||||
apply (rule set_eqI)
|
apply (rule set_eqI)
|
||||||
apply (clarsimp simp: ep_waiting_set_recv_def sym_refs_def)
|
apply (clarsimp simp: ep_waiting_set_recv_def sym_refs_def)
|
||||||
apply (drule_tac x = x in spec)
|
apply (rename_tac ptr t payload)
|
||||||
|
apply (drule_tac x = ptr in spec)
|
||||||
apply (clarsimp simp:state_refs_of_def)
|
apply (clarsimp simp:state_refs_of_def)
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
defer
|
defer
|
||||||
|
@ -1689,7 +1698,8 @@ lemma get_endpoint_pick:
|
||||||
apply (rule sym)
|
apply (rule sym)
|
||||||
apply (rule antisym)
|
apply (rule antisym)
|
||||||
apply (clarsimp simp:ep_waiting_set_recv_def sym_refs_def)
|
apply (clarsimp simp:ep_waiting_set_recv_def sym_refs_def)
|
||||||
apply (drule_tac x = x in spec)
|
apply (rename_tac ptr t payload)
|
||||||
|
apply (drule_tac x = ptr in spec)
|
||||||
apply (clarsimp simp:state_refs_of_def)
|
apply (clarsimp simp:state_refs_of_def)
|
||||||
apply (clarsimp simp:ep_waiting_set_recv_def sym_refs_def)
|
apply (clarsimp simp:ep_waiting_set_recv_def sym_refs_def)
|
||||||
apply (drule_tac x= epptr in spec)
|
apply (drule_tac x= epptr in spec)
|
||||||
|
@ -1700,7 +1710,7 @@ lemma get_endpoint_pick:
|
||||||
apply (case_tac y)
|
apply (case_tac y)
|
||||||
apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def
|
apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def
|
||||||
split:Structures_A.kernel_object.splits)+
|
split:Structures_A.kernel_object.splits)+
|
||||||
apply (clarsimp simp: tcb_bound_refs_def2 split:Structures_A.thread_state.splits)
|
apply (force simp: tcb_bound_refs_def2 split:Structures_A.thread_state.splits)
|
||||||
apply (clarsimp simp:ep_waiting_set_recv_def)
|
apply (clarsimp simp:ep_waiting_set_recv_def)
|
||||||
apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def
|
apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def
|
||||||
split:Structures_A.kernel_object.splits)+
|
split:Structures_A.kernel_object.splits)+
|
||||||
|
@ -1714,7 +1724,8 @@ lemma get_endpoint_pick:
|
||||||
apply (clarsimp simp:none_is_sending_ep_def)
|
apply (clarsimp simp:none_is_sending_ep_def)
|
||||||
apply (rule set_eqI)
|
apply (rule set_eqI)
|
||||||
apply (clarsimp simp: ep_waiting_set_send_def sym_refs_def)
|
apply (clarsimp simp: ep_waiting_set_send_def sym_refs_def)
|
||||||
apply (drule_tac x = x in spec)
|
apply (rename_tac ptr t payload)
|
||||||
|
apply (drule_tac x = ptr in spec)
|
||||||
apply (clarsimp simp:state_refs_of_def)
|
apply (clarsimp simp:state_refs_of_def)
|
||||||
apply (rename_tac list)
|
apply (rename_tac list)
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
|
@ -1937,12 +1948,12 @@ lemma is_thread_blocked_on_sth:
|
||||||
= (get_waiting_sync_recv_threads ep s) \<union> (get_waiting_sync_send_threads ep s) \<union> (get_waiting_ntfn_recv_threads ep s)"
|
= (get_waiting_sync_recv_threads ep s) \<union> (get_waiting_sync_send_threads ep s) \<union> (get_waiting_ntfn_recv_threads ep s)"
|
||||||
apply (rule set_eqI)
|
apply (rule set_eqI)
|
||||||
apply (rule iffI)
|
apply (rule iffI)
|
||||||
apply (clarsimp simp:is_thread_blocked_on_endpoint_def split:option.splits)
|
apply (clarsimp simp: is_thread_blocked_on_endpoint_def split: option.splits)
|
||||||
apply (case_tac y)
|
apply (case_tac y; simp add: get_waiting_sync_recv_threads_def get_waiting_sync_send_threads_def
|
||||||
apply (simp_all add: get_waiting_sync_recv_threads_def get_waiting_sync_send_threads_def get_waiting_ntfn_recv_threads_def)
|
get_waiting_ntfn_recv_threads_def)
|
||||||
apply safe
|
apply (fastforce simp: is_thread_blocked_on_endpoint_def get_waiting_sync_recv_threads_def
|
||||||
apply (clarsimp simp:is_thread_blocked_on_endpoint_def)+
|
get_waiting_sync_send_threads_def get_waiting_ntfn_recv_threads_def)
|
||||||
done
|
done
|
||||||
|
|
||||||
lemma set_ep_exec_wp: (* generalise? *)
|
lemma set_ep_exec_wp: (* generalise? *)
|
||||||
"\<lbrace>(=) s\<rbrace> set_endpoint epptr ep \<lbrace>\<lambda>r s'. s' = update_kheap ((kheap s)(epptr \<mapsto> Endpoint ep)) s\<rbrace> "
|
"\<lbrace>(=) s\<rbrace> set_endpoint epptr ep \<lbrace>\<lambda>r s'. s' = update_kheap ((kheap s)(epptr \<mapsto> Endpoint ep)) s\<rbrace> "
|
||||||
|
|
|
@ -542,16 +542,16 @@ lemma transform_intent_isnot_TcbIntent:
|
||||||
(label \<noteq> TCBUnbindNotification) \<and>
|
(label \<noteq> TCBUnbindNotification) \<and>
|
||||||
(label \<noteq> TCBSetTLSBase))"
|
(label \<noteq> TCBSetTLSBase))"
|
||||||
apply(rule iffI)
|
apply(rule iffI)
|
||||||
|
subgoal
|
||||||
apply(erule contrapos_np)
|
apply(erule contrapos_np)
|
||||||
apply(clarsimp simp: transform_intent_def)
|
apply(clarsimp simp: transform_intent_def)
|
||||||
apply(case_labels label)
|
apply(case_labels label; simp)
|
||||||
apply(simp_all)
|
apply(fastforce simp: transform_intent_tcb_defs option_map_def
|
||||||
apply(fastforce simp: transform_intent_tcb_defs
|
|
||||||
option_map_def
|
|
||||||
split: list.split)+
|
split: list.split)+
|
||||||
|
done
|
||||||
apply(unfold transform_intent_def)
|
apply(unfold transform_intent_def)
|
||||||
apply(case_labels label, simp_all add: option_map_def split: option.split)
|
apply(case_labels label, simp_all add: option_map_def split: option.split)
|
||||||
apply (auto simp: transform_intent_tcb_defs
|
apply(auto simp: transform_intent_tcb_defs
|
||||||
split: list.splits arch_invocation_label.splits)
|
split: list.splits arch_invocation_label.splits)
|
||||||
done
|
done
|
||||||
|
|
||||||
|
@ -622,8 +622,8 @@ where
|
||||||
Types_D.EndpointCap ptr badge cap_rights_
|
Types_D.EndpointCap ptr badge cap_rights_
|
||||||
| Structures_A.NotificationCap ptr badge cap_rights_ \<Rightarrow>
|
| Structures_A.NotificationCap ptr badge cap_rights_ \<Rightarrow>
|
||||||
Types_D.NotificationCap ptr badge cap_rights_
|
Types_D.NotificationCap ptr badge cap_rights_
|
||||||
| Structures_A.ReplyCap ptr is_master \<Rightarrow>
|
| Structures_A.ReplyCap ptr is_master cap_rights_ \<Rightarrow>
|
||||||
if is_master then Types_D.MasterReplyCap ptr else Types_D.ReplyCap ptr
|
if is_master then Types_D.MasterReplyCap ptr else Types_D.ReplyCap ptr cap_rights_
|
||||||
| Structures_A.CNodeCap ptr size_bits guard \<Rightarrow>
|
| Structures_A.CNodeCap ptr size_bits guard \<Rightarrow>
|
||||||
Types_D.CNodeCap ptr (of_bl guard) (length guard) size_bits
|
Types_D.CNodeCap ptr (of_bl guard) (length guard) size_bits
|
||||||
| Structures_A.ThreadCap ptr \<Rightarrow>
|
| Structures_A.ThreadCap ptr \<Rightarrow>
|
||||||
|
@ -707,16 +707,17 @@ definition
|
||||||
where
|
where
|
||||||
"infer_tcb_pending_op ptr t \<equiv>
|
"infer_tcb_pending_op ptr t \<equiv>
|
||||||
case t of
|
case t of
|
||||||
Structures_A.BlockedOnReceive ptr \<Rightarrow>
|
Structures_A.BlockedOnReceive ptr payload \<Rightarrow>
|
||||||
PendingSyncRecvCap ptr False
|
PendingSyncRecvCap ptr False (receiver_can_grant payload)
|
||||||
|
|
||||||
|Structures_A.BlockedOnReply \<Rightarrow>
|
| Structures_A.BlockedOnReply \<Rightarrow>
|
||||||
PendingSyncRecvCap ptr True
|
PendingSyncRecvCap ptr True False
|
||||||
|
|
||||||
| Structures_A.BlockedOnSend ptr payload \<Rightarrow>
|
| Structures_A.BlockedOnSend ptr payload \<Rightarrow>
|
||||||
PendingSyncSendCap ptr
|
PendingSyncSendCap ptr
|
||||||
(sender_badge payload) (sender_is_call payload)
|
(sender_badge payload) (sender_is_call payload)
|
||||||
(sender_can_grant payload) False
|
(sender_can_grant payload) (sender_can_grant_reply payload)
|
||||||
|
False
|
||||||
|
|
||||||
| Structures_A.BlockedOnNotification ptr \<Rightarrow>
|
| Structures_A.BlockedOnNotification ptr \<Rightarrow>
|
||||||
PendingNtfnRecvCap ptr
|
PendingNtfnRecvCap ptr
|
||||||
|
|
|
@ -30,15 +30,15 @@ where
|
||||||
Invocations_A.InvokeUntyped iu \<Rightarrow>
|
Invocations_A.InvokeUntyped iu \<Rightarrow>
|
||||||
Invocations_D.InvokeUntyped $
|
Invocations_D.InvokeUntyped $
|
||||||
translate_untyped_invocation iu
|
translate_untyped_invocation iu
|
||||||
| Invocations_A.InvokeEndpoint ep bdg grant \<Rightarrow>
|
| Invocations_A.InvokeEndpoint ep bdg grant grant_reply \<Rightarrow>
|
||||||
Invocations_D.InvokeEndpoint $
|
Invocations_D.InvokeEndpoint $
|
||||||
SyncMessage bdg grant ep
|
SyncMessage bdg grant grant_reply ep
|
||||||
| Invocations_A.InvokeNotification ntfn aebdg \<Rightarrow>
|
| Invocations_A.InvokeNotification ntfn aebdg \<Rightarrow>
|
||||||
Invocations_D.InvokeNotification $
|
Invocations_D.InvokeNotification $
|
||||||
Signal aebdg ntfn
|
Signal aebdg ntfn
|
||||||
| Invocations_A.InvokeReply target_tcb reply_slot \<Rightarrow>
|
| Invocations_A.InvokeReply target_tcb reply_slot grant \<Rightarrow>
|
||||||
Invocations_D.InvokeReply $
|
Invocations_D.InvokeReply $
|
||||||
ReplyMessage target_tcb (transform_cslot_ptr reply_slot)
|
ReplyMessage target_tcb (transform_cslot_ptr reply_slot) grant
|
||||||
| Invocations_A.InvokeCNode icn \<Rightarrow>
|
| Invocations_A.InvokeCNode icn \<Rightarrow>
|
||||||
Invocations_D.InvokeCNode $
|
Invocations_D.InvokeCNode $
|
||||||
translate_cnode_invocation icn
|
translate_cnode_invocation icn
|
||||||
|
@ -150,7 +150,7 @@ lemma decode_invocation_replycap_corres:
|
||||||
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
|
invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
|
||||||
invoked_cap = transform_cap invoked_cap';
|
invoked_cap = transform_cap invoked_cap';
|
||||||
excaps = transform_cap_list excaps';
|
excaps = transform_cap_list excaps';
|
||||||
invoked_cap' = cap.ReplyCap a b \<rbrakk> \<Longrightarrow>
|
invoked_cap' = cap.ReplyCap a b c \<rbrakk> \<Longrightarrow>
|
||||||
dcorres (dc \<oplus> cdl_invocation_relation) \<top> (cte_wp_at (Not\<circ> is_master_reply_cap) invoked_cap_ref' and cte_wp_at (diminished invoked_cap') invoked_cap_ref')
|
dcorres (dc \<oplus> cdl_invocation_relation) \<top> (cte_wp_at (Not\<circ> is_master_reply_cap) invoked_cap_ref' and cte_wp_at (diminished invoked_cap') invoked_cap_ref')
|
||||||
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
|
(Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
|
||||||
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
|
(Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')"
|
||||||
|
@ -702,7 +702,7 @@ lemma perform_invocation_corres:
|
||||||
apply (wp | clarsimp)+
|
apply (wp | clarsimp)+
|
||||||
|
|
||||||
(* invoke_reply *)
|
(* invoke_reply *)
|
||||||
apply (rename_tac word a b)
|
apply (rename_tac word a b c)
|
||||||
apply (clarsimp simp:invoke_reply_def)
|
apply (clarsimp simp:invoke_reply_def)
|
||||||
apply (rule corres_guard_imp)
|
apply (rule corres_guard_imp)
|
||||||
apply (rule corres_split[OF _ get_cur_thread_corres])
|
apply (rule corres_split[OF _ get_cur_thread_corres])
|
||||||
|
@ -718,7 +718,7 @@ lemma perform_invocation_corres:
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (drule (1) valid_reply_capsD)
|
apply (drule (1) valid_reply_capsD)
|
||||||
apply (clarsimp simp: valid_idle_def not_idle_thread_def pred_tcb_at_def obj_at_def)
|
apply (clarsimp simp: valid_idle_def not_idle_thread_def pred_tcb_at_def obj_at_def)
|
||||||
apply (fastforce simp: has_reply_cap_def)
|
apply (fastforce simp: has_reply_cap_def is_reply_cap_to_def)
|
||||||
|
|
||||||
(* invoke_tcb *)
|
(* invoke_tcb *)
|
||||||
apply (rule corres_guard_imp)
|
apply (rule corres_guard_imp)
|
||||||
|
@ -1355,6 +1355,7 @@ crunch cur_thread[wp]: complete_signal "\<lambda>s. P (cur_thread s)"
|
||||||
|
|
||||||
lemma receive_ipc_cur_thread:
|
lemma receive_ipc_cur_thread:
|
||||||
notes do_nbrecv_failed_transfer_def[simp]
|
notes do_nbrecv_failed_transfer_def[simp]
|
||||||
|
if_split[split del]
|
||||||
shows
|
shows
|
||||||
" \<lbrace>\<lambda>s. valid_objs s \<and> P (cur_thread (s :: det_ext state))\<rbrace> receive_ipc a b c \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>"
|
" \<lbrace>\<lambda>s. valid_objs s \<and> P (cur_thread (s :: det_ext state))\<rbrace> receive_ipc a b c \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>"
|
||||||
apply (simp add:receive_ipc_def bind_assoc)
|
apply (simp add:receive_ipc_def bind_assoc)
|
||||||
|
@ -1362,11 +1363,8 @@ lemma receive_ipc_cur_thread:
|
||||||
apply (simp add:setup_caller_cap_def)
|
apply (simp add:setup_caller_cap_def)
|
||||||
apply (wp dxo_wp_weak | simp)+
|
apply (wp dxo_wp_weak | simp)+
|
||||||
apply (rule_tac Q="\<lambda>r s. P (cur_thread s)" in hoare_strengthen_post)
|
apply (rule_tac Q="\<lambda>r s. P (cur_thread s)" in hoare_strengthen_post)
|
||||||
apply wp
|
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (wp|wpc)+
|
apply (wp|wpc)+
|
||||||
apply (rule_tac Q="\<lambda>r s. P (cur_thread s)" in hoare_strengthen_post)
|
|
||||||
apply wp
|
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (clarsimp simp:neq_Nil_conv)
|
apply (clarsimp simp:neq_Nil_conv)
|
||||||
apply (rename_tac list queue sender)
|
apply (rename_tac list queue sender)
|
||||||
|
@ -1419,7 +1417,8 @@ lemma handle_recv_corres:
|
||||||
apply (rule corres_alternate1)
|
apply (rule corres_alternate1)
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (rule corres_split[where r'=dc])
|
apply (rule corres_split[where r'=dc])
|
||||||
apply (rule_tac epptr=word1 in recv_sync_ipc_corres)
|
apply (rule_tac epptr=word1 in recv_sync_ipc_corres
|
||||||
|
[where ep_cap="cap.EndpointCap _ _ _", simplified])
|
||||||
apply (simp add: cap_ep_ptr_def delete_caller_cap_def)+
|
apply (simp add: cap_ep_ptr_def delete_caller_cap_def)+
|
||||||
apply (simp add: transform_tcb_slot_simp[symmetric])
|
apply (simp add: transform_tcb_slot_simp[symmetric])
|
||||||
apply (rule delete_cap_simple_corres)
|
apply (rule delete_cap_simple_corres)
|
||||||
|
@ -1495,7 +1494,7 @@ lemma handle_reply_corres:
|
||||||
in corres_split [OF _ get_cap_corres])
|
in corres_split [OF _ get_cap_corres])
|
||||||
apply (simp add: transform_cap_def corres_fail split: cap.split)
|
apply (simp add: transform_cap_def corres_fail split: cap.split)
|
||||||
apply (clarsimp simp: corres_fail dc_def[symmetric] split: bool.split)
|
apply (clarsimp simp: corres_fail dc_def[symmetric] split: bool.split)
|
||||||
apply (rename_tac word)
|
apply (rename_tac word rights)
|
||||||
apply (rule corres_guard_imp)
|
apply (rule corres_guard_imp)
|
||||||
apply (rule do_reply_transfer_corres)
|
apply (rule do_reply_transfer_corres)
|
||||||
apply (simp add: transform_tcb_slot_simp)
|
apply (simp add: transform_tcb_slot_simp)
|
||||||
|
@ -1505,8 +1504,10 @@ lemma handle_reply_corres:
|
||||||
apply (clarsimp simp:cte_wp_at_caps_of_state)
|
apply (clarsimp simp:cte_wp_at_caps_of_state)
|
||||||
apply (simp add:valid_cap_def)+
|
apply (simp add:valid_cap_def)+
|
||||||
apply (clarsimp simp:valid_state_def invs_def valid_reply_caps_def dest!:has_reply_cap_cte_wpD)
|
apply (clarsimp simp:valid_state_def invs_def valid_reply_caps_def dest!:has_reply_cap_cte_wpD)
|
||||||
apply (drule_tac x = word in spec,simp)
|
apply (drule_tac x = word in spec, simp add: cte_wp_at_def)
|
||||||
apply (clarsimp simp:not_idle_thread_def pred_tcb_at_def obj_at_def valid_idle_def)
|
apply (clarsimp simp:not_idle_thread_def pred_tcb_at_def obj_at_def valid_idle_def
|
||||||
|
cte_wp_at_def has_reply_cap_def is_reply_cap_to_def)
|
||||||
|
apply blast
|
||||||
apply (clarsimp simp: transform_tcb_slot_simp|(wp get_cap_wp)+)+
|
apply (clarsimp simp: transform_tcb_slot_simp|(wp get_cap_wp)+)+
|
||||||
apply (clarsimp simp:ct_in_state_def invs_def valid_state_def pred_tcb_at_def tcb_at_def obj_at_def)
|
apply (clarsimp simp:ct_in_state_def invs_def valid_state_def pred_tcb_at_def tcb_at_def obj_at_def)
|
||||||
done
|
done
|
||||||
|
|
|
@ -481,10 +481,11 @@ lemma dcorres_setup_reply_master:
|
||||||
apply (rule TrueI)
|
apply (rule TrueI)
|
||||||
apply (clarsimp simp: not_idle_thread_def)
|
apply (clarsimp simp: not_idle_thread_def)
|
||||||
apply (clarsimp simp:when_def is_master_reply_cap_def split:cap.split_asm)
|
apply (clarsimp simp:when_def is_master_reply_cap_def split:cap.split_asm)
|
||||||
|
apply (rename_tac rc_rights)
|
||||||
apply (subgoal_tac "opt_cap (obj_id,tcb_replycap_slot) (transform s')
|
apply (subgoal_tac "opt_cap (obj_id,tcb_replycap_slot) (transform s')
|
||||||
= Some (cdl_cap.MasterReplyCap obj_id)")
|
= Some (cdl_cap.MasterReplyCap obj_id)")
|
||||||
apply (clarsimp simp:corres_underlying_def set_cap_is_noop_opt_cap return_def)
|
apply (clarsimp simp:corres_underlying_def set_cap_is_noop_opt_cap return_def)
|
||||||
apply (subgoal_tac "cte_wp_at ((=) (cap.ReplyCap obj_id True))
|
apply (subgoal_tac "cte_wp_at ((=) (cap.ReplyCap obj_id True rc_rights))
|
||||||
(obj_id,tcb_cnode_index 2) s'")
|
(obj_id,tcb_cnode_index 2) s'")
|
||||||
apply (clarsimp dest!:iffD1[OF cte_wp_at_caps_of_state])
|
apply (clarsimp dest!:iffD1[OF cte_wp_at_caps_of_state])
|
||||||
apply (drule caps_of_state_transform_opt_cap)
|
apply (drule caps_of_state_transform_opt_cap)
|
||||||
|
|
|
@ -151,12 +151,12 @@ definition
|
||||||
where "cancel_ipc ptr \<equiv>
|
where "cancel_ipc ptr \<equiv>
|
||||||
do cap \<leftarrow> KHeap_D.get_cap (ptr,tcb_pending_op_slot);
|
do cap \<leftarrow> KHeap_D.get_cap (ptr,tcb_pending_op_slot);
|
||||||
(case cap of
|
(case cap of
|
||||||
PendingSyncRecvCap _ is_reply \<Rightarrow> ( do
|
PendingSyncRecvCap _ is_reply _ \<Rightarrow> ( do
|
||||||
when is_reply $ update_thread_fault ptr (\<lambda>x. False);
|
when is_reply $ update_thread_fault ptr (\<lambda>x. False);
|
||||||
revoke_cap_simple (ptr,tcb_replycap_slot);
|
revoke_cap_simple (ptr,tcb_replycap_slot);
|
||||||
when (\<not> is_reply) $ set_cap (ptr,tcb_pending_op_slot) NullCap
|
when (\<not> is_reply) $ set_cap (ptr,tcb_pending_op_slot) NullCap
|
||||||
od )
|
od )
|
||||||
| PendingSyncSendCap _ _ _ _ _ \<Rightarrow> (do
|
| PendingSyncSendCap _ _ _ _ _ _ \<Rightarrow> (do
|
||||||
revoke_cap_simple (ptr,tcb_replycap_slot);
|
revoke_cap_simple (ptr,tcb_replycap_slot);
|
||||||
set_cap (ptr,tcb_pending_op_slot) NullCap
|
set_cap (ptr,tcb_pending_op_slot) NullCap
|
||||||
od)
|
od)
|
||||||
|
@ -188,7 +188,7 @@ where
|
||||||
unbind_maybe_notification r;
|
unbind_maybe_notification r;
|
||||||
cancel_all_ipc r
|
cancel_all_ipc r
|
||||||
od)"
|
od)"
|
||||||
| "finalise_cap (ReplyCap r) final = return (NullCap, NullCap)"
|
| "finalise_cap (ReplyCap r R) final = return (NullCap, NullCap)"
|
||||||
| "finalise_cap (MasterReplyCap r) final = return (NullCap, NullCap)"
|
| "finalise_cap (MasterReplyCap r) final = return (NullCap, NullCap)"
|
||||||
| "finalise_cap (CNodeCap r bits g sz) final =
|
| "finalise_cap (CNodeCap r bits g sz) final =
|
||||||
(return (if final then ZombieCap r else NullCap, NullCap))"
|
(return (if final then ZombieCap r else NullCap, NullCap))"
|
||||||
|
@ -200,8 +200,8 @@ where
|
||||||
prepare_thread_delete r od);
|
prepare_thread_delete r od);
|
||||||
return (if final then (ZombieCap r) else NullCap, NullCap)
|
return (if final then (ZombieCap r) else NullCap, NullCap)
|
||||||
od)"
|
od)"
|
||||||
| "finalise_cap (PendingSyncSendCap r _ _ _ _) final = return (NullCap, NullCap)"
|
| "finalise_cap (PendingSyncSendCap r _ _ _ _ _) final = return (NullCap, NullCap)"
|
||||||
| "finalise_cap (PendingSyncRecvCap r _ ) final = return (NullCap, NullCap)"
|
| "finalise_cap (PendingSyncRecvCap r _ _) final = return (NullCap, NullCap)"
|
||||||
| "finalise_cap (PendingNtfnRecvCap r) final = return (NullCap, NullCap)"
|
| "finalise_cap (PendingNtfnRecvCap r) final = return (NullCap, NullCap)"
|
||||||
| "finalise_cap IrqControlCap final = return (NullCap, NullCap)"
|
| "finalise_cap IrqControlCap final = return (NullCap, NullCap)"
|
||||||
| "finalise_cap (IrqHandlerCap irq) final = (
|
| "finalise_cap (IrqHandlerCap irq) final = (
|
||||||
|
@ -436,7 +436,7 @@ definition
|
||||||
where
|
where
|
||||||
"get_tcb_ep_badge t \<equiv>
|
"get_tcb_ep_badge t \<equiv>
|
||||||
case (cdl_tcb_caps t tcb_pending_op_slot) of
|
case (cdl_tcb_caps t tcb_pending_op_slot) of
|
||||||
Some (PendingSyncSendCap _ badge _ _ _) \<Rightarrow> Some badge
|
Some (PendingSyncSendCap _ badge _ _ _ _) \<Rightarrow> Some badge
|
||||||
| _ \<Rightarrow> None"
|
| _ \<Rightarrow> None"
|
||||||
|
|
||||||
(*
|
(*
|
||||||
|
@ -658,7 +658,7 @@ definition
|
||||||
where
|
where
|
||||||
"derive_cap slot cap \<equiv> case cap of
|
"derive_cap slot cap \<equiv> case cap of
|
||||||
UntypedCap _ _ _ \<Rightarrow> doE ensure_no_children slot; returnOk cap odE
|
UntypedCap _ _ _ \<Rightarrow> doE ensure_no_children slot; returnOk cap odE
|
||||||
| ReplyCap _ \<Rightarrow> returnOk NullCap
|
| ReplyCap _ _ \<Rightarrow> returnOk NullCap
|
||||||
| MasterReplyCap oref \<Rightarrow> returnOk NullCap
|
| MasterReplyCap oref \<Rightarrow> returnOk NullCap
|
||||||
| IrqControlCap \<Rightarrow> returnOk NullCap
|
| IrqControlCap \<Rightarrow> returnOk NullCap
|
||||||
| ZombieCap _ \<Rightarrow> returnOk NullCap
|
| ZombieCap _ \<Rightarrow> returnOk NullCap
|
||||||
|
|
|
@ -120,7 +120,7 @@ where
|
||||||
* regardless of the user's actual intent. *)
|
* regardless of the user's actual intent. *)
|
||||||
EndpointCap o_id badge rights \<Rightarrow>
|
EndpointCap o_id badge rights \<Rightarrow>
|
||||||
(if Write \<in> rights then
|
(if Write \<in> rights then
|
||||||
returnOk $ InvokeEndpoint (SyncMessage badge (Grant \<in> rights) o_id)
|
returnOk $ InvokeEndpoint (SyncMessage badge (Grant \<in> rights) (GrantReply \<in> rights) o_id)
|
||||||
else
|
else
|
||||||
throw)
|
throw)
|
||||||
| NotificationCap o_id badge rights \<Rightarrow>
|
| NotificationCap o_id badge rights \<Rightarrow>
|
||||||
|
@ -128,8 +128,8 @@ where
|
||||||
returnOk $ InvokeNotification (Signal badge o_id)
|
returnOk $ InvokeNotification (Signal badge o_id)
|
||||||
else
|
else
|
||||||
throw)
|
throw)
|
||||||
| ReplyCap o_id\<Rightarrow>
|
| ReplyCap o_id rights \<Rightarrow>
|
||||||
returnOk $ InvokeReply (ReplyMessage o_id invoked_cap_ref)
|
returnOk $ InvokeReply (ReplyMessage o_id invoked_cap_ref (Grant \<in> rights))
|
||||||
|
|
||||||
(*
|
(*
|
||||||
* For other operations, we only perform the user's intent
|
* For other operations, we only perform the user's intent
|
||||||
|
|
|
@ -18,11 +18,14 @@ begin
|
||||||
|
|
||||||
(* Inject the reply cap into the target TCB *)
|
(* Inject the reply cap into the target TCB *)
|
||||||
definition
|
definition
|
||||||
inject_reply_cap :: "cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> unit k_monad"
|
inject_reply_cap :: "cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> bool \<Rightarrow> unit k_monad"
|
||||||
where
|
where
|
||||||
"inject_reply_cap src_tcb_id dst_tcb_id \<equiv> do
|
"inject_reply_cap src_tcb_id dst_tcb_id can_grant \<equiv> do
|
||||||
set_cap (src_tcb_id,tcb_pending_op_slot) $ cdl_cap.PendingSyncRecvCap src_tcb_id True;
|
set_cap (src_tcb_id, tcb_pending_op_slot) $
|
||||||
insert_cap_child (ReplyCap src_tcb_id) (src_tcb_id, tcb_replycap_slot) (dst_tcb_id, tcb_caller_slot);
|
cdl_cap.PendingSyncRecvCap src_tcb_id True False;
|
||||||
|
insert_cap_child (ReplyCap src_tcb_id (if can_grant then {Grant, Write} else {Write}))
|
||||||
|
(src_tcb_id, tcb_replycap_slot)
|
||||||
|
(dst_tcb_id, tcb_caller_slot);
|
||||||
return ()
|
return ()
|
||||||
od"
|
od"
|
||||||
|
|
||||||
|
@ -189,19 +192,19 @@ definition
|
||||||
get_waiting_sync_recv_threads :: "cdl_object_id \<Rightarrow> cdl_state \<Rightarrow> cdl_object_id set"
|
get_waiting_sync_recv_threads :: "cdl_object_id \<Rightarrow> cdl_state \<Rightarrow> cdl_object_id set"
|
||||||
where
|
where
|
||||||
"get_waiting_sync_recv_threads target state \<equiv>
|
"get_waiting_sync_recv_threads target state \<equiv>
|
||||||
{ x. \<exists>a. (cdl_objects state) x = Some (Tcb a) \<and>
|
{x. \<exists>a. (cdl_objects state) x = Some (Tcb a) \<and>
|
||||||
(((cdl_tcb_caps a) tcb_pending_op_slot) = Some (PendingSyncRecvCap target False)) }"
|
(\<exists>can_grant. (cdl_tcb_caps a) tcb_pending_op_slot = Some (PendingSyncRecvCap target False can_grant)) }"
|
||||||
|
|
||||||
(*
|
(*
|
||||||
* Get the set of threads waiting to send to the given sync endpoint.
|
* Get the set of threads waiting to send to the given sync endpoint.
|
||||||
* Return a tuple of (thread, is_call, can_grant).
|
|
||||||
*)
|
*)
|
||||||
definition
|
definition
|
||||||
get_waiting_sync_send_threads :: "cdl_object_id \<Rightarrow> cdl_state \<Rightarrow> cdl_object_id set"
|
get_waiting_sync_send_threads :: "cdl_object_id \<Rightarrow> cdl_state \<Rightarrow> cdl_object_id set"
|
||||||
where
|
where
|
||||||
"get_waiting_sync_send_threads target state \<equiv>
|
"get_waiting_sync_send_threads target state \<equiv>
|
||||||
{x. \<exists> rights grant call a b. (cdl_objects state) x = Some (Tcb a) \<and>
|
{t. \<exists>fault a b. (cdl_objects state) t = Some (Tcb a) \<and>
|
||||||
(((cdl_tcb_caps a) tcb_pending_op_slot) = Some (PendingSyncSendCap target b call grant rights)) }"
|
(\<exists>call can_grant can_grant_reply. (cdl_tcb_caps a) tcb_pending_op_slot =
|
||||||
|
Some (PendingSyncSendCap target b call can_grant can_grant_reply fault)) }"
|
||||||
|
|
||||||
(*
|
(*
|
||||||
* Get the set of threads which are bound to the given ntfn, but are
|
* Get the set of threads which are bound to the given ntfn, but are
|
||||||
|
@ -212,8 +215,8 @@ definition
|
||||||
where
|
where
|
||||||
"get_waiting_sync_bound_ntfn_threads ntfn_id state \<equiv>
|
"get_waiting_sync_bound_ntfn_threads ntfn_id state \<equiv>
|
||||||
{x. \<exists>a ep_id. (cdl_objects state) x = Some (Tcb a) \<and>
|
{x. \<exists>a ep_id. (cdl_objects state) x = Some (Tcb a) \<and>
|
||||||
(((cdl_tcb_caps a) tcb_pending_op_slot) = Some (PendingSyncRecvCap ep_id False)) \<and>
|
(\<exists>can_grant. (cdl_tcb_caps a) tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and>
|
||||||
(((cdl_tcb_caps a) tcb_boundntfn_slot) = Some (BoundNotificationCap ntfn_id))}"
|
((cdl_tcb_caps a) tcb_boundntfn_slot = Some (BoundNotificationCap ntfn_id))}"
|
||||||
|
|
||||||
(*
|
(*
|
||||||
* Mark a thread blocked on IPC.
|
* Mark a thread blocked on IPC.
|
||||||
|
@ -264,30 +267,26 @@ where
|
||||||
(*
|
(*
|
||||||
* Transfer a message from "sender" to "receiver" using a reply capability.
|
* Transfer a message from "sender" to "receiver" using a reply capability.
|
||||||
*
|
*
|
||||||
* A reply capability always gives the sender the right to grant caps
|
* The sender may have the right to grant caps over the channel.
|
||||||
* over the channel. As the original sender must have had grant rights
|
|
||||||
* to establish the reply cap to begin with (and hence could have
|
|
||||||
* granted the other side a return communication path), this does not
|
|
||||||
* increase any rights.
|
|
||||||
*
|
*
|
||||||
* If a fault is pending in the receiver, the fault is transferred.
|
* If a fault is pending in the receiver, the fault is transferred.
|
||||||
*)
|
*)
|
||||||
|
|
||||||
definition
|
definition
|
||||||
do_reply_transfer :: "cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> cdl_cap_ref \<Rightarrow> unit k_monad"
|
do_reply_transfer :: "cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> cdl_cap_ref \<Rightarrow> bool \<Rightarrow> unit k_monad"
|
||||||
where
|
where
|
||||||
"do_reply_transfer sender_id receiver_id reply_cap_slot \<equiv>
|
"do_reply_transfer sender_id receiver_id reply_cap_slot can_grant \<equiv>
|
||||||
do
|
do
|
||||||
has_fault \<leftarrow> get_thread_fault receiver_id;
|
has_fault \<leftarrow> get_thread_fault receiver_id;
|
||||||
when (\<not> has_fault) $ do_ipc_transfer None sender_id receiver_id True;
|
when (\<not> has_fault) $ do_ipc_transfer None sender_id receiver_id can_grant;
|
||||||
(* Clear out any pending operation caps. *)
|
(* Clear out any pending operation caps. *)
|
||||||
delete_cap_simple reply_cap_slot;
|
delete_cap_simple reply_cap_slot;
|
||||||
when (has_fault) $ (do corrupt_tcb_intent receiver_id;
|
when (has_fault) $ (do corrupt_tcb_intent receiver_id;
|
||||||
update_thread_fault receiver_id (\<lambda>_. False) od );
|
update_thread_fault receiver_id (\<lambda>_. False) od );
|
||||||
if ( \<not> has_fault) then set_cap (receiver_id,tcb_pending_op_slot) RunningCap
|
if ( \<not> has_fault) then set_cap (receiver_id, tcb_pending_op_slot) RunningCap
|
||||||
else
|
else
|
||||||
(set_cap (receiver_id,tcb_pending_op_slot) NullCap
|
(set_cap (receiver_id,tcb_pending_op_slot) NullCap
|
||||||
\<sqinter> set_cap (receiver_id,tcb_pending_op_slot) RestartCap )
|
\<sqinter> set_cap (receiver_id,tcb_pending_op_slot) RestartCap)
|
||||||
od"
|
od"
|
||||||
|
|
||||||
(* Wake-up a thread waiting on an notification. *)
|
(* Wake-up a thread waiting on an notification. *)
|
||||||
|
@ -349,9 +348,9 @@ where
|
||||||
* them up. Otherwise, we put the sender to sleep.
|
* them up. Otherwise, we put the sender to sleep.
|
||||||
*)
|
*)
|
||||||
definition
|
definition
|
||||||
send_ipc :: "bool \<Rightarrow> bool \<Rightarrow> cdl_badge \<Rightarrow> bool \<Rightarrow> cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> unit k_monad"
|
send_ipc :: "bool \<Rightarrow> bool \<Rightarrow> cdl_badge \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> unit k_monad"
|
||||||
where
|
where
|
||||||
"send_ipc block call badge can_grant tcb_id_sender ep_id \<equiv>
|
"send_ipc block call badge can_grant can_grant_reply tcb_id_sender ep_id \<equiv>
|
||||||
do
|
do
|
||||||
waiters \<leftarrow> gets $ get_waiting_sync_recv_threads ep_id;
|
waiters \<leftarrow> gets $ get_waiting_sync_recv_threads ep_id;
|
||||||
t \<leftarrow> option_select waiters;
|
t \<leftarrow> option_select waiters;
|
||||||
|
@ -359,14 +358,23 @@ where
|
||||||
None \<Rightarrow>
|
None \<Rightarrow>
|
||||||
if block then
|
if block then
|
||||||
block_thread_on_ipc tcb_id_sender
|
block_thread_on_ipc tcb_id_sender
|
||||||
(PendingSyncSendCap ep_id badge call can_grant False)
|
(PendingSyncSendCap ep_id badge call can_grant can_grant_reply False)
|
||||||
else
|
else
|
||||||
return ()
|
return ()
|
||||||
| Some tcb_id_receiver \<Rightarrow> do
|
| Some tcb_id_receiver \<Rightarrow> do
|
||||||
|
\<comment> \<open>liftM instead of bind+return avoids early unfolding in send_ipc_corres\<close>
|
||||||
|
recv_state \<leftarrow> liftM (\<lambda>tcb. the (cdl_tcb_caps tcb tcb_pending_op_slot)) $
|
||||||
|
get_thread tcb_id_receiver;
|
||||||
|
reply_can_grant \<leftarrow>
|
||||||
|
(case recv_state of
|
||||||
|
PendingSyncRecvCap target False receiver_grant \<Rightarrow> do
|
||||||
do_ipc_transfer (Some ep_id) tcb_id_sender tcb_id_receiver can_grant;
|
do_ipc_transfer (Some ep_id) tcb_id_sender tcb_id_receiver can_grant;
|
||||||
|
return receiver_grant od
|
||||||
|
| _ \<Rightarrow> fail);
|
||||||
set_cap (tcb_id_receiver,tcb_pending_op_slot) RunningCap;
|
set_cap (tcb_id_receiver,tcb_pending_op_slot) RunningCap;
|
||||||
(when (can_grant) $ (inject_reply_cap tcb_id_sender tcb_id_receiver)) \<sqinter>
|
(when (can_grant \<or> can_grant_reply) $
|
||||||
set_cap (tcb_id_sender,tcb_pending_op_slot) NullCap \<sqinter> return ()
|
(inject_reply_cap tcb_id_sender tcb_id_receiver reply_can_grant))
|
||||||
|
\<sqinter> set_cap (tcb_id_sender,tcb_pending_op_slot) NullCap \<sqinter> return ()
|
||||||
od
|
od
|
||||||
od"
|
od"
|
||||||
|
|
||||||
|
@ -375,24 +383,25 @@ where
|
||||||
* wake them up. Otherwise, we put the receiver to sleep.
|
* wake them up. Otherwise, we put the receiver to sleep.
|
||||||
*)
|
*)
|
||||||
definition
|
definition
|
||||||
receive_sync :: "cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> unit k_monad"
|
receive_sync :: "cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> bool \<Rightarrow> unit k_monad"
|
||||||
where
|
where
|
||||||
"receive_sync thread ep_id \<equiv> do
|
"receive_sync thread ep_id receiver_can_grant \<equiv> do
|
||||||
waiters \<leftarrow> gets $ get_waiting_sync_send_threads ep_id;
|
waiters \<leftarrow> gets $ get_waiting_sync_send_threads ep_id;
|
||||||
t \<leftarrow> option_select waiters;
|
waiter \<leftarrow> option_select waiters;
|
||||||
(case t of
|
(case waiter of
|
||||||
None \<Rightarrow>
|
None \<Rightarrow>
|
||||||
block_thread_on_ipc thread (PendingSyncRecvCap ep_id False) \<sqinter> corrupt_tcb_intent thread
|
block_thread_on_ipc thread (PendingSyncRecvCap ep_id False receiver_can_grant)
|
||||||
|
\<sqinter> corrupt_tcb_intent thread
|
||||||
| Some tcb_id_sender \<Rightarrow> (do
|
| Some tcb_id_sender \<Rightarrow> (do
|
||||||
tcb \<leftarrow> get_thread tcb_id_sender;
|
tcb \<leftarrow> get_thread tcb_id_sender;
|
||||||
case ((cdl_tcb_caps tcb) tcb_pending_op_slot) of
|
case ((cdl_tcb_caps tcb) tcb_pending_op_slot) of
|
||||||
Some (PendingSyncSendCap target _ call grant rights)\<Rightarrow>(do
|
Some (PendingSyncSendCap target _ call can_grant can_grant_reply fault) \<Rightarrow> (do
|
||||||
do_ipc_transfer (Some ep_id) tcb_id_sender thread grant;
|
do_ipc_transfer (Some ep_id) tcb_id_sender thread can_grant;
|
||||||
(when (grant) $ (inject_reply_cap tcb_id_sender thread)) \<sqinter>
|
(when (can_grant \<or> can_grant_reply) $
|
||||||
set_cap (tcb_id_sender,tcb_pending_op_slot) RunningCap \<sqinter>
|
(inject_reply_cap tcb_id_sender thread receiver_can_grant)) \<sqinter>
|
||||||
|
set_cap (tcb_id_sender, tcb_pending_op_slot) RunningCap \<sqinter>
|
||||||
set_cap (tcb_id_sender, tcb_pending_op_slot) NullCap
|
set_cap (tcb_id_sender, tcb_pending_op_slot) NullCap
|
||||||
od)
|
od)
|
||||||
|
|
||||||
od)
|
od)
|
||||||
)
|
)
|
||||||
od"
|
od"
|
||||||
|
@ -400,17 +409,17 @@ where
|
||||||
(* This is more nonderministic than is really required, but
|
(* This is more nonderministic than is really required, but
|
||||||
it makes the refinement proofs much easier *)
|
it makes the refinement proofs much easier *)
|
||||||
definition
|
definition
|
||||||
receive_ipc :: "cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> unit k_monad"
|
receive_ipc :: "cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> bool \<Rightarrow> unit k_monad"
|
||||||
where
|
where
|
||||||
"receive_ipc thread ep_id \<equiv> corrupt_tcb_intent thread \<sqinter> receive_sync thread ep_id"
|
"receive_ipc thread ep_id can_grant \<equiv> corrupt_tcb_intent thread \<sqinter> receive_sync thread ep_id can_grant"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
invoke_endpoint :: "bool \<Rightarrow> bool \<Rightarrow> cdl_endpoint_invocation \<Rightarrow> unit k_monad"
|
invoke_endpoint :: "bool \<Rightarrow> bool \<Rightarrow> cdl_endpoint_invocation \<Rightarrow> unit k_monad"
|
||||||
where
|
where
|
||||||
"invoke_endpoint is_call can_block params \<equiv> case params of
|
"invoke_endpoint is_call can_block params \<equiv> case params of
|
||||||
SyncMessage badge can_grant ep_id \<Rightarrow> do
|
SyncMessage badge can_grant can_grant_reply ep_id \<Rightarrow> do
|
||||||
thread \<leftarrow> gets_the cdl_current_thread;
|
thread \<leftarrow> gets_the cdl_current_thread;
|
||||||
send_ipc can_block is_call badge can_grant thread ep_id
|
send_ipc can_block is_call badge can_grant can_grant_reply thread ep_id
|
||||||
od"
|
od"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
|
@ -424,9 +433,9 @@ definition
|
||||||
invoke_reply :: "cdl_reply_invocation \<Rightarrow> unit k_monad"
|
invoke_reply :: "cdl_reply_invocation \<Rightarrow> unit k_monad"
|
||||||
where
|
where
|
||||||
"invoke_reply params \<equiv> case params of
|
"invoke_reply params \<equiv> case params of
|
||||||
ReplyMessage recv reply_cap_ref \<Rightarrow> do
|
ReplyMessage recv reply_cap_ref rights \<Rightarrow> do
|
||||||
send \<leftarrow> gets_the cdl_current_thread;
|
send \<leftarrow> gets_the cdl_current_thread;
|
||||||
do_reply_transfer send recv reply_cap_ref
|
do_reply_transfer send recv reply_cap_ref rights
|
||||||
od"
|
od"
|
||||||
|
|
||||||
|
|
||||||
|
@ -444,10 +453,10 @@ definition
|
||||||
handler_cap \<leftarrow> lookup_cap tcb_id target_ep_cptr;
|
handler_cap \<leftarrow> lookup_cap tcb_id target_ep_cptr;
|
||||||
(case handler_cap of
|
(case handler_cap of
|
||||||
EndpointCap ref badge rights \<Rightarrow>
|
EndpointCap ref badge rights \<Rightarrow>
|
||||||
if Write \<in> rights \<and> Grant \<in> rights then
|
if Write \<in> rights \<and> (Grant \<in> rights \<or> GrantReply \<in> rights) then
|
||||||
liftE $ do
|
liftE $ do
|
||||||
update_thread_fault tcb_id (\<lambda>_. True);
|
update_thread_fault tcb_id (\<lambda>_. True);
|
||||||
send_ipc True False badge True tcb_id ref
|
send_ipc True True badge (Grant \<in> rights) True tcb_id ref
|
||||||
od
|
od
|
||||||
else
|
else
|
||||||
throw
|
throw
|
||||||
|
|
|
@ -50,6 +50,9 @@ abbreviation (input) Write::rights
|
||||||
abbreviation (input) Grant::rights
|
abbreviation (input) Grant::rights
|
||||||
where "Grant \<equiv> AllowGrant"
|
where "Grant \<equiv> AllowGrant"
|
||||||
|
|
||||||
|
abbreviation (input) GrantReply::rights
|
||||||
|
where "GrantReply \<equiv> AllowGrantReply"
|
||||||
|
|
||||||
(* Capability data, such as guard information. *)
|
(* Capability data, such as guard information. *)
|
||||||
type_synonym cdl_raw_capdata = word32
|
type_synonym cdl_raw_capdata = word32
|
||||||
|
|
||||||
|
@ -183,6 +186,7 @@ datatype cdl_asid_pool_intent =
|
||||||
datatype cdl_notification_intent =
|
datatype cdl_notification_intent =
|
||||||
SendSignalIntent word32
|
SendSignalIntent word32
|
||||||
|
|
||||||
|
(* Also used with reply caps *)
|
||||||
datatype cdl_endpoint_intent =
|
datatype cdl_endpoint_intent =
|
||||||
SendMessageIntent "cdl_cptr list"
|
SendMessageIntent "cdl_cptr list"
|
||||||
|
|
||||||
|
|
|
@ -52,17 +52,17 @@ datatype cdl_irq_handler_invocation =
|
||||||
| ClearIrqHandler cdl_irq
|
| ClearIrqHandler cdl_irq
|
||||||
|
|
||||||
datatype cdl_endpoint_invocation =
|
datatype cdl_endpoint_invocation =
|
||||||
(* badge, grant, ep *)
|
(* We need not track the "block" or "call" bits because they
|
||||||
(* Invoking an endpoint is always a blocking, non-call operation,
|
are handled separately in the top-level syscall interface. *)
|
||||||
* so we need not track the "block" or "call" bits. *)
|
(* badge, grant, grant reply, ep *)
|
||||||
SyncMessage cdl_badge bool cdl_object_id
|
SyncMessage cdl_badge bool bool cdl_object_id
|
||||||
|
|
||||||
datatype cdl_notification_invocation =
|
datatype cdl_notification_invocation =
|
||||||
(* badge (notification word) and notification object *)
|
(* badge (notification word) and notification object *)
|
||||||
Signal cdl_badge cdl_object_id
|
Signal cdl_badge cdl_object_id
|
||||||
|
|
||||||
datatype cdl_reply_invocation =
|
datatype cdl_reply_invocation =
|
||||||
ReplyMessage cdl_object_id cdl_cap_ref
|
ReplyMessage cdl_object_id cdl_cap_ref bool (* can grant *)
|
||||||
|
|
||||||
datatype cdl_page_table_invocation =
|
datatype cdl_page_table_invocation =
|
||||||
(* PageTableMap <real_pt_cap> <pt_cap> <pt_cap_ref> <pd_target_slot> *)
|
(* PageTableMap <real_pt_cap> <pt_cap> <pt_cap_ref> <pd_target_slot> *)
|
||||||
|
|
|
@ -41,8 +41,8 @@ definition
|
||||||
where
|
where
|
||||||
"is_thread_blocked_on_endpoint t ep \<equiv>
|
"is_thread_blocked_on_endpoint t ep \<equiv>
|
||||||
case (cdl_tcb_caps t tcb_pending_op_slot) of
|
case (cdl_tcb_caps t tcb_pending_op_slot) of
|
||||||
Some (PendingSyncSendCap p _ _ _ _) \<Rightarrow> p = ep
|
Some (PendingSyncSendCap p _ _ _ _ _) \<Rightarrow> p = ep
|
||||||
| Some (PendingSyncRecvCap p is_reply ) \<Rightarrow> p = ep \<and> \<not> is_reply
|
| Some (PendingSyncRecvCap p is_reply _) \<Rightarrow> p = ep \<and> \<not> is_reply
|
||||||
| Some (PendingNtfnRecvCap p) \<Rightarrow> p = ep
|
| Some (PendingNtfnRecvCap p) \<Rightarrow> p = ep
|
||||||
| _ \<Rightarrow> False"
|
| _ \<Rightarrow> False"
|
||||||
|
|
||||||
|
@ -113,15 +113,15 @@ where
|
||||||
|
|
||||||
definition
|
definition
|
||||||
can_fast_finalise :: "cdl_cap \<Rightarrow> bool" where
|
can_fast_finalise :: "cdl_cap \<Rightarrow> bool" where
|
||||||
"can_fast_finalise cap \<equiv> case cap of ReplyCap r \<Rightarrow> True
|
"can_fast_finalise cap \<equiv> case cap of ReplyCap r R \<Rightarrow> True
|
||||||
| MasterReplyCap r \<Rightarrow> True
|
| MasterReplyCap r \<Rightarrow> True
|
||||||
| EndpointCap r b R \<Rightarrow> True
|
| EndpointCap r b R \<Rightarrow> True
|
||||||
| NotificationCap r b R \<Rightarrow> True
|
| NotificationCap r b R \<Rightarrow> True
|
||||||
| NullCap \<Rightarrow> True
|
| NullCap \<Rightarrow> True
|
||||||
| RestartCap \<Rightarrow> True
|
| RestartCap \<Rightarrow> True
|
||||||
| RunningCap \<Rightarrow> True
|
| RunningCap \<Rightarrow> True
|
||||||
| PendingSyncSendCap r _ _ _ _ \<Rightarrow> True
|
| PendingSyncSendCap r _ _ _ _ _ \<Rightarrow> True
|
||||||
| PendingSyncRecvCap r _ \<Rightarrow> True
|
| PendingSyncRecvCap r _ _ \<Rightarrow> True
|
||||||
| PendingNtfnRecvCap r \<Rightarrow> True
|
| PendingNtfnRecvCap r \<Rightarrow> True
|
||||||
| DomainCap \<Rightarrow> True
|
| DomainCap \<Rightarrow> True
|
||||||
| PageDirectoryCap _ x _ \<Rightarrow> \<not>(x = Real)
|
| PageDirectoryCap _ x _ \<Rightarrow> \<not>(x = Real)
|
||||||
|
@ -139,7 +139,7 @@ where
|
||||||
"fast_finalise NullCap final = return ()"
|
"fast_finalise NullCap final = return ()"
|
||||||
| "fast_finalise (RestartCap) final = return ()"
|
| "fast_finalise (RestartCap) final = return ()"
|
||||||
| "fast_finalise (RunningCap) final = return ()"
|
| "fast_finalise (RunningCap) final = return ()"
|
||||||
| "fast_finalise (ReplyCap r) final = return ()"
|
| "fast_finalise (ReplyCap r R) final = return ()"
|
||||||
| "fast_finalise (MasterReplyCap r) final = return ()"
|
| "fast_finalise (MasterReplyCap r) final = return ()"
|
||||||
| "fast_finalise (EndpointCap r b R) final =
|
| "fast_finalise (EndpointCap r b R) final =
|
||||||
(when final $ cancel_all_ipc r)"
|
(when final $ cancel_all_ipc r)"
|
||||||
|
@ -148,8 +148,8 @@ where
|
||||||
unbind_maybe_notification r;
|
unbind_maybe_notification r;
|
||||||
cancel_all_ipc r
|
cancel_all_ipc r
|
||||||
od)"
|
od)"
|
||||||
| "fast_finalise (PendingSyncSendCap r _ _ _ _) final = return()"
|
| "fast_finalise (PendingSyncSendCap r _ _ _ _ _) final = return()"
|
||||||
| "fast_finalise (PendingSyncRecvCap r _) final = return()"
|
| "fast_finalise (PendingSyncRecvCap r _ _) final = return()"
|
||||||
| "fast_finalise (PendingNtfnRecvCap r) final = return()"
|
| "fast_finalise (PendingNtfnRecvCap r) final = return()"
|
||||||
| "fast_finalise DomainCap final = return ()"
|
| "fast_finalise DomainCap final = return ()"
|
||||||
| "fast_finalise (PageDirectoryCap _ x _) _ = (if x = Real then fail else return())"
|
| "fast_finalise (PageDirectoryCap _ x _) _ = (if x = Real then fail else return())"
|
||||||
|
@ -165,12 +165,12 @@ definition
|
||||||
"cap_counts cap \<equiv> (case cap of
|
"cap_counts cap \<equiv> (case cap of
|
||||||
cdl_cap.NullCap \<Rightarrow> False
|
cdl_cap.NullCap \<Rightarrow> False
|
||||||
| UntypedCap _ _ _ \<Rightarrow> False
|
| UntypedCap _ _ _ \<Rightarrow> False
|
||||||
| ReplyCap _ \<Rightarrow> False
|
| ReplyCap _ _ \<Rightarrow> False
|
||||||
| MasterReplyCap _ \<Rightarrow> False
|
| MasterReplyCap _ \<Rightarrow> False
|
||||||
| RestartCap \<Rightarrow> False
|
| RestartCap \<Rightarrow> False
|
||||||
| RunningCap \<Rightarrow> False
|
| RunningCap \<Rightarrow> False
|
||||||
| PendingSyncSendCap _ _ _ _ _ \<Rightarrow> False
|
| PendingSyncSendCap _ _ _ _ _ _ \<Rightarrow> False
|
||||||
| PendingSyncRecvCap _ _ \<Rightarrow> False
|
| PendingSyncRecvCap _ _ _ \<Rightarrow> False
|
||||||
| PendingNtfnRecvCap _ \<Rightarrow> False
|
| PendingNtfnRecvCap _ \<Rightarrow> False
|
||||||
| DomainCap \<Rightarrow> False
|
| DomainCap \<Rightarrow> False
|
||||||
| BoundNotificationCap _ \<Rightarrow> False
|
| BoundNotificationCap _ \<Rightarrow> False
|
||||||
|
|
|
@ -87,7 +87,7 @@ definition ep_related_cap :: "cdl_cap \<Rightarrow> bool"
|
||||||
where "ep_related_cap cap \<equiv> case cap of
|
where "ep_related_cap cap \<equiv> case cap of
|
||||||
cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True
|
cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True
|
||||||
| cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True
|
| cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True
|
||||||
| cdl_cap.ReplyCap o_id \<Rightarrow> True
|
| cdl_cap.ReplyCap o_id rights \<Rightarrow> True
|
||||||
| _ \<Rightarrow> False"
|
| _ \<Rightarrow> False"
|
||||||
|
|
||||||
definition "has_restart_cap \<equiv> \<lambda>tcb_id. do
|
definition "has_restart_cap \<equiv> \<lambda>tcb_id. do
|
||||||
|
@ -163,7 +163,7 @@ where
|
||||||
if Read \<in> rights then
|
if Read \<in> rights then
|
||||||
(liftE $ do
|
(liftE $ do
|
||||||
delete_cap_simple (tcb_id, tcb_caller_slot);
|
delete_cap_simple (tcb_id, tcb_caller_slot);
|
||||||
receive_ipc tcb_id (cap_object ep_cap)
|
receive_ipc tcb_id (cap_object ep_cap) (Grant \<in> rights)
|
||||||
od) \<sqinter> throw
|
od) \<sqinter> throw
|
||||||
else
|
else
|
||||||
throw
|
throw
|
||||||
|
@ -189,7 +189,7 @@ where
|
||||||
caller_cap \<leftarrow> get_cap (tcb_id, tcb_caller_slot);
|
caller_cap \<leftarrow> get_cap (tcb_id, tcb_caller_slot);
|
||||||
|
|
||||||
case caller_cap of
|
case caller_cap of
|
||||||
ReplyCap target \<Rightarrow> do_reply_transfer tcb_id target (tcb_id, tcb_caller_slot)
|
ReplyCap target rights \<Rightarrow> do_reply_transfer tcb_id target (tcb_id, tcb_caller_slot) (Grant \<in> rights)
|
||||||
| NullCap \<Rightarrow> return ()
|
| NullCap \<Rightarrow> return ()
|
||||||
| _ \<Rightarrow> fail
|
| _ \<Rightarrow> fail
|
||||||
od
|
od
|
||||||
|
|
|
@ -93,7 +93,7 @@ datatype cdl_cap =
|
||||||
| UntypedCap bool cdl_object_set cdl_object_set
|
| UntypedCap bool cdl_object_set cdl_object_set
|
||||||
| EndpointCap cdl_object_id cdl_badge "cdl_right set"
|
| EndpointCap cdl_object_id cdl_badge "cdl_right set"
|
||||||
| NotificationCap cdl_object_id cdl_badge "cdl_right set"
|
| NotificationCap cdl_object_id cdl_badge "cdl_right set"
|
||||||
| ReplyCap cdl_object_id (* The id of the tcb of the target thread *)
|
| ReplyCap cdl_object_id "cdl_right set" (* The id of the tcb of the target thread *)
|
||||||
| MasterReplyCap cdl_object_id
|
| MasterReplyCap cdl_object_id
|
||||||
| CNodeCap cdl_object_id cdl_cap_guard cdl_cap_guard_size cdl_size_bits
|
| CNodeCap cdl_object_id cdl_cap_guard cdl_cap_guard_size cdl_size_bits
|
||||||
| TcbCap cdl_object_id
|
| TcbCap cdl_object_id
|
||||||
|
@ -101,17 +101,11 @@ datatype cdl_cap =
|
||||||
|
|
||||||
(*
|
(*
|
||||||
* Capabilities representing threads waiting in endpoint queues.
|
* Capabilities representing threads waiting in endpoint queues.
|
||||||
*
|
|
||||||
* The PendingSyncSendCap has booleans indicating if the pending
|
|
||||||
* send is a call, if it has grant rights, and if the send is a
|
|
||||||
* fault IPC respectively.
|
|
||||||
*)
|
*)
|
||||||
| PendingSyncSendCap cdl_object_id cdl_badge bool bool bool
|
(* thread, badge, is call, can grant, can grant reply, is fault ipc *)
|
||||||
|
| PendingSyncSendCap cdl_object_id cdl_badge bool bool bool bool
|
||||||
(* The PendingSyncRecvCap has booleans indicating if
|
(* thread, is waiting for reply, can grant *)
|
||||||
it is waiting for a reply or not
|
| PendingSyncRecvCap cdl_object_id bool bool
|
||||||
*)
|
|
||||||
| PendingSyncRecvCap cdl_object_id bool
|
|
||||||
| PendingNtfnRecvCap cdl_object_id
|
| PendingNtfnRecvCap cdl_object_id
|
||||||
|
|
||||||
(* Indicate that the thread is ready for Reschedule *)
|
(* Indicate that the thread is ready for Reschedule *)
|
||||||
|
@ -328,13 +322,13 @@ where
|
||||||
| "cap_objects (TcbCap x) = {x}"
|
| "cap_objects (TcbCap x) = {x}"
|
||||||
| "cap_objects (CNodeCap x _ _ _) = {x}"
|
| "cap_objects (CNodeCap x _ _ _) = {x}"
|
||||||
| "cap_objects (MasterReplyCap x) = {x}"
|
| "cap_objects (MasterReplyCap x) = {x}"
|
||||||
| "cap_objects (ReplyCap x) = {x}"
|
| "cap_objects (ReplyCap x _) = {x}"
|
||||||
| "cap_objects (NotificationCap x _ _) = {x}"
|
| "cap_objects (NotificationCap x _ _) = {x}"
|
||||||
| "cap_objects (EndpointCap x _ _) = {x}"
|
| "cap_objects (EndpointCap x _ _) = {x}"
|
||||||
| "cap_objects (UntypedCap _ x a) = x"
|
| "cap_objects (UntypedCap _ x a) = x"
|
||||||
| "cap_objects (ZombieCap x) = {x}"
|
| "cap_objects (ZombieCap x) = {x}"
|
||||||
| "cap_objects (PendingSyncSendCap x _ _ _ _) = {x}"
|
| "cap_objects (PendingSyncSendCap x _ _ _ _ _) = {x}"
|
||||||
| "cap_objects (PendingSyncRecvCap x _ ) = {x}"
|
| "cap_objects (PendingSyncRecvCap x _ _) = {x}"
|
||||||
| "cap_objects (PendingNtfnRecvCap x) = {x}"
|
| "cap_objects (PendingNtfnRecvCap x) = {x}"
|
||||||
| "cap_objects (BoundNotificationCap x) = {x}"
|
| "cap_objects (BoundNotificationCap x) = {x}"
|
||||||
|
|
||||||
|
@ -371,12 +365,12 @@ lemma cap_object_simps:
|
||||||
"cap_object (TcbCap x) = x"
|
"cap_object (TcbCap x) = x"
|
||||||
"cap_object (CNodeCap x k l sz) = x"
|
"cap_object (CNodeCap x k l sz) = x"
|
||||||
"cap_object (MasterReplyCap x) = x"
|
"cap_object (MasterReplyCap x) = x"
|
||||||
"cap_object (ReplyCap x) = x"
|
"cap_object (ReplyCap x q) = x"
|
||||||
"cap_object (NotificationCap x m n) = x"
|
"cap_object (NotificationCap x m n) = x"
|
||||||
"cap_object (EndpointCap x p q) = x"
|
"cap_object (EndpointCap x p q) = x"
|
||||||
"cap_object (ZombieCap x) = x"
|
"cap_object (ZombieCap x) = x"
|
||||||
"cap_object (PendingSyncSendCap x s t u v) = x"
|
"cap_object (PendingSyncSendCap x s t u v w) = x"
|
||||||
"cap_object (PendingSyncRecvCap x t) = x"
|
"cap_object (PendingSyncRecvCap x t u) = x"
|
||||||
"cap_object (PendingNtfnRecvCap x) = x"
|
"cap_object (PendingNtfnRecvCap x) = x"
|
||||||
"cap_object (BoundNotificationCap x) = x"
|
"cap_object (BoundNotificationCap x) = x"
|
||||||
by (simp_all add:cap_object_def Nitpick.The_psimp cap_has_object_def)
|
by (simp_all add:cap_object_def Nitpick.The_psimp cap_has_object_def)
|
||||||
|
@ -395,7 +389,7 @@ where
|
||||||
| _ \<Rightarrow> c"
|
| _ \<Rightarrow> c"
|
||||||
|
|
||||||
definition all_cdl_rights :: "cdl_right set" where
|
definition all_cdl_rights :: "cdl_right set" where
|
||||||
"all_cdl_rights = {Read, Write, Grant}"
|
"all_cdl_rights = {Read, Write, Grant, GrantReply}"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
cap_rights :: "cdl_cap \<Rightarrow> cdl_right set"
|
cap_rights :: "cdl_cap \<Rightarrow> cdl_right set"
|
||||||
|
@ -404,6 +398,7 @@ where
|
||||||
FrameCap _ _ x _ _ _ \<Rightarrow> x
|
FrameCap _ _ x _ _ _ \<Rightarrow> x
|
||||||
| NotificationCap _ _ x \<Rightarrow> x
|
| NotificationCap _ _ x \<Rightarrow> x
|
||||||
| EndpointCap _ _ x \<Rightarrow> x
|
| EndpointCap _ _ x \<Rightarrow> x
|
||||||
|
| ReplyCap _ x \<Rightarrow> x
|
||||||
| _ \<Rightarrow> all_cdl_rights"
|
| _ \<Rightarrow> all_cdl_rights"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
|
@ -411,8 +406,9 @@ definition
|
||||||
where
|
where
|
||||||
"update_cap_rights r c \<equiv> case c of
|
"update_cap_rights r c \<equiv> case c of
|
||||||
FrameCap dev f1 _ f2 f3 f4 \<Rightarrow> FrameCap dev f1 (validate_vm_rights r) f2 f3 f4
|
FrameCap dev f1 _ f2 f3 f4 \<Rightarrow> FrameCap dev f1 (validate_vm_rights r) f2 f3 f4
|
||||||
| NotificationCap f1 f2 _ \<Rightarrow> NotificationCap f1 f2 (r - {Grant})
|
| NotificationCap f1 f2 _ \<Rightarrow> NotificationCap f1 f2 (r - {Grant, GrantReply})
|
||||||
| EndpointCap f1 f2 _ \<Rightarrow> EndpointCap f1 f2 r
|
| EndpointCap f1 f2 _ \<Rightarrow> EndpointCap f1 f2 r
|
||||||
|
| ReplyCap f1 _ \<Rightarrow> ReplyCap f1 (r - {Read, GrantReply} \<union> {Write})
|
||||||
| _ \<Rightarrow> c"
|
| _ \<Rightarrow> c"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
|
@ -584,9 +580,9 @@ lemma update_cap_guard_size [simp]:
|
||||||
|
|
||||||
definition is_pending_cap :: "cdl_cap \<Rightarrow> bool"
|
definition is_pending_cap :: "cdl_cap \<Rightarrow> bool"
|
||||||
where "is_pending_cap c \<equiv> case c of
|
where "is_pending_cap c \<equiv> case c of
|
||||||
PendingSyncRecvCap _ _ \<Rightarrow> True
|
PendingSyncRecvCap _ _ _ \<Rightarrow> True
|
||||||
| PendingNtfnRecvCap _ \<Rightarrow> True
|
| PendingNtfnRecvCap _ \<Rightarrow> True
|
||||||
| PendingSyncSendCap _ _ _ _ _ \<Rightarrow> True
|
| PendingSyncSendCap _ _ _ _ _ _ \<Rightarrow> True
|
||||||
| _ \<Rightarrow> False"
|
| _ \<Rightarrow> False"
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue