Theory Deadlocked
section ‹Preservation of Deadlock›
theory Deadlocked
imports
ProgressThreaded
begin
context J_progress begin
lemma red_wt_hconf_hext:
assumes wf: "wf_J_prog P"
and hconf: "hconf H"
and tconf: "P,H ⊢ t √t"
shows "⟦ convert_extTA extNTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; P,E,H ⊢ e : T; hext H (hp s) ⟧
⟹ ∃ta' e' s'. convert_extTA extNTA,P,t ⊢ ⟨e, (H, lcl s)⟩ -ta'→ ⟨e', s'⟩ ∧
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⇙"
and "⟦ convert_extTA extNTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; P,E,H ⊢ es [:] Ts; hext H (hp s) ⟧
⟹ ∃ta' es' s'. convert_extTA extNTA,P,t ⊢ ⟨es, (H, lcl s)⟩ [-ta'→] ⟨es', s'⟩ ∧
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⇙"
proof(induct arbitrary: E T and E Ts rule: red_reds.inducts)
case (RedNew h' a h C l)
thus ?case
by(cases "allocate H (Class_type C) = {}")(fastforce simp add: ta_upd_simps intro: RedNewFail red_reds.RedNew)+
next
case (RedNewFail h C l)
thus ?case
by(cases "allocate H (Class_type C) = {}")(fastforce simp add: ta_upd_simps intro: red_reds.RedNewFail RedNew)+
next
case NewArrayRed thus ?case by(fastforce intro: red_reds.intros)
next
case (RedNewArray i h' a h T l E T')
thus ?case
by(cases "allocate H (Array_type T (nat (sint i))) = {}")(fastforce simp add: ta_upd_simps intro: red_reds.RedNewArray RedNewArrayFail)+
next
case RedNewArrayNegative thus ?case by(fastforce intro: red_reds.intros)
next
case (RedNewArrayFail i h T l E T')
thus ?case
by(cases "allocate H (Array_type T (nat (sint i))) = {}")(fastforce simp add: ta_upd_simps intro: RedNewArray red_reds.RedNewArrayFail)+
next
case CastRed thus ?case by(fastforce intro: red_reds.intros)
next
case (RedCast s v U T E T')
from ‹P,E,H ⊢ Cast T (Val v) : T'› show ?case
proof(rule WTrt_elim_cases)
fix T''
assume wt: "P,E,H ⊢ Val v : T''" "T' = T"
thus ?thesis
by(cases "P ⊢ T'' ≤ T")(fastforce intro: red_reds.RedCast red_reds.RedCastFail)+
qed
next
case (RedCastFail s v U T E T')
from ‹P,E,H ⊢ Cast T (Val v) : T'›
obtain T'' where "P,E,H ⊢ Val v : T''" "T = T'" by auto
thus ?case
by(cases "P ⊢ T'' ≤ T")(fastforce intro: red_reds.RedCast red_reds.RedCastFail)+
next
case InstanceOfRed thus ?case by(fastforce intro: red_reds.intros)
next
case RedInstanceOf thus ?case
using [[hypsubst_thin = true]]
by auto((rule exI conjI red_reds.RedInstanceOf)+, auto)
next
case BinOpRed1 thus ?case by(fastforce intro: red_reds.intros)
next
case BinOpRed2 thus ?case by(fastforce intro: red_reds.intros)
next
case RedBinOp thus ?case by(fastforce intro: red_reds.intros)
next
case RedBinOpFail thus ?case by(fastforce intro: red_reds.intros)
next
case RedVar thus ?case by(fastforce intro: red_reds.intros)
next
case LAssRed thus ?case by(fastforce intro: red_reds.intros)
next
case RedLAss thus ?case by(fastforce intro: red_reds.intros)
next
case AAccRed1 thus ?case by(fastforce intro: red_reds.intros)
next
case AAccRed2 thus ?case by(fastforce intro: red_reds.intros)
next
case RedAAccNull thus ?case by(fastforce intro: red_reds.intros)
next
case RedAAccBounds thus ?case
by(fastforce intro: red_reds.RedAAccBounds dest: hext_arrD)
next
case (RedAAcc h a T n i v l E T')
from ‹P,E,H ⊢ addr a⌊Val (Intg i)⌉ : T'›
have wt: "P,E,H ⊢ addr a : T'⌊⌉" by(auto)
with ‹H ⊴ hp (h, l)› ‹typeof_addr h a = ⌊Array_type T n⌋›
have Ha: "typeof_addr H a = ⌊Array_type T n⌋" by(auto dest: hext_arrD)
with ‹0 <=s i› ‹sint i < int n›
have "nat (sint i) < n"
by (simp add: word_sle_eq nat_less_iff)
with Ha have "P,H ⊢ a@ACell (nat (sint i)) : T"
by(auto intro: addr_loc_type.intros)
from heap_read_total[OF hconf this]
obtain v where "heap_read H a (ACell (nat (sint i))) v" by blast
with Ha ‹0 <=s i› ‹sint i < int n› show ?case
by(fastforce intro: red_reds.RedAAcc simp add: ta_upd_simps)
next
case AAssRed1 thus ?case by(fastforce intro: red_reds.intros)
next
case AAssRed2 thus ?case by(fastforce intro: red_reds.intros)
next
case AAssRed3 thus ?case by(fastforce intro: red_reds.intros)
next
case RedAAssNull thus ?case by(fastforce intro: red_reds.intros)
next
case RedAAssBounds thus ?case by(fastforce intro: red_reds.RedAAssBounds dest: hext_arrD)
next
case (RedAAssStore s a T n i w U E T')
from ‹P,E,H ⊢ addr a⌊Val (Intg i)⌉ := Val w : T'›
obtain T'' T''' where wt: "P,E,H ⊢ addr a : T''⌊⌉"
and wtw: "P,E,H ⊢ Val w : T'''" by auto
with ‹H ⊴ hp s› ‹typeof_addr (hp s) a = ⌊Array_type T n⌋›
have Ha: "typeof_addr H a = ⌊Array_type T n⌋" by(auto dest: hext_arrD)
from ‹typeof⇘hp s⇙ w = ⌊U⌋› wtw ‹H ⊴ hp s› have "typeof⇘H⇙ w = ⌊U⌋"
by(auto dest: type_of_hext_type_of)
with Ha ‹0 <=s i› ‹sint i < int n› ‹¬ P ⊢ U ≤ T› show ?case
by(fastforce intro: red_reds.RedAAssStore)
next
case (RedAAss h a T n i w U h' l E T')
from ‹P,E,H ⊢ addr a⌊Val (Intg i)⌉ := Val w : T'›
obtain T'' T''' where wt: "P,E,H ⊢ addr a : T''⌊⌉"
and wtw: "P,E,H ⊢ Val w : T'''" by auto
with ‹H ⊴ hp (h, l)› ‹typeof_addr h a = ⌊Array_type T n⌋›
have Ha: "typeof_addr H a = ⌊Array_type T n⌋" by(auto dest: hext_arrD)
from ‹typeof⇘h⇙ w = ⌊U⌋› wtw ‹H ⊴ hp (h, l)› have "typeof⇘H⇙ w = ⌊U⌋"
by(auto dest: type_of_hext_type_of)
moreover
with ‹P ⊢ U ≤ T› have conf: "P,H ⊢ w :≤ T"
by(auto simp add: conf_def)
from ‹0 <=s i› ‹sint i < int n›
have "nat (sint i) < n"
by (simp add: word_sle_eq nat_less_iff)
with Ha have "P,H ⊢ a@ACell (nat (sint i)) : T"
by(auto intro: addr_loc_type.intros)
from heap_write_total[OF hconf this conf]
obtain H' where "heap_write H a (ACell (nat (sint i))) w H'" ..
ultimately show ?case using ‹0 <=s i› ‹sint i < int n› Ha ‹P ⊢ U ≤ T›
by(fastforce simp del: split_paired_Ex intro: red_reds.RedAAss)
next
case ALengthRed thus ?case by(fastforce intro: red_reds.intros)
next
case (RedALength h a T n l E T')
from ‹P,E,H ⊢ addr a∙length : T'›
obtain T'' where [simp]: "T' = Integer"
and wta: "P,E,H ⊢ addr a : T''⌊⌉" by(auto)
then obtain n'' where "typeof_addr H a = ⌊Array_type T'' n''⌋" by(auto)
thus ?case by(fastforce intro: red_reds.RedALength)
next
case RedALengthNull show ?case by(fastforce intro: red_reds.RedALengthNull)
next
case FAccRed thus ?case by(fastforce intro: red_reds.intros)
next
case (RedFAcc h a D F v l E T)
from ‹P,E,H ⊢ addr a∙F{D} : T› obtain U C' fm
where wt: "P,E,H ⊢ addr a : U"
and icto: "class_type_of' U = ⌊C'⌋"
and has: "P ⊢ C' has F:T (fm) in D"
by(auto)
then obtain hU where Ha: "typeof_addr H a = ⌊hU⌋" "U = ty_of_htype hU" by(auto)
with icto ‹P ⊢ C' has F:T (fm) in D› have "P,H ⊢ a@CField D F : T"
by(auto intro: addr_loc_type.intros)
from heap_read_total[OF hconf this]
obtain v where "heap_read H a (CField D F) v" by blast
thus ?case by(fastforce intro: red_reds.RedFAcc simp add: ta_upd_simps)
next
case RedFAccNull thus ?case by(fastforce intro: red_reds.intros)
next
case FAssRed1 thus ?case by(fastforce intro: red_reds.intros)
next
case FAssRed2 thus ?case by(fastforce intro: red_reds.intros)
next
case RedFAssNull thus ?case by(fastforce intro: red_reds.intros)
next
case (RedFAss h a D F v h' l E T)
from ‹P,E,H ⊢ addr a∙F{D} := Val v : T› obtain U C' T' T2 fm
where wt: "P,E,H ⊢ addr a : U"
and icto: "class_type_of' U = ⌊C'⌋"
and has: "P ⊢ C' has F:T' (fm) in D"
and wtv: "P,E,H ⊢ Val v : T2"
and T2T: "P ⊢ T2 ≤ T'" by(auto)
moreover from wt obtain hU where Ha: "typeof_addr H a = ⌊hU⌋" "U = ty_of_htype hU" by(auto)
with icto has have adal: "P,H ⊢ a@CField D F : T'" by(auto intro: addr_loc_type.intros)
from wtv T2T have "P,H ⊢ v :≤ T'" by(auto simp add: conf_def)
from heap_write_total[OF hconf adal this]
obtain h' where "heap_write H a (CField D F) v h'" ..
thus ?case by(fastforce intro: red_reds.RedFAss)
next
case CASRed1 thus ?case by(fastforce intro: red_reds.intros)
next
case CASRed2 thus ?case by(fastforce intro: red_reds.intros)
next
case CASRed3 thus ?case by(fastforce intro: red_reds.intros)
next
case CASNull thus ?case by(fastforce intro: red_reds.intros)
next
case (RedCASSucceed h a D F v v' h' l)
note split_paired_Ex[simp del]
from RedCASSucceed.prems(1) obtain T' fm T2 T3 U C where *:
"T = Boolean" "class_type_of' U = ⌊C⌋" "P ⊢ C has F:T' (fm) in D"
"volatile fm" "P ⊢ T2 ≤ T'" "P ⊢ T3 ≤ T'"
"P,E,H ⊢ Val v : T2" "P,E,H ⊢ Val v' : T3" "P,E,H ⊢ addr a : U" by auto
then have adal: "P,H ⊢ a@CField D F : T'" by(auto intro: addr_loc_type.intros)
from heap_read_total[OF hconf this] obtain v'' where v': "heap_read H a (CField D F) v''" by blast
show ?case
proof(cases "v'' = v")
case True
from * have "P,H ⊢ v' :≤ T'" by(auto simp add: conf_def)
from heap_write_total[OF hconf adal this] True * v'
show ?thesis by(fastforce intro: red_reds.RedCASSucceed)
next
case False
then show ?thesis using * v' by(fastforce intro: RedCASFail)
qed
next
case (RedCASFail h a D F v'' v v' l)
note split_paired_Ex[simp del]
from RedCASFail.prems(1) obtain T' fm T2 T3 U C where *:
"T = Boolean" "class_type_of' U = ⌊C⌋" "P ⊢ C has F:T' (fm) in D"
"volatile fm" "P ⊢ T2 ≤ T'" "P ⊢ T3 ≤ T'"
"P,E,H ⊢ Val v : T2" "P,E,H ⊢ Val v' : T3" "P,E,H ⊢ addr a : U" by auto
then have adal: "P,H ⊢ a@CField D F : T'" by(auto intro: addr_loc_type.intros)
from heap_read_total[OF hconf this] obtain v''' where v'': "heap_read H a (CField D F) v'''" by blast
show ?case
proof(cases "v''' = v")
case True
from * have "P,H ⊢ v' :≤ T'" by(auto simp add: conf_def)
from heap_write_total[OF hconf adal this] True * v''
show ?thesis by(fastforce intro: red_reds.RedCASSucceed)
next
case False
then show ?thesis using * v'' by(fastforce intro: red_reds.RedCASFail)
qed
next
case CallObj thus ?case by(fastforce intro: red_reds.intros)
next
case CallParams thus ?case by(fastforce intro: red_reds.intros)
next
case (RedCall s a U M Ts T pns body D vs E T')
from ‹P,E,H ⊢ addr a∙M(map Val vs) : T'›
obtain U' C' Ts' meth D' Ts''
where wta: "P,E,H ⊢ addr a : U'"
and icto: "class_type_of' U' = ⌊C'⌋"
and sees: "P ⊢ C' sees M: Ts'→T' = meth in D'"
and wtes: "P,E,H ⊢ map Val vs [:] Ts''"
and widens: "P ⊢ Ts'' [≤] Ts'" by auto
from wta obtain hU' where Ha: "typeof_addr H a = ⌊hU'⌋" "U' = ty_of_htype hU'" by(auto)
moreover from ‹typeof_addr (hp s) a = ⌊U⌋› ‹H ⊴ hp s› Ha
have [simp]: "U = hU'" by(auto dest: typeof_addr_hext_mono)
from wtes have "length vs = length Ts''"
by(auto intro: map_eq_imp_length_eq)
moreover from widens have "length Ts'' = length Ts'"
by(auto dest: widens_lengthD)
moreover from sees icto sees ‹P ⊢ class_type_of U sees M: Ts→T = ⌊(pns, body)⌋ in D› Ha
have [simp]: "meth = ⌊(pns, body)⌋" by(auto dest: sees_method_fun)
with sees wf have "wf_mdecl wf_J_mdecl P D' (M, Ts', T', ⌊(pns, body)⌋)"
by(auto intro: sees_wf_mdecl)
hence "length pns = length Ts'" by(simp add: wf_mdecl_def)
ultimately show ?case using sees icto
by(fastforce intro: red_reds.RedCall)
next
case (RedCallExternal s a U M Ts T' D vs ta va h' ta' e' s')
from ‹P,E,H ⊢ addr a∙M(map Val vs) : T›
obtain U' C' Ts' meth D' Ts''
where wta: "P,E,H ⊢ addr a : U'" and icto: "class_type_of' U' = ⌊C'⌋"
and sees: "P ⊢ C' sees M: Ts'→T = meth in D'"
and wtvs: "P,E,H ⊢ map Val vs [:] Ts''"
and sub: "P ⊢ Ts'' [≤] Ts'" by auto
from wta ‹typeof_addr (hp s) a = ⌊U⌋› ‹hext H (hp s)› have [simp]: "U' = ty_of_htype U"
by(auto dest: typeof_addr_hext_mono)
with icto have [simp]: "C' = class_type_of U" by(auto)
from sees ‹P ⊢ class_type_of U sees M: Ts→T' = Native in D›
have [simp]: "meth = Native" by(auto dest: sees_method_fun)
with wta sees icto wtvs sub have "P,H ⊢ a∙M(vs) : T"
by(cases U)(auto 4 4 simp add: external_WT'_iff)
from red_external_wt_hconf_hext[OF wf ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩› ‹H ⊴ hp s› this tconf hconf]
wta icto sees ‹ta' = convert_extTA extNTA ta› ‹e' = extRet2J (addr a∙M(map Val vs)) va› ‹s' = (h', lcl s)›
show ?case by(cases U)(auto 4 5 intro: red_reds.RedCallExternal simp del: split_paired_Ex)
next
case RedCallNull thus ?case by(fastforce intro: red_reds.intros)
next
case (BlockRed e h l V vo ta e' h' l' T E T')
note IH = BlockRed.hyps(2)
from IH[of "E(V ↦ T)" T'] ‹P,E,H ⊢ {V:T=vo; e} : T'› ‹hext H (hp (h, l))›
show ?case by(fastforce dest: red_reds.BlockRed)
next
case RedBlock thus ?case by(fastforce intro: red_reds.intros)
next
case SynchronizedRed1 thus ?case by(fastforce intro: red_reds.intros)
next
case SynchronizedNull thus ?case by(fastforce intro: red_reds.intros)
next
case LockSynchronized thus ?case by(fastforce intro: red_reds.intros)
next
case SynchronizedRed2 thus ?case by(fastforce intro: red_reds.intros)
next
case UnlockSynchronized thus ?case by(fastforce intro: red_reds.intros)
next
case SeqRed thus ?case by(fastforce intro: red_reds.intros)
next
case RedSeq thus ?case by(fastforce intro: red_reds.intros)
next
case CondRed thus ?case by(fastforce intro: red_reds.intros)
next
case RedCondT thus ?case by(fastforce intro: red_reds.intros)
next
case RedCondF thus ?case by(fastforce intro: red_reds.intros)
next
case RedWhile thus ?case by(fastforce intro: red_reds.intros)
next
case ThrowRed thus ?case by(fastforce intro: red_reds.intros)
next
case RedThrowNull thus ?case by(fastforce intro: red_reds.intros)
next
case TryRed thus ?case by(fastforce intro: red_reds.intros)
next
case RedTry thus ?case by(fastforce intro: red_reds.intros)
next
case (RedTryCatch s a D C V e2 E T)
from ‹P,E,H ⊢ try Throw a catch(C V) e2 : T›
obtain T' where "P,E,H ⊢ addr a : T'" by auto
with ‹typeof_addr (hp s) a = ⌊Class_type D⌋› ‹hext H (hp s)›
have Ha: "typeof_addr H a = ⌊Class_type D⌋"
by(auto dest: typeof_addr_hext_mono)
with ‹P ⊢ D ≼⇧* C› show ?case
by(fastforce intro: red_reds.RedTryCatch)
next
case (RedTryFail s a D C V e2 E T)
from ‹P,E,H ⊢ try Throw a catch(C V) e2 : T›
obtain T' where "P,E,H ⊢ addr a : T'" by auto
with ‹typeof_addr (hp s) a = ⌊Class_type D⌋› ‹hext H (hp s)›
have Ha: "typeof_addr H a = ⌊Class_type D⌋"
by(auto dest: typeof_addr_hext_mono)
with ‹¬ P ⊢ D ≼⇧* C› show ?case
by(fastforce intro: red_reds.RedTryFail)
next
case ListRed1 thus ?case by(fastforce intro: red_reds.intros)
next
case ListRed2 thus ?case by(fastforce intro: red_reds.intros)
next
case NewArrayThrow thus ?case by(fastforce intro: red_reds.intros)
next
case CastThrow thus ?case by(fastforce intro: red_reds.intros)
next
case InstanceOfThrow thus ?case by(fastforce intro: red_reds.intros)
next
case BinOpThrow1 thus ?case by(fastforce intro: red_reds.intros)
next
case BinOpThrow2 thus ?case by(fastforce intro: red_reds.intros)
next
case LAssThrow thus ?case by(fastforce intro: red_reds.intros)
next
case AAccThrow1 thus ?case by(fastforce intro: red_reds.intros)
next
case AAccThrow2 thus ?case by(fastforce intro: red_reds.intros)
next
case AAssThrow1 thus ?case by(fastforce intro: red_reds.intros)
next
case AAssThrow2 thus ?case by(fastforce intro: red_reds.intros)
next
case AAssThrow3 thus ?case by(fastforce intro: red_reds.intros)
next
case ALengthThrow thus ?case by(fastforce intro: red_reds.intros)
next
case FAccThrow thus ?case by(fastforce intro: red_reds.intros)
next
case FAssThrow1 thus ?case by(fastforce intro: red_reds.intros)
next
case FAssThrow2 thus ?case by(fastforce intro: red_reds.intros)
next
case CASThrow thus ?case by(fastforce intro: red_reds.intros)
next
case CASThrow2 thus ?case by(fastforce intro: red_reds.intros)
next
case CASThrow3 thus ?case by(fastforce intro: red_reds.intros)
next
case CallThrowObj thus ?case by(fastforce intro: red_reds.intros)
next
case CallThrowParams thus ?case by(fastforce intro: red_reds.intros)
next
case BlockThrow thus ?case by(fastforce intro: red_reds.intros)
next
case SynchronizedThrow1 thus ?case by(fastforce intro: red_reds.intros)
next
case SynchronizedThrow2 thus ?case by(fastforce intro: red_reds.intros)
next
case SeqThrow thus ?case by(fastforce intro: red_reds.intros)
next
case CondThrow thus ?case by(fastforce intro: red_reds.intros)
next
case ThrowThrow thus ?case by(fastforce intro: red_reds.intros)
qed
lemma can_lock_devreserp:
"⟦ wf_J_prog P; red_mthr.can_sync P t (e, l) h' L; P,E,h ⊢ e : T; P,h ⊢ t √t; hconf h; h ⊴ h' ⟧
⟹ red_mthr.can_sync P t (e, l) h L"
apply(erule red_mthr.can_syncE)
apply(clarsimp)
apply(drule red_wt_hconf_hext, assumption+)
apply(simp)
apply(fastforce intro!: red_mthr.can_syncI)
done
end
context J_typesafe begin
lemma preserve_deadlocked:
assumes wf: "wf_J_prog P"
shows "preserve_deadlocked final_expr (mred P) convert_RA ({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 "preserve_deadlocked _ _ _ ?wf_state")
proof(unfold_locales)
show inv: "invariant3p (mredT P) ?wf_state"
by(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]])
fix s t' ta' s' t x ln
assume wfs: "s ∈ ?wf_state"
and redT: "P ⊢ s -t'▹ta'→ s'"
and tst: "thr s t = ⌊(x, ln)⌋"
from redT have hext: "shr s ⊴ shr s'" by(rule redT_hext_incr)
from inv redT wfs have wfs': "s' ∈ ?wf_state" by(rule invariant3pD)
from redT tst obtain x' ln' where ts't: "thr s' t= ⌊(x', ln')⌋"
by(cases "thr s' t")(cases s, cases s', auto dest: red_mthr.redT_thread_not_disappear)
from wfs tst obtain E T where wt: "P,E,shr s ⊢ fst x : T"
and hconf: "hconf (shr s)"
and da: "𝒟 (fst x) ⌊dom (snd x)⌋"
and tconf: "P,shr s ⊢ t √t"
by(force dest: ts_invD ts_okD simp add: type_ok_def sconf_def sconf_type_ok_def)
from wt hext have wt': "P,E,shr s' ⊢ fst x : T" by(rule WTrt_hext_mono)
from wfs' ts't have hconf': "hconf (shr s')"
by(auto dest: ts_invD simp add: type_ok_def sconf_def sconf_type_ok_def)
{
assume cs: "red_mthr.must_sync P t x (shr s)"
from cs have "¬ final (fst x)" by(auto elim!: red_mthr.must_syncE simp add: split_beta)
from progress[OF wf_prog_wwf_prog[OF wf] hconf' wt' da this, of "extTA2J P" t]
obtain e' h x' ta where "P,t ⊢ ⟨fst x,(shr s', snd x)⟩ -ta→ ⟨e', (h, x')⟩" by auto
with red_ta_satisfiable[OF this]
show "red_mthr.must_sync P t x (shr s')"
by-(rule red_mthr.must_syncI, fastforce simp add: split_beta)
next
fix LT
assume "red_mthr.can_sync P t x (shr s') LT"
with can_lock_devreserp[OF wf _ wt tconf hconf hext, of "snd x" LT]
show "∃LT'⊆LT. red_mthr.can_sync P t x (shr s) LT'" by auto
}
qed
end
end