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

arch_split: IpcCancel_AI [VER-567]

This commit is contained in:
Alejandro Gomez-Londono 2016-06-02 17:49:05 +10:00
parent 9c608c62dc
commit eb40bef27c
2 changed files with 20 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy
View File

@ -16,18 +16,18 @@ context Arch begin
named_theorems IpcCancel_AI_asms
definition "IpcCancel_AI_dummy_const \<equiv> (1 :: nat)"
crunch v_ker_map[wp,IpcCancel_AI_asms]: set_endpoint "valid_kernel_mappings"
(ignore: set_object wp: set_object_v_ker_map crunch_wps)
lemma IpcCancel_AI_trivial_result[IpcCancel_AI_asms]:
"IpcCancel_AI_dummy_const > 0"
by (simp add: IpcCancel_AI_dummy_const_def)
crunch eq_ker_map[wp,IpcCancel_AI_asms]: set_endpoint "equal_kernel_mappings"
(ignore: set_object wp: set_object_equal_mappings crunch_wps)
end
interpretation IpcCancel_AI: IpcCancel_AI
where IpcCancel_AI_dummy_const = Arch.IpcCancel_AI_dummy_const proof goal_cases
interpretation IpcCancel_AI?: IpcCancel_AI
proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact IpcCancel_AI_asms)?)
case 1 show ?case by (intro_locales; (unfold_locales; fact IpcCancel_AI_asms)?)
qed
end

40
proof/invariant-abstract/IpcCancel_AI.thy
View File

@ -12,27 +12,23 @@ theory IpcCancel_AI
imports "./$L4V_ARCH/ArchSchedule_AI"
begin
locale IpcCancel_AI begin
extend_locale
fixes IpcCancel_AI_dummy_const :: nat
assumes IpcCancel_AI_trivial_asm: "IpcCancel_AI_dummy_const > 0"
end
locale IpcCancel_AI =
fixes state_ext_type :: "('a :: state_ext) itself"
assumes set_endpoint_eq_ker_map:
"\<lbrace>equal_kernel_mappings\<rbrace> (set_endpoint a b :: (unit, 'a) s_monad) \<lbrace>\<lambda>_. equal_kernel_mappings\<rbrace>"
assumes set_endpoint_v_ker_map:
"\<lbrace>valid_kernel_mappings\<rbrace> (set_endpoint a b :: (unit, 'a) s_monad) \<lbrace>\<lambda>_. valid_kernel_mappings\<rbrace>"
lemma blocked_cancel_ipc_simple:
"\<lbrace>tcb_at t\<rbrace> blocked_cancel_ipc ts t \<lbrace>\<lambda>rv. st_tcb_at simple t\<rbrace>"
by (simp add: blocked_cancel_ipc_def | wp sts_st_tcb_at')+
lemma cancel_signal_simple:
"\<lbrace>\<top>\<rbrace> cancel_signal t ntfn \<lbrace>\<lambda>rv. st_tcb_at simple t\<rbrace>"
by (simp add: cancel_signal_def | wp sts_st_tcb_at')+
crunch typ_at: cancel_all_ipc "\<lambda>s. P (typ_at T p s)" (wp: crunch_wps mapM_x_wp)
lemma cancel_all_helper:
" \<lbrace>valid_objs and
(\<lambda>s. \<forall>t \<in> set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s) \<rbrace>
@ -247,18 +243,18 @@ definition
"emptyable \<equiv> \<lambda>p s. (tcb_at (fst p) s \<and> snd p = tcb_cnode_index 2) \<longrightarrow>
st_tcb_at halted (fst p) s"
locale delete_one_abs =
fixes state_ext_type :: "('a :: state_ext) itself"
assumes delete_one_invs:
"\<And>p. \<lbrace>invs and emptyable p\<rbrace> (cap_delete_one p :: (unit,'a::state_ext) s_monad) \<lbrace>\<lambda>rv. invs\<rbrace>"
"\<And>p. \<lbrace>invs and emptyable p\<rbrace> (cap_delete_one p :: (unit,'a) s_monad) \<lbrace>\<lambda>rv. invs\<rbrace>"
assumes delete_one_deletes:
"\<lbrace>\<top>\<rbrace> (cap_delete_one sl :: (unit,'a::state_ext) s_monad) \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = cap.NullCap) sl\<rbrace>"
"\<lbrace>\<top>\<rbrace> (cap_delete_one sl :: (unit,'a) s_monad) \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = cap.NullCap) sl\<rbrace>"
assumes delete_one_caps_of_state:
"\<And>P p. \<lbrace>\<lambda>s. cte_wp_at can_fast_finalise p s
\<longrightarrow> P ((caps_of_state s) (p \<mapsto> cap.NullCap))\<rbrace>
(cap_delete_one p :: (unit,'a::state_ext) s_monad)
(cap_delete_one p :: (unit,'a) s_monad)
\<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>"
@ -325,16 +321,6 @@ lemma get_epq_sp:
apply (wp|simp)+
done
context begin interpretation Arch . (*FIXME: arch_split*)
crunch v_ker_map[wp]: set_endpoint "valid_kernel_mappings"
(ignore: set_object wp: set_object_v_ker_map crunch_wps)
crunch eq_ker_map[wp]: set_endpoint "equal_kernel_mappings"
(ignore: set_object wp: set_object_equal_mappings crunch_wps)
end
lemma set_ep_cap_refs_in_kernel_window [wp]:
"\<lbrace>cap_refs_in_kernel_window\<rbrace> set_endpoint ep p \<lbrace>\<lambda>_. cap_refs_in_kernel_window\<rbrace>"
unfolding set_endpoint_def
@ -343,6 +329,7 @@ lemma set_ep_cap_refs_in_kernel_window [wp]:
split: Structures_A.kernel_object.splits)
done
lemma set_endpoint_valid_ioc[wp]:
"\<lbrace>valid_ioc\<rbrace> set_endpoint ptr ep \<lbrace>\<lambda>rv. valid_ioc\<rbrace>"
@ -676,11 +663,11 @@ crunch cte_wp_at[wp]: blocked_cancel_ipc "cte_wp_at P p"
crunch cte_wp_at[wp]: cancel_signal "cte_wp_at P p"
(wp: crunch_wps)
locale delete_one_pre =
fixes state_ext_type :: "('a :: state_ext) itself"
assumes delete_one_cte_wp_at_preserved:
"(\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap) \<Longrightarrow>
\<lbrace>cte_wp_at P sl\<rbrace> (cap_delete_one sl' :: (unit,'a::state_ext) s_monad) \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>"
\<lbrace>cte_wp_at P sl\<rbrace> (cap_delete_one sl' :: (unit,'a) s_monad) \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>"
lemma (in delete_one_pre) reply_cancel_ipc_cte_wp_at_preserved:
@ -1264,5 +1251,4 @@ lemma real_cte_emptyable_strg:
"real_cte_at p s \<longrightarrow> emptyable p s"
by (clarsimp simp: emptyable_def obj_at_def is_tcb is_cap_table)
end