Theory ProgressThreaded
section ‹Progress and type safety theorem for the multithreaded system›
theory ProgressThreaded
imports
Threaded
TypeSafe
"../Framework/FWProgress"
begin
lemma lock_ok_ls_Some_ex_ts_not_final:
assumes lock: "lock_ok ls ts"
and hl: "has_lock (ls $ l) t"
shows "∃e x ln. ts t = ⌊((e, x), ln)⌋ ∧ ¬ final e"
proof -
from lock have "lock_thread_ok ls ts"
by(rule lock_ok_lock_thread_ok)
with hl obtain e x ln
where tst: "ts t = ⌊((e, x), ln)⌋"
by(auto dest!: lock_thread_okD)
{ assume "final e"
hence "expr_locks e l = 0" by(rule final_locks)
with lock tst have "has_locks (ls $ l) t = 0"
by(auto dest: lock_okD2[rule_format, where l=l])
with hl have False by simp }
with tst show ?thesis by auto
qed
subsection ‹Preservation lemmata›
subsection ‹Definite assignment›
abbreviation
def_ass_ts_ok :: "('addr,'thread_id,'addr expr × 'addr locals) thread_info ⇒ 'heap ⇒ bool"
where
"def_ass_ts_ok ≡ ts_ok (λt (e, x) h. 𝒟 e ⌊dom x⌋)"
context J_heap_base begin
lemma assumes wf: "wf_J_prog P"
shows red_def_ass_new_thread:
"⟦ P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; NewThread t'' (e'', x'') c'' ∈ set ⦃ta⦄⇘t⇙ ⟧ ⟹ 𝒟 e'' ⌊dom x''⌋"
and reds_def_ass_new_thread:
"⟦ P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; NewThread t'' (e'', x'') c'' ∈ set ⦃ta⦄⇘t⇙ ⟧ ⟹ 𝒟 e'' ⌊dom x''⌋"
proof(induct rule: red_reds.inducts)
case (RedCallExternal s a T M vs ta va h' ta' e' s')
then obtain C fs a where subThread: "P ⊢ C ≼⇧* Thread" and ext: "extNTA2J P (C, run, a) = (e'', x'')"
by(fastforce dest: red_external_new_thread_sub_thread)
from sub_Thread_sees_run[OF wf subThread] obtain D pns body
where sees: "P ⊢ C sees run: []→Void = ⌊(pns, body)⌋ in D" by auto
from sees_wf_mdecl[OF wf this] have "𝒟 body ⌊{this}⌋"
by(auto simp add: wf_mdecl_def)
with sees ext show ?case by(clarsimp simp del: fun_upd_apply)
qed(auto simp add: ta_upd_simps)
lemma lifting_wf_def_ass: "wf_J_prog P ⟹ lifting_wf final_expr (mred P) (λt (e, x) m. 𝒟 e ⌊dom x⌋)"
apply(unfold_locales)
apply(auto dest: red_preserves_defass red_def_ass_new_thread)
done
lemma def_ass_ts_ok_J_start_state:
"⟦ wf_J_prog P; P ⊢ C sees M:Ts→T = ⌊(pns, body)⌋ in D; length vs = length Ts ⟧ ⟹
def_ass_ts_ok (thr (J_start_state P C M vs)) h"
apply(rule ts_okI)
apply(drule (1) sees_wf_mdecl)
apply(clarsimp simp add: wf_mdecl_def start_state_def split: if_split_asm)
done
end
subsection ‹typeability›
context J_heap_base begin
definition type_ok :: "'addr J_prog ⇒ env × ty ⇒ 'addr expr ⇒ 'heap ⇒ bool"
where "type_ok P ≡ (λ(E, T) e c. (∃T'. (P,E,c ⊢ e : T' ∧ P ⊢ T' ≤ T)))"
definition J_sconf_type_ET_start :: "'m prog ⇒ cname ⇒ mname ⇒ ('thread_id ⇀ (env × ty))"
where
"J_sconf_type_ET_start P C M ≡
let (_, _, T, _) = method P C M
in ([start_tid ↦ (Map.empty, T)])"
lemma fixes E :: env
assumes wf: "wf_J_prog P"
shows red_type_newthread:
"⟦ P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; P,E,hp s ⊢ e : T; NewThread t'' (e'', x'') (hp s') ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ ∃E T. P,E,hp s' ⊢ e'' : T ∧ P,hp s' ⊢ x'' (:≤) E"
and reds_type_newthread:
"⟦ P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; NewThread t'' (e'', x'') (hp s') ∈ set ⦃ta⦄⇘t⇙; P,E,hp s ⊢ es [:] Ts ⟧
⟹ ∃E T. P,E,hp s' ⊢ e'' : T ∧ P,hp s' ⊢ x'' (:≤) E"
proof(induct arbitrary: E T and E Ts rule: red_reds.inducts)
case (RedCallExternal s a U M Ts T' D vs ta va h' ta' e' s')
from ‹NewThread t'' (e'', x'') (hp s') ∈ set ⦃ta'⦄⇘t⇙› ‹ta' = extTA2J P ta›
obtain C' M' a' where nt: "NewThread t'' (C', M', a') (hp s') ∈ set ⦃ta⦄⇘t⇙"
and "extNTA2J P (C', M', a') = (e'', x'')" by fastforce
from red_external_new_thread_sees[OF wf ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩› nt] ‹typeof_addr (hp s) a = ⌊U⌋›
obtain T pns body D where h'a': "typeof_addr h' a' = ⌊Class_type C'⌋"
and sees: " P ⊢ C' sees M': []→T = ⌊(pns, body)⌋ in D" by auto
from sees_wf_mdecl[OF wf sees] obtain T where "P,[this ↦ Class D] ⊢ body :: T"
by(auto simp add: wf_mdecl_def)
hence "WTrt P (hp s') [this ↦ Class D] body T" by(rule WT_implies_WTrt)
moreover from sees have "P ⊢ C' ≼⇧* D" by(rule sees_method_decl_above)
with h'a' have "P,h' ⊢ [this ↦ Addr a'] (:≤) [this ↦ Class D]" by(auto simp add: lconf_def conf_def)
ultimately show ?case using h'a' sees ‹s' = (h', lcl s)›
‹extNTA2J P (C', M', a') = (e'', x'')› by(fastforce intro: sees_method_decl_above)
qed(fastforce simp add: ta_upd_simps)+
end
context J_heap_conf_base begin
definition sconf_type_ok :: "(env × ty) ⇒ 'thread_id ⇒ 'addr expr × 'addr locals ⇒ 'heap ⇒ bool"
where
"sconf_type_ok ET t ex h ≡ fst ET ⊢ (h, snd ex) √ ∧ type_ok P ET (fst ex) h ∧ P,h ⊢ t √t"
abbreviation sconf_type_ts_ok ::
"('thread_id ⇀ (env × ty)) ⇒ ('addr,'thread_id,'addr expr × 'addr locals) thread_info ⇒ 'heap ⇒ bool"
where
"sconf_type_ts_ok ≡ ts_inv sconf_type_ok"
lemma ts_inv_ok_J_sconf_type_ET_start:
"ts_inv_ok (thr (J_start_state P C M vs)) (J_sconf_type_ET_start P C M)"
by(rule ts_inv_okI)(simp add: start_state_def J_sconf_type_ET_start_def split_beta)
end
lemma (in J_heap) red_preserve_welltype:
"⟦ extTA,P,t ⊢ ⟨e, (h, x)⟩ -ta→ ⟨e', (h', x')⟩; P,E,h ⊢ e'' : T ⟧ ⟹ P,E,h' ⊢ e'' : T"
by(auto elim: WTrt_hext_mono dest!: red_hext_incr)
context J_heap_conf begin
lemma sconf_type_ts_ok_J_start_state:
"⟦ wf_J_prog P; wf_start_state P C M vs ⟧
⟹ sconf_type_ts_ok (J_sconf_type_ET_start P C M) (thr (J_start_state P C M vs)) (shr (J_start_state P C M vs))"
apply(erule wf_start_state.cases)
apply(rule ts_invI)
apply(simp add: start_state_def split: if_split_asm)
apply(frule (1) sees_wf_mdecl)
apply(auto simp add: wf_mdecl_def J_sconf_type_ET_start_def sconf_type_ok_def sconf_def type_ok_def)
apply(erule hconf_start_heap)
apply(erule preallocated_start_heap)
apply(erule wf_prog_wf_syscls)
apply(frule list_all2_lengthD)
apply(auto simp add: wt_blocks confs_conv_map intro: WT_implies_WTrt)[1]
apply(erule tconf_start_heap_start_tid)
apply(erule wf_prog_wf_syscls)
done
lemma J_start_state_sconf_type_ok:
assumes wf: "wf_J_prog P"
and ok: "wf_start_state P C M vs"
shows "ts_ok (λt x h. ∃ET. sconf_type_ok ET t x h) (thr (J_start_state P C M vs)) start_heap"
using sconf_type_ts_ok_J_start_state[OF assms]
unfolding shr_start_state by(rule ts_inv_into_ts_ok_Ex)
end
context J_conf_read begin
lemma red_preserves_type_ok:
"⟦ extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩; wf_J_prog P; E ⊢ s √; type_ok P (E, T) e (hp s); P,hp s ⊢ t √t ⟧ ⟹ type_ok P (E, T) e' (hp s')"
apply(clarsimp simp add: type_ok_def)
apply(subgoal_tac "∃T''. P,E,hp s' ⊢ e' : T'' ∧ P ⊢ T'' ≤ T'")
apply(fast elim: widen_trans)
by(rule subject_reduction)
lemma lifting_inv_sconf_subject_ok:
assumes wf: "wf_J_prog P"
shows "lifting_inv final_expr (mred P) sconf_type_ok"
proof(unfold_locales)
fix t x m ta x' m' i
assume mred: "mred P t (x, m) ta (x', m')"
and "sconf_type_ok i t x m"
moreover obtain e l where x [simp]: "x = (e, l)" by(cases x, auto)
moreover obtain e' l' where x' [simp]: "x' = (e', l')" by(cases x', auto)
moreover obtain E T where i [simp]: "i = (E, T)" by(cases i, auto)
ultimately have sconf_type: "sconf_type_ok (E, T) t (e, l) m"
and red: "P,t ⊢ ⟨e, (m, l)⟩ -ta→ ⟨e', (m', l')⟩" by auto
from sconf_type have sconf: "E ⊢ (m, l) √" and "type_ok P (E, T) e m" and tconf: "P,m ⊢ t √t"
by(auto simp add: sconf_type_ok_def)
then obtain T' where "P,E,m ⊢ e : T'" "P ⊢ T' ≤ T" by(auto simp add: type_ok_def)
from ‹E ⊢ (m, l) √› ‹P,E,m ⊢ e : T'› red tconf
have "E ⊢ (m', l') √" by(auto elim: red_preserves_sconf)
moreover
from red ‹P,E,m ⊢ e : T'› wf ‹E ⊢ (m, l) √› tconf
obtain T'' where "P,E,m' ⊢ e' : T''" "P ⊢ T'' ≤ T'"
by(auto dest: subject_reduction)
note ‹P,E,m' ⊢ e' : T''›
moreover
from ‹P ⊢ T'' ≤ T'› ‹P ⊢ T' ≤ T›
have "P ⊢ T'' ≤ T" by(rule widen_trans)
moreover from mred tconf have "P,m' ⊢ t √t" by(rule red_tconf.preserves_red)
ultimately have "sconf_type_ok (E, T) t (e', l') m'"
by(auto simp add: sconf_type_ok_def type_ok_def)
thus "sconf_type_ok i t x' m'" by simp
next
fix t x m ta x' m' i t'' x''
assume mred: "mred P t (x, m) ta (x', m')"
and "sconf_type_ok i t x m"
and "NewThread t'' x'' m' ∈ set ⦃ta⦄⇘t⇙"
moreover obtain e l where x [simp]: "x = (e, l)" by(cases x, auto)
moreover obtain e' l' where x' [simp]: "x' = (e', l')" by(cases x', auto)
moreover obtain E T where i [simp]: "i = (E, T)" by(cases i, auto)
moreover obtain e'' l'' where x'' [simp]: "x'' = (e'', l'')" by(cases x'', auto)
ultimately have sconf_type: "sconf_type_ok (E, T) t (e, l) m"
and red: "P,t ⊢ ⟨e, (m, l)⟩ -ta→ ⟨e', (m', l')⟩"
and nt: "NewThread t'' (e'', l'') m' ∈ set ⦃ta⦄⇘t⇙" by auto
from sconf_type have sconf: "E ⊢ (m, l) √" and "type_ok P (E, T) e m" and tconf: "P,m ⊢ t √t"
by(auto simp add: sconf_type_ok_def)
then obtain T' where "P,E,m ⊢ e : T'" "P ⊢ T' ≤ T" by(auto simp add: type_ok_def)
from nt ‹P,E,m ⊢ e : T'› red have "∃E T. P,E,m' ⊢ e'' : T ∧ P,m' ⊢ l'' (:≤) E"
by(fastforce dest: red_type_newthread[OF wf])
then obtain E'' T'' where "P,E'',m' ⊢ e'' : T''" "P,m' ⊢ l'' (:≤) E''" by blast
moreover
from sconf red ‹P,E,m ⊢ e : T'› tconf have "E ⊢ (m', l') √"
by(auto intro: red_preserves_sconf)
moreover from mred tconf ‹NewThread t'' x'' m' ∈ set ⦃ta⦄⇘t⇙› have "P,m' ⊢ t'' √t"
by(rule red_tconf.preserves_NewThread)
ultimately show "∃i''. sconf_type_ok i'' t'' x'' m'"
by(auto simp add: sconf_type_ok_def type_ok_def sconf_def)
next
fix t x m ta x' m' i i'' t'' x''
assume mred: "mred P t (x, m) ta (x', m')"
and "sconf_type_ok i t x m"
and "sconf_type_ok i'' t'' x'' m"
moreover obtain e l where x [simp]: "x = (e, l)" by(cases x, auto)
moreover obtain e' l' where x' [simp]: "x' = (e', l')" by(cases x', auto)
moreover obtain E T where i [simp]: "i = (E, T)" by(cases i, auto)
moreover obtain e'' l'' where x'' [simp]: "x'' = (e'', l'')" by(cases x'', auto)
moreover obtain E'' T'' where i'' [simp]: "i'' = (E'', T'')" by(cases i'', auto)
ultimately have sconf_type: "sconf_type_ok (E, T) t (e, l) m"
and red: "P,t ⊢ ⟨e, (m, l)⟩ -ta→ ⟨e', (m', l')⟩"
and sc: "sconf_type_ok (E'', T'') t'' (e'', l'') m" by auto
from sconf_type obtain T' where "P,E,m ⊢ e : T'" and "P,m ⊢ t √t"
by(auto simp add: sconf_type_ok_def type_ok_def)
from sc have sconf: "E'' ⊢ (m, l'') √" and "type_ok P (E'', T'') e'' m" and "P,m ⊢ t'' √t"
by(auto simp add: sconf_type_ok_def)
then obtain T''' where "P,E'',m ⊢ e'' : T'''" "P ⊢ T''' ≤ T''" by(auto simp add: type_ok_def)
moreover from red ‹P,E'',m ⊢ e'' : T'''› have "P,E'',m' ⊢ e'' : T'''"
by(rule red_preserve_welltype)
moreover from sconf red ‹P,E,m ⊢ e : T'› have "hconf m'"
unfolding sconf_def by(auto dest: red_preserves_hconf)
moreover {
from red have "hext m m'" by(auto dest: red_hext_incr)
moreover from sconf have "P,m ⊢ l'' (:≤) E''" "preallocated m"
by(simp_all add: sconf_def)
ultimately have "P,m' ⊢ l'' (:≤) E''" "preallocated m'"
by(blast intro: lconf_hext preallocated_hext)+ }
moreover from mred ‹P,m ⊢ t √t› ‹P,m ⊢ t'' √t›
have "P,m' ⊢ t'' √t" by(rule red_tconf.preserves_other)
ultimately have "sconf_type_ok (E'', T'') t'' (e'', l'') m'"
by(auto simp add: sconf_type_ok_def sconf_def type_ok_def)
thus "sconf_type_ok i'' t'' x'' m'" by simp
qed
end
subsection ‹@{term "wf_red"}›
context J_progress begin
context begin
declare red_mthr.actions_ok_iff [simp del]
declare red_mthr.actions_ok.cases [rule del]
declare red_mthr.actions_ok.intros [rule del]
lemma assumes wf: "wf_prog wf_md P"
shows red_wf_red_aux:
"⟦ P,t ⊢ ⟨e, s⟩ -ta→ ⟨e',s'⟩; ¬ red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta;
sync_ok e; hconf (hp s); P,hp s ⊢ t √t;
∀l. has_locks (ls $ l) t ≥ expr_locks e l;
ws t = None ∨
(∃a vs w T Ts Tr D. call e = ⌊(a, wait, vs)⌋ ∧ typeof_addr (hp s) a = ⌊T⌋ ∧ P ⊢ class_type_of T sees wait: Ts→Tr = Native in D ∧ ws t = ⌊PostWS w⌋) ⟧
⟹ ∃e'' s'' ta'. P,t ⊢ ⟨e, s⟩ -ta'→ ⟨e'',s''⟩ ∧
(red_mthr.actions_ok (ls, (ts, m), ws, is) t ta' ∨
red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta' ∧ red_mthr.actions_subset ta' ta)"
(is "⟦ _; _; _; _; _; _; ?wakeup e s ⟧ ⟹ ?concl e s ta")
and reds_wf_red_aux:
"⟦ P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es',s'⟩; ¬ red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta;
sync_oks es; hconf (hp s); P,hp s ⊢ t √t;
∀l. has_locks (ls $ l) t ≥ expr_lockss es l;
ws t = None ∨
(∃a vs w T Ts T Tr D. calls es = ⌊(a, wait, vs)⌋ ∧ typeof_addr (hp s) a = ⌊T⌋ ∧ P ⊢ class_type_of T sees wait: Ts→Tr = Native in D ∧ ws t = ⌊PostWS w⌋) ⟧
⟹ ∃es'' s'' ta'. P,t ⊢ ⟨es, s⟩ [-ta'→] ⟨es'',s''⟩ ∧
(red_mthr.actions_ok (ls, (ts, m), ws, is) t ta' ∨
red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta' ∧ red_mthr.actions_subset ta' ta)"
proof(induct rule: red_reds.inducts)
case (SynchronizedRed2 e s ta e' s' a)
note IH = ‹⟦¬ red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta; sync_ok e; hconf (hp s); P,hp s ⊢ t √t;
∀l. expr_locks e l ≤ has_locks (ls $ l) t; ?wakeup e s⟧
⟹ ?concl e s ta›
note ‹¬ red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta›
moreover from ‹sync_ok (insync(a) e)› have "sync_ok e" by simp
moreover note ‹hconf (hp s)› ‹P,hp s ⊢ t √t›
moreover from ‹∀l. expr_locks (insync(a) e) l ≤ has_locks (ls $ l) t›
have "∀l. expr_locks e l ≤ has_locks (ls $ l) t" by(force split: if_split_asm)
moreover from ‹?wakeup (insync(a) e) s› have "?wakeup e s" by auto
ultimately have "?concl e s ta" by(rule IH)
thus ?case by(fastforce intro: red_reds.SynchronizedRed2)
next
case RedCall thus ?case
by(auto simp add: is_val_iff contains_insync_conv contains_insyncs_conv red_mthr.actions_ok'_empty red_mthr.actions_ok'_ta_upd_obs dest: sees_method_fun)
next
case (RedCallExternal s a U M Ts T D vs ta va h' ta' e' s')
from ‹?wakeup (addr a∙M(map Val vs)) s›
have "wset (ls, (ts, m), ws, is) t = None ∨ (M = wait ∧ (∃w. wset (ls, (ts, m), ws, is) t = ⌊PostWS w⌋))" by auto
with wf ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va, h'⟩› ‹P,hp s ⊢ t √t› ‹hconf (hp s)›
obtain ta'' va' h'' where red': "P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta''→ext ⟨va',h''⟩"
and aok: "red_mthr.actions_ok (ls, (ts, m), ws, is) t ta'' ∨
red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta'' ∧ final_thread.actions_subset ta'' ta"
by(rule red_external_wf_red)
from aok ‹ta' = extTA2J P ta›
have "red_mthr.actions_ok (ls, (ts, m), ws, is) t (extTA2J P ta'') ∨
red_mthr.actions_ok' (ls, (ts, m), ws, is) t (extTA2J P ta'') ∧ red_mthr.actions_subset (extTA2J P ta'') ta'"
by(auto simp add: red_mthr.actions_ok'_convert_extTA red_mthr.actions_ok_iff elim: final_thread.actions_subset.cases del: subsetI)
moreover from red' ‹typeof_addr (hp s) a = ⌊U⌋› ‹P ⊢ class_type_of U sees M: Ts→T = Native in D›
obtain s'' e'' where "P,t ⊢ ⟨addr a∙M(map Val vs),s⟩ -extTA2J P ta''→ ⟨e'',s''⟩"
by(fastforce intro: red_reds.RedCallExternal)
ultimately show ?case by blast
next
case LockSynchronized
hence False by(auto simp add: lock_ok_las'_def finfun_upd_apply ta_upd_simps)
thus ?case ..
next
case (UnlockSynchronized a v s)
from ‹∀l. expr_locks (insync(a) Val v) l ≤ has_locks (ls $ l) t›
have "has_lock (ls $ a) t" by(force split: if_split_asm)
with UnlockSynchronized have False by(auto simp add: lock_ok_las'_def finfun_upd_apply ta_upd_simps)
thus ?case ..
next
case (SynchronizedThrow2 a ad s)
from ‹∀l. expr_locks (insync(a) Throw ad) l ≤ has_locks (ls $ l) t›
have "has_lock (ls $ a) t" by(force split: if_split_asm)
with SynchronizedThrow2 have False
by(auto simp add: lock_ok_las'_def finfun_upd_apply ta_upd_simps)
thus ?case ..
next
case BlockRed thus ?case by(simp)(blast intro: red_reds.intros)
qed
(simp_all add: is_val_iff contains_insync_conv contains_insyncs_conv red_mthr.actions_ok'_empty
red_mthr.actions_ok'_ta_upd_obs thread_action'_to_thread_action.simps red_mthr.actions_ok_iff
split: if_split_asm del: split_paired_Ex,
(blast intro: red_reds.intros elim: add_leE)+)
end
end
context J_heap_base begin
lemma shows red_ta_satisfiable:
"P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ ∃s. red_mthr.actions_ok s t ta"
and reds_ta_satisfiable:
"P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ ∃s. red_mthr.actions_ok s t ta"
apply(induct rule: red_reds.inducts)
apply(fastforce simp add: lock_ok_las_def finfun_upd_apply intro: exI[where x="K$ None"] exI[where x="K$ ⌊(t, 0)⌋"] may_lock.intros dest: red_external_ta_satisfiable[where final="final_expr :: ('addr expr × 'addr locals) ⇒ bool"])+
done
end
context J_typesafe begin
lemma wf_progress:
assumes wf: "wf_J_prog P"
shows "progress final_expr (mred P)
(red_mthr.wset_Suspend_ok P ({s. sync_es_ok (thr s) (shr s) ∧ lock_ok (locks s) (thr s)} ∩ {s. ∃Es. sconf_type_ts_ok Es (thr s) (shr s)} ∩ {s. def_ass_ts_ok (thr s) (shr s)}))"
(is "progress _ _ ?wf_state")
proof
{
fix s t x ta x' m' w
assume "mred P t (x, shr s) ta (x', m')"
and Suspend: "Suspend w ∈ set ⦃ta⦄⇘w⇙"
moreover obtain e xs where x: "x = (e, xs)" by(cases x)
moreover obtain e' xs' where x': "x' = (e', xs')" by(cases x')
ultimately have red: "P,t ⊢ ⟨e, (shr s, xs)⟩ -ta→ ⟨e', (m', xs')⟩" by simp
from red_Suspend_is_call[OF red Suspend]
show "¬ final_expr x'" by(auto simp add: x')
}
note Suspend_final = this
{
fix s
assume s: "s ∈ ?wf_state"
hence "lock_thread_ok (locks s) (thr s)"
by(auto dest: red_mthr.wset_Suspend_okD1 intro: lock_ok_lock_thread_ok)
moreover
have "red_mthr.wset_final_ok (wset s) (thr s)"
proof(rule red_mthr.wset_final_okI)
fix t w
assume "wset s t = ⌊w⌋"
from red_mthr.wset_Suspend_okD2[OF s this]
obtain x0 ta x m1 w' ln'' and s0 :: "('addr, 'thread_id, 'heap) J_state"
where mred: "mred P t (x0, shr s0) ta (x, m1)"
and Suspend: "Suspend w' ∈ set ⦃ta⦄⇘w⇙"
and tst: "thr s t = ⌊(x, ln'')⌋" by blast
from Suspend_final[OF mred Suspend] tst
show " ∃x ln. thr s t = ⌊(x, ln)⌋ ∧ ¬ final_expr x" by blast
qed
ultimately show "lock_thread_ok (locks s) (thr s) ∧ red_mthr.wset_final_ok (wset s) (thr s)" ..
}
next
fix s t ex ta e'x' m'
assume wfs: "s ∈ ?wf_state"
and "thr s t = ⌊(ex, no_wait_locks)⌋"
and "mred P t (ex, shr s) ta (e'x', m')"
and wait: "¬ waiting (wset s t)"
moreover obtain ls ts m ws "is" where s: "s = (ls, (ts, m), ws, is)" by(cases s) fastforce
moreover obtain e x where ex: "ex = (e, x)" by(cases ex)
moreover obtain e' x' where e'x': "e'x' = (e', x')" by(cases e'x')
ultimately have tst: "ts t = ⌊(ex, no_wait_locks)⌋"
and red: "P,t ⊢ ⟨e, (m, x)⟩ -ta→ ⟨e', (m', x')⟩" by auto
from wf have wwf: "wwf_J_prog P" by(rule wf_prog_wwf_prog)
from wfs s obtain Es where aeos: "sync_es_ok ts m"
and lockok: "lock_ok ls ts"
and "sconf_type_ts_ok Es ts m"
by(auto dest: red_mthr.wset_Suspend_okD1)
with tst ex obtain E T where sconf: "sconf_type_ok (E, T) t (e, x) m"
and aoe: "sync_ok e" by(fastforce dest: ts_okD ts_invD)
then obtain T' where "hconf m" "P,E,m ⊢ e : T'" "preallocated m"
by(auto simp add: sconf_type_ok_def sconf_def type_ok_def)
from ‹sconf_type_ts_ok Es ts m› s have "thread_conf P (thr s) (shr s)"
by(auto dest: ts_invD intro!: ts_okI simp add: sconf_type_ok_def)
with ‹thr s t = ⌊(ex, no_wait_locks)⌋› have "P,shr s ⊢ t √t" by(auto dest: ts_okD)
show "∃ta' x' m'. mred P t (ex, shr s) ta' (x', m') ∧
(red_mthr.actions_ok s t ta' ∨ red_mthr.actions_ok' s t ta' ∧ red_mthr.actions_subset ta' ta)"
proof(cases "red_mthr.actions_ok' s t ta")
case True
have "red_mthr.actions_subset ta ta" ..
with True ‹mred P t (ex, shr s) ta (e'x', m')› show ?thesis by blast
next
case False
from lock_okD2[OF lockok, OF tst[unfolded ex]]
have locks: "∀l. has_locks (ls $ l) t ≥ expr_locks e l" by simp
have "ws t = None ∨ (∃a vs w T Ts Tr D. call e = ⌊(a, wait, vs)⌋ ∧ typeof_addr (hp (m, x)) a = ⌊T⌋ ∧ P ⊢ class_type_of T sees wait: Ts→Tr = Native in D ∧ ws t = ⌊PostWS w⌋)"
proof(cases "ws t")
case None thus ?thesis ..
next
case (Some w)
with red_mthr.wset_Suspend_okD2[OF wfs, of t w] tst ex s
obtain e0 x0 m0 ta0 w' s1 tta1
where red0: "P,t ⊢ ⟨e0, (m0, x0)⟩ -ta0→ ⟨e, (shr s1, x)⟩"
and Suspend: "Suspend w' ∈ set ⦃ta0⦄⇘w⇙"
and s1: "P ⊢ s1 -▹tta1→* s" by auto
from red_Suspend_is_call[OF red0 Suspend] obtain a vs T Ts Tr D
where call: "call e = ⌊(a, wait, vs)⌋"
and type: "typeof_addr m0 a = ⌊T⌋"
and iec: "P ⊢ class_type_of T sees wait: Ts→Tr = Native in D" by fastforce
from red0 have "m0 ⊴ shr s1" by(auto dest: red_hext_incr)
also from s1 have "shr s1 ⊴ shr s" by(rule RedT_hext_incr)
finally have "typeof_addr (shr s) a = ⌊T⌋" using type
by(rule typeof_addr_hext_mono)
moreover from Some wait s obtain w' where "ws t = ⌊PostWS w'⌋"
by(auto simp add: not_waiting_iff)
ultimately show ?thesis using call iec s by auto
qed
from red_wf_red_aux[OF wf red False[unfolded s] aoe _ _ locks, OF _ _ this] ‹hconf m› ‹P,shr s ⊢ t √t› ex s
show ?thesis by fastforce
qed
next
fix s t x
assume wfs: "s ∈ ?wf_state"
and tst: "thr s t = ⌊(x, no_wait_locks)⌋"
and nfin: "¬ final_expr x"
obtain e xs where x: "x = (e, xs)" by(cases x)
from wfs have "def_ass_ts_ok (thr s) (shr s)" by(auto dest: red_mthr.wset_Suspend_okD1)
with tst x have DA: "𝒟 e ⌊dom xs⌋" by(auto dest: ts_okD)
from wfs obtain Es where "sconf_type_ts_ok Es (thr s) (shr s)"
by(auto dest: red_mthr.wset_Suspend_okD1)
with tst x obtain E T where "sconf_type_ok (E, T) t (e, xs) (shr s)" by(auto dest: ts_invD)
then obtain T' where "hconf (shr s)" "P,E,shr s ⊢ e : T'"
by(auto simp add: sconf_type_ok_def sconf_def type_ok_def)
from red_progress(1)[OF wf_prog_wwf_prog[OF wf] this DA, where extTA="extTA2J P" and t=t] nfin x
show "∃ta x' m'. mred P t (x, shr s) ta (x', m')" by fastforce
next
fix s t x xm ta xm'
assume "s ∈ ?wf_state"
and "thr s t = ⌊(x, no_wait_locks)⌋"
and "mred P t xm ta xm'"
and "Notified ∈ set ⦃ta⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta⦄⇘w⇙"
thus "collect_waits ta = {}"
by(auto dest: red_ta_Wakeup_no_Join_no_Lock_no_Interrupt simp: split_beta)
next
fix s t x ta x' m'
assume "s ∈ ?wf_state"
and "thr s t = ⌊(x, no_wait_locks)⌋"
and "mred P t (x, shr s) ta (x', m')"
thus "∃s'. red_mthr.actions_ok s' t ta"
by(fastforce simp add: split_beta dest!: red_ta_satisfiable)
qed
lemma redT_progress_deadlock:
assumes wf: "wf_J_prog P"
and wf_start: "wf_start_state P C M vs"
and Red: "P ⊢ J_start_state P C M vs -▹ttas→* s"
and ndead: "¬ red_mthr.deadlock P s"
shows "∃t' ta' s'. P ⊢ s -t'▹ta'→ s'"
proof -
let ?wf_state = "red_mthr.wset_Suspend_ok P ({s. sync_es_ok (thr s) (shr s) ∧ lock_ok (locks s) (thr s)} ∩ {s. ∃Es. sconf_type_ts_ok Es (thr s) (shr s)} ∩ {s. def_ass_ts_ok (thr s) (shr s)})"
interpret red_mthr: progress
final_expr "mred P" convert_RA ?wf_state
using wf by(rule wf_progress)
from wf_start obtain Ts T pns body D
where start: "start_heap_ok" "P ⊢ C sees M:Ts→T = ⌊(pns, body)⌋ in D" "P,start_heap ⊢ vs [:≤] Ts"
by(cases) auto
from start have len: "length Ts = length vs" by(auto dest: list_all2_lengthD)
have "invariant3p (mredT P) ?wf_state"
by(rule red_mthr.invariant3p_wset_Suspend_ok) (intro invariant3p_IntI invariant3p_sync_es_ok_lock_ok[OF wf] lifting_inv.invariant3p_ts_inv[OF lifting_inv_sconf_subject_ok[OF wf]] lifting_wf.invariant3p_ts_ok[OF lifting_wf_def_ass[OF wf]])
moreover note Red moreover
have start': "J_start_state P C M vs ∈ ?wf_state"
apply(rule red_mthr.wset_Suspend_okI)
apply(blast intro: sconf_type_ts_ok_J_start_state sync_es_ok_J_start_state lock_ok_J_start_state def_ass_ts_ok_J_start_state start wf len len[symmetric] wf_start)
apply(simp add: start_state_def split_beta)
done
ultimately have "s ∈ ?wf_state" unfolding red_mthr.RedT_def
by(rule invariant3p_rtrancl3p)
thus ?thesis using ndead by(rule red_mthr.redT_progress)
qed
lemma redT_progress_deadlocked:
assumes wf: "wf_J_prog P"
and wf_start: "wf_start_state P C M vs"
and Red: "P ⊢ J_start_state P C M vs -▹ttas→* s"
and ndead: "red_mthr.not_final_thread s t" "¬ t ∈ red_mthr.deadlocked P s"
shows "∃t' ta' s'. P ⊢ s -t'▹ta'→ s'"
using wf wf_start Red
proof(rule redT_progress_deadlock)
from ndead show "¬ red_mthr.deadlock P s"
unfolding red_mthr.deadlock_eq_deadlocked'
by(auto simp add: red_mthr.deadlocked'_def)
qed
subsection ‹Type safety proof›
theorem TypeSafetyT:
fixes C and M and ttas and Es
defines "Es == J_sconf_type_ET_start P C M"
and "Es' == upd_invs Es sconf_type_ok (concat (map (thr_a ∘ snd) ttas))"
assumes wf: "wf_J_prog P"
and start_wf: "wf_start_state P C M vs"
and RedT: "P ⊢ J_start_state P C M vs -▹ttas→* s'"
and nored: "¬ (∃t ta s''. P ⊢ s' -t▹ta→ s'')"
shows "thread_conf P (thr s') (shr s')"
and "thr s' t = ⌊((e', x'), ln')⌋ ⟹
(∃v. e' = Val v ∧ (∃E T. Es' t = ⌊(E, T)⌋ ∧ P,shr s' ⊢ v :≤ T) ∧ ln' = no_wait_locks)
∨ (∃a C. e' = Throw a ∧ typeof_addr (shr s') a = ⌊Class_type C⌋ ∧ P ⊢ C ≼⇧* Throwable ∧ ln' = no_wait_locks)
∨ (t ∈ red_mthr.deadlocked P s' ∧ (∃E T. Es' t = ⌊(E, T)⌋ ∧ (∃T'. P,E,shr s' ⊢ e' : T' ∧ P ⊢ T' ≤ T)))"
(is "_ ⟹ ?thesis2")
and "Es ⊆⇩m Es'"
proof -
from start_wf obtain Ts T pns body D
where start_heap: "start_heap_ok"
and sees: "P ⊢ C sees M:Ts→T = ⌊(pns, body)⌋ in D"
and conf: "P,start_heap ⊢ vs [:≤] Ts"
by cases auto
from RedT show "thread_conf P (thr s') (shr s')"
by(rule red_tconf.RedT_preserves)(rule thread_conf_start_state[OF start_heap wf_prog_wf_syscls[OF wf]])
show "Es ⊆⇩m Es'" using RedT ts_inv_ok_J_sconf_type_ET_start
unfolding Es'_def Es_def by(rule red_mthr.RedT_upd_inv_ext)
assume "thr s' t = ⌊((e', x'), ln')⌋"
moreover obtain ls' ts' m' ws' is' where s' [simp]: "s' = (ls', (ts', m'), ws', is')" by(cases s') fastforce
ultimately have es't: "ts' t = ⌊((e', x'), ln')⌋" by simp
from wf have wwf: "wwf_J_prog P" by(rule wf_prog_wwf_prog)
from conf have len: "length vs = length Ts" by(rule list_all2_lengthD)
from RedT def_ass_ts_ok_J_start_state[OF wf sees len] have defass': "def_ass_ts_ok ts' m'"
by(fastforce dest: lifting_wf.RedT_preserves[OF lifting_wf_def_ass, OF wf])
from RedT sync_es_ok_J_start_state[OF wf sees len[symmetric]] lock_ok_J_start_state[OF wf sees len[symmetric]]
have lock': "lock_ok ls' ts'" by (fastforce dest: RedT_preserves_lock_ok[OF wf])
from RedT sync_es_ok_J_start_state[OF wf sees len[symmetric]] have addr': "sync_es_ok ts' m'"
by(fastforce dest: RedT_preserves_sync_ok[OF wf])
from RedT sconf_type_ts_ok_J_start_state[OF wf start_wf]
have sconf_subject': "sconf_type_ts_ok Es' ts' m'" unfolding Es'_def Es_def
by(fastforce dest: lifting_inv.RedT_invariant[OF lifting_inv_sconf_subject_ok, OF wf] intro: thread_conf_start_state[OF _ wf_prog_wf_syscls[OF wf]])
with es't obtain E T where ET: "Es' t = ⌊(E, T)⌋"
and "sconf_type_ok (E, T) t (e', x') m'" by(auto dest!: ts_invD)
{ assume "final e'"
have "ln' = no_wait_locks"
proof(rule ccontr)
assume "ln' ≠ no_wait_locks"
then obtain l where "ln' $ l > 0"
by(auto simp add: neq_no_wait_locks_conv)
from lock' es't have "has_locks (ls' $ l) t + ln' $ l = expr_locks e' l"
by(auto dest: lock_okD2)
with ‹ln' $ l > 0› have "expr_locks e' l > 0" by simp
moreover from ‹final e'› have "expr_locks e' l = 0" by(rule final_locks)
ultimately show False by simp
qed }
note ln' = this
{ assume "∃v. e' = Val v"
then obtain v where v: "e' = Val v" by blast
with sconf_subject' ET es't have "P,m' ⊢ v :≤ T"
by(auto dest: ts_invD simp add: type_ok_def sconf_type_ok_def conf_def)
moreover from v ln' have "ln' = no_wait_locks" by(auto)
ultimately have "∃v. e' = Val v ∧ (∃E T. Es' t = ⌊(E, T)⌋ ∧ P,m' ⊢ v :≤ T ∧ ln' = no_wait_locks)"
using ET v by blast }
moreover
{ assume "∃a. e' = Throw a"
then obtain a where a: "e' = Throw a" by blast
with sconf_subject' ET es't have "∃T'. P,E,m' ⊢ e' : T' ∧ P ⊢ T' ≤ T"
apply -
apply(drule ts_invD, assumption)
by(clarsimp simp add: type_ok_def sconf_type_ok_def)
then obtain T' where "P,E,m' ⊢ e' : T'" and "P ⊢ T' ≤ T" by blast
with a have "∃C. typeof_addr m' a = ⌊Class_type C⌋ ∧ P ⊢ C ≼⇧* Throwable"
by(auto simp add: widen_Class)
moreover from a ln' have "ln' = no_wait_locks" by(auto)
ultimately have "∃a C. e' = Throw a ∧ typeof_addr m' a = ⌊Class_type C⌋ ∧ P ⊢ C ≼⇧* Throwable ∧ ln' = no_wait_locks"
using a by blast }
moreover
{ assume nfine': "¬ final e'"
with es't have "red_mthr.not_final_thread s' t"
by(auto intro: red_mthr.not_final_thread.intros)
with nored have "t ∈ red_mthr.deadlocked P s'"
by -(erule contrapos_np, rule redT_progress_deadlocked[OF wf start_wf RedT])
moreover
from ‹sconf_type_ok (E, T) t (e', x') m'›
obtain T'' where "P,E,m' ⊢ e' : T''" "P ⊢ T'' ≤ T"
by(auto simp add: sconf_type_ok_def type_ok_def)
with ET have "∃E T. Es' t = ⌊(E, T)⌋ ∧ (∃T'. P,E,m' ⊢ e' : T' ∧ P ⊢ T' ≤ T)"
by blast
ultimately have "t ∈ red_mthr.deadlocked P s' ∧ (∃E T. Es' t = ⌊(E, T)⌋ ∧ (∃T'. P,E,m' ⊢ e' : T' ∧ P ⊢ T' ≤ T))" .. }
ultimately show ?thesis2 by simp(blast)
qed
end
end