```(*  Title:      JinjaThreads/Framework/FWDeadlock.thy
Author:     Andreas Lochbihler
*)

imports
FWProgressAux
begin

definition all_final_except :: "('l,'t,'x,'m,'w) state ⇒ 't set ⇒ bool" where
"all_final_except s Ts ≡ ∀t. not_final_thread s t ⟶ t ∈ Ts"

lemma all_final_except_mono [mono]:
"(⋀x. x ∈ A ⟶ x ∈ B) ⟹ all_final_except ts A ⟶ all_final_except ts B"

lemma all_final_except_mono':
"⟦ all_final_except ts A; ⋀x. x ∈ A ⟹ x ∈ B ⟧ ⟹ all_final_except ts B"
by(blast intro: all_final_except_mono[rule_format])

lemma all_final_exceptI:
"(⋀t. not_final_thread s t ⟹ t ∈ Ts) ⟹ all_final_except s Ts"

lemma all_final_exceptD:
"⟦ all_final_except s Ts; not_final_thread s t ⟧ ⟹ t ∈ Ts"

inductive must_wait :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ ('l + 't + 't) ⇒ 't set ⇒ bool"
for s :: "('l,'t,'x,'m,'w) state" and t :: "'t" where
― ‹Lock l›
"⟦ has_lock (locks s \$ l) t'; t' ≠ t; t' ∈ Ts ⟧ ⟹ must_wait s t (Inl l) Ts"
| ― ‹Join t'›
"⟦ not_final_thread s t'; t' ∈ Ts ⟧ ⟹ must_wait s t (Inr (Inl t')) Ts"
| ― ‹IsInterrupted t' True›
"⟦ all_final_except s Ts; t' ∉ interrupts s ⟧ ⟹ must_wait s t (Inr (Inr t')) Ts"

declare must_wait.cases [elim]
declare must_wait.intros [intro]

lemma must_wait_elims [consumes 1, case_names lock join interrupt, cases pred]:
assumes "must_wait s t lt Ts"
obtains l t' where "lt = Inl l" "has_lock (locks s \$ l) t'" "t' ≠ t" "t' ∈ Ts"
| t' where "lt = Inr (Inl t')" "not_final_thread s t'" "t' ∈ Ts"
| t' where "lt = Inr (Inr t')" "all_final_except s Ts" "t' ∉ interrupts s"
using assms
by(auto)

inductive_cases must_wait_elims2 [elim!]:
"must_wait s t (Inl l) Ts"
"must_wait s t (Inr (Inl t'')) Ts"
"must_wait s t (Inr (Inr t'')) Ts"

lemma must_wait_iff:
"must_wait s t lt Ts ⟷
(case lt of Inl l ⇒ ∃t'∈Ts. t ≠ t' ∧ has_lock (locks s \$ l) t'
| Inr (Inl t') ⇒ not_final_thread s t' ∧ t' ∈ Ts
| Inr (Inr t') ⇒ all_final_except s Ts ∧ t' ∉ interrupts s)"
by(auto simp add: must_wait.simps split: sum.splits)

end

definition
deadlock :: "('l,'t,'x,'m,'w) state ⇒ bool"
where
≡   (∀t x. thr s t = ⌊(x, no_wait_locks)⌋ ∧ ¬ final x ∧ wset s t = None
⟶ t ⊢ ⟨x, shr s⟩ ≀ ∧ (∀LT. t ⊢ ⟨x, shr s⟩ LT ≀ ⟶ (∃lt ∈ LT. must_wait s t lt (dom (thr s)))))
∧ (∀t x ln. thr s t = ⌊(x, ln)⌋ ∧ (∃l. ln \$ l > 0) ∧ ¬ waiting (wset s t)
⟶ (∃l t'. ln \$ l > 0 ∧ t ≠ t' ∧ thr s t' ≠ None ∧ has_lock (locks s \$ l) t'))
∧ (∀t x w. thr s t = ⌊(x, no_wait_locks)⌋ ⟶ wset s t ≠ ⌊PostWS w⌋)"

"⟦ ⋀t x. ⟦ thr s t = ⌊(x, no_wait_locks)⌋; ¬ final x; wset s t = None ⟧
⟹ t ⊢ ⟨x, shr s⟩ ≀ ∧ (∀LT. t ⊢ ⟨x, shr s⟩ LT ≀ ⟶ (∃lt ∈ LT. must_wait s t lt (dom (thr s))));
⋀t x ln l. ⟦ thr s t = ⌊(x, ln)⌋; ln \$ l > 0; ¬ waiting (wset s t) ⟧
⟹ ∃l t'. ln \$ l > 0 ∧ t ≠ t' ∧ thr s t' ≠ None ∧ has_lock (locks s \$ l) t';
⋀t x w. thr s t = ⌊(x, no_wait_locks)⌋ ⟹ wset s t ≠ ⌊PostWS w⌋ ⟧

obtains "∀t x. thr s t = ⌊(x, no_wait_locks)⌋ ∧ ¬ final x ∧ wset s t = None
⟶ t ⊢ ⟨x, shr s⟩ ≀ ∧ (∀LT. t ⊢ ⟨x, shr s⟩ LT ≀ ⟶ (∃lt ∈ LT. must_wait s t lt (dom (thr s))))"
and "∀t x ln. thr s t = ⌊(x, ln)⌋ ∧ (∃l. ln \$ l > 0) ∧ ¬ waiting (wset s t)
⟶ (∃l t'. ln \$ l > 0 ∧ t ≠ t' ∧ thr s t' ≠ None ∧ has_lock (locks s \$ l) t')"
and "∀t x w. thr s t = ⌊(x, no_wait_locks)⌋ ⟶ wset s t ≠ ⌊PostWS w⌋"

and "thr s t = ⌊(x, no_wait_locks)⌋"
and "¬ final x"
and "wset s t = None"
obtains "t ⊢ ⟨x, shr s⟩ ≀"
and "∀LT. t ⊢ ⟨x, shr s⟩ LT ≀ ⟶ (∃lt ∈ LT. must_wait s t lt (dom (thr s)))"

fixes ln
and "thr s t = ⌊(x, ln)⌋"
and "ln \$ l > 0"
and "¬ waiting (wset s t)"
obtains l' t' where "ln \$ l' > 0" "t ≠ t'" "thr s t' ≠ None" "has_lock (locks s \$ l') t'"
using assms unfolding deadlock_def by blast

and "thr s t = ⌊(x, no_wait_locks)⌋"
shows "∀w. wset s t ≠ ⌊PostWS w⌋"
using assms unfolding deadlock_def by blast

(∀t x. thr s t = ⌊(x, no_wait_locks)⌋ ∧ ¬ final x ∧ wset s t = None
⟶ t ⊢ ⟨x, shr s⟩ ≀ ∧ (∀LT. t ⊢ ⟨x, shr s⟩ LT ≀ ⟶ (∃lt ∈ LT. must_wait s t lt (dom (thr s)))))
∧ (∀t x ln. thr s t = ⌊(x, ln)⌋ ∧ ln ≠ no_wait_locks ∧ ¬ waiting (wset s t)
⟶ (∃l. ln \$ l > 0 ∧ must_wait s t (Inl l) (dom (thr s))))
∧ (∀t x w. thr s t = ⌊(x, no_wait_locks)⌋ ⟶ wset s t ≠ ⌊PostWS WSNotified⌋ ∧ wset s t ≠ ⌊PostWS WSWokenUp⌋)"
unfolding neq_no_wait_locks_conv
apply(rule iffI)
apply(intro strip conjI)
apply(elim conjE exE)
apply blast
apply(rotate_tac 1)
apply(erule allE, rotate_tac -1)
apply(erule allE, rotate_tac -1)
apply(erule allE, rotate_tac -1)
apply(erule impE, blast)
apply(elim exE conjE)
apply(erule must_wait.cases)
apply(clarify)
apply(rotate_tac 3)
apply(rule exI conjI|erule not_sym|assumption)+
apply blast
apply blast
apply blast
apply blast
apply(case_tac w)
apply blast
apply blast
done

assumes "lock_thread_ok (locks s) (thr s)"
and normal: "⋀t x. ⟦ thr s t = ⌊(x, no_wait_locks)⌋; ¬ final x; wset s t = None ⟧
⟹ t ⊢ ⟨x, shr s⟩ ≀ ∧ (∀LT. t ⊢ ⟨x, shr s⟩ LT ≀ ⟶ (∃lt ∈ LT. must_wait s t lt (dom (thr s))))"
and acquire: "⋀t x ln l. ⟦ thr s t = ⌊(x, ln)⌋; ¬ waiting (wset s t); ln \$ l > 0 ⟧
⟹ ∃l'. ln \$ l' > 0 ∧ ¬ may_lock (locks s \$ l') t"
and wakeup: "⋀t x w. thr s t = ⌊(x, no_wait_locks)⌋ ⟹ wset s t ≠ ⌊PostWS w⌋"
fix T X
assume "thr s T = ⌊(X, no_wait_locks)⌋" "¬ final X" "wset s T = None"
thus "T ⊢ ⟨X, shr s⟩ ≀ ∧ (∀LT. T ⊢ ⟨X, shr s⟩ LT ≀ ⟶ (∃lt∈LT. must_wait s T lt (dom (thr s))))"
by(rule normal)
next
fix T X LN l'
assume "thr s T = ⌊(X, LN)⌋"
and "0 < LN \$ l'"
and wset: "¬ waiting (wset s T)"
from acquire[OF ‹thr s T = ⌊(X, LN)⌋› wset, OF ‹0 < LN \$ l'›]
obtain l' where "0 < LN \$ l'" "¬ may_lock (locks s \$ l') T" by blast
then obtain t' where "T ≠ t'" "has_lock (locks s \$ l') t'"
unfolding not_may_lock_conv by fastforce
moreover with ‹lock_thread_ok (locks s) (thr s)›
have "thr s t' ≠ None" by(auto dest: lock_thread_okD)
ultimately show "∃l t'. 0 < LN \$ l ∧ T ≠ t' ∧ thr s t' ≠ None ∧ has_lock (locks s \$ l) t'"
using ‹0 < LN \$ l'› by(auto)
qed(rule wakeup)

unfolding mfinal_def2

lemma must_wait_mono:
"(⋀x. x ∈ A ⟶ x ∈ B) ⟹ must_wait s t lt A ⟶ must_wait s t lt B"
by(auto simp add: must_wait_iff split: sum.split elim: all_final_except_mono')

lemma must_wait_mono':
"⟦ must_wait s t lt A; A ⊆ B ⟧ ⟹ must_wait s t lt B"
using must_wait_mono[of A B s t lt]
by blast

end

lemma UN_mono: "⟦ x ∈ A ⟶ x ∈ A'; x ∈ B ⟶ x ∈ B' ⟧ ⟹ x ∈ A ∪ B ⟶ x ∈ A' ∪ B'"
by blast

lemma Collect_mono_conv [mono]: "x ∈ {x. P x} ⟷ P x"
by blast

coinductive_set deadlocked :: "('l,'t,'x,'m,'w) state ⇒ 't set"
for s :: "('l,'t,'x,'m,'w) state" where
"⟦ thr s t = ⌊(x, no_wait_locks)⌋; t ⊢ ⟨x, shr s⟩ ≀; wset s t = None;
⋀LT. t ⊢ ⟨x, shr s⟩ LT ≀ ⟹ ∃lt ∈ LT. must_wait s t lt (deadlocked s ∪ final_threads s) ⟧

"⋀ln. ⟦ thr s t = ⌊(x, ln)⌋; all_final_except s (deadlocked s); waiting (wset s t) ⟧ ⟹ t ∈ deadlocked s"

"⋀ln. ⟦ thr s t = ⌊(x, ln)⌋; ¬ waiting (wset s t); ln \$ l > 0; has_lock (locks s \$ l) t'; t' ≠ t;
monos must_wait_mono UN_mono

"⋀ln. ⟦ thr s t = ⌊(x, ln)⌋; ¬ waiting (wset s t); ln \$ l > 0; must_wait s t (Inl l) (deadlocked s ∪ final_threads s) ⟧
apply(erule must_wait_elims)
apply auto
done

lemma deadlocked_elims [consumes 1, case_names lock wait acquire]:
and lock: "⋀x. ⟦ thr s t = ⌊(x, no_wait_locks)⌋; t ⊢ ⟨x, shr s⟩ ≀; wset s t = None;
⋀LT. t ⊢ ⟨x, shr s⟩ LT ≀ ⟹ ∃lt ∈ LT. must_wait s t lt (deadlocked s ∪ final_threads s) ⟧
⟹ thesis"
and wait: "⋀x ln. ⟦ thr s t = ⌊(x, ln)⌋; all_final_except s (deadlocked s); waiting (wset s t) ⟧
⟹ thesis"
and acquire: "⋀x ln l t'.
⟦ thr s t = ⌊(x, ln)⌋; ¬ waiting (wset s t); 0 < ln \$ l; has_lock (locks s \$ l) t'; t ≠ t';
shows thesis
using assms by cases blast+

assumes major: "t ∈ X"
and step:
"⋀t. t ∈ X ⟹
(∃x. thr s t = ⌊(x, no_wait_locks)⌋ ∧ t ⊢ ⟨x, shr s⟩ ≀ ∧ wset s t = None ∧
(∀LT. t ⊢ ⟨x, shr s⟩ LT ≀ ⟶ (∃lt∈LT. must_wait s t lt (X ∪ deadlocked s ∪ final_threads s)))) ∨
(∃x ln. thr s t = ⌊(x, ln)⌋ ∧ all_final_except s (X ∪ deadlocked s) ∧ waiting (wset s t)) ∨
(∃x l t' ln. thr s t = ⌊(x, ln)⌋ ∧ ¬ waiting (wset s t) ∧ 0 < ln \$ l ∧ has_lock (locks s \$ l) t' ∧
t' ≠ t ∧ ((t' ∈ X ∨ t' ∈ deadlocked s) ∨ final_thread s t'))"
using major
proof(coinduct)
have "X ∪ deadlocked s ∪ final_threads s = {x. x ∈ X ∨ x ∈ deadlocked s ∨ x ∈ final_threads s}"
by auto
moreover have "X ∪ deadlocked s = {x. x ∈ X ∨ x ∈ deadlocked s}" by blast
ultimately show ?case using step[OF deadlocked] by(elim disjE) simp_all
qed

definition deadlocked' :: "('l,'t,'x,'m,'w) state ⇒ bool" where

and "⋀x ln. thr s t = ⌊(x, ln)⌋ ⟹ thesis"
shows thesis
using assms
by cases blast+

end

assumes P: "s -t▹ta→ s'"
shows False
proof -
from P show False
proof(cases)
case (redT_normal x x' m')
note red = ‹t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩›
note tst = ‹thr s t = ⌊(x, no_wait_locks)⌋›
note aok = ‹actions_ok s t ta›
show False
proof(cases "∃w. wset s t = ⌊InWS w⌋")
case True with aok show ?thesis by(auto simp add: wset_actions_ok_def split: if_split_asm)
next
case False
have mle: "t ⊢ ⟨x, shr s⟩ ≀"
and cledead: "∀LT. t ⊢ ⟨x, shr s⟩ LT ≀ ⟶ (∃lt ∈ LT. must_wait s t lt (deadlocked s ∪ final_threads s))"
let ?LT = "collect_waits ta"
from red have "t ⊢ ⟨x, shr s⟩ ?LT ≀" by(auto intro: can_syncI)
then obtain lt where lt: "lt ∈ ?LT" and mw: "must_wait s t lt (deadlocked s ∪ final_threads s)"
from mw show False
proof(cases rule: must_wait_elims)
case (lock l t')
from ‹lt = Inl l› lt have "l ∈ collect_locks ⦃ta⦄⇘l⇙" by(auto)
with aok have "may_lock (locks s \$ l) t"
by(auto elim!: collect_locksE lock_ok_las_may_lock)
with ‹has_lock (locks s \$ l) t'› have "t' = t"
by(auto dest: has_lock_may_lock_t_eq)
with ‹t' ≠ t› show False by contradiction
next
case (join t')
from ‹lt = Inr (Inl t')› lt have "Join t' ∈ set ⦃ta⦄⇘c⇙" by auto
from ‹not_final_thread s t'›  obtain x'' ln''
where "thr s t' = ⌊(x'', ln'')⌋" by(rule not_final_thread_existsE)
moreover with ‹Join t' ∈ set ⦃ta⦄⇘c⇙› aok
have "final x''" "ln'' = no_wait_locks" "wset s t' = None"
by(auto dest: cond_action_oks_Join)
ultimately show False using ‹not_final_thread s t'› by(auto)
next
case (interrupt t')
from  aok lt ‹lt = Inr (Inr t')›
have "t' ∈ interrupts s"
by(auto intro: collect_interrupts_interrupted)
with ‹t' ∉ interrupts s› show False by contradiction
qed
qed
next
case (redT_acquire x n ln)
show False
proof(cases "∃w. wset s t = ⌊InWS w⌋")
case True with ‹¬ waiting (wset s t)› show ?thesis
next
case False
with dead ‹thr s t = ⌊(x, ln)⌋› ‹0 < ln \$ n›
obtain l t' where "0 < ln \$ l" "t ≠ t'"
and "has_lock (locks s \$ l) t'"
hence "¬ may_acquire_all (locks s) t ln"
by(auto elim: may_acquire_allE dest: has_lock_may_lock_t_eq)
with ‹may_acquire_all (locks s) t ln› show ?thesis by contradiction
qed
qed
qed

"⟦ s -t▹ta→ s'; deadlocked' s ⟧ ⟹ False"
apply(assumption)

"thr s t = ⌊xln⌋ ⟹ not_final_thread s t ∨ t ∈ deadlocked s ∨ final_thread s t"

and "lock_thread_ok (locks s) (thr s)"
and normal: "⋀t x. ⟦ thr s t = ⌊(x, no_wait_locks)⌋; ¬ final x; wset s t = None ⟧
⟹ t ⊢ ⟨x, shr s⟩ ≀ ∧ (∀LT. t ⊢ ⟨x, shr s⟩ LT ≀ ⟶ (∃lt∈LT. must_wait s t lt (final_threads s)))"
and acquire: "⋀t x ln l. ⟦ thr s t = ⌊(x, ln)⌋; ¬ waiting (wset s t); ln \$ l > 0 ⟧
⟹ ∃l'. ln \$ l' > 0 ∧ ¬ may_lock (locks s \$ l') t"
and wakeup: "⋀t x w. thr s t = ⌊(x, no_wait_locks)⌋ ⟹ wset s t ≠ ⌊PostWS w⌋"
proof -
have "t ∈ {t. not_final_thread s t}" by simp
thus ?thesis
proof(coinduct)
hence "not_final_thread s z" by simp
then obtain x' ln' where "thr s z = ⌊(x', ln')⌋" by(fastforce elim!: not_final_thread_existsE)
{
assume "wset s z = None" "¬ final x'"
and [simp]: "ln' = no_wait_locks"
with ‹thr s z = ⌊(x', ln')⌋›
have "z ⊢ ⟨x', shr s⟩ ≀ ∧ (∀LT. z ⊢ ⟨x', shr s⟩ LT ≀ ⟶ (∃lt ∈ LT. must_wait s z lt (final_threads s)))"
by(auto dest: normal)
then obtain "z ⊢ ⟨x', shr s⟩ ≀"
and clnml: "⋀LT. z ⊢ ⟨x', shr s⟩ LT ≀ ⟹ ∃lt ∈ LT. must_wait s z lt (final_threads s)" by(blast)
{ fix LT
assume "z ⊢ ⟨x', shr s⟩ LT ≀"
then obtain lt where mw: "must_wait s z lt (final_threads s)" and lt: "lt ∈ LT"
by(blast dest: clnml)
from mw have "must_wait s z lt ({t. not_final_thread s t} ∪ deadlocked s ∪ final_threads s)"
by(blast intro: must_wait_mono')
with lt have "∃lt ∈ LT. must_wait s z lt ({t. not_final_thread s t} ∪ deadlocked s ∪ final_threads s)"
by blast }
with ‹z ⊢ ⟨x', shr s⟩ ≀› ‹thr s z = ⌊(x', ln')⌋› ‹wset s z = None› have ?case by(simp) }
note c1 = this
{
assume wsz: "¬ waiting (wset s z)"
and "ln' ≠ no_wait_locks"
from ‹ln' ≠ no_wait_locks› obtain l where "0 < ln' \$ l"
with wsz ‹thr s z = ⌊(x', ln')⌋›
obtain l' where "0 < ln' \$ l'" "¬ may_lock (locks s \$ l') z"
by(blast dest: acquire)
then obtain t'' where "t'' ≠ z" "has_lock (locks s \$ l') t''"
unfolding not_may_lock_conv by blast
with ‹lock_thread_ok (locks s) (thr s)›
obtain x'' ln'' where "thr s t'' = ⌊(x'', ln'')⌋"
with wsz ‹0 < ln' \$ l'› ‹thr s z = ⌊(x', ln')⌋› ‹t'' ≠ z› ‹has_lock (locks s \$ l') t''›
have ?Acquire by simp blast
hence ?case by simp }
note c2 = this
{ fix w
assume "waiting (wset s z)"
with ‹thr s z = ⌊(x', ln')⌋›
have "?Wait" by(clarsimp simp add: all_final_except_def)
hence ?case by simp }
note c3 = this
from ‹not_final_thread s z› ‹thr s z = ⌊(x', ln')⌋› show ?case
case final show ?thesis
proof(cases "wset s z")
case None show ?thesis
proof(cases "ln' = no_wait_locks")
case True with None final show ?thesis by(rule c1)
next
case False
from None have "¬ waiting (wset s z)" by(simp add: not_waiting_iff)
thus ?thesis using False by(rule c2)
qed
next
case (Some w)
show ?thesis
proof(cases w)
case (InWS w')
with Some have "waiting (wset s z)" by(simp add: waiting_def)
thus ?thesis by(rule c3)
next
case (PostWS w')
with Some have "¬ waiting (wset s z)" by(simp add: not_waiting_iff)
moreover from PostWS ‹thr s z = ⌊(x', ln')⌋› Some
have "ln' ≠ no_wait_locks" by(auto dest: wakeup)
ultimately show ?thesis by(rule c2)
qed
qed
next
case wait_locks show ?thesis
proof(cases "wset s z")
case None
hence "¬ waiting (wset s z)" by(simp add: not_waiting_iff)
thus ?thesis using wait_locks by(rule c2)
next
case (Some w)
show ?thesis
proof(cases w)
case (InWS w')
with Some have "waiting (wset s z)" by(simp add: waiting_def)
thus ?thesis by(rule c3)
next
case (PostWS w')
with Some have "¬ waiting (wset s z)" by(simp add: not_waiting_iff)
moreover from PostWS ‹thr s z = ⌊(x', ln')⌋› Some
have "ln' ≠ no_wait_locks" by(auto dest: wakeup)
ultimately show ?thesis by(rule c2)
qed
qed
next
case (wait_set w)
show ?thesis
proof(cases w)
case (InWS w')
with wait_set have "waiting (wset s z)" by(simp add: waiting_def)
thus ?thesis by(rule c3)
next
case (PostWS w')
with wait_set have "¬ waiting (wset s z)" by(simp add: not_waiting_iff)
moreover from PostWS ‹thr s z = ⌊(x', ln')⌋› wait_set
have "ln' ≠ no_wait_locks" by(auto dest: wakeup[simplified])
ultimately show ?thesis by(rule c2)
qed
qed
qed
qed

text ‹Equivalence proof for both notions of deadlock›

proof -
show ?thesis
fix t
hence "t ∈ {t. not_final_thread s t}" ..
proof(coinduct)
then obtain x'' ln'' where tst'': "thr s t'' = ⌊(x'', ln'')⌋"
{ assume "waiting (wset s t'')"
moreover
with tst'' have nfine: "not_final_thread s t''"
unfolding waiting_def
ultimately have ?case using tst''
note c1 = this
{
assume wst'': "¬ waiting (wset s t'')"
and "ln'' ≠ no_wait_locks"
then obtain l where l: "ln'' \$ l > 0"
with dead wst'' tst'' obtain l' T
where "ln'' \$ l' > 0" "t'' ≠ T"
and hl: "has_lock (locks s \$ l') T"
and tsT: "thr s T ≠ None"
moreover from ‹thr s T ≠ None›
obtain xln where tsT: "thr s T = ⌊xln⌋" by auto
then obtain X LN where "thr s T = ⌊(X, LN)⌋"
by(cases xln, auto)
ultimately have ?case using wst'' tst'' by blast }
note c2 = this
{ assume "wset s t'' = None"
and [simp]: "ln'' = no_wait_locks"
moreover
have "¬ final x''" by(auto)
ultimately obtain "t'' ⊢ ⟨x'', shr s⟩ ≀"
and clnml: "⋀LT. t'' ⊢ ⟨x'', shr s⟩ LT ≀ ⟹ ∃t'. thr s t' ≠ None ∧ (∃lt∈LT. must_wait s t'' lt (dom (thr s)))"
using ‹thr s t'' = ⌊(x'', ln'')⌋› ‹deadlock s›
{ fix LT
assume "t'' ⊢ ⟨x'', shr s⟩ LT ≀"
then obtain lt where lt: "lt ∈ LT"
and mw: "must_wait s t'' lt (dom (thr s))"
by(blast dest: clnml)
note mw
finally have "∃lt∈LT. must_wait s t'' lt ({t. not_final_thread s t} ∪ deadlocked s ∪ final_threads s)"
using lt by blast }
with ‹t'' ⊢ ⟨x'', shr s⟩ ≀› tst'' ‹wset s t'' = None› have ?case by(simp) }
note c3 = this
from ‹not_final_thread s t''› tst'' show ?case
case final show ?thesis
proof(cases "wset s t''")
case None show ?thesis
proof(cases "ln'' = no_wait_locks")
case True with None show ?thesis by(rule c3)
next
case False
from None have "¬ waiting (wset s t'')" by(simp add: not_waiting_iff)
thus ?thesis using False by(rule c2)
qed
next
case (Some w)
show ?thesis
proof(cases w)
case (InWS w')
with Some have "waiting (wset s t'')" by(simp add: waiting_def)
thus ?thesis by(rule c1)
next
case (PostWS w')
hence "¬ waiting (wset s t'')" using Some by(simp add: not_waiting_iff)
moreover from PostWS Some tst''
ultimately show ?thesis by(rule c2)
qed
qed
next
case wait_locks show ?thesis
proof(cases "waiting (wset s t'')")
case False
thus ?thesis using wait_locks by(rule c2)
next
case True thus ?thesis by(rule c1)
qed
next
case (wait_set w)
show ?thesis
proof(cases w)
case InWS
with wait_set have "waiting (wset s t'')" by(simp add: waiting_def)
thus ?thesis by(rule c1)
next
case (PostWS w')
hence "¬ waiting (wset s t'')" using wait_set
moreover from PostWS wait_set tst''
ultimately show ?thesis by(rule c2)
qed
qed
qed
qed
qed

proof -
show ?thesis
fix t' x'
assume "thr s t' = ⌊(x', no_wait_locks)⌋"
and "¬ final x'"
and "wset s t' = None"
thus "t' ⊢ ⟨x', shr s⟩ ≀ ∧ (∀LT. t' ⊢ ⟨x', shr s⟩ LT ≀ ⟶ (∃lt ∈ LT. must_wait s t' lt (dom (thr s))))"
case (lock x'')
note lock = ‹⋀LT. t' ⊢ ⟨x'', shr s⟩ LT ≀ ⟹ ∃lt ∈ LT. must_wait s t' lt (deadlocked s ∪ final_threads s)›
from ‹thr s t' = ⌊(x'', no_wait_locks)⌋› ‹thr s t' = ⌊(x', no_wait_locks)⌋›
have [simp]: "x' = x''" by auto
{ fix LT
assume "t' ⊢ ⟨x'', shr s⟩ LT ≀"
from lock[OF this] obtain lt where lt: "lt ∈ LT"
and mw: "must_wait s t' lt (deadlocked s ∪ final_threads s)" by blast
with mw have "must_wait s t' lt (dom (thr s))" by(rule must_wait_mono')
with lt have "∃lt∈LT. must_wait s t' lt (dom (thr s))" by blast }
with ‹t' ⊢ ⟨x'', shr s⟩ ≀› show ?thesis by(auto)
next
case (wait x'' ln'')
from ‹wset s t' = None› ‹waiting (wset s t')›
thus ?thesis ..
next
case (acquire x'' ln'' l'' T)
from ‹thr s t' = ⌊(x'', ln'')⌋› ‹thr s t' = ⌊(x', no_wait_locks)⌋› ‹0 < ln'' \$ l''›
have False by(auto)
thus ?thesis ..
qed
next
fix t' x' ln' l
assume "thr s t' = ⌊(x', ln')⌋"
and "0 < ln' \$ l"
and wst': "¬ waiting (wset s t')"
thus "∃l T. 0 < ln' \$ l ∧ t' ≠ T ∧ thr s T ≠ None ∧ has_lock (locks s \$ l) T"
case (lock x'')
from ‹thr s t' = ⌊(x', ln')⌋› ‹thr s t' = ⌊(x'', no_wait_locks)⌋› ‹0 < ln' \$ l›
have False by auto
thus ?thesis ..
next
case (wait x' ln')
from wst' ‹waiting (wset s t')›
thus ?thesis ..
next
case (acquire x'' ln'' l'' t'')
from ‹thr s t' = ⌊(x'', ln'')⌋› ‹thr s t' = ⌊(x', ln')⌋›
have [simp]: "x' = x''" "ln' = ln''" by auto
have "thr s t'' ≠ None"
with ‹0 < ln'' \$ l''› ‹has_lock (locks s \$ l'') t''› ‹t' ≠ t''› ‹thr s t' = ⌊(x'', ln'')⌋›
show ?thesis by auto
qed
next
fix t x w
assume tst: "thr s t = ⌊(x, no_wait_locks)⌋"
show "wset s t ≠ ⌊PostWS w⌋"
proof
assume "wset s t = ⌊PostWS w⌋"
moreover with tst have "not_final_thread s t"
ultimately show False using tst
qed
qed
qed

"⟦ s -t▹ta→ s'; deadlock s ⟧ ⟹ False"

proof(rule equals0I)
fix t
assume active: "t ∈ active_threads s"
then obtain ta s' where "s -t▹ta→ s'" by(auto dest: active_thread_ex_red)
qed

end

for final :: "'x ⇒ bool"
and r :: "('l,'t,'x,'m,'w,'o) semantics" ("_ ⊢ _ -_→ _" [50,0,0,50] 80)
and convert_RA :: "'l released_locks ⇒ 'o list"
+
fixes wf_state :: "('l,'t,'x,'m,'w) state set"
assumes invariant3p_wf_state: "invariant3p redT wf_state"
assumes can_lock_preserved:
"⟦ s ∈ wf_state; s -t'▹ta'→ s';
thr s t = ⌊(x, no_wait_locks)⌋; t ⊢ ⟨x, shr s⟩ ≀ ⟧
⟹ t ⊢ ⟨x, shr s'⟩ ≀"
and can_lock_devreserp:
"⟦ s ∈ wf_state; s -t'▹ta'→ s';
thr s t = ⌊(x, no_wait_locks)⌋; t ⊢ ⟨x, shr s'⟩ L ≀ ⟧
⟹ ∃L'⊆L. t ⊢ ⟨x, shr s⟩ L' ≀"
begin

assumes wfs: "s ∈ wf_state"
and Red: "s -t▹ta→ s'"
proof
fix t'
with t'dead have t't: "t' ≠ t" by auto
{ fix t'
then obtain x' ln' where tst': "thr s t' = ⌊(x', ln')⌋" by(auto elim!: final_threadE)
with ‹final_thread s t'› have "final x'"
and "wset s t' = None" and [simp]: "ln' = no_wait_locks"
with Red tst' have "t ≠ t'" by cases(auto dest: final_no_red)
with Red tst' have "thr s' t' = ⌊(x', ln')⌋"
by cases(auto intro: redT_updTs_Some)
moreover from Red  ‹t ≠ t'› ‹wset s t' = None›
have "wset s' t' = None" by cases(auto simp: redT_updWs_None_implies_None)
ultimately have "final_thread s' t'" using tst' ‹final x'›

from Red show "t' ∈ deadlocked s'"
proof(cases)
case (redT_normal x x' m')
note red = ‹t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩›
and tst = ‹thr s t = ⌊(x, no_wait_locks)⌋›
and aok = ‹actions_ok s t ta›
and s' = ‹redT_upd s t ta x' m' s'›
from red have "¬ final x" by(auto dest: final_no_red)
proof(coinduct)
with Red have t''t: "t'' ≠ t"
case (lock X)
hence est'': "thr s t'' = ⌊(X, no_wait_locks)⌋"
and msE: "t'' ⊢ ⟨X, shr s⟩ ≀"
and csexdead: "⋀LT. t'' ⊢ ⟨X, shr s⟩ LT ≀ ⟹ ∃lt ∈ LT. must_wait s t'' lt (deadlocked s ∪ final_threads s)"
by auto
from t''t Red est''
have es't'': "thr s' t'' = ⌊(X, no_wait_locks)⌋"
by(cases s)(cases s', auto elim!: redT_ts_Some_inv)
note es't'' moreover
from wfs Red est'' msE have msE': "t'' ⊢ ⟨X, shr s'⟩ ≀" by(rule can_lock_preserved)
moreover
{ fix LT
assume clL'': "t'' ⊢ ⟨X, shr s'⟩ LT ≀"
with est'' have "∃LT'⊆LT. t'' ⊢ ⟨X, shr s⟩ LT' ≀"
by(rule can_lock_devreserp[OF wfs Red])
then obtain LT' where clL': "t'' ⊢ ⟨X, shr s⟩ LT' ≀"
and LL': "LT' ⊆ LT" by blast
where lt: "lt ∈ LT" and mw: "must_wait s t'' lt (deadlocked s ∪ final_threads s)"
by blast
proof(cases rule: must_wait_elims)
case (lock l t')
from ‹t' ∈ deadlocked s ∪ final_threads s› Red have tt': "t ≠ t'"
from aok have "lock_actions_ok (locks s \$ l) t (⦃ta⦄⇘l⇙ \$ l)"
with tt' ‹has_lock (locks s \$ l) t'› s'
have hl't': "has_lock (locks s' \$ l) t'" by(auto)
moreover note ‹t' ≠ t''›
using subset by blast
ultimately show ?thesis unfolding ‹lt = Inl l› ..
next
case (join t')
with Red have tt': "t ≠ t'"
note nftt' = ‹not_final_thread s t'›
from t'dead Red aok s' tt' have ts't': "thr s' t' = thr s t'"
from nftt' have "thr s t' ≠ None" by auto
case (lock x'')
from ‹t' ⊢ ⟨x'', shr s⟩ ≀› have "¬ final x''"
by(auto elim: must_syncE dest: final_no_red)
with ‹thr s t' = ⌊(x'', no_wait_locks)⌋› ts't' show ?thesis
next
case (wait x'' ln'')
from ‹¬ final x› tst ‹all_final_except s (deadlocked s)›
with Red have False by(auto dest: red_no_deadlock)
thus ?thesis ..
next
case (acquire x'' ln'' l'' T'')
from ‹thr s t' = ⌊(x'', ln'')⌋› ‹0 < ln'' \$ l''› ts't'
qed
ultimately show ?thesis unfolding ‹lt = Inr (Inl t')› ..
next
case (interrupt t')
from tst red aok have "not_final_thread s t"
ultimately have False by blast
thus ?thesis ..
qed
with lt have "∃lt∈LT. must_wait s' t'' lt (deadlocked s ∪ deadlocked s' ∪ final_threads s')" by blast }
moreover have "wset s' t'' = None" using s' t''t ‹wset s t'' = None›
by(auto intro: redT_updWs_None_implies_None)
ultimately show ?thesis by(auto)
next
case (wait x ln)
from ‹all_final_except s (deadlocked s)› nafe have False by simp
thus ?thesis by simp
next
case (acquire X ln l T)
from t''t Red ‹thr s t'' = ⌊(X, ln)⌋› s'
have es't'': "thr s' t'' = ⌊(X, ln)⌋"
by(cases s)(auto dest: redT_ts_Some_inv)
moreover
have "T ≠ t"
proof(rule disjE)
with Red show ?thesis by(auto dest: red_no_deadlock)
next
with Red show ?thesis
qed
with s' tst Red ‹has_lock (locks s \$ l) T› have "has_lock (locks s' \$ l) T"
by -(cases s, auto dest: redT_has_lock_inv[THEN iffD2])
moreover
from s' ‹T ≠ t› have wset: "wset s T = None ⟹ wset s' T = None"
by(auto intro: redT_updWs_None_implies_None)
{ fix x
assume "thr s T = ⌊(x, no_wait_locks)⌋"
with ‹T ≠ t› Red s' aok tst have "thr s' T = ⌊(x, no_wait_locks)⌋"
by(auto intro: redT_updTs_Some) }
moreover
moreover from ‹¬ waiting (wset s t'')› s' t''t
have "¬ waiting (wset s' t'')"
by(auto simp add: redT_updWs_None_implies_None redT_updWs_PostWS_imp_PostWS not_waiting_iff)
ultimately have ?Acquire
using ‹0 < ln \$ l› ‹t'' ≠ T› ‹T ∈ deadlocked s ∨ final_thread s T› by(auto)
thus ?thesis by simp
qed
qed
next
case (redT_acquire x n ln)
hence [simp]: "ta = (K\$ [], [], [], [], [], convert_RA ln)"
and s': "s' = (acquire_all (locks s) t ln, ((thr s)(t ↦ (x, no_wait_locks)), shr s), wset s, interrupts s)"
and tst: "thr s t = ⌊(x, ln)⌋"
and wst: "¬ waiting (wset s t)" by auto
proof(coinduct)
with Red have t''t: "t'' ≠ t"
case (lock X)
note clnml = ‹⋀LT. t'' ⊢ ⟨X, shr s⟩ LT ≀ ⟹ ∃lt ∈ LT. must_wait s t'' lt (deadlocked s ∪ final_threads s)›
note tst'' = ‹thr s t'' = ⌊(X, no_wait_locks)⌋›
with s' t''t have ts't'': "thr s' t'' = ⌊(X, no_wait_locks)⌋" by simp
moreover
{ fix LT
assume "t'' ⊢ ⟨X, shr s'⟩ LT ≀"
hence "t'' ⊢ ⟨X, shr s⟩ LT ≀" using s' by simp
then obtain lt where lt: "lt ∈ LT" and hlnft: "must_wait s t'' lt (deadlocked s ∪ final_threads s)"
by(blast dest: clnml)
proof(cases rule: must_wait_elims)
case (lock l' T)
from ‹has_lock (locks s \$ l') T› s'
have "has_lock (locks s' \$ l') T"
by(auto intro: has_lock_has_lock_acquire_locks)
moreover note ‹T ≠ t''›
ultimately show ?thesis unfolding ‹lt = Inl l'› ..
next
case (join T)
from ‹not_final_thread s T› have "thr s T ≠ None"
moreover
have "T ≠ t"
proof
with Red show ?thesis by(auto dest: red_no_deadlock)
next
with ‹0 < ln \$ n› tst show ?thesis
qed
ultimately show ?thesis unfolding ‹lt = Inr (Inl T)› ..
next
case (interrupt T)
from tst wst ‹0 < ln \$ n› have "not_final_thread s t"
moreover have "¬ final_thread s t" using tst ‹0 < ln \$ n› by(auto simp add: final_thread_def)
ultimately have False by blast
thus ?thesis ..
qed
with lt have "∃lt∈LT. must_wait s' t'' lt (deadlocked s ∪ deadlocked s' ∪ final_threads s')" by blast }
moreover from ‹wset s t'' = None› s' have "wset s' t'' = None" by simp
ultimately show ?thesis using ‹thr s t'' = ⌊(X, no_wait_locks)⌋› ‹t'' ⊢ ⟨X, shr s⟩ ≀› s' by fastforce
next
case (wait X LN)
proof(rule all_final_exceptI)
fix T
hence "not_final_thread s T" using wst tst s'
with ‹all_final_except s (deadlocked s)› ‹thr s t = ⌊(x, ln)⌋›
show "T ∈ deadlocked s" by-(erule all_final_exceptD)
qed
by(rule all_final_except_mono') blast
with t''t ‹thr s t'' = ⌊(X, LN)⌋› ‹waiting (wset s t'')› s'
have ?Wait by simp
thus ?thesis by simp
next
case (acquire X LN l T)
from ‹thr s t'' = ⌊(X, LN)⌋› t''t s'
have "thr s' t'' = ⌊(X, LN)⌋" by(simp)
moreover from ‹T ∈ deadlocked s ∨ final_thread s T› s' tst
moreover from ‹has_lock (locks s \$ l) T› s'
have "has_lock (locks s' \$ l) T"
by(auto intro: has_lock_has_lock_acquire_locks)
moreover have "¬ waiting (wset s' t'')" using ‹¬ waiting (wset s t'')› s' by simp
ultimately show ?thesis using ‹0 < LN \$ l› ‹t'' ≠ T› by blast
qed
qed
qed
qed