Theory ExternalCallWF
section ‹Properties of external calls in well-formed programs›
theory ExternalCallWF
imports
WellForm
"../Framework/FWSemantics"
begin
lemma external_WT_defs_is_type:
assumes "wf_prog wf_md P" and "C∙M(Ts) :: T"
shows "is_class P C" and "is_type P T" "set Ts ⊆ types P"
using assms by(auto elim: external_WT_defs.cases)
context heap_base begin
lemma WT_red_external_aggr_imp_red_external:
"⟦ wf_prog wf_md P; (ta, va, h') ∈ red_external_aggr P t a M vs h; P,h ⊢ a∙M(vs) : U; P,h ⊢ t √t ⟧
⟹ P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩"
apply(drule tconfD)
apply(erule external_WT'.cases)
apply(clarsimp)
apply(drule (1) sees_wf_native)
apply(erule external_WT_defs.cases)
apply(case_tac [!] hT)
apply(auto 4 4 simp add: red_external_aggr_def widen_Class intro: red_external.intros heap_base.red_external.intros[where addr2thread_id=addr2thread_id and thread_id2addr=thread_id2addr and spurious_wakeups=True and empty_heap=empty_heap and allocate=allocate and typeof_addr=typeof_addr and heap_read=heap_read and heap_write=heap_write] heap_base.red_external.intros[where addr2thread_id=addr2thread_id and thread_id2addr=thread_id2addr and spurious_wakeups=False and empty_heap=empty_heap and allocate=allocate and typeof_addr=typeof_addr and heap_read=heap_read and heap_write=heap_write] split: if_split_asm dest: sees_method_decl_above)
done
lemma WT_red_external_list_conv:
"⟦ wf_prog wf_md P; P,h ⊢ a∙M(vs) : U; P,h ⊢ t √t ⟧
⟹ P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩ ⟷ (ta, va, h') ∈ red_external_aggr P t a M vs h"
by(blast intro: WT_red_external_aggr_imp_red_external red_external_imp_red_external_aggr)
lemma red_external_new_thread_sees:
"⟦ wf_prog wf_md P; P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩; NewThread t' (C, M', a') h'' ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ typeof_addr h' a' = ⌊Class_type C⌋ ∧ (∃T meth D. P ⊢ C sees M':[]→T = ⌊meth⌋ in D)"
by(fastforce elim!: red_external.cases simp add: widen_Class ta_upd_simps dest: sub_Thread_sees_run)
end
subsection ‹Preservation of heap conformance›
context heap_conf_read begin
lemma hconf_heap_copy_loc_mono:
assumes "heap_copy_loc a a' al h obs h'"
and "hconf h"
and "P,h ⊢ a@al : T" "P,h ⊢ a'@al : T"
shows "hconf h'"
proof -
from ‹heap_copy_loc a a' al h obs h'› obtain v
where read: "heap_read h a al v"
and "write": "heap_write h a' al v h'" by cases auto
from read ‹P,h ⊢ a@al : T› ‹hconf h› have "P,h ⊢ v :≤ T"
by(rule heap_read_conf)
with "write" ‹hconf h› ‹P,h ⊢ a'@al : T› show ?thesis
by(rule hconf_heap_write_mono)
qed
lemma hconf_heap_copies_mono:
assumes "heap_copies a a' als h obs h'"
and "hconf h"
and "list_all2 (λal T. P,h ⊢ a@al : T) als Ts"
and "list_all2 (λal T. P,h ⊢ a'@al : T) als Ts"
shows "hconf h'"
using assms
proof(induct arbitrary: Ts)
case Nil thus ?case by simp
next
case (Cons al h ob h' als obs h'')
note step = ‹heap_copy_loc a a' al h ob h'›
from ‹list_all2 (λal T. P,h ⊢ a@al : T) (al # als) Ts›
obtain T Ts' where [simp]: "Ts = T # Ts'"
and "P,h ⊢ a@al : T" "list_all2 (λal T. P,h ⊢ a@al : T) als Ts'"
by(auto simp add: list_all2_Cons1)
from ‹list_all2 (λal T. P,h ⊢ a'@al : T) (al # als) Ts›
have "P,h ⊢ a'@al : T" "list_all2 (λal T. P,h ⊢ a'@al : T) als Ts'" by simp_all
from step ‹hconf h› ‹P,h ⊢ a@al : T› ‹P,h ⊢ a'@al : T›
have "hconf h'" by(rule hconf_heap_copy_loc_mono)
moreover from step have "h ⊴ h'" by(rule hext_heap_copy_loc)
from ‹list_all2 (λal T. P,h ⊢ a@al : T) als Ts'›
have "list_all2 (λal T. P,h' ⊢ a@al : T) als Ts'"
by(rule list_all2_mono)(rule addr_loc_type_hext_mono[OF _ ‹h ⊴ h'›])
moreover from ‹list_all2 (λal T. P,h ⊢ a'@al : T) als Ts'›
have "list_all2 (λal T. P,h' ⊢ a'@al : T) als Ts'"
by(rule list_all2_mono)(rule addr_loc_type_hext_mono[OF _ ‹h ⊴ h'›])
ultimately show ?case by(rule Cons)
qed
lemma hconf_heap_clone_mono:
assumes "heap_clone P h a h' res"
and "hconf h"
shows "hconf h'"
using ‹heap_clone P h a h' res›
proof cases
case CloneFail thus ?thesis using ‹hconf h›
by(fastforce intro: hconf_heap_ops_mono dest: typeof_addr_is_type)
next
case (ObjClone C h'' a' FDTs obs)
note FDTs = ‹P ⊢ C has_fields FDTs›
let ?als = "map (λ((F, D), Tfm). CField D F) FDTs"
let ?Ts = "map (λ(FD, T). fst (the (map_of FDTs FD))) FDTs"
note ‹heap_copies a a' ?als h'' obs h'›
moreover from ‹typeof_addr h a = ⌊Class_type C⌋› ‹hconf h› have "is_class P C"
by(auto dest: typeof_addr_is_type)
from ‹(h'', a') ∈ allocate h (Class_type C)› have "h ⊴ h''" "hconf h''"
by(rule hext_heap_ops hconf_allocate_mono)+(simp_all add: ‹hconf h› ‹is_class P C›)
note ‹hconf h''›
moreover
from ‹typeof_addr h a = ⌊Class_type C⌋› FDTs
have "list_all2 (λal T. P,h ⊢ a@al : T) ?als ?Ts"
unfolding list_all2_map1 list_all2_map2 list_all2_same
by(fastforce intro: addr_loc_type.intros simp add: has_field_def dest: weak_map_of_SomeI)
hence "list_all2 (λal T. P,h'' ⊢ a@al : T) ?als ?Ts"
by(rule list_all2_mono)(rule addr_loc_type_hext_mono[OF _ ‹h ⊴ h''›])
moreover from ‹(h'', a') ∈ allocate h (Class_type C)› ‹is_class P C›
have "typeof_addr h'' a' = ⌊Class_type C⌋" by(auto dest: allocate_SomeD)
with FDTs have "list_all2 (λal T. P,h'' ⊢ a'@al : T) ?als ?Ts"
unfolding list_all2_map1 list_all2_map2 list_all2_same
by(fastforce intro: addr_loc_type.intros simp add: has_field_def dest: weak_map_of_SomeI)
ultimately have "hconf h'" by(rule hconf_heap_copies_mono)
thus ?thesis using ObjClone by simp
next
case (ArrClone T n h'' a' FDTs obs)
let ?als = "map (λ((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]"
let ?Ts = "map (λ(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T"
note ‹heap_copies a a' ?als h'' obs h'›
moreover from ‹typeof_addr h a = ⌊Array_type T n⌋› ‹hconf h› have "is_type P (T⌊⌉)"
by(auto dest: typeof_addr_is_type)
from ‹(h'', a') ∈ allocate h (Array_type T n)› have "h ⊴ h''" "hconf h''"
by(rule hext_heap_ops hconf_allocate_mono)+(simp_all add: ‹hconf h› ‹is_type P (T⌊⌉)›[simplified])
note ‹hconf h''›
moreover from ‹h ⊴ h''› ‹typeof_addr h a = ⌊Array_type T n⌋›
have type'a: "typeof_addr h'' a = ⌊Array_type T n⌋" by(auto intro: hext_arrD)
note FDTs = ‹P ⊢ Object has_fields FDTs›
from type'a FDTs have "list_all2 (λal T. P,h'' ⊢ a@al : T) ?als ?Ts"
by(fastforce intro: list_all2_all_nthI addr_loc_type.intros simp add: has_field_def distinct_fst_def list_all2_append list_all2_map1 list_all2_map2 list_all2_same dest: weak_map_of_SomeI)
moreover from ‹(h'', a') ∈ allocate h (Array_type T n)› ‹is_type P (T⌊⌉)›
have "typeof_addr h'' a' = ⌊Array_type T n⌋" by(auto dest: allocate_SomeD)
hence "list_all2 (λal T. P,h'' ⊢ a'@al : T) ?als ?Ts" using FDTs
by(fastforce intro: list_all2_all_nthI addr_loc_type.intros simp add: has_field_def distinct_fst_def list_all2_append list_all2_map1 list_all2_map2 list_all2_same dest: weak_map_of_SomeI)
ultimately have "hconf h'" by(rule hconf_heap_copies_mono)
thus ?thesis using ArrClone by simp
qed
theorem external_call_hconf:
assumes major: "P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩"
and minor: "P,h ⊢ a∙M(vs) : U" "hconf h"
shows "hconf h'"
using major minor
by cases(fastforce intro: hconf_heap_clone_mono)+
end
context heap_base begin
primrec conf_extRet :: "'m prog ⇒ 'heap ⇒ 'addr extCallRet ⇒ ty ⇒ bool" where
"conf_extRet P h (RetVal v) T = (P,h ⊢ v :≤ T)"
| "conf_extRet P h (RetExc a) T = (P,h ⊢ Addr a :≤ Class Throwable)"
| "conf_extRet P h RetStaySame T = True"
end
context heap_conf begin
lemma red_external_conf_extRet:
assumes wf: "wf_prog wf_md P"
shows "⟦P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩; P,h ⊢ a∙M(vs) : U; hconf h; preallocated h; P,h ⊢ t √t ⟧
⟹ conf_extRet P h' va U"
using wf apply -
apply(frule red_external_hext)
apply(drule (1) preallocated_hext)
apply(auto elim!: red_external.cases external_WT'.cases external_WT_defs_cases dest!: sees_wf_native[OF wf])
apply(auto simp add: conf_def tconf_def intro: xcpt_subcls_Throwable dest!: hext_heap_write)
apply(case_tac hT)
apply(auto 4 4 dest!: typeof_addr_heap_clone dest: typeof_addr_is_type intro: widen_array_object subcls_C_Object)
done
end
subsection ‹Progress theorems for external calls›
context heap_progress begin
lemma heap_copy_loc_progress:
assumes hconf: "hconf h"
and alconfa: "P,h ⊢ a@al : T"
and alconfa': "P,h ⊢ a'@al : T"
shows "∃v h'. heap_copy_loc a a' al h ([ReadMem a al v, WriteMem a' al v]) h' ∧ P,h ⊢ v :≤ T ∧ hconf h'"
proof -
from heap_read_total[OF hconf alconfa]
obtain v where "heap_read h a al v" "P,h ⊢ v :≤ T" by blast
moreover from heap_write_total[OF hconf alconfa' ‹P,h ⊢ v :≤ T›] obtain h' where "heap_write h a' al v h'" ..
moreover hence "hconf h'" using hconf alconfa' ‹P,h ⊢ v :≤ T› by(rule hconf_heap_write_mono)
ultimately show ?thesis by(blast intro: heap_copy_loc.intros)
qed
lemma heap_copies_progress:
assumes "hconf h"
and "list_all2 (λal T. P,h ⊢ a@al : T) als Ts"
and "list_all2 (λal T. P,h ⊢ a'@al : T) als Ts"
shows "∃vs h'. heap_copies a a' als h (concat (map (λ(al, v). [ReadMem a al v, WriteMem a' al v]) (zip als vs))) h' ∧ hconf h'"
using assms
proof(induct als arbitrary: h Ts)
case Nil thus ?case by(auto intro: heap_copies.Nil)
next
case (Cons al als)
from ‹list_all2 (λal T. P,h ⊢ a@al : T) (al # als) Ts›
obtain T' Ts' where [simp]: "Ts = T' # Ts'"
and "P,h ⊢ a@al : T'" "list_all2 (λal T. P,h ⊢ a@al : T) als Ts'"
by(auto simp add: list_all2_Cons1)
from ‹list_all2 (λal T. P,h ⊢ a'@al : T) (al # als) Ts›
have "P,h ⊢ a'@al : T'" and "list_all2 (λal T. P,h ⊢ a'@al : T) als Ts'" by simp_all
from ‹hconf h› ‹P,h ⊢ a@al : T'› ‹P,h ⊢ a'@al : T'›
obtain v h' where "heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h'"
and "hconf h'" by(fastforce dest: heap_copy_loc_progress)
moreover hence "h ⊴ h'" by-(rule hext_heap_copy_loc)
{
note ‹hconf h'›
moreover from ‹list_all2 (λal T. P,h ⊢ a@al : T) als Ts'›
have "list_all2 (λal T. P,h' ⊢ a@al : T) als Ts'"
by(rule list_all2_mono)(rule addr_loc_type_hext_mono[OF _ ‹h ⊴ h'›])
moreover from ‹list_all2 (λal T. P,h ⊢ a'@al : T) als Ts'›
have "list_all2 (λal T. P,h' ⊢ a'@al : T) als Ts'"
by(rule list_all2_mono)(rule addr_loc_type_hext_mono[OF _ ‹h ⊴ h'›])
ultimately have "∃vs h''. heap_copies a a' als h' (concat (map (λ(al, v). [ReadMem a al v, WriteMem a' al v]) (zip als vs))) h'' ∧ hconf h''"
by(rule Cons) }
then obtain vs h''
where "heap_copies a a' als h' (concat (map (λ(al, v). [ReadMem a al v, WriteMem a' al v]) (zip als vs))) h''"
and "hconf h''" by blast
ultimately
have "heap_copies a a' (al # als) h ([ReadMem a al v, WriteMem a' al v] @ (concat (map (λ(al, v). [ReadMem a al v, WriteMem a' al v]) (zip als vs)))) h''"
by- (rule heap_copies.Cons)
also have "[ReadMem a al v, WriteMem a' al v] @ (concat (map (λ(al, v). [ReadMem a al v, WriteMem a' al v]) (zip als vs))) =
(concat (map (λ(al, v). [ReadMem a al v, WriteMem a' al v]) (zip (al # als) (v # vs))))" by simp
finally show ?case using ‹hconf h''› by blast
qed
lemma heap_clone_progress:
assumes wf: "wf_prog wf_md P"
and typea: "typeof_addr h a = ⌊hT⌋"
and hconf: "hconf h"
shows "∃h' res. heap_clone P h a h' res"
proof -
from typea hconf have "is_htype P hT" by(rule typeof_addr_is_type)
show ?thesis
proof(cases "allocate h hT = {}")
case True
with typea CloneFail[of h a hT P]
show ?thesis by auto
next
case False
then obtain h' a' where new: "(h', a') ∈ allocate h hT" by(rule not_empty_pairE)
hence "h ⊴ h'" by(rule hext_allocate)
have "hconf h'" using new hconf ‹is_htype P hT› by(rule hconf_allocate_mono)
show ?thesis
proof(cases hT)
case [simp]: (Class_type C)
from ‹is_htype P hT› have "is_class P C" by simp
from wf_Fields_Ex[OF wf this]
obtain FDTs where FDTs: "P ⊢ C has_fields FDTs" ..
let ?als = "map (λ((F, D), Tfm). CField D F) FDTs"
let ?Ts = "map (λ(FD, T). fst (the (map_of FDTs FD))) FDTs"
from typea FDTs have "list_all2 (λal T. P,h ⊢ a@al : T) ?als ?Ts"
unfolding list_all2_map1 list_all2_map2 list_all2_same
by(fastforce intro: addr_loc_type.intros simp add: has_field_def dest: weak_map_of_SomeI)
hence "list_all2 (λal T. P,h' ⊢ a@al : T) ?als ?Ts"
by(rule list_all2_mono)(simp add: addr_loc_type_hext_mono[OF _ ‹h ⊴ h'›] split_def)
moreover from new ‹is_class P C›
have "typeof_addr h' a' = ⌊Class_type C⌋" by(auto dest: allocate_SomeD)
with FDTs have "list_all2 (λal T. P,h' ⊢ a'@al : T) ?als ?Ts"
unfolding list_all2_map1 list_all2_map2 list_all2_same
by(fastforce intro: addr_loc_type.intros map_of_SomeI simp add: has_field_def dest: weak_map_of_SomeI)
ultimately obtain obs h'' where "heap_copies a a' ?als h' obs h''" "hconf h''"
by(blast dest: heap_copies_progress[OF ‹hconf h'›])
with typea new FDTs ObjClone[of h a C h' a' P FDTs obs h'']
show ?thesis by auto
next
case [simp]: (Array_type T n)
from wf obtain FDTs where FDTs: "P ⊢ Object has_fields FDTs"
by(blast dest: wf_Fields_Ex is_class_Object)
let ?als = "map (λ((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]"
let ?Ts = "map (λ(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T"
from ‹h ⊴ h'› typea have type'a: "typeof_addr h' a = ⌊Array_type T n⌋"
by(auto intro: hext_arrD)
from type'a FDTs have "list_all2 (λal T. P,h' ⊢ a@al : T) ?als ?Ts"
by(fastforce intro: list_all2_all_nthI addr_loc_type.intros simp add: has_field_def list_all2_append list_all2_map1 list_all2_map2 list_all2_same dest: weak_map_of_SomeI)
moreover from new ‹is_htype P hT›
have "typeof_addr h' a' = ⌊Array_type T n⌋"
by(auto dest: allocate_SomeD)
hence "list_all2 (λal T. P,h' ⊢ a'@al : T) ?als ?Ts" using FDTs
by(fastforce intro: list_all2_all_nthI addr_loc_type.intros simp add: has_field_def list_all2_append list_all2_map1 list_all2_map2 list_all2_same dest: weak_map_of_SomeI)
ultimately obtain obs h'' where "heap_copies a a' ?als h' obs h''" "hconf h''"
by(blast dest: heap_copies_progress[OF ‹hconf h'›])
with typea new FDTs ArrClone[of h a T n h' a' P FDTs obs h'']
show ?thesis by auto
qed
qed
qed
theorem external_call_progress:
assumes wf: "wf_prog wf_md P"
and wt: "P,h ⊢ a∙M(vs) : U"
and hconf: "hconf h"
shows "∃ta va h'. P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩"
proof -
note [simp del] = split_paired_Ex
from wt obtain hT Ts Ts' D
where T: "typeof_addr h a = ⌊hT⌋" and Ts: "map typeof⇘h⇙ vs = map Some Ts"
and "P ⊢ class_type_of hT sees M:Ts'→U = Native in D" and subTs: "P ⊢ Ts [≤] Ts'"
unfolding external_WT'_iff by blast
from wf ‹P ⊢ class_type_of hT sees M:Ts'→U = Native in D›
have "D∙M(Ts') :: U" by(rule sees_wf_native)
moreover from ‹P ⊢ class_type_of hT sees M:Ts'→U = Native in D›
have "P ⊢ ty_of_htype hT ≤ Class D"
by(cases hT)(auto dest: sees_method_decl_above intro: widen_trans widen_array_object)
ultimately show ?thesis using T Ts subTs
proof cases
assume [simp]: "D = Object" "M = clone" "Ts' = []" "U = Class Object"
from heap_clone_progress[OF wf T hconf] obtain h' res where "heap_clone P h a h' res" by blast
thus ?thesis using subTs Ts by(cases res)(auto intro: red_external.intros)
qed(auto simp add: widen_Class intro: red_external.intros)
qed
end
subsection ‹Lemmas for preservation of deadlocked threads›
context heap_progress begin
lemma red_external_wt_hconf_hext:
assumes wf: "wf_prog wf_md P"
and red: "P,t ⊢ ⟨a∙M(vs),h⟩ -ta→ext ⟨va,h'⟩"
and hext: "h'' ⊴ h"
and wt: "P,h'' ⊢ a∙M(vs) : U"
and tconf: "P,h'' ⊢ t √t"
and hconf: "hconf h''"
shows "∃ta' va' h'''. P,t ⊢ ⟨a∙M(vs),h''⟩ -ta'→ext ⟨va', h'''⟩ ∧
collect_locks ⦃ta⦄⇘l⇙ = collect_locks ⦃ta'⦄⇘l⇙ ∧
collect_cond_actions ⦃ta⦄⇘c⇙ = collect_cond_actions ⦃ta'⦄⇘c⇙ ∧
collect_interrupts ⦃ta⦄⇘i⇙ = collect_interrupts ⦃ta'⦄⇘i⇙"
using red wt hext
proof cases
case (RedClone obs a')
from wt obtain hT C Ts Ts' D
where T: "typeof_addr h'' a = ⌊hT⌋"
unfolding external_WT'_iff by blast
from heap_clone_progress[OF wf T hconf]
obtain h''' res where "heap_clone P h'' a h''' res" by blast
thus ?thesis using RedClone
by(cases res)(fastforce intro: red_external.intros)+
next
case RedCloneFail
from wt obtain hT Ts Ts'
where T: "typeof_addr h'' a = ⌊hT⌋"
unfolding external_WT'_iff by blast
from heap_clone_progress[OF wf T hconf]
obtain h''' res where "heap_clone P h'' a h''' res" by blast
thus ?thesis using RedCloneFail
by(cases res)(fastforce intro: red_external.intros)+
qed(fastforce simp add: ta_upd_simps elim!: external_WT'.cases intro: red_external.intros[simplified] dest: typeof_addr_hext_mono)+
lemma red_external_wf_red:
assumes wf: "wf_prog wf_md P"
and red: "P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩"
and tconf: "P,h ⊢ t √t"
and hconf: "hconf h"
and wst: "wset s t = None ∨ (M = wait ∧ (∃w. wset s t = ⌊PostWS w⌋))"
obtains ta' va' h''
where "P,t ⊢ ⟨a∙M(vs), h⟩ -ta'→ext ⟨va', h''⟩"
and "final_thread.actions_ok final s t ta' ∨ final_thread.actions_ok' s t ta' ∧ final_thread.actions_subset ta' ta"
proof(atomize_elim)
let ?a_t = "thread_id2addr t"
let ?t_a = "addr2thread_id a"
from tconf obtain C where ht: "typeof_addr h ?a_t = ⌊Class_type C⌋"
and sub: "P ⊢ C ≼⇧* Thread" by(fastforce dest: tconfD)
show "∃ta' va' h'. P,t ⊢ ⟨a∙M(vs), h⟩ -ta'→ext ⟨va', h'⟩ ∧ (final_thread.actions_ok final s t ta' ∨ final_thread.actions_ok' s t ta' ∧ final_thread.actions_subset ta' ta)"
proof(cases "final_thread.actions_ok' s t ta")
case True
have "final_thread.actions_subset ta ta" by(rule final_thread.actions_subset_refl)
with True red show ?thesis by blast
next
case False
note [simp] = final_thread.actions_ok'_iff lock_ok_las'_def final_thread.cond_action_oks'_subset_Join
final_thread.actions_subset_iff ta_upd_simps collect_cond_actions_def collect_interrupts_def
note [rule del] = subsetI
note [intro] = collect_locks'_subset_collect_locks red_external.intros[simplified]
show ?thesis
proof(cases "wset s t")
case [simp]: (Some w)
with wst obtain w' where [simp]: "w = PostWS w'" "M = wait" by auto
from red have [simp]: "vs = []" by(auto elim: red_external.cases)
show ?thesis
proof(cases w')
case [simp]: WSWokenUp
let ?ta' = "⦃WokenUp, ClearInterrupt t, ObsInterrupted t⦄"
have "final_thread.actions_ok' s t ?ta'" by(simp add: wset_actions_ok_def)
moreover have "final_thread.actions_subset ?ta' ta"
by(auto simp add: collect_locks'_def finfun_upd_apply)
moreover from RedWaitInterrupted
have "∃va h'. P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by auto
ultimately show ?thesis by blast
next
case [simp]: WSNotified
let ?ta' = "⦃Notified⦄"
have "final_thread.actions_ok' s t ?ta'" by(simp add: wset_actions_ok_def)
moreover have "final_thread.actions_subset ?ta' ta"
by(auto simp add: collect_locks'_def finfun_upd_apply)
moreover from RedWaitNotified
have "∃va h'. P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by auto
ultimately show ?thesis by blast
qed
next
case None
from red False show ?thesis
proof cases
case (RedNewThread C)
note ta = ‹ta = ⦃NewThread ?t_a (C, run, a) h, ThreadStart ?t_a⦄›
let ?ta' = "⦃ThreadExists ?t_a True⦄"
from ta False None have "final_thread.actions_ok' s t ?ta'" by(auto)
moreover from ta have "final_thread.actions_subset ?ta' ta" by(auto)
ultimately show ?thesis using RedNewThread by(fastforce)
next
case RedNewThreadFail
then obtain va' h' x where "P,t ⊢ ⟨a∙M(vs), h⟩ -⦃NewThread ?t_a x h', ThreadStart ?t_a⦄→ext ⟨va', h'⟩"
by(fastforce)
moreover from ‹ta = ⦃ThreadExists ?t_a True⦄› False None
have "final_thread.actions_ok' s t ⦃NewThread ?t_a x h', ThreadStart ?t_a⦄" by(auto)
moreover from ‹ta = ⦃ThreadExists ?t_a True⦄›
have "final_thread.actions_subset ⦃NewThread ?t_a x h', ThreadStart ?t_a⦄ ta" by(auto)
ultimately show ?thesis by blast
next
case RedJoin
let ?ta = "⦃IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄"
from ‹ta = ⦃Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)⦄› None False
have "t ∈ interrupts s" by(auto)
hence "final_thread.actions_ok final s t ?ta"
using None by(auto simp add: final_thread.actions_ok_iff final_thread.cond_action_oks.simps)
moreover obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta→ext ⟨va,h'⟩" using RedJoinInterrupt RedJoin by auto
ultimately show ?thesis by blast
next
case RedJoinInterrupt
hence False using False None by(auto)
thus ?thesis ..
next
case RedInterrupt
let ?ta = "⦃ThreadExists (addr2thread_id a) False⦄"
from RedInterrupt None False
have "free_thread_id (thr s) (addr2thread_id a)" by(auto simp add: wset_actions_ok_def)
hence "final_thread.actions_ok final s t ?ta" using None
by(auto simp add: final_thread.actions_ok_iff final_thread.cond_action_oks.simps)
moreover obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta→ext ⟨va,h'⟩" using RedInterruptInexist RedInterrupt by auto
ultimately show ?thesis by blast
next
case RedInterruptInexist
let ?ta = "⦃ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)⦄"
from RedInterruptInexist None False
have "¬ free_thread_id (thr s) (addr2thread_id a)" by(auto simp add: wset_actions_ok_def)
hence "final_thread.actions_ok final s t ?ta" using None
by(auto simp add: final_thread.actions_ok_iff final_thread.cond_action_oks.simps wset_actions_ok_def)
moreover obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta→ext ⟨va,h'⟩" using RedInterruptInexist RedInterrupt by auto
ultimately show ?thesis by blast
next
case (RedIsInterruptedTrue C)
let ?ta' = "⦃IsInterrupted ?t_a False⦄"
from RedIsInterruptedTrue False None have "?t_a ∉ interrupts s" by(auto)
hence "final_thread.actions_ok' s t ?ta'" using None by auto
moreover from RedIsInterruptedTrue have "final_thread.actions_subset ?ta' ta" by auto
moreover from RedIsInterruptedTrue RedIsInterruptedFalse obtain va h'
where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by auto
ultimately show ?thesis by blast
next
case (RedIsInterruptedFalse C)
let ?ta' = "⦃IsInterrupted ?t_a True, ObsInterrupted ?t_a⦄"
from RedIsInterruptedFalse have "?t_a ∈ interrupts s"
using False None by(auto)
hence "final_thread.actions_ok final s t ?ta'"
using None by(auto simp add: final_thread.actions_ok_iff final_thread.cond_action_oks.simps)
moreover obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩"
using RedIsInterruptedFalse RedIsInterruptedTrue by auto
ultimately show ?thesis by blast
next
case RedWaitInterrupt
note ta = ‹ta = ⦃Unlock→a, Lock→a, IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄›
from ta False None have hli: "¬ has_lock (locks s $ a) t ∨ t ∉ interrupts s"
by(fastforce simp add: lock_actions_ok'_iff finfun_upd_apply split: if_split_asm dest: may_lock_t_may_lock_unlock_lock_t dest: has_lock_may_lock)
show ?thesis
proof(cases "has_lock (locks s $ a) t")
case True
let ?ta' = "⦃Suspend a, Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a ⦄"
from True hli have "t ∉ interrupts s" by simp
with True False have "final_thread.actions_ok' s t ?ta'" using None
by(auto simp add: lock_actions_ok'_iff finfun_upd_apply wset_actions_ok_def Cons_eq_append_conv)
moreover from ta have "final_thread.actions_subset ?ta' ta"
by(auto simp add: collect_locks'_def finfun_upd_apply)
moreover from RedWait RedWaitInterrupt obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by auto
ultimately show ?thesis by blast
next
case False
let ?ta' = "⦃UnlockFail→a⦄"
from False have "final_thread.actions_ok' s t ?ta'" using None
by(auto simp add: lock_actions_ok'_iff finfun_upd_apply)
moreover from ta have "final_thread.actions_subset ?ta' ta"
by(auto simp add: collect_locks'_def finfun_upd_apply)
moreover from RedWaitInterrupt obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by(fastforce)
ultimately show ?thesis by blast
qed
next
case RedWait
note ta = ‹ta = ⦃Suspend a, Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a⦄›
from ta False None have hli: "¬ has_lock (locks s $ a) t ∨ t ∈ interrupts s"
by(auto simp add: lock_actions_ok'_iff finfun_upd_apply wset_actions_ok_def Cons_eq_append_conv split: if_split_asm dest: may_lock_t_may_lock_unlock_lock_t dest: has_lock_may_lock)
show ?thesis
proof(cases "has_lock (locks s $ a) t")
case True
let ?ta' = "⦃Unlock→a, Lock→a, IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄"
from True hli have "t ∈ interrupts s" by simp
with True False have "final_thread.actions_ok final s t ?ta'" using None
by(auto simp add: final_thread.actions_ok_iff final_thread.cond_action_oks.simps lock_ok_las_def finfun_upd_apply has_lock_may_lock)
moreover from RedWait RedWaitInterrupt obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by auto
ultimately show ?thesis by blast
next
case False
let ?ta' = "⦃UnlockFail→a⦄"
from False have "final_thread.actions_ok' s t ?ta'" using None
by(auto simp add: lock_actions_ok'_iff finfun_upd_apply)
moreover from ta have "final_thread.actions_subset ?ta' ta"
by(auto simp add: collect_locks'_def finfun_upd_apply)
moreover from RedWait RedWaitFail obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by(fastforce)
ultimately show ?thesis by blast
qed
next
case RedWaitFail
note ta = ‹ta = ⦃UnlockFail→a⦄›
let ?ta' = "if t ∈ interrupts s
then ⦃Unlock→a, Lock→a, IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄
else ⦃Suspend a, Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a ⦄"
from ta False None have "has_lock (locks s $ a) t"
by(auto simp add: finfun_upd_apply split: if_split_asm)
hence "final_thread.actions_ok final s t ?ta'" using None
by(auto simp add: final_thread.actions_ok_iff final_thread.cond_action_oks.simps lock_ok_las_def finfun_upd_apply has_lock_may_lock wset_actions_ok_def)
moreover from RedWaitFail RedWait RedWaitInterrupt
obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩"
by(cases "t ∈ interrupts s") (auto)
ultimately show ?thesis by blast
next
case RedWaitNotified
note ta = ‹ta = ⦃Notified⦄›
let ?ta' = "if has_lock (locks s $ a) t
then (if t ∈ interrupts s
then ⦃Unlock→a, Lock→a, IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄
else ⦃Suspend a, Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a ⦄)
else ⦃UnlockFail→a⦄"
have "final_thread.actions_ok final s t ?ta'" using None
by(auto simp add: final_thread.actions_ok_iff final_thread.cond_action_oks.simps lock_ok_las_def finfun_upd_apply has_lock_may_lock wset_actions_ok_def)
moreover from RedWaitNotified RedWait RedWaitInterrupt RedWaitFail
have "∃va h'. P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by auto
ultimately show ?thesis by blast
next
case RedWaitInterrupted
note ta = ‹ta = ⦃WokenUp, ClearInterrupt t, ObsInterrupted t⦄›
let ?ta' = "if has_lock (locks s $ a) t
then (if t ∈ interrupts s
then ⦃Unlock→a, Lock→a, IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄
else ⦃Suspend a, Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a ⦄)
else ⦃UnlockFail→a⦄"
have "final_thread.actions_ok final s t ?ta'" using None
by(auto simp add: final_thread.actions_ok_iff final_thread.cond_action_oks.simps lock_ok_las_def finfun_upd_apply has_lock_may_lock wset_actions_ok_def)
moreover from RedWaitInterrupted RedWait RedWaitInterrupt RedWaitFail
have "∃va h'. P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by auto
ultimately show ?thesis by blast
next
case RedWaitSpurious
note ta = ‹ta = ⦃Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a⦄›
from ta False None have hli: "¬ has_lock (locks s $ a) t ∨ t ∈ interrupts s"
by(auto simp add: lock_actions_ok'_iff finfun_upd_apply wset_actions_ok_def Cons_eq_append_conv split: if_split_asm dest: may_lock_t_may_lock_unlock_lock_t dest: has_lock_may_lock)
show ?thesis
proof(cases "has_lock (locks s $ a) t")
case True
let ?ta' = "⦃Unlock→a, Lock→a, IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄"
from True hli have "t ∈ interrupts s" by simp
with True False have "final_thread.actions_ok final s t ?ta'" using None
by(auto simp add: final_thread.actions_ok_iff final_thread.cond_action_oks.simps lock_ok_las_def finfun_upd_apply has_lock_may_lock)
moreover from RedWaitInterrupt RedWaitSpurious(1-5)
obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by auto
ultimately show ?thesis by blast
next
case False
let ?ta' = "⦃UnlockFail→a⦄"
from False have "final_thread.actions_ok' s t ?ta'" using None
by(auto simp add: lock_actions_ok'_iff finfun_upd_apply)
moreover from ta have "final_thread.actions_subset ?ta' ta"
by(auto simp add: collect_locks'_def finfun_upd_apply)
moreover from RedWaitSpurious(1-5) RedWaitFail
obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by(fastforce)
ultimately show ?thesis by blast
qed
next
case RedNotify
note ta = ‹ta = ⦃Notify a, Unlock→a, Lock→a⦄›
let ?ta' = "⦃UnlockFail→a⦄"
from ta False None have "¬ has_lock (locks s $ a) t"
by(fastforce simp add: lock_actions_ok'_iff finfun_upd_apply wset_actions_ok_def Cons_eq_append_conv split: if_split_asm dest: may_lock_t_may_lock_unlock_lock_t has_lock_may_lock)
hence "final_thread.actions_ok' s t ?ta'" using None
by(auto simp add: lock_actions_ok'_iff finfun_upd_apply)
moreover from ta have "final_thread.actions_subset ?ta' ta"
by(auto simp add: collect_locks'_def finfun_upd_apply)
moreover from RedNotify obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by(fastforce)
ultimately show ?thesis by blast
next
case RedNotifyFail
note ta = ‹ta = ⦃UnlockFail→a⦄›
let ?ta' = "⦃Notify a, Unlock→a, Lock→a⦄"
from ta False None have "has_lock (locks s $ a) t"
by(auto simp add: finfun_upd_apply split: if_split_asm)
hence "final_thread.actions_ok' s t ?ta'" using None
by(auto simp add: finfun_upd_apply simp add: wset_actions_ok_def intro: has_lock_may_lock)
moreover from ta have "final_thread.actions_subset ?ta' ta"
by(auto simp add: collect_locks'_def finfun_upd_apply)
moreover from RedNotifyFail obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by(fastforce)
ultimately show ?thesis by blast
next
case RedNotifyAll
note ta = ‹ta = ⦃NotifyAll a, Unlock→a, Lock→a⦄›
let ?ta' = "⦃UnlockFail→a⦄"
from ta False None have "¬ has_lock (locks s $ a) t"
by(auto simp add: lock_actions_ok'_iff finfun_upd_apply wset_actions_ok_def Cons_eq_append_conv split: if_split_asm dest: may_lock_t_may_lock_unlock_lock_t)
hence "final_thread.actions_ok' s t ?ta'" using None
by(auto simp add: lock_actions_ok'_iff finfun_upd_apply)
moreover from ta have "final_thread.actions_subset ?ta' ta"
by(auto simp add: collect_locks'_def finfun_upd_apply)
moreover from RedNotifyAll obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by(fastforce)
ultimately show ?thesis by blast
next
case RedNotifyAllFail
note ta = ‹ta = ⦃UnlockFail→a⦄›
let ?ta' = "⦃NotifyAll a, Unlock→a, Lock→a⦄"
from ta False None have "has_lock (locks s $ a) t"
by(auto simp add: finfun_upd_apply split: if_split_asm)
hence "final_thread.actions_ok' s t ?ta'" using None
by(auto simp add: finfun_upd_apply wset_actions_ok_def intro: has_lock_may_lock)
moreover from ta have "final_thread.actions_subset ?ta' ta"
by(auto simp add: collect_locks'_def finfun_upd_apply)
moreover from RedNotifyAllFail obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩" by(fastforce)
ultimately show ?thesis by blast
next
case RedInterruptedTrue
let ?ta' = "⦃IsInterrupted t False⦄"
from RedInterruptedTrue have "final_thread.actions_ok final s t ?ta'"
using None False by(auto simp add: final_thread.actions_ok_iff final_thread.cond_action_oks.simps)
moreover obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩"
using RedInterruptedFalse RedInterruptedTrue by auto
ultimately show ?thesis by blast
next
case RedInterruptedFalse
let ?ta' = "⦃IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄"
from RedInterruptedFalse have "final_thread.actions_ok final s t ?ta'"
using None False
by(auto simp add: final_thread.actions_ok_iff final_thread.cond_action_oks.simps)
moreover obtain va h' where "P,t ⊢ ⟨a∙M(vs),h⟩ -?ta'→ext ⟨va,h'⟩"
using RedInterruptedFalse RedInterruptedTrue by auto
ultimately show ?thesis by blast
qed(auto simp add: None)
qed
qed
qed
end
context heap_base begin
lemma red_external_ta_satisfiable:
fixes final
assumes "P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩"
shows "∃s. final_thread.actions_ok final s t ta"
proof -
note [simp] =
final_thread.actions_ok_iff final_thread.cond_action_oks.simps final_thread.cond_action_ok.simps
lock_ok_las_def finfun_upd_apply wset_actions_ok_def has_lock_may_lock
and [intro] =
free_thread_id.intros
and [cong] = conj_cong
from assms show ?thesis by cases(fastforce intro: exI[where x="(K$ None)(a $:= ⌊(t, 0)⌋)"] exI[where x="(K$ None)"])+
qed
lemma red_external_aggr_ta_satisfiable:
fixes final
assumes "(ta, va, h') ∈ red_external_aggr P t a M vs h"
shows "∃s. final_thread.actions_ok final s t ta"
proof -
note [simp] =
final_thread.actions_ok_iff final_thread.cond_action_oks.simps final_thread.cond_action_ok.simps
lock_ok_las_def finfun_upd_apply wset_actions_ok_def has_lock_may_lock
and [intro] =
free_thread_id.intros
and [cong] = conj_cong
from assms show ?thesis
by(fastforce simp add: red_external_aggr_def split_beta ta_upd_simps split: if_split_asm intro: exI[where x="Map.empty"] exI[where x="(K$ None)(a $:= ⌊(t, 0)⌋)"] exI[where x="K$ None"])
qed
end
subsection ‹Determinism›
context heap_base begin
lemma heap_copy_loc_deterministic:
assumes det: "deterministic_heap_ops"
and copy: "heap_copy_loc a a' al h ops h'" "heap_copy_loc a a' al h ops' h''"
shows "ops = ops' ∧ h' = h''"
using copy
by(auto elim!: heap_copy_loc.cases dest: deterministic_heap_ops_readD[OF det] deterministic_heap_ops_writeD[OF det])
lemma heap_copies_deterministic:
assumes det: "deterministic_heap_ops"
and copy: "heap_copies a a' als h ops h'" "heap_copies a a' als h ops' h''"
shows "ops = ops' ∧ h' = h''"
using copy
apply(induct arbitrary: ops' h'')
apply(fastforce elim!: heap_copies_cases)
apply(erule heap_copies_cases)
apply clarify
apply(drule (1) heap_copy_loc_deterministic[OF det])
apply clarify
apply(unfold same_append_eq)
apply blast
done
lemma heap_clone_deterministic:
assumes det: "deterministic_heap_ops"
and clone: "heap_clone P h a h' obs" "heap_clone P h a h'' obs'"
shows "h' = h'' ∧ obs = obs'"
using clone
by(auto 4 4 elim!: heap_clone.cases dest: heap_copies_deterministic[OF det] deterministic_heap_ops_allocateD[OF det] has_fields_fun)
lemma red_external_deterministic:
fixes final
assumes det: "deterministic_heap_ops"
and red: "P,t ⊢ ⟨a∙M(vs), (shr s)⟩ -ta→ext ⟨va, h'⟩" "P,t ⊢ ⟨a∙M(vs), (shr s)⟩ -ta'→ext ⟨va', h''⟩"
and aok: "final_thread.actions_ok final s t ta" "final_thread.actions_ok final s t ta'"
shows "ta = ta' ∧ va = va' ∧ h' = h''"
using red aok
apply(simp add: final_thread.actions_ok_iff lock_ok_las_def)
apply(erule red_external.cases)
apply(erule_tac [!] red_external.cases)
apply simp_all
apply(auto simp add: finfun_upd_apply wset_actions_ok_def dest: heap_clone_deterministic[OF det] split: if_split_asm)
using deterministic_heap_ops_no_spurious_wakeups[OF det]
apply simp_all
done
end
end