Theory FWBisimDeadlock
section ‹Preservation of deadlock across bisimulations›
theory FWBisimDeadlock
imports
FWBisimulation
FWDeadlock
begin
context FWdelay_bisimulation_obs begin
lemma actions_ok1_ex_actions_ok2:
assumes "r1.actions_ok s1 t ta1"
and "ta1 ∼m ta2"
obtains s2 where "r2.actions_ok s2 t ta2"
proof -
let ?s2 = "(locks s1, (λt. map_option (λ(x1, ln). (SOME x2. if final1 x1 then final2 x2 else ¬ final2 x2, ln)) (thr s1 t), undefined), wset s1, interrupts s1)"
from ‹ta1 ∼m ta2› have "⦃ta1⦄⇘c⇙ = ⦃ta2⦄⇘c⇙" by(simp add: ta_bisim_def)
with ‹r1.actions_ok s1 t ta1› have cao1: "r1.cond_action_oks s1 t ⦃ta2⦄⇘c⇙" by auto
have "r2.cond_action_oks ?s2 t ⦃ta2⦄⇘c⇙" unfolding r2.cond_action_oks_conv_set
proof
fix ct
assume "ct ∈ set ⦃ta2⦄⇘c⇙"
with cao1 have "r1.cond_action_ok s1 t ct"
unfolding r1.cond_action_oks_conv_set by auto
thus "r2.cond_action_ok ?s2 t ct" using ex_final1_conv_ex_final2
by(cases ct)(fastforce intro: someI_ex[where P=final2])+
qed
hence "r2.actions_ok ?s2 t ta2"
using assms by(auto simp add: ta_bisim_def split del: if_split elim: rev_iffD1[OF _ thread_oks_bisim_inv])
thus thesis by(rule that)
qed
lemma actions_ok2_ex_actions_ok1:
assumes "r2.actions_ok s2 t ta2"
and "ta1 ∼m ta2"
obtains s1 where "r1.actions_ok s1 t ta1"
using FWdelay_bisimulation_obs.actions_ok1_ex_actions_ok2[OF FWdelay_bisimulation_obs_flip] assms
unfolding flip_simps .
lemma ex_actions_ok1_conv_ex_actions_ok2:
"ta1 ∼m ta2 ⟹ (∃s1. r1.actions_ok s1 t ta1) ⟷ (∃s2. r2.actions_ok s2 t ta2)"
by(metis actions_ok1_ex_actions_ok2 actions_ok2_ex_actions_ok1)
end
context FWdelay_bisimulation_diverge begin
lemma no_τMove1_τs_to_no_τMove2:
fixes no_τmoves1 no_τmoves2
defines "no_τmoves1 ≡ λs1 t. wset s1 t = None ∧ (∃x. thr s1 t = ⌊(x, no_wait_locks)⌋ ∧ (∀x' m'. ¬ r1.silent_move t (x, shr s1) (x', m')))"
defines "no_τmoves2 ≡ λs2 t. wset s2 t = None ∧ (∃x. thr s2 t = ⌊(x, no_wait_locks)⌋ ∧ (∀x' m'. ¬ r2.silent_move t (x, shr s2) (x', m')))"
assumes mbisim: "s1 ≈m (ls2, (ts2, m2), ws2, is2)"
shows "∃ts2'. r2.mthr.silent_moves (ls2, (ts2, m2), ws2, is2) (ls2, (ts2', m2), ws2, is2) ∧
(∀t. no_τmoves1 s1 t ⟶ no_τmoves2 (ls2, (ts2', m2), ws2, is2) t) ∧ s1 ≈m (ls2, (ts2', m2), ws2, is2)"
proof -
from mbisim have "finite (dom (thr s1))" by(simp add: mbisim_def)
hence "finite {t. no_τmoves1 s1 t}" unfolding no_τmoves1_def
by-(rule finite_subset, auto)
thus ?thesis using ‹s1 ≈m (ls2, (ts2, m2), ws2, is2)›
proof(induct A≡"{t. no_τmoves1 s1 t}" arbitrary: s1 ts2 rule: finite_induct)
case empty
from ‹{} = {t. no_τmoves1 s1 t}›[symmetric] have "no_τmoves1 s1 = (λt. False)"
by(auto intro: ext)
thus ?case using ‹s1 ≈m (ls2, (ts2, m2), ws2, is2)› by auto
next
case (insert t A)
note mbisim = ‹s1 ≈m (ls2, (ts2, m2), ws2, is2)›
from ‹insert t A = {t. no_τmoves1 s1 t}›
have "no_τmoves1 s1 t" by auto
then obtain x1 where ts1t: "thr s1 t = ⌊(x1, no_wait_locks)⌋"
and ws1t: "wset s1 t = None"
and τ1: "⋀x1m1'. ¬ r1.silent_move t (x1, shr s1) x1m1'"
by(auto simp add: no_τmoves1_def)
from ts1t mbisim obtain x2 where ts2t: "ts2 t = ⌊(x2, no_wait_locks)⌋"
and "t ⊢ (x1, shr s1) ≈ (x2, m2)" by(auto dest: mbisim_thrD1)
from mbisim ws1t have "ws2 t = None" by(simp add: mbisim_def)
let ?s1 = "(locks s1, ((thr s1)(t := None), shr s1), wset s1, interrupts s1)"
let ?s2 = "(ls2, (ts2(t := None), m2), ws2, is2)"
from ‹insert t A = {t. no_τmoves1 s1 t}› ‹t ∉ A›
have A: "A = {t. no_τmoves1 ?s1 t}" by(auto simp add: no_τmoves1_def)
have "?s1 ≈m ?s2"
proof(rule mbisimI)
from mbisim
show "finite (dom (thr ?s1))" "locks ?s1 = locks ?s2" "wset ?s1 = wset ?s2" "interrupts ?s1 = interrupts ?s2"
by(simp_all add: mbisim_def)
next
from mbisim_wset_thread_ok1[OF mbisim] ws1t show "wset_thread_ok (wset ?s1) (thr ?s1)"
by(auto intro!: wset_thread_okI dest: wset_thread_okD split: if_split_asm)
next
fix t'
assume "thr ?s1 t' = None"
with mbisim_thrNone_eq[OF mbisim, of t']
show "thr ?s2 t' = None" by auto
next
fix t' x1 ln
assume "thr ?s1 t' = ⌊(x1, ln)⌋"
hence "thr s1 t' = ⌊(x1, ln)⌋" "t' ≠ t" by(auto split: if_split_asm)
with mbisim_thrD1[OF mbisim ‹thr s1 t' = ⌊(x1, ln)⌋›] mbisim
show "∃x2. thr ?s2 t' = ⌊(x2, ln)⌋ ∧ t' ⊢ (x1, shr ?s1) ≈ (x2, shr ?s2) ∧ (wset ?s2 t' = None ∨ x1 ≈w x2)"
by(auto simp add: mbisim_def)
qed
with A have "∃ts2'. r2.mthr.silent_moves ?s2 (ls2, (ts2', m2), ws2, is2) ∧ (∀t. no_τmoves1 ?s1 t ⟶ no_τmoves2 (ls2, (ts2', m2), ws2, is2) t) ∧ ?s1 ≈m (ls2, (ts2', m2), ws2, is2)" by(rule insert)
then obtain ts2' where "r2.mthr.silent_moves ?s2 (ls2, (ts2', m2), ws2, is2)"
and no_τ: "⋀t. no_τmoves1 ?s1 t ⟹ no_τmoves2 (ls2, (ts2', m2), ws2, is2) t"
and "?s1 ≈m (ls2, (ts2', m2), ws2, is2)" by auto
let ?s2' = "(ls2, (ts2'(t ↦ (x2, no_wait_locks)), m2), ws2, is2)"
from ts2t have "ts2(t ↦ (x2, no_wait_locks)) = ts2" by(auto intro: ext)
with r2.τmRedT_add_thread_inv[OF ‹r2.mthr.silent_moves ?s2 (ls2, (ts2', m2), ws2, is2)›, of t "(x2, no_wait_locks)"]
have "r2.mthr.silent_moves (ls2, (ts2, m2), ws2, is2) ?s2'" by simp
from no_τmove1_τs_to_no_τmove2[OF ‹t ⊢ (x1, shr s1) ≈ (x2, m2)› τ1]
obtain x2' m2' where "r2.silent_moves t (x2, m2) (x2', m2')"
and "⋀x2'' m2''. ¬ r2.silent_move t (x2', m2') (x2'', m2'')"
and "t ⊢ (x1, shr s1) ≈ (x2', m2')" by auto
let ?s2'' = "(ls2, (ts2'(t ↦ (x2', no_wait_locks)), m2'), ws2, is2)"
from red2_rtrancl_τ_heapD[OF ‹r2.silent_moves t (x2, m2) (x2', m2')› ‹t ⊢ (x1, shr s1) ≈ (x2, m2)›]
have "m2' = m2" by simp
with ‹r2.silent_moves t (x2, m2) (x2', m2')› have "r2.silent_moves t (x2, shr ?s2') (x2', m2)" by simp
hence "r2.mthr.silent_moves ?s2' (redT_upd_ε ?s2' t x2' m2)"
by(rule red2_rtrancl_τ_into_RedT_τ)(auto simp add: ‹ws2 t = None› intro: ‹t ⊢ (x1, shr s1) ≈ (x2, m2)›)
also have "redT_upd_ε ?s2' t x2' m2 = ?s2''" using ‹m2' = m2›
by(auto simp add: fun_eq_iff redT_updLns_def finfun_Diag_const2 o_def)
finally (back_subst) have "r2.mthr.silent_moves (ls2, (ts2, m2), ws2, is2) ?s2''"
using ‹r2.mthr.silent_moves (ls2, (ts2, m2), ws2, is2) ?s2'› by-(rule rtranclp_trans)
moreover {
fix t'
assume no_τ1: "no_τmoves1 s1 t'"
have "no_τmoves2 ?s2'' t'"
proof(cases "t' = t")
case True thus ?thesis
using ‹ws2 t = None› ‹⋀x2'' m2''. ¬ r2.silent_move t (x2', m2') (x2'', m2'')› by(simp add: no_τmoves2_def)
next
case False
with no_τ1 have "no_τmoves1 ?s1 t'" by(simp add: no_τmoves1_def)
hence "no_τmoves2 (ls2, (ts2', m2), ws2, is2) t'"
by(rule ‹no_τmoves1 ?s1 t' ⟹ no_τmoves2 (ls2, (ts2', m2), ws2, is2) t'›)
with False ‹m2' = m2› show ?thesis by(simp add: no_τmoves2_def)
qed }
moreover have "s1 ≈m ?s2''"
proof(rule mbisimI)
from mbisim
show "finite (dom (thr s1))" "locks s1 = locks ?s2''" "wset s1 = wset ?s2''" "interrupts s1 = interrupts ?s2''"
by(simp_all add: mbisim_def)
next
from mbisim show "wset_thread_ok (wset s1) (thr s1)" by(rule mbisim_wset_thread_ok1)
next
fix t'
assume "thr s1 t' = None"
hence "thr ?s1 t' = None" "t' ≠ t" using ts1t by auto
with mbisim_thrNone_eq[OF ‹?s1 ≈m (ls2, (ts2', m2), ws2, is2)›, of t']
show "thr ?s2'' t' = None" by simp
next
fix t' x1' ln'
assume "thr s1 t' = ⌊(x1', ln')⌋"
show "∃x2. thr ?s2'' t' = ⌊(x2, ln')⌋ ∧ t' ⊢ (x1', shr s1) ≈ (x2, shr ?s2'') ∧ (wset ?s2'' t' = None ∨ x1' ≈w x2)"
proof(cases "t = t'")
case True
with ‹thr s1 t' = ⌊(x1', ln')⌋› ts1t ‹t ⊢ (x1, shr s1) ≈ (x2', m2')› ‹m2' = m2› ‹ws2 t = None›
show ?thesis by auto
next
case False
with mbisim_thrD1[OF ‹?s1 ≈m (ls2, (ts2', m2), ws2, is2)›, of t' x1' ln'] ‹thr s1 t' = ⌊(x1', ln')⌋› ‹m2' = m2› mbisim
show ?thesis by(auto simp add: mbisim_def)
qed
qed
ultimately show ?case unfolding ‹m2' = m2› by blast
qed
qed
lemma no_τMove2_τs_to_no_τMove1:
fixes no_τmoves1 no_τmoves2
defines "no_τmoves1 ≡ λs1 t. wset s1 t = None ∧ (∃x. thr s1 t = ⌊(x, no_wait_locks)⌋ ∧ (∀x' m'. ¬ r1.silent_move t (x, shr s1) (x', m')))"
defines "no_τmoves2 ≡ λs2 t. wset s2 t = None ∧ (∃x. thr s2 t = ⌊(x, no_wait_locks)⌋ ∧ (∀x' m'. ¬ r2.silent_move t (x, shr s2) (x', m')))"
assumes "(ls1, (ts1, m1), ws1, is1) ≈m s2"
shows "∃ts1'. r1.mthr.silent_moves (ls1, (ts1, m1), ws1, is1) (ls1, (ts1', m1), ws1, is1) ∧
(∀t. no_τmoves2 s2 t ⟶ no_τmoves1 (ls1, (ts1', m1), ws1, is1) t) ∧ (ls1, (ts1', m1), ws1, is1) ≈m s2"
using assms FWdelay_bisimulation_diverge.no_τMove1_τs_to_no_τMove2[OF FWdelay_bisimulation_diverge_flip]
unfolding flip_simps by blast
lemma deadlock_mbisim_not_final_thread_pres:
assumes dead: "t ∈ r1.deadlocked s1 ∨ r1.deadlock s1"
and nfin: "r1.not_final_thread s1 t"
and fin: "r1.final_thread s1 t ⟹ r2.final_thread s2 t"
and mbisim: "s1 ≈m s2"
shows "r2.not_final_thread s2 t"
proof -
from nfin obtain x1 ln where "thr s1 t = ⌊(x1, ln)⌋" by cases auto
with mbisim obtain x2 where "thr s2 t = ⌊(x2, ln)⌋" "t ⊢ (x1, shr s1) ≈ (x2, shr s2)" "wset s1 t = None ∨ x1 ≈w x2"
by(auto dest: mbisim_thrD1)
show "r2.not_final_thread s2 t"
proof(cases "wset s1 t = None ∧ ln = no_wait_locks")
case False
with ‹r1.not_final_thread s1 t› ‹thr s1 t = ⌊(x1, ln)⌋› ‹thr s2 t = ⌊(x2, ln)⌋› mbisim
show ?thesis by cases(auto simp add: mbisim_def r2.not_final_thread_iff)
next
case True
with ‹r1.not_final_thread s1 t› ‹thr s1 t = ⌊(x1, ln)⌋› have "¬ final1 x1" by(cases) auto
have "¬ final2 x2"
proof
assume "final2 x2"
with final2_simulation[OF ‹t ⊢ (x1, shr s1) ≈ (x2, shr s2)›]
obtain x1' m1' where "r1.silent_moves t (x1, shr s1) (x1', m1')" "t ⊢ (x1', m1') ≈ (x2, shr s2)" "final1 x1'" by auto
from ‹r1.silent_moves t (x1, shr s1) (x1', m1')› have "x1' = x1"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names refl step])
case (step x1'' m1'')
from ‹r1.silent_move t (x1, shr s1) (x1'', m1'')›
have "t ⊢ (x1, shr s1) -1-ε→ (x1'', m1'')" by(auto dest: r1.silent_tl)
hence "r1.redT s1 (t, ε) (redT_upd_ε s1 t x1'' m1'')"
using ‹thr s1 t = ⌊(x1, ln)⌋› True
by -(erule r1.redT_normal, auto simp add: redT_updLns_def finfun_Diag_const2 o_def redT_updWs_def)
hence False using dead by(auto intro: r1.deadlock_no_red r1.red_no_deadlock)
thus ?thesis ..
qed simp
with ‹¬ final1 x1› ‹final1 x1'› show False by simp
qed
thus ?thesis using ‹thr s2 t = ⌊(x2, ln)⌋› by(auto simp add: r2.not_final_thread_iff)
qed
qed
lemma deadlocked1_imp_τs_deadlocked2:
assumes mbisim: "s1 ≈m s2"
and dead: "t ∈ r1.deadlocked s1"
shows "∃s2'. r2.mthr.silent_moves s2 s2' ∧ t ∈ r2.deadlocked s2' ∧ s1 ≈m s2'"
proof -
from mfinal1_inv_simulation[OF mbisim]
obtain ls2 ts2 m2 ws2 is2 where red1: "r2.mthr.silent_moves s2 (ls2, (ts2, m2), ws2, is2)"
and "s1 ≈m (ls2, (ts2, m2), ws2, is2)" and "m2 = shr s2"
and fin: "⋀t. r1.final_thread s1 t ⟹ r2.final_thread (ls2, (ts2, m2), ws2, is2) t" by fastforce
from no_τMove1_τs_to_no_τMove2[OF ‹s1 ≈m (ls2, (ts2, m2), ws2, is2)›]
obtain ts2' where red2: "r2.mthr.silent_moves (ls2, (ts2, m2), ws2, is2) (ls2, (ts2', m2), ws2, is2)"
and no_τ: "⋀t x1 x2 x2' m2'. ⟦ wset s1 t = None; thr s1 t = ⌊(x1, no_wait_locks)⌋; ts2' t = ⌊(x2, no_wait_locks)⌋;
⋀x' m'. r1.silent_move t (x1, shr s1) (x', m') ⟹ False ⟧
⟹ ¬ r2.silent_move t (x2, m2) (x2', m2')"
and mbisim: "s1 ≈m (ls2, (ts2', m2), ws2, is2)" by fastforce
from mbisim have mbisim_eqs: "ls2 = locks s1" "ws2 = wset s1" "is2 = interrupts s1"
by(simp_all add: mbisim_def)
let ?s2 = "(ls2, (ts2', m2), ws2, is2)"
from red2 have fin': "⋀t. r1.final_thread s1 t ⟹ r2.final_thread ?s2 t"
by(rule r2.τmRedT_preserves_final_thread)(rule fin)
from dead
have "t ∈ r2.deadlocked ?s2"
proof(coinduct)
case (deadlocked t)
thus ?case
proof(cases rule: r1.deadlocked_elims)
case (lock x1)
hence csmw: "⋀LT. r1.can_sync t x1 (shr s1) LT ⟹
∃lt∈LT. r1.must_wait s1 t lt (r1.deadlocked s1 ∪ r1.final_threads s1)"
by blast
from ‹thr s1 t = ⌊(x1, no_wait_locks)⌋› mbisim obtain x2
where "ts2' t = ⌊(x2, no_wait_locks)⌋" and bisim: "t ⊢ (x1, shr s1) ≈ (x2, m2)"
by(auto dest: mbisim_thrD1)
note ‹ts2' t = ⌊(x2, no_wait_locks)⌋› moreover
{ from ‹r1.must_sync t x1 (shr s1)› obtain ta1 x1' m1'
where r1: "t ⊢ (x1, shr s1) -1-ta1→ (x1', m1')"
and s1': "∃s1'. r1.actions_ok s1' t ta1" by(fastforce elim: r1.must_syncE)
have "¬ τmove1 (x1, shr s1) ta1 (x1', m1')" (is "¬ ?τ")
proof
assume "?τ"
hence "ta1 = ε" by(rule r1.silent_tl)
with r1 have "r1.can_sync t x1 (shr s1) {}"
by(auto intro!: r1.can_syncI simp add: collect_locks_def collect_interrupts_def)
from csmw[OF this] show False by blast
qed
from simulation1[OF bisim r1 this]
obtain x2' m2' x2'' m2'' ta2 where r2: "r2.silent_moves t (x2, m2) (x2', m2')"
and r2': "t ⊢ (x2', m2') -2-ta2→ (x2'', m2'')"
and τ2: "¬ τmove2 (x2', m2') ta2 (x2'', m2'')"
and bisim': "t ⊢ (x1', m1') ≈ (x2'', m2'')" and tasim: "ta1 ∼m ta2" by auto
from r2
have "∃ta2 x2' m2' s2'. t ⊢ (x2, m2) -2-ta2→ (x2', m2') ∧ r2.actions_ok s2' t ta2"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names base step])
case base
from r2'[folded base] s1'[unfolded ex_actions_ok1_conv_ex_actions_ok2[OF tasim]]
show ?thesis by blast
next
case (step x2''' m2''')
hence "t ⊢ (x2, m2) -2-ε→ (x2''', m2''')" by(auto dest: r2.silent_tl)
moreover have "r2.actions_ok (undefined, (undefined, undefined), Map.empty, undefined) t ε" by auto
ultimately show ?thesis by-(rule exI conjI|assumption)+
qed
hence "r2.must_sync t x2 m2" unfolding r2.must_sync_def2 . }
moreover
{ fix LT
assume "r2.can_sync t x2 m2 LT"
then obtain ta2 x2' m2' where r2: "t ⊢ (x2, m2) -2-ta2→ (x2', m2')"
and LT: "LT = collect_locks ⦃ta2⦄⇘l⇙ <+> collect_cond_actions ⦃ta2⦄⇘c⇙ <+> collect_interrupts ⦃ta2⦄⇘i⇙"
by(auto elim: r2.can_syncE)
from ‹wset s1 t = None› ‹thr s1 t = ⌊(x1, no_wait_locks)⌋› ‹ts2' t = ⌊(x2, no_wait_locks)⌋›
have "¬ r2.silent_move t (x2, m2) (x2', m2')"
proof(rule no_τ)
fix x1' m1'
assume "r1.silent_move t (x1, shr s1) (x1', m1')"
hence "t ⊢ (x1, shr s1) -1-ε→ (x1', m1')" by(auto dest: r1.silent_tl)
hence "r1.can_sync t x1 (shr s1) {}"
by(auto intro: r1.can_syncI simp add: collect_locks_def collect_interrupts_def)
with csmw[OF this] show False by blast
qed
with r2 have "¬ τmove2 (x2, m2) ta2 (x2', m2')" by auto
from simulation2[OF bisim r2 this] obtain x1' m1' x1'' m1'' ta1
where τr1: "r1.silent_moves t (x1, shr s1) (x1', m1')"
and r1: "t ⊢ (x1', m1') -1-ta1→ (x1'', m1'')"
and nτ1: "¬ τmove1 (x1', m1') ta1 (x1'', m1'')"
and bisim': "t ⊢ (x1'', m1'') ≈ (x2', m2')"
and tlsim: "ta1 ∼m ta2" by auto
from τr1 obtain [simp]: "x1' = x1" "m1' = shr s1"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names refl step])
case (step X M)
from ‹r1.silent_move t (x1, shr s1) (X, M)›
have "t ⊢ (x1, shr s1) -1-ε→ (X, M)" by(auto dest: r1.silent_tl)
hence "r1.can_sync t x1 (shr s1) {}"
by(auto intro: r1.can_syncI simp add: collect_locks_def collect_interrupts_def)
with csmw[OF this] have False by blast
thus ?thesis ..
qed blast
from tlsim LT have "LT = collect_locks ⦃ta1⦄⇘l⇙ <+> collect_cond_actions ⦃ta1⦄⇘c⇙ <+> collect_interrupts ⦃ta1⦄⇘i⇙"
by(auto simp add: ta_bisim_def)
with r1 have "r1.can_sync t x1 (shr s1) LT" by(auto intro: r1.can_syncI)
from csmw[OF this] obtain lt
where lt: "lt ∈ LT" and mw: "r1.must_wait s1 t lt (r1.deadlocked s1 ∪ r1.final_threads s1)" by blast
have subset: "r1.deadlocked s1 ∪ r1.final_threads s1 ⊆ r1.deadlocked s1 ∪ r2.deadlocked s2 ∪ r2.final_threads ?s2"
by(auto dest: fin')
from mw have "r2.must_wait ?s2 t lt (r1.deadlocked s1 ∪ r2.deadlocked ?s2 ∪ r2.final_threads ?s2)"
proof(cases rule: r1.must_wait_elims)
case lock thus ?thesis by(auto simp add: mbisim_eqs dest!: fin')
next
case (join t')
from ‹r1.not_final_thread s1 t'› obtain x1 ln
where "thr s1 t' = ⌊(x1, ln)⌋" by cases auto
with mbisim obtain x2 where "ts2' t' = ⌊(x2, ln)⌋" "t' ⊢ (x1, shr s1) ≈ (x2, m2)" by(auto dest: mbisim_thrD1)
show ?thesis
proof(cases "wset s1 t' = None ∧ ln = no_wait_locks")
case False
with ‹r1.not_final_thread s1 t'› ‹thr s1 t' = ⌊(x1, ln)⌋› ‹ts2' t' = ⌊(x2, ln)⌋› ‹lt = Inr (Inl t')› join
show ?thesis by(auto simp add: mbisim_eqs r2.not_final_thread_iff r1.final_thread_def)
next
case True
with ‹r1.not_final_thread s1 t'› ‹thr s1 t' = ⌊(x1, ln)⌋› have "¬ final1 x1" by(cases) auto
with join ‹thr s1 t' = ⌊(x1, ln)⌋› have "t' ∈ r1.deadlocked s1" by(auto simp add: r1.final_thread_def)
have "¬ final2 x2"
proof
assume "final2 x2"
with final2_simulation[OF ‹t' ⊢ (x1, shr s1) ≈ (x2, m2)›]
obtain x1' m1' where "r1.silent_moves t' (x1, shr s1) (x1', m1')"
and "t' ⊢ (x1', m1') ≈ (x2, m2)" "final1 x1'" by auto
from ‹r1.silent_moves t' (x1, shr s1) (x1', m1')› have "x1' = x1"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names refl step])
case (step x1'' m1'')
from ‹r1.silent_move t' (x1, shr s1) (x1'', m1'')›
have "t' ⊢ (x1, shr s1) -1-ε→ (x1'', m1'')" by(auto dest: r1.silent_tl)
hence "r1.redT s1 (t', ε) (redT_upd_ε s1 t' x1'' m1'')"
using ‹thr s1 t' = ⌊(x1, ln)⌋› True
by -(erule r1.redT_normal, auto simp add: redT_updLns_def redT_updWs_def finfun_Diag_const2 o_def)
hence False using ‹t' ∈ r1.deadlocked s1› by(rule r1.red_no_deadlock)
thus ?thesis ..
qed simp
with ‹¬ final1 x1› ‹final1 x1'› show False by simp
qed
thus ?thesis using ‹ts2' t' = ⌊(x2, ln)⌋› join
by(auto simp add: r2.not_final_thread_iff r1.final_thread_def)
qed
next
case (interrupt t')
have "r2.all_final_except ?s2 (r1.deadlocked s1 ∪ r2.deadlocked ?s2 ∪ r2.final_threads ?s2)"
proof(rule r2.all_final_exceptI)
fix t''
assume "r2.not_final_thread ?s2 t''"
then obtain x2 ln where "thr ?s2 t'' = ⌊(x2, ln)⌋"
and fin: "¬ final2 x2 ∨ ln ≠ no_wait_locks ∨ wset ?s2 t'' ≠ None"
by(auto simp add: r2.not_final_thread_iff)
from ‹thr ?s2 t'' = ⌊(x2, ln)⌋› mbisim
obtain x1 where ts1t'': "thr s1 t'' = ⌊(x1, ln)⌋"
and bisim'': "t'' ⊢ (x1, shr s1) ≈ (x2, shr ?s2)"
by(auto dest: mbisim_thrD2)
have "r1.not_final_thread s1 t''"
proof(cases "wset ?s2 t'' = None ∧ ln = no_wait_locks")
case True
with fin have "¬ final2 x2" by simp
hence "¬ final1 x1"
proof(rule contrapos_nn)
assume "final1 x1"
with final1_simulation[OF bisim'']
obtain x2' m2' where τs2: "r2.silent_moves t'' (x2, shr ?s2) (x2', m2')"
and bisim''': "t'' ⊢ (x1, shr s1) ≈ (x2', m2')"
and "final2 x2'" by auto
from τs2 have "x2' = x2"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names refl step])
case refl thus ?thesis by simp
next
case (step x2'' m2'')
from True have "wset s1 t'' = None" "thr s1 t'' = ⌊(x1, no_wait_locks)⌋" "ts2' t'' = ⌊(x2, no_wait_locks)⌋"
using ts1t'' ‹thr ?s2 t'' = ⌊(x2, ln)⌋› mbisim by(simp_all add: mbisim_def)
hence no_τ2: "¬ r2.silent_move t'' (x2, m2) (x2'', m2'')"
proof(rule no_τ)
fix x1' m1'
assume "r1.silent_move t'' (x1, shr s1) (x1', m1')"
with ‹final1 x1› show False by(auto dest: r1.final_no_red)
qed
with ‹r2.silent_move t'' (x2, shr ?s2) (x2'', m2'')› have False by simp
thus ?thesis ..
qed
with ‹final2 x2'› show "final2 x2" by simp
qed
with ts1t'' show ?thesis ..
next
case False
with ts1t'' mbisim show ?thesis by(auto simp add: r1.not_final_thread_iff mbisim_def)
qed
with ‹r1.all_final_except s1 (r1.deadlocked s1 ∪ r1.final_threads s1)›
have "t'' ∈ r1.deadlocked s1 ∪ r1.final_threads s1" by(rule r1.all_final_exceptD)
thus "t'' ∈ r1.deadlocked s1 ∪ r2.deadlocked ?s2 ∪ r2.final_threads ?s2"
by(auto dest: fin' simp add: mbisim_eqs)
qed
thus ?thesis using interrupt mbisim by(auto simp add: mbisim_def)
qed
hence "∃lt∈LT. r2.must_wait ?s2 t lt (r1.deadlocked s1 ∪ r2.deadlocked ?s2 ∪ r2.final_threads ?s2)"
using ‹lt ∈ LT› by blast }
moreover from mbisim ‹wset s1 t = None› have "wset ?s2 t = None" by(simp add: mbisim_def)
ultimately have ?Lock by simp
thus ?thesis ..
next
case (wait x1 ln)
from mbisim ‹thr s1 t = ⌊(x1, ln)⌋›
obtain x2 where "ts2' t = ⌊(x2, ln)⌋" by(auto dest: mbisim_thrD1)
moreover
have "r2.all_final_except ?s2 (r1.deadlocked s1)"
proof(rule r2.all_final_exceptI)
fix t
assume "r2.not_final_thread ?s2 t"
then obtain x2 ln where "ts2' t = ⌊(x2, ln)⌋" by(auto simp add: r2.not_final_thread_iff)
with mbisim obtain x1 where "thr s1 t = ⌊(x1, ln)⌋" "t ⊢ (x1, shr s1) ≈ (x2, m2)" by(auto dest: mbisim_thrD2)
hence "r1.not_final_thread s1 t" using ‹r2.not_final_thread ?s2 t› ‹ts2' t = ⌊(x2, ln)⌋› mbisim fin'[of t]
by(cases "wset s1 t")(auto simp add: r1.not_final_thread_iff r2.not_final_thread_iff mbisim_def r1.final_thread_def r2.final_thread_def)
with ‹r1.all_final_except s1 (r1.deadlocked s1)›
show "t ∈ r1.deadlocked s1" by(rule r1.all_final_exceptD)
qed
hence "r2.all_final_except ?s2 (r1.deadlocked s1 ∪ r2.deadlocked ?s2)"
by(rule r2.all_final_except_mono') blast
moreover
from ‹waiting (wset s1 t)› mbisim
have "waiting (wset ?s2 t)" by(simp add: mbisim_def)
ultimately have ?Wait by simp
thus ?thesis by blast
next
case (acquire x1 ln l t')
from mbisim ‹thr s1 t = ⌊(x1, ln)⌋›
obtain x2 where "ts2' t = ⌊(x2, ln)⌋" by(auto dest: mbisim_thrD1)
moreover
from ‹t' ∈ r1.deadlocked s1 ∨ r1.final_thread s1 t'›
have "(t' ∈ r1.deadlocked s1 ∨ t' ∈ r2.deadlocked ?s2) ∨ r2.final_thread ?s2 t'" by(blast dest: fin')
moreover
from mbisim ‹has_lock (locks s1 $ l) t'›
have "has_lock (locks ?s2 $ l) t'" by(simp add: mbisim_def)
ultimately have ?Acquire
using ‹0 < ln $ l› ‹t ≠ t'› ‹¬ waiting (wset s1 t)› mbisim
by(auto simp add: mbisim_def)
thus ?thesis by blast
qed
qed
with red1 red2 mbisim show ?thesis by(blast intro: rtranclp_trans)
qed
lemma deadlocked2_imp_τs_deadlocked1:
"⟦ s1 ≈m s2; t ∈ r2.deadlocked s2 ⟧
⟹ ∃s1'. r1.mthr.silent_moves s1 s1' ∧ t ∈ r1.deadlocked s1' ∧ s1' ≈m s2"
using FWdelay_bisimulation_diverge.deadlocked1_imp_τs_deadlocked2[OF FWdelay_bisimulation_diverge_flip]
unfolding flip_simps .
lemma deadlock1_imp_τs_deadlock2:
assumes mbisim: "s1 ≈m s2"
and dead: "r1.deadlock s1"
shows "∃s2'. r2.mthr.silent_moves s2 s2' ∧ r2.deadlock s2' ∧ s1 ≈m s2'"
proof(cases "∃t. r1.not_final_thread s1 t")
case True
then obtain t where nfin: "r1.not_final_thread s1 t" ..
from mfinal1_inv_simulation[OF mbisim]
obtain ls2 ts2 m2 ws2 is2 where red1: "r2.mthr.silent_moves s2 (ls2, (ts2, m2), ws2, is2)"
and "s1 ≈m (ls2, (ts2, m2), ws2, is2)" and "m2 = shr s2"
and fin: "⋀t. r1.final_thread s1 t ⟹ r2.final_thread (ls2, (ts2, m2), ws2, is2) t" by fastforce
from no_τMove1_τs_to_no_τMove2[OF ‹s1 ≈m (ls2, (ts2, m2), ws2, is2)›]
obtain ts2' where red2: "r2.mthr.silent_moves (ls2, (ts2, m2), ws2, is2) (ls2, (ts2', m2), ws2, is2)"
and no_τ: "⋀t x1 x2 x2' m2'. ⟦ wset s1 t = None; thr s1 t = ⌊(x1, no_wait_locks)⌋; ts2' t = ⌊(x2, no_wait_locks)⌋;
⋀x' m'. r1.silent_move t (x1, shr s1) (x', m') ⟹ False ⟧
⟹ ¬ r2.silent_move t (x2, m2) (x2', m2')"
and mbisim: "s1 ≈m (ls2, (ts2', m2), ws2, is2)" by fastforce
from mbisim have mbisim_eqs: "ls2 = locks s1" "ws2 = wset s1" "is2 = interrupts s1"
by(simp_all add: mbisim_def)
let ?s2 = "(ls2, (ts2', m2), ws2, is2)"
from red2 have fin': "⋀t. r1.final_thread s1 t ⟹ r2.final_thread ?s2 t"
by(rule r2.τmRedT_preserves_final_thread)(rule fin)
have "r2.deadlock ?s2"
proof(rule r2.deadlockI, goal_cases)
case (1 t x2)
note ts2t = ‹thr ?s2 t = ⌊(x2, no_wait_locks)⌋›
with mbisim obtain x1 where ts1t: "thr s1 t = ⌊(x1, no_wait_locks)⌋"
and bisim: "t ⊢ (x1, shr s1) ≈ (x2, m2)" by(auto dest: mbisim_thrD2)
from ‹wset ?s2 t = None› mbisim have ws1t: "wset s1 t = None" by(simp add: mbisim_def)
have "¬ final1 x1"
proof
assume "final1 x1"
with ts1t ws1t have "r1.final_thread s1 t" by(simp add: r1.final_thread_def)
hence "r2.final_thread ?s2 t" by(rule fin')
with ‹¬ final2 x2› ts2t ‹wset ?s2 t = None› show False by(simp add: r2.final_thread_def)
qed
from r1.deadlockD1[OF dead ts1t this ‹wset s1 t = None›]
have ms: "r1.must_sync t x1 (shr s1)"
and csmw: "⋀LT. r1.can_sync t x1 (shr s1) LT ⟹ ∃lt∈LT. r1.must_wait s1 t lt (dom (thr s1))"
by blast+
{
from ‹r1.must_sync t x1 (shr s1)› obtain ta1 x1' m1'
where r1: "t ⊢ (x1, shr s1) -1-ta1→ (x1', m1')"
and s1': "∃s1'. r1.actions_ok s1' t ta1" by(fastforce elim: r1.must_syncE)
have "¬ τmove1 (x1, shr s1) ta1 (x1', m1')" (is "¬ ?τ")
proof
assume "?τ"
hence "ta1 = ε" by(rule r1.silent_tl)
with r1 have "r1.can_sync t x1 (shr s1) {}"
by(auto intro!: r1.can_syncI simp add: collect_locks_def collect_interrupts_def)
from csmw[OF this] show False by blast
qed
from simulation1[OF bisim r1 this]
obtain x2' m2' x2'' m2'' ta2 where r2: "r2.silent_moves t (x2, m2) (x2', m2')"
and r2': "t ⊢ (x2', m2') -2-ta2→ (x2'', m2'')"
and bisim': "t ⊢ (x1', m1') ≈ (x2'', m2'')" and tasim: "ta1 ∼m ta2" by auto
from r2
have "∃ta2 x2' m2' s2'. t ⊢ (x2, m2) -2-ta2→ (x2', m2') ∧ r2.actions_ok s2' t ta2"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names base step])
case base
from r2'[folded base] s1'[unfolded ex_actions_ok1_conv_ex_actions_ok2[OF tasim]]
show ?thesis by blast
next
case (step x2''' m2''')
hence "t ⊢ (x2, m2) -2-ε→ (x2''', m2''')" by(auto dest: r2.silent_tl)
moreover have "r2.actions_ok (undefined, (undefined, undefined), Map.empty, undefined) t ε" by auto
ultimately show ?thesis by-(rule exI conjI|assumption)+
qed
hence "r2.must_sync t x2 m2" unfolding r2.must_sync_def2 . }
moreover
{ fix LT
assume "r2.can_sync t x2 m2 LT"
then obtain ta2 x2' m2' where r2: "t ⊢ (x2, m2) -2-ta2→ (x2', m2')"
and LT: "LT = collect_locks ⦃ta2⦄⇘l⇙ <+> collect_cond_actions ⦃ta2⦄⇘c⇙ <+> collect_interrupts ⦃ta2⦄⇘i⇙"
by(auto elim: r2.can_syncE)
from ts2t have "ts2' t = ⌊(x2, no_wait_locks)⌋" by simp
with ws1t ts1t have "¬ r2.silent_move t (x2, m2) (x2', m2')"
proof(rule no_τ)
fix x1' m1'
assume "r1.silent_move t (x1, shr s1) (x1', m1')"
hence "t ⊢ (x1, shr s1) -1-ε→ (x1', m1')" by(auto dest: r1.silent_tl)
hence "r1.can_sync t x1 (shr s1) {}"
by(auto intro: r1.can_syncI simp add: collect_locks_def collect_interrupts_def)
with csmw[OF this] show False by blast
qed
with r2 have "¬ τmove2 (x2, m2) ta2 (x2', m2')" by auto
from simulation2[OF bisim r2 this] obtain x1' m1' x1'' m1'' ta1
where τr1: "r1.silent_moves t (x1, shr s1) (x1', m1')"
and r1: "t ⊢ (x1', m1') -1-ta1→ (x1'', m1'')"
and nτ1: "¬ τmove1 (x1', m1') ta1 (x1'', m1'')"
and bisim': "t ⊢ (x1'', m1'') ≈ (x2', m2')"
and tlsim: "ta1 ∼m ta2" by auto
from τr1 obtain [simp]: "x1' = x1" "m1' = shr s1"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names refl step])
case (step X M)
from ‹r1.silent_move t (x1, shr s1) (X, M)›
have "t ⊢ (x1, shr s1) -1-ε→ (X, M)" by(auto dest: r1.silent_tl)
hence "r1.can_sync t x1 (shr s1) {}"
by(auto intro: r1.can_syncI simp add: collect_locks_def collect_interrupts_def)
with csmw[OF this] have False by blast
thus ?thesis ..
qed blast
from tlsim LT have "LT = collect_locks ⦃ta1⦄⇘l⇙ <+> collect_cond_actions ⦃ta1⦄⇘c⇙ <+> collect_interrupts ⦃ta1⦄⇘i⇙"
by(auto simp add: ta_bisim_def)
with r1 have "r1.can_sync t x1 (shr s1) LT" by(auto intro: r1.can_syncI)
from csmw[OF this] obtain lt
where lt: "lt ∈ LT" "r1.must_wait s1 t lt (dom (thr s1))" by blast
from ‹r1.must_wait s1 t lt (dom (thr s1))› have "r2.must_wait ?s2 t lt (dom (thr ?s2))"
proof(cases rule: r1.must_wait_elims)
case (lock l)
with mbisim_dom_eq[OF mbisim] show ?thesis by(auto simp add: mbisim_eqs)
next
case (join t')
from dead deadlock_mbisim_not_final_thread_pres[OF _ ‹r1.not_final_thread s1 t'› fin' mbisim]
have "r2.not_final_thread ?s2 t'" by auto
thus ?thesis using join mbisim_dom_eq[OF mbisim] by auto
next
case (interrupt t')
have "r2.all_final_except ?s2 (dom (thr ?s2))" by(auto intro!: r2.all_final_exceptI)
with interrupt show ?thesis by(auto simp add: mbisim_eqs)
qed
with lt have "∃lt∈LT. r2.must_wait ?s2 t lt (dom (thr ?s2))" by blast }
ultimately show ?case by fastforce
next
case (2 t x2 ln l)
note dead moreover
from mbisim ‹thr ?s2 t = ⌊(x2, ln)⌋›
obtain x1 where "thr s1 t = ⌊(x1, ln)⌋" by(auto dest: mbisim_thrD2)
moreover note ‹0 < ln $ l›
moreover from ‹¬ waiting (wset ?s2 t)› mbisim
have "¬ waiting (wset s1 t)" by(simp add: mbisim_def)
ultimately obtain l' t' where "0 < ln $ l'" "t ≠ t'" "thr s1 t' ≠ None" "has_lock (locks s1 $ l') t'"
by(rule r1.deadlockD2)
thus ?case using mbisim_thrNone_eq[OF mbisim, of t'] mbisim by(auto simp add: mbisim_def)
next
case (3 t x2 w)
from mbisim_thrD2[OF mbisim this]
obtain x1 where "thr s1 t = ⌊(x1, no_wait_locks)⌋" by auto
with dead have "wset s1 t ≠ ⌊PostWS w⌋" by(rule r1.deadlockD3[rule_format])
with mbisim show ?case by(simp add: mbisim_def)
qed
with red1 red2 mbisim show ?thesis by(blast intro: rtranclp_trans)
next
case False
hence "r1.mfinal s1" by(auto intro: r1.mfinalI simp add: r1.not_final_thread_iff)
from mfinal1_simulation[OF mbisim this]
obtain s2' where "τmRed2 s2 s2'" "s1 ≈m s2'" "r2.mfinal s2'" "shr s2' = shr s2" by blast
thus ?thesis by(blast intro: r2.mfinal_deadlock)
qed
lemma deadlock2_imp_τs_deadlock1:
"⟦ s1 ≈m s2; r2.deadlock s2 ⟧
⟹ ∃s1'. r1.mthr.silent_moves s1 s1' ∧ r1.deadlock s1' ∧ s1' ≈m s2"
using FWdelay_bisimulation_diverge.deadlock1_imp_τs_deadlock2[OF FWdelay_bisimulation_diverge_flip]
unfolding flip_simps .
lemma deadlocked'1_imp_τs_deadlocked'2:
"⟦ s1 ≈m s2; r1.deadlocked' s1 ⟧
⟹ ∃s2'. r2.mthr.silent_moves s2 s2' ∧ r2.deadlocked' s2' ∧ s1 ≈m s2'"
unfolding r1.deadlock_eq_deadlocked'[symmetric] r2.deadlock_eq_deadlocked'[symmetric]
by(rule deadlock1_imp_τs_deadlock2)
lemma deadlocked'2_imp_τs_deadlocked'1:
"⟦ s1 ≈m s2; r2.deadlocked' s2 ⟧ ⟹ ∃s1'. r1.mthr.silent_moves s1 s1' ∧ r1.deadlocked' s1' ∧ s1' ≈m s2"
unfolding r1.deadlock_eq_deadlocked'[symmetric] r2.deadlock_eq_deadlocked'[symmetric]
by(rule deadlock2_imp_τs_deadlock1)
end
context FWbisimulation begin
lemma mbisim_final_thread_preserve1:
assumes mbisim: "s1 ≈m s2" and fin: "r1.final_thread s1 t"
shows "r2.final_thread s2 t"
proof -
from fin obtain x1 where ts1t: "thr s1 t = ⌊(x1, no_wait_locks)⌋"
and fin1: "final1 x1" and ws1t: "wset s1 t = None"
by(auto elim: r1.final_threadE)
from mbisim ts1t obtain x2
where ts2t: "thr s2 t = ⌊(x2, no_wait_locks)⌋"
and bisim: "t ⊢ (x1, shr s1) ≈ (x2, shr s2)" by(auto dest: mbisim_thrD1)
note ts2t moreover from fin1 bisim have "final2 x2" by(auto dest: bisim_final)
moreover from mbisim ws1t have "wset s2 t = None" by(simp add: mbisim_def)
ultimately show ?thesis by(rule r2.final_threadI)
qed
lemma mbisim_final_thread_preserve2:
"⟦ s1 ≈m s2; r2.final_thread s2 t ⟧ ⟹ r1.final_thread s1 t"
using FWbisimulation.mbisim_final_thread_preserve1[OF FWbisimulation_flip]
unfolding flip_simps .
lemma mbisim_final_thread_inv:
"s1 ≈m s2 ⟹ r1.final_thread s1 t ⟷ r2.final_thread s2 t"
by(blast intro: mbisim_final_thread_preserve1 mbisim_final_thread_preserve2)
lemma mbisim_not_final_thread_inv:
assumes bisim: "mbisim s1 s2"
shows "r1.not_final_thread s1 = r2.not_final_thread s2"
proof(rule ext)
fix t
show "r1.not_final_thread s1 t = r2.not_final_thread s2 t"
proof(cases "thr s1 t")
case None
with mbisim_thrNone_eq[OF bisim, of t] have "thr s2 t = None" by simp
with None show ?thesis
by(auto elim!: r2.not_final_thread.cases r1.not_final_thread.cases
intro: r2.not_final_thread.intros r1.not_final_thread.intros)
next
case (Some a)
then obtain x1 ln where tst1: "thr s1 t = ⌊(x1, ln)⌋" by(cases a) auto
from mbisim_thrD1[OF bisim tst1] obtain x2
where tst2: "thr s2 t = ⌊(x2, ln)⌋" and bisimt: "t ⊢ (x1, shr s1) ≈ (x2, shr s2)" by blast
from bisim have "wset s2 = wset s1" by(simp add: mbisim_def)
with tst2 tst1 bisim_final[OF bisimt] show ?thesis
by(simp add: r1.not_final_thread_conv r2.not_final_thread_conv)(rule mbisim_final_thread_inv[OF bisim])
qed
qed
lemma mbisim_deadlocked_preserve1:
assumes mbisim: "s1 ≈m s2" and dead: "t ∈ r1.deadlocked s1"
shows "t ∈ r2.deadlocked s2"
proof -
from deadlocked1_imp_τs_deadlocked2[OF mbisim dead]
obtain s2' where "r2.mthr.silent_moves s2 s2'"
and "t ∈ r2.deadlocked s2'" by blast
from ‹r2.mthr.silent_moves s2 s2'› have "s2' = s2"
by(rule converse_rtranclpE)(auto elim: r2.mτmove.cases)
with ‹t ∈ r2.deadlocked s2'› show ?thesis by simp
qed
lemma mbisim_deadlocked_preserve2:
"⟦ s1 ≈m s2; t ∈ r2.deadlocked s2 ⟧ ⟹ t ∈ r1.deadlocked s1"
using FWbisimulation.mbisim_deadlocked_preserve1[OF FWbisimulation_flip]
unfolding flip_simps .
lemma mbisim_deadlocked_inv:
"s1 ≈m s2 ⟹ r1.deadlocked s1 = r2.deadlocked s2"
by(blast intro!: mbisim_deadlocked_preserve1 mbisim_deadlocked_preserve2)
lemma mbisim_deadlocked'_inv:
"s1 ≈m s2 ⟹ r1.deadlocked' s1 ⟷ r2.deadlocked' s2"
unfolding r1.deadlocked'_def r2.deadlocked'_def
by(simp add: mbisim_not_final_thread_inv mbisim_deadlocked_inv)
lemma mbisim_deadlock_inv:
"s1 ≈m s2 ⟹ r1.deadlock s1 = r2.deadlock s2"
unfolding r1.deadlock_eq_deadlocked' r2.deadlock_eq_deadlocked'
by(rule mbisim_deadlocked'_inv)
end
context FWbisimulation begin
lemma bisim_can_sync_preserve1:
assumes bisim: "t ⊢ (x1, m1) ≈ (x2, m2)" and cs: "t ⊢ ⟨x1, m1⟩ LT ≀1"
shows "t ⊢ ⟨x2, m2⟩ LT ≀2"
proof -
from cs obtain ta1 x1' m1' where red1: "t ⊢ (x1, m1) -1-ta1→ (x1', m1')"
and LT: "LT = collect_locks ⦃ta1⦄⇘l⇙ <+> collect_cond_actions ⦃ta1⦄⇘c⇙ <+> collect_interrupts ⦃ta1⦄⇘i⇙" by(rule r1.can_syncE)
from bisimulation.simulation1[OF bisimulation_axioms, OF bisim red1] obtain x2' ta2 m2'
where red2: "t ⊢ (x2, m2) -2-ta2→ (x2', m2')"
and tasim: "ta1 ∼m ta2" by fastforce
from tasim LT have "LT = collect_locks ⦃ta2⦄⇘l⇙ <+> collect_cond_actions ⦃ta2⦄⇘c⇙ <+> collect_interrupts ⦃ta2⦄⇘i⇙"
by(auto simp add: ta_bisim_def)
with red2 show ?thesis by(rule r2.can_syncI)
qed
lemma bisim_can_sync_preserve2:
"⟦ t ⊢ (x1, m1) ≈ (x2, m2); t ⊢ ⟨x2, m2⟩ LT ≀2 ⟧ ⟹ t ⊢ ⟨x1, m1⟩ LT ≀1"
using FWbisimulation.bisim_can_sync_preserve1[OF FWbisimulation_flip]
unfolding flip_simps .
lemma bisim_can_sync_inv:
"t ⊢ (x1, m1) ≈ (x2, m2) ⟹ t ⊢ ⟨x1, m1⟩ LT ≀1 ⟷ t ⊢ ⟨x2, m2⟩ LT ≀2"
by(blast intro: bisim_can_sync_preserve1 bisim_can_sync_preserve2)
lemma bisim_must_sync_preserve1:
assumes bisim: "t ⊢ (x1, m1) ≈ (x2, m2)" and ms: "t ⊢ ⟨x1, m1⟩ ≀1"
shows "t ⊢ ⟨x2, m2⟩ ≀2"
proof -
from ms obtain ta1 x1' m1' where red1: "t ⊢ (x1, m1) -1-ta1→ (x1', m1')"
and s1': "∃s1'. r1.actions_ok s1' t ta1" by(fastforce elim: r1.must_syncE)
from bisimulation.simulation1[OF bisimulation_axioms, OF bisim red1] obtain x2' ta2 m2'
where red2: "t ⊢ (x2, m2) -2-ta2→ (x2', m2')"
and tasim: "ta1 ∼m ta2" by fastforce
from ex_actions_ok1_conv_ex_actions_ok2[OF tasim, of t] s1' red2
show ?thesis unfolding r2.must_sync_def2 by blast
qed
lemma bisim_must_sync_preserve2:
"⟦ t ⊢ (x1, m1) ≈ (x2, m2); t ⊢ ⟨x2, m2⟩ ≀2 ⟧ ⟹ t ⊢ ⟨x1, m1⟩ ≀1"
using FWbisimulation.bisim_must_sync_preserve1[OF FWbisimulation_flip]
unfolding flip_simps .
lemma bisim_must_sync_inv:
"t ⊢ (x1, m1) ≈ (x2, m2) ⟹ t ⊢ ⟨x1, m1⟩ ≀1 ⟷ t ⊢ ⟨x2, m2⟩ ≀2"
by(blast intro: bisim_must_sync_preserve1 bisim_must_sync_preserve2)
end
end