Theory JVMDeadlocked

(*  Title:      JinjaThreads/BV/JVMDeadlocked.thy
    Author:     Andreas Lochbihler
*)

header{* \isaheader{Preservation of deadlock for the JVMs} *}

theory JVMDeadlocked imports BVProgressThreaded begin

lemma join_hext:
  assumes wf: "wf_jvm_progΦ P"
  and cs: "P,Φ \<turnstile> (xcp, h, frs) \<surd>"
  and red: "P \<turnstile> Normal (xcp, h, frs) -ta-jvmd-> Normal (xcp', m', frs')"
  and join: "Join t ∈ set \<lbrace>ta\<rbrace>c"
  and hext: "hext h h'"
  shows "P \<turnstile> Normal (xcp, h', frs) -ta-jvmd-> Normal (xcp', h', frs')"
proof -
  from wf obtain wfmd where wfp: "wf_prog wfmd P" by(blast dest: wt_jvm_progD)
  from red obtain f Frs
    where check: "check P (xcp, h, frs)" 
    and exec: "(ta, xcp', m', frs') ∈ set (exec P (xcp, h, frs))" 
    and "(xcp, h, frs) = (xcp, h, f # Frs)"
    by(blast elim: jvmd_NormalE)
  hence [simp]: "frs = f # Frs" by auto
  obtain stk loc C M pc where [simp]: "f = (stk, loc, C, M, pc)" by(cases f, blast)
  from join exec have [simp]: "xcp = None" by(cases xcp, auto)
  from cs obtain Ts T mxs mxl0 ins xt ST LT 
    where "P \<turnstile> h \<surd>"
    and sees: "P \<turnstile> C sees M: Ts->T = (mxs, mxl0, ins, xt) in C"
    and "Φ C M ! pc = ⌊(ST, LT)⌋"
    and "conf_f P h (ST, LT) ins (stk, loc, C, M, pc)"
    and "conf_fs P h Φ M (length Ts) T Frs"
    by(fastsimp simp add: correct_state_def)
  from exec join have [simp]: "xcp = None" by simp
  from sees exec join show ?thesis
  proof(cases "ins ! pc")
    case (Invoke M' n)
    with check exec sees join obtain a ao Ts U Ta 
      where a: "stk ! n = Addr a"
      and n: "n < length stk"
      and ao: "h a = ⌊ao⌋"
      and Ta: "typeofh (Addr a) = ⌊Ta⌋"
      and iec: "is_external_call P Ta M'"
      and wtext: "P \<turnstile> Ta•M'(Ts) :: U"
      and Ts: "map typeofh (rev (take n stk)) = map Some Ts"
      by(auto simp add: check_def is_Ref_def has_method_def external_WT'_iff split: split_if_asm heapobj.split_asm elim!: is_ArrE dest: external_call_not_sees_method[OF wfp])
    from exec iec Ta n a sees Invoke join obtain ta' va m''
      where exec': "(ta', va, m'') ∈ set (red_external_list P a M' (rev (take n stk)) h)"
      and ta: "ta = extTA2JVM P ta'"
      and va: "(xcp', m', frs') = extRet2JVM n m'' stk loc C M pc Frs va"
      by(auto)
    from va have [simp]: "m'' = m'" by(cases va) simp_all
    from Ta Ts wtext have wtext': "P,h \<turnstile> a•M'(rev (take n stk)) : U" by(rule external_WT'.intros)
    with exec' have red: "P \<turnstile> ⟨a•M'(rev (take n stk)), h⟩ -ta'->ext ⟨va, m'⟩"
      by(simp add: WT_red_external_list_conv)
    from join ta have "Join t ∈ set \<lbrace>ta'\<rbrace>c" by simp
    from red_external_Join_hext[OF red this hext] ao
    have "P \<turnstile> ⟨a•M'(rev (take n stk)),h'⟩ -ta'->ext ⟨va,h'⟩" by simp
    moreover from ao hext obtain ao' where "h' a = ⌊ao'⌋" by(auto dest: hext_objarrD)
    moreover from hext Ta have "typeofh' (Addr a) = ⌊Ta⌋" by(rule hext_typeof_mono)
    ultimately have "(ta, xcp', h', frs') ∈ set (exec P (xcp, h', frs))" using ta a n iec Invoke sees va
      by(cases va)(force intro: red_external_imp_red_external_list)+
    moreover from Ts hext have "map typeofh' (rev (take n stk)) = map Some Ts"
      by(rule map_typeof_hext_mono)
    with `typeofh' (Addr a) = ⌊Ta⌋` `h' a = ⌊ao'⌋` iec Invoke a n wtext
    have "check_instr (ins ! pc) P h' stk loc C M pc Frs" by(auto simp add: is_Ref_def external_WT'_iff)
    with check sees have "check P (xcp, h', frs)" by(simp add: check_def)
    ultimately show "P \<turnstile> Normal (xcp, h', frs) -ta-jvmd-> Normal (xcp', h', frs')"
      by -(rule exec_1_d.exec_1_d_NormalI, auto simp add: exec_d_def)
  qed(auto simp add: split_beta split: split_if_asm)
qed

lemma must_sync_preserved_d:
  assumes wf: "wf_jvm_progΦ P"
  and ml: "P \<turnstile> ⟨(xcp, h, frs)⟩d LT \<wrong>" 
  and LTnempty: "LT ≠ {}"
  and hext: "hext h h'"
  and cs: "P,Φ \<turnstile> (xcp, h, frs) \<surd>"
  shows "P \<turnstile> ⟨(xcp, h', frs)⟩d \<wrong>"
proof(rule multithreaded_base.must_syncI)
  from ml obtain ta xcp' frs' m'
    where red: "P \<turnstile> Normal (xcp, h, frs) -ta-jvmd-> Normal (xcp', m', frs')"
    and LT: "LT = collect_locks \<lbrace>ta\<rbrace>l <+> {t. Join t ∈ set \<lbrace>ta\<rbrace>c}"
    by(auto elim: multithreaded_base.can_syncE)
  with LTnempty have lj: "(∃l. Lock ∈ set (\<lbrace>ta\<rbrace>lf l)) ∨ (∃t. Join t ∈ set \<lbrace>ta\<rbrace>c)"
    by(auto simp add: collect_locks_def)
  from red obtain f Frs
    where check: "check P (xcp, h, frs)"
    and exec: "(ta, xcp', m', frs') ∈ set (exec P (xcp, h, frs))"
    and [simp]: "frs = f # Frs"
    by(auto elim: jvmd_NormalE)
  obtain stk loc C M pc where [simp]: "f = (stk, loc, C, M, pc)" by (cases f, blast)
  from lj exec have [simp]: "xcp = None" by(cases xcp, auto)

  from cs obtain ST LT Ts T mxs mxl ins xt where
    hconf:  "P \<turnstile> h \<surd>" and
    meth:   "P \<turnstile> C sees M:Ts->T = (mxs, mxl, ins, xt) in C" and
    Φ:      "Φ C M ! pc = Some (ST,LT)" and
    frame:  "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
    frames: "conf_fs P h Φ M (size Ts) T Frs"
    by (fastsimp simp add: correct_state_def dest: sees_method_fun)

  from wf obtain wfmd where wfp: "wf_prog wfmd P" by(auto dest: wt_jvm_progD)

  from lj have "∃ta xcp' h'' frs'. P \<turnstile> Normal (None, h', (stk, loc, C, M, pc) # Frs) -ta-jvmd-> Normal (xcp', h'', frs')"
  proof(rule disjE)
    assume "∃l. Lock ∈ set (\<lbrace>ta\<rbrace>lf l)"
    then obtain l where l: "Lock ∈ set (\<lbrace>ta\<rbrace>lf l)" by blast
    with meth exec show ?thesis
    proof(cases "ins ! pc")
      case (Invoke M' n)
      with check exec meth l obtain a ao Ts U Ta 
        where a: "stk ! n = Addr a"
        and n: "n < length stk"
        and ao: "h a = ⌊ao⌋"
        and Ta: "typeofh (Addr a) = ⌊Ta⌋"
        and iec: "is_external_call P Ta M'"
        and wtext: "P \<turnstile> Ta•M'(Ts) :: U"
        and Ts: "map typeofh (rev (take n stk)) = map Some Ts"
        by(auto simp add: check_def is_Ref_def has_method_def external_WT'_iff split: split_if_asm heapobj.split_asm elim!: is_ArrE dest: external_call_not_sees_method[OF wfp])
      from exec iec Ta n a meth Invoke l obtain ta' va m''
        where exec': "(ta', va, m'') ∈ set (red_external_list P a M' (rev (take n stk)) h)"
        and ta: "ta = extTA2JVM P ta'"
        and va: "(xcp', m', frs') = extRet2JVM n m'' stk loc C M pc Frs va"
        by(auto simp add: min_def)
      from va have [simp]: "m'' = m'" by(cases va) simp_all
      from Ta Ts wtext have wtext': "P,h \<turnstile> a•M'(rev (take n stk)) : U" by(rule external_WT'.intros)
      with exec' have red: "P \<turnstile> ⟨a•M'(rev (take n stk)), h⟩ -ta'->ext ⟨va, m'⟩"
        by(simp add: WT_red_external_list_conv)
      from l ta have "Lock ∈ set (\<lbrace>ta'\<rbrace>lf l)" by simp
      from red_external_Lock_hext[OF red this hext] ao
      have "P \<turnstile> ⟨a•M'(rev (take n stk)),h'⟩ -ta'->ext ⟨va,h'⟩" by simp
      moreover from ao hext obtain ao' where "h' a = ⌊ao'⌋" by(auto dest: hext_objarrD)
      moreover from hext Ta have "typeofh' (Addr a) = ⌊Ta⌋" by(rule hext_typeof_mono)
      ultimately have "(ta, xcp', h', frs') ∈ set (exec P (xcp, h', frs))" using ta a n iec Invoke meth va
        by(cases va)(force intro: red_external_imp_red_external_list)+
      moreover from Ts hext have "map typeofh' (rev (take n stk)) = map Some Ts"
        by(rule map_typeof_hext_mono)
      with `typeofh' (Addr a) = ⌊Ta⌋` `h' a = ⌊ao'⌋` iec Invoke a n wtext
      have "check_instr (ins ! pc) P h' stk loc C M pc Frs" by(auto simp add: is_Ref_def external_WT'_iff)
      with check meth have "check P (xcp, h', frs)" by(simp add: check_def)
      ultimately have "P \<turnstile> Normal (xcp, h', frs) -ta-jvmd-> Normal (xcp', h', frs')"
        by -(rule exec_1_d.exec_1_d_NormalI, auto simp add: exec_d_def)
      thus ?thesis by auto
    next
      case MEnter
      with meth l exec have "hd stk ≠ Null" by(auto)
      with check meth MEnter obtain a where [simp]: "hd stk = Addr a"
        by(auto elim: is_AddrE simp add: check_def is_Ref_def)
      from meth exec have "(ta, xcp', h', frs') ∈ set (exec P (xcp, h', frs))" by(simp add: MEnter)
      moreover from meth check MEnter have "check P (xcp, h', frs)" by(simp add: check_def)
      ultimately have "P \<turnstile> Normal (xcp, h', frs) -ta-jvmd-> Normal (xcp', h', frs')"
        by -(rule exec_1_d_NormalI, auto simp add: exec_d_def)
      thus ?thesis by auto
    qed(auto split: split_if_asm simp add: finfun_upd_apply)
  next
    assume "∃t. Join t ∈ set \<lbrace>ta\<rbrace>c"
    then obtain t where t: "Join t ∈ set \<lbrace>ta\<rbrace>c" by blast
    from join_hext[OF wf cs red t hext] show ?thesis by auto
  qed
  thus "∃ta x' m'. mexecd P ((fst (xcp, h', frs), snd (snd (xcp, h', frs))), fst (snd (xcp, h', frs))) ta (x', m')"
    by(fastsimp simp add: split_paired_Ex)
qed


lemma can_sync_devreserp_d:
  assumes wf: "wf_jvm_progΦ P"
  and cl': "P \<turnstile> ⟨(xcp, h', frs)⟩d L \<wrong>" 
  and cs: "P,Φ \<turnstile> (xcp, h, frs) \<surd>"
  and hext: "hext h h'"
  shows "∃L'⊆L. P \<turnstile> ⟨(xcp, h, frs)⟩d L' \<wrong>"
proof -
  from cl' obtain ta xcp' frs' m'
    where red: "P \<turnstile> Normal (xcp, h', frs) -ta-jvmd-> Normal (xcp', m', frs')"
    and L: "L = collect_locks \<lbrace>ta\<rbrace>l <+> {t. Join t ∈ set \<lbrace>ta\<rbrace>c}"
    by -(erule  multithreaded_base.can_syncE, auto)
  then obtain f Frs
    where check: "check P (xcp, h', frs)"
    and exec: "(ta, xcp', m', frs') ∈ set (exec P (xcp, h', frs))"
    and [simp]: "frs = f # Frs"
    by(auto elim: jvmd_NormalE simp add: finfun_upd_apply)
  obtain stk loc C M pc where [simp]: "f = (stk, loc, C, M, pc)" by (cases f, blast)
  from cs obtain ST LT Ts T mxs mxl ins xt where
    hconf:  "P \<turnstile> h \<surd>" and
    meth:   "P \<turnstile> C sees M:Ts->T = (mxs, mxl, ins, xt) in C" and
    Φ:      "Φ C M ! pc = Some (ST,LT)" and
    frame:  "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
    frames: "conf_fs P h Φ M (size Ts) T Frs"
    by (fastsimp simp add: correct_state_def dest: sees_method_fun)
  have "exec P (xcp, h, f # frs) ≠ []" by(rule exec_not_empty)
  with no_type_error[OF wf cs] have check': "check P (xcp, h, frs)"
    by(auto simp add: exec_d_def split: split_if_asm)
  from wf obtain wfmd where wfp: "wf_prog wfmd P" by(auto dest: wt_jvm_progD)
  show ?thesis
  proof(cases xcp)
    case (Some a)[simp]
    with exec have [simp]: "m' = h'" by(auto)
    from `P,Φ \<turnstile> (xcp, h, frs) \<surd>` obtain D fs where "h a = ⌊Obj D fs⌋" by(auto simp add: correct_state_def)
    with hext have "cname_of h a = cname_of h' a" by(auto dest: hext_objD)
    with exec have "(ta, xcp', h, frs') ∈ set (exec P (xcp, h, frs))" by auto
    moreover from check have "check P (xcp, h, frs)" by(simp add: check_def)
    ultimately have "P \<turnstile> Normal (xcp, h, frs) -ta-jvmd-> Normal (xcp', h, frs')"
      by -(rule exec_1_d_NormalI, simp only: exec_d_def if_True)
    with L have "multithreaded_base.can_sync (mexecd P) (xcp, frs) h L"
      by(auto intro: multithreaded_base.can_syncI)
    thus ?thesis by auto
  next
    case None[simp]
    from exec meth have "∃ta' σ'. (ta', σ') ∈ set (exec P (xcp, h, frs)) ∧ collect_locks \<lbrace>ta'\<rbrace>l ⊆ collect_locks \<lbrace>ta\<rbrace>l ∧ {t. Join t ∈ set \<lbrace>ta'\<rbrace>c} ⊆ {t. Join t ∈ set \<lbrace>ta\<rbrace>c}"
    proof(cases "ins ! pc")
      case (Invoke M' n)
      show ?thesis
      proof(cases "stk ! n = Null")
        case True with Invoke exec meth show ?thesis by simp
      next
        case False
        with check meth obtain a where a: "stk ! n = Addr a" and n: "n < length stk"
          by(auto simp add: check_def is_Ref_def Invoke)
        from frame have stk: "P,h \<turnstile> stk [:≤] ST" by(auto simp add: conf_f_def)
        hence "P,h \<turnstile> stk ! n :≤ ST ! n" using n by(rule list_all2_nthD)
        with a obtain ao Ta where ao: "h a = ⌊ao⌋" and Ta: "typeofh (Addr a) = ⌊Ta⌋"
          by(auto split: heapobj.splits simp add: conf_def)
        from hext Ta have Ta': "typeofh' (Addr a) = ⌊Ta⌋" by(rule hext_typeof_mono)
        show ?thesis
        proof(cases "is_external_call P Ta M'")
          case False
          with exec meth a Ta Ta' Invoke n ao show ?thesis by(simp add: split_beta)
        next
          case True
          with exec meth a Ta Ta' Invoke n ao
          obtain ta' va h'' where ta': "ta = extTA2JVM P ta'"
            and va: "(xcp', m', frs') = extRet2JVM n h'' stk loc C M pc Frs va"
            and exec': "(ta', va, h'') ∈ set (red_external_list P a M' (rev (take n stk)) h')"
            by(fastsimp)
          from va have [simp]: "h'' = m'" by(cases va) simp_all
          note Ta moreover from check True Invoke Ta meth a n Ta'
          obtain U where "P,h' \<turnstile> a•M'(rev (take n stk)) : U" by(auto simp add: check_def)
          with exec' have red: "P \<turnstile> ⟨a•M'(rev (take n stk)), h'⟩ -ta'->ext ⟨va, m'⟩"
            by(simp add: WT_red_external_list_conv)
          from stk have "P,h \<turnstile> take n stk [:≤] take n ST" by(rule list_all2_takeI)
          then obtain Ts where "map typeofh (take n stk) = map Some Ts"
            by(auto simp add: confs_conv_map)
          hence "map typeofh (rev (take n stk)) = map Some (rev Ts)" by(simp only: rev_map[symmetric])
          moreover hence "map typeofh' (rev (take n stk)) = map Some (rev Ts)" using hext by(rule map_typeof_hext_mono)
          with `P,h' \<turnstile> a•M'(rev (take n stk)) : U` Ta' have "P \<turnstile> Ta•M'(rev Ts) :: U"
            by(auto simp add: external_WT'_iff)
          ultimately have "P,h \<turnstile> a•M'(rev (take n stk)) : U" by(rule external_WT'.intros)
          from red_external_wt_hconf_hext[OF red this hext]
          obtain ta'' va' h''' where "P \<turnstile> ⟨a•M'(rev (take n stk)),h⟩ -ta''->ext ⟨va',h'''⟩"
            and ta'': "\<lbrace>ta''\<rbrace>l = \<lbrace>ta'\<rbrace>l" "\<lbrace>ta''\<rbrace>w = \<lbrace>ta'\<rbrace>w" "\<lbrace>ta''\<rbrace>c = \<lbrace>ta'\<rbrace>c" by auto
          with True a Ta Invoke meth Ta' n
          have "(extTA2JVM P ta'', extRet2JVM n h''' stk loc C M pc Frs va') ∈ set (exec P (xcp, h, frs))"
            by(force intro: red_external_imp_red_external_list)
          with ta'' ta' show ?thesis by auto
        qed
      qed
    qed(auto split: split_if_asm)
    with check' have "∃ta' σ'. P \<turnstile> Normal (xcp, h, frs) -ta'-jvmd-> Normal σ' ∧ collect_locks \<lbrace>ta'\<rbrace>l ⊆ collect_locks \<lbrace>ta\<rbrace>l ∧ {t. Join t ∈ set \<lbrace>ta'\<rbrace>c} ⊆ {t. Join t ∈ set \<lbrace>ta\<rbrace>c}"
      apply clarify
      apply(rule exI conjI)+
      apply(rule exec_1_d.exec_1_d_NormalI, auto simp add: exec_d_def)
      done
    with L show ?thesis
      apply -
      apply(erule exE conjE|rule exI conjI)+
      prefer 2
      apply(rule_tac x'="(fst σ', snd (snd σ'))" and m'="fst (snd σ')" in multithreaded_base.can_syncI)
      apply auto
      done
  qed
qed


lemma execd_preserve_deadlocked:
  assumes wf: "wf_jvm_progΦ P"
  and lto: "lock_thread_ok (locks S) (thr S)"
  and cs: "correct_state_ts P Φ (thr S) (shr S)"
  shows "preserve_deadlocked JVM_final (mexecd P) S"
proof(unfold_locales)
  from `lock_thread_ok (locks S) (thr S)`
  show "lock_thread_ok (locks S) (thr S)" .
next
  fix tta s t' ta' s' t x ln LT
  assume Red: "P \<turnstile> S -\<triangleright>tta->jvmd* s"
    and red: "P \<turnstile> s -t'\<triangleright>ta'->jvmd s'"
    and tst: "thr s t = ⌊(x, ln)⌋"
    and "multithreaded_base.can_sync (mexecd P) x (shr s) LT"
    and LTnempty: "LT ≠ {}"
  moreover obtain xcp frs where x [simp]: "x = (xcp, frs)" by(cases x, auto)
  ultimately have ml: "P \<turnstile> ⟨(xcp, shr s, frs)⟩d LT \<wrong>" by auto
  moreover from cs Red have cs': "correct_state_ts P Φ (thr s) (shr s)"
    by-(rule preserves_correct_state_d[OF wf])
  with tst have "P,Φ \<turnstile> (xcp, shr s, frs) \<surd>"
    by(auto dest: ts_okD)
  moreover from red have "hext (shr s) (shr s')"
    by(rule execd_hext)
  ultimately have "P \<turnstile> ⟨(xcp, shr s', frs)⟩d \<wrong>" using LTnempty
    by-(rule must_sync_preserved_d[OF wf])
  thus "multithreaded_base.must_sync (mexecd P) x (shr s')" by simp
next
  fix tta s t' ta' s' t x ln L
  assume Red: "P \<turnstile> S -\<triangleright>tta->jvmd* s"
    and red: "P \<turnstile> s -t'\<triangleright>ta'->jvmd s'"
    and tst: "thr s t = ⌊(x, ln)⌋"
    and "multithreaded_base.can_sync (mexecd P) x (shr s') L"
  moreover obtain xcp frs where x [simp]: "x = (xcp, frs)" by(cases x, auto)
  ultimately have ml: "P \<turnstile> ⟨(xcp, shr s', frs)⟩d L \<wrong>" by auto
  moreover from cs Red have cs': "correct_state_ts P Φ (thr s) (shr s)"
    by-(rule preserves_correct_state_d[OF wf])
  with tst have "P,Φ \<turnstile> (xcp, shr s, frs) \<surd>"
    by(auto dest: ts_okD)
  moreover from red have "hext (shr s) (shr s')"
    by(rule execd_hext)
  ultimately have "∃L' ⊆ L. P \<turnstile> ⟨(xcp, shr s, frs)⟩d L' \<wrong>"
    by-(rule can_sync_devreserp_d[OF wf])
  thus "∃L' ⊆ L. multithreaded_base.can_sync (mexecd P) x (shr s) L'" by simp
qed


text {* and now everything again for the aggresive VM *}

lemma must_lock_d_eq_must_lock:
  "[| wf_jvm_progΦ P; P,Φ \<turnstile> (xcp, h, frs) \<surd> |]
  ==> P \<turnstile> ⟨(xcp, h, frs)⟩d \<wrong> = P \<turnstile> ⟨(xcp, h, frs)⟩ \<wrong>"
apply(simp)
apply(rule iffI)
 apply(rule multithreaded_base.must_syncI)
 apply(erule multithreaded_base.must_syncE)
 apply(simp only: mexec_eq_mexecd)
 apply(blast)
apply(rule multithreaded_base.must_syncI)
apply(erule multithreaded_base.must_syncE)
apply(simp only: mexec_eq_mexecd[symmetric])
apply(blast)
done

lemma can_lock_d_eq_can_lock:
  "[| wf_jvm_progΦ P; P,Φ \<turnstile> (xcp, h, frs) \<surd> |]
  ==> P \<turnstile> ⟨(xcp, h, frs)⟩d L \<wrong> = P \<turnstile> ⟨(xcp, h, frs)⟩ L \<wrong>"
apply(simp)
apply(rule iffI)
 apply(erule multithreaded_base.can_syncE)
 apply(rule multithreaded_base.can_syncI)
   apply(simp only: mexec_eq_mexecd)
  apply(assumption)+
apply(erule multithreaded_base.can_syncE)
apply(rule multithreaded_base.can_syncI)
 by(simp only: mexec_eq_mexecd)

lemma exec_preserve_deadlocked:
  assumes wf: "wf_jvm_progΦ P"
  and lto: "lock_thread_ok (locks S) (thr S)"
  and cs: "correct_state_ts P Φ (thr S) (shr S)"
  shows "preserve_deadlocked JVM_final (mexec P) S"
proof -
  { fix tta s t' ta' s' t x ln
    assume Red: "P \<turnstile> S -\<triangleright>tta->jvm* s"
      and red: "P \<turnstile> s -t'\<triangleright>ta'->jvm s'"
      and tst: "thr s t = ⌊(x, ln)⌋"
    obtain xcp frs where x [simp]: "x = (xcp, frs)" by(cases x, auto)
    from wf cs Red have Redd: "P \<turnstile> S -\<triangleright>tta->jvmd* s"
      by(simp add: mExecT_eq_mExecdT)
    moreover from Red cs have css: "correct_state_ts P Φ (thr s) (shr s)" 
      by-(rule preserves_correct_state[OF wf])
    with red have redd: "P \<turnstile> s -t'\<triangleright>ta'->jvmd s'"
      by(simp add: mexecT_eq_mexecdT[OF wf])
    from css tst have cst: "P,Φ \<turnstile> (xcp, shr s, frs) \<surd>" by(auto dest: ts_okD)
    from redd have cst': "P,Φ \<turnstile> (xcp, shr s', frs) \<surd>"
    proof(induct rule: execd_mthr.redT_elims[consumes 1, case_names normal acquire])
      case acquire with cst show ?case by simp
    next
      case (normal X X' TA)
      obtain XCP FRS where X [simp]: "X = (XCP, FRS)" by(cases X, auto)
      obtain XCP' FRS' where X' [simp]: "X' = (XCP', FRS')" by(cases X', auto)
      from `mexecd P (X, shr s) TA (X', shr s')`
      have "P \<turnstile> Normal (XCP, shr s, FRS) -TA-jvmd-> Normal (XCP', shr s', FRS')" by simp
      moreover from `thr s t' = ⌊(X, no_wait_locks)⌋` css
      have "P,Φ \<turnstile> (XCP, shr s, FRS) \<surd>" by(auto dest: ts_okD)
      ultimately show ?case using `P,Φ \<turnstile> (xcp, shr s, frs) \<surd>` by -(rule correct_state_heap_change[OF wf])
    qed
    { fix L
      assume "multithreaded_base.can_sync (mexec P) x (shr s) L"
        and L: "L ≠ {}"
      hence ml: "P \<turnstile> ⟨(xcp, shr s, frs)⟩ L \<wrong>" by simp
      with cst have "P \<turnstile> ⟨(xcp, shr s, frs)⟩d L \<wrong>"
        by(auto dest: can_lock_d_eq_can_lock[OF wf])
      hence "multithreaded_base.must_sync (mexecd P) x (shr s')"
        by-(rule preserve_lock_behav.can_lock_preserved[OF preserve_deadlocked.axioms(2)[OF execd_preserve_deadlocked[OF wf lto cs]] Redd redd tst _ L], simp)
      with cst' have "multithreaded_base.must_sync (mexec P) x (shr s')"
        by(auto dest: must_lock_d_eq_must_lock[OF wf]) }
    note ml = this
    { fix L
      assume "multithreaded_base.can_sync (mexec P) x (shr s') L"
      hence cl: "P \<turnstile> ⟨(xcp, shr s', frs)⟩ L \<wrong>" by simp
      with cst' have "P \<turnstile> ⟨(xcp, shr s', frs)⟩d L \<wrong>"
        by(auto dest: can_lock_d_eq_can_lock[OF wf])
      with Redd redd tst
      have "∃L' ⊆ L. multithreaded_base.can_sync (mexecd P) x (shr s) L'"
        by -(rule preserve_lock_behav.can_lock_devreserp[OF preserve_deadlocked.axioms(2)[OF execd_preserve_deadlocked[OF wf lto cs]]], auto)
      then obtain L' where "multithreaded_base.can_sync (mexecd P) x (shr s) L'" 
        and L': "L'⊆ L" by blast
      with cst have "multithreaded_base.can_sync (mexec P) x (shr s) L'"
        by(auto dest: can_lock_d_eq_can_lock[OF wf])
      with L' have "∃L' ⊆ L. multithreaded_base.can_sync (mexec P) x (shr s) L'"
        by(blast) }
    note this ml }
  thus ?thesis using lto by(unfold_locales)
qed


end