header {* \isaheader{Deadlock formalisation} *}
theory FWDeadlock imports FWProgressAux begin
context final_thread begin
inductive must_wait :: "('l,'t,'x,'m,'w) state => 't => ('l + 't) => 't => bool"
for s :: "('l,'t,'x,'m,'w) state" and t :: "'t" where
"[| has_lock ((locks s)f l) t'; t' ≠ t |] ==> must_wait s t (Inl l) t'"
| "not_final_thread s t' ==> must_wait s t (Inr t') t'"
declare must_wait.cases [elim]
declare must_wait.intros [intro]
lemma must_wait_elims [consumes 1, case_names lock thread]:
"[| must_wait s t lt t'; !!l. [|lt = Inl l;
has_lock ((locks s)f l) t'; t' ≠ t|] ==> thesis;
[|lt = Inr t'; not_final_thread s t'|] ==> thesis |]
==> thesis"
by(auto)
inductive_cases must_wait_elims2 [elim!]:
"must_wait s t (Inl l) t'"
"must_wait s t (Inr t'') t'"
lemma must_wait_iff:
"must_wait s t lt t' <-> (case lt of Inl l => t ≠ t' ∧ has_lock ((locks s)f l) t'
| Inr t'' => t' = t'' ∧ not_final_thread s t'')"
by(cases lt)(auto)
text{* Deadlock as a system-wide property *}
end
context multithreaded_base begin
definition
deadlock :: "('l,'t,'x,'m,'w) state => bool"
where
"deadlock s
≡ (∃t. not_final_thread s t)
∧ (∀t x. thr s t = ⌊(x, no_wait_locks)⌋ ∧ ¬ final x ∧ wset s t = None
--> ⟨x, shr s⟩ \<wrong> ∧ (∀LT. ⟨x, shr s⟩ LT \<wrong> --> (∃t'. thr s t' ≠ None ∧ (∃lt ∈ LT. must_wait s t lt t'))))
∧ (∀t x ln. thr s t = ⌊(x, ln)⌋ ∧ (∃l. lnf l > 0) ∧ wset s t = None
--> (∃l t'. lnf l > 0 ∧ t ≠ t' ∧ thr s t' ≠ None ∧ has_lock ((locks s)f l) t'))"
end
context final_thread_wf begin
lemma deadlockI:
"[| not_final_thread s t;
!!t x. [| thr s t = ⌊(x, no_wait_locks)⌋; ¬ final x; wset s t = None |]
==> ⟨x, shr s⟩ \<wrong> ∧ (∀LT. ⟨x, shr s⟩ LT \<wrong> --> (∃t'. thr s t' ≠ None ∧ (∃lt ∈ LT. must_wait s t lt t')));
!!t x ln l. [| thr s t = ⌊(x, ln)⌋; lnf l > 0; wset s t = None |]
==> ∃l t'. lnf l > 0 ∧ t ≠ t' ∧ thr s t' ≠ None ∧ has_lock ((locks s)f l) t' |]
==> deadlock s"
by(auto simp add: deadlock_def)
lemma deadlockE:
assumes "deadlock s"
obtains t ln x w
where "thr s t = ⌊(x, ln)⌋"
and "not_final_thread s t"
and "∀t x. thr s t = ⌊(x, no_wait_locks)⌋ ∧ ¬ final x ∧ wset s t = None
--> ⟨x, shr s⟩ \<wrong> ∧ (∀LT. ⟨x, shr s⟩ LT \<wrong> --> (∃t'. thr s t' ≠ None ∧ (∃lt ∈ LT. must_wait s t lt t')))"
and "∀t x ln. thr s t = ⌊(x, ln)⌋ ∧ (∃l. lnf l > 0) ∧ wset s t = None --> (∃l t'. lnf l > 0 ∧ t ≠ t' ∧ thr s t' ≠ None ∧ has_lock ((locks s)f l) t')"
using assms unfolding deadlock_def
by(blast)
lemma deadlockD1:
assumes "deadlock s"
and "thr s t = ⌊(x, no_wait_locks)⌋"
and "¬ final x"
and "wset s t = None"
obtains "⟨x, shr s⟩ \<wrong>"
and "∀LT. ⟨x, shr s⟩ LT \<wrong> --> (∃t'. thr s t' ≠ None ∧ (∃lt ∈ LT. must_wait s t lt t'))"
using assms
unfolding deadlock_def by(blast)
lemma deadlockD2:
assumes "deadlock s"
and "thr s t = ⌊(x, ln)⌋"
and "lnf l > 0"
and "wset s t = None"
obtains l' t' where "lnf l' > 0" "t ≠ t'" "thr s t' ≠ None" "has_lock ((locks s)f l') t'"
using assms unfolding deadlock_def by blast
lemma all_waiting_implies_deadlock:
assumes "not_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 |]
==> ⟨x, shr s⟩ \<wrong> ∧ (∀LT. ⟨x, shr s⟩ LT \<wrong> --> (∃t'. thr s t' ≠ None ∧ (∃lt ∈ LT. must_wait s t lt t')))"
and acquire: "!!t x ln l. [| thr s t = ⌊(x, ln)⌋; wset s t = None; lnf l > 0 |] ==> ∃l'. lnf l' > 0 ∧ ¬ may_lock ((locks s)f l') t"
shows "deadlock s"
proof(rule deadlockI)
from `not_final_thread s t` show "not_final_thread s t" .
next
fix T X
assume tsT: "thr s T = ⌊(X, no_wait_locks)⌋"
and "¬ final X"
and "wset s T = None"
show "⟨X, shr s⟩ \<wrong> ∧ (∀LT. ⟨X, shr s⟩ LT \<wrong> --> (∃t'. thr s t' ≠ None ∧ (∃lt∈LT. must_wait s T lt t')))"
by(rule normal[OF tsT `¬ final X` `wset s T = None`])
next
fix T X LN l'
assume "thr s T = ⌊(X, LN)⌋"
and "0 < LNf l'"
and "wset s T = None"
from acquire[OF `thr s T = ⌊(X, LN)⌋` `wset s T = None`, OF `0 < LNf l'`]
obtain l' where "0 < LNf l'" "¬ may_lock ((locks s)f l') T" by blast
then obtain t' where "T ≠ t'" "has_lock ((locks s)f l') t'"
unfolding not_may_lock_conv by fastsimp
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 < LNf l ∧ T ≠ t' ∧ thr s t' ≠ None ∧ has_lock ((locks s)f l) t'"
using `0 < LNf l'` by(auto)
qed
end
text {* Now deadlock for single threads *}
context final_thread begin
definition all_final_except :: "('l,'t,'x,'m,'w) state => ('t => bool) => bool" where
"all_final_except s P ≡ ∀t. not_final_thread s t --> P t"
lemma all_final_except_mono [mono]:
"(!!x. A x --> B x) ==> all_final_except ts A --> all_final_except ts B"
by(auto simp add: all_final_except_def)
lemma all_final_except_mono':
"[| all_final_except ts A; !!x. A x ==> B x |] ==> all_final_except ts B"
by(blast intro: all_final_except_mono[rule_format])
lemma all_final_exceptI:
"(!!t. not_final_thread s t ==> P t) ==> all_final_except s P"
by(auto simp add: all_final_except_def)
lemma all_final_exceptD:
"[| all_final_except s P; not_final_thread s t |] ==> P t"
by(auto simp add: all_final_except_def)
end
context multithreaded_base begin
coinductive deadlocked :: "('l,'t,'x,'m,'w) state => 't => bool"
for s :: "('l,'t,'x,'m,'w) state" where
deadlockedLock:
"[| thr s t = ⌊(x, no_wait_locks)⌋; ⟨x, shr s⟩ \<wrong>; wset s t = None;
!!LT. ⟨x, shr s⟩ LT \<wrong> ==> ∃t'. (deadlocked s t' ∨ final_thread s t') ∧ (∃lt ∈ LT. must_wait s t lt t') |]
==> deadlocked s t"
| deadlockedWait:
"[| thr s t = ⌊(x, ln)⌋; all_final_except s (deadlocked s); wset s t = ⌊w⌋ |] ==> deadlocked s t"
| deadlockedAcquire:
"[| thr s t = ⌊(x, ln)⌋; lnf l > 0; has_lock ((locks s)f l) t'; t' ≠ t;
deadlocked s t' ∨ final_thread s t' |]
==> deadlocked s t"
lemma deadlocked_elims [consumes 1, case_names lock wait acquire]:
assumes "deadlocked s t"
and lock: "!!x. [| thr s t = ⌊(x, no_wait_locks)⌋; ⟨x, shr s⟩ \<wrong>; wset s t = None;
!!LT. ⟨x, shr s⟩ LT \<wrong> ==> ∃t'. (deadlocked s t' ∨ final_thread s t') ∧ (∃lt ∈ LT. must_wait s t lt t') |]
==> thesis"
and wait: "!!x ln w. [| thr s t = ⌊(x, ln)⌋; all_final_except s (deadlocked s); wset s t = ⌊w⌋|] ==> thesis"
and acquire: "!!x ln l t'. [| thr s t = ⌊(x, ln)⌋; 0 < lnf l; has_lock ((locks s)f l) t'; t ≠ t';
deadlocked s t' ∨ final_thread s t' |] ==> thesis"
shows thesis
using `deadlocked s t`
apply(rule deadlocked.cases)
apply(rule lock, blast+)
apply(rule wait, blast+)
apply(rule acquire, blast+)
done
definition deadlocked' :: "('l,'t,'x,'m,'w) state => bool" where
"deadlocked' s ≡ (∃t. not_final_thread s t) ∧ (∀t. not_final_thread s t --> deadlocked s t)"
lemma deadlocked'I:
"[| not_final_thread s t; !!t. not_final_thread s t ==> deadlocked s t |] ==> deadlocked' s"
by(auto simp add: deadlocked'_def)
lemma deadlocked'D1E:
"[| deadlocked' s; !!t. not_final_thread s t ==> thesis |] ==> thesis"
by(auto simp add: deadlocked'_def)
lemma deadlocked'D2:
"[| deadlocked' s; not_final_thread s t; deadlocked s t ==> thesis |] ==> thesis"
by(auto simp add: deadlocked'_def)
lemma not_deadlocked'I:
"[| not_final_thread s t; ¬ deadlocked s t |] ==> ¬ deadlocked' s"
by(auto dest: deadlocked'D2)
lemma deadlocked'_intro:
"[| not_final_thread s t; ∀t. not_final_thread s t --> deadlocked s t |] ==> deadlocked' s"
by(rule deadlocked'I)(blast)+
lemma deadlocked_thread_exists:
assumes "deadlocked s t"
obtains x ln where "thr s t = ⌊(x, ln)⌋"
using assms
by(blast elim: deadlocked.cases)
end
context final_thread_wf begin
lemma red_no_deadlock:
assumes P: "s -t\<triangleright>ta-> s'"
and dead: "deadlocked s t"
shows False
proof -
obtain las tas cas was obs where ta: "ta = (las, tas, cas, was, obs)" by(cases ta)
obtain ls ts m ws where s: "s = (ls, (ts, m), ws)" by (cases s, auto)
obtain ls' ts' m' ws' where s': "s' = (ls', (ts', m'), ws')" by (cases s', auto)
with P s have "⟨ls, (ts, m), ws⟩ -t\<triangleright>ta-> ⟨ls', (ts', m'), ws'⟩" by simp
thus False
proof(induct rule: redT_elims4)
case (normal x x' ta')
with ta have Pe: "⟨x, m⟩ -ta'-> ⟨x', m'⟩"
and est: "ts t = ⌊(x, no_wait_locks)⌋"
and lot: "lock_ok_las ls t las"
and cct: "thread_oks ts tas"
and cdt: "cond_action_oks (ls, (ts, m), ws) t cas"
and wst: "ws t = None"
and [simp]: "ta = observable_ta_of ta'"
by(auto)
show False
proof(cases "all_final_except s (deadlocked s) ∧ (∃w. ws t = ⌊w⌋)")
case True with wst show ?thesis by simp
next
case False
with dead est s
have mle: "⟨x, m⟩ \<wrong>"
and cledead: "∀LT. ⟨x, m⟩ LT \<wrong> --> (∃t'. (deadlocked s t' ∨ final_thread s t') ∧ (∃lt ∈ LT. must_wait s t lt t'))"
by - (erule deadlocked.cases, fastsimp+)+
let ?LT = "collect_locks las <+> {t. Join t ∈ set cas}"
from Pe ta have "⟨x, m⟩ ?LT \<wrong>" by(auto intro: can_syncI simp add: observable_ta_of_def)
then obtain t' lt where "deadlocked s t' ∨ final_thread s t'"
and lt: "lt ∈ ?LT" and mw: "must_wait s t lt t'"
by(blast dest: cledead[rule_format])
from mw show False
proof(induct rule: must_wait_elims)
case (lock l)
from `lt = Inl l` lt have "l ∈ collect_locks las" by(auto)
with lot have "may_lock (lsf l) t"
by(auto elim!: collect_locksE lock_ok_las_may_lock)
with `has_lock ((locks s)f l) t'` s have "t' = t"
by(auto dest: has_lock_may_lock_t_eq)
with `t' ≠ t` show False by contradiction
next
case thread
from `lt = Inr t'` lt have "Join t' ∈ set cas" 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 cas` cdt s
have "final x''" "ln'' = no_wait_locks" "ws t' = None"
by(auto dest: cond_action_oks_Join)
ultimately show False using `not_final_thread s t'` s by(auto)
qed
qed
next
case (acquire x ln n)
show False
proof(cases "all_final_except s (deadlocked s) ∧ (∃w. ws t = ⌊w⌋)")
case True with `ws t = None` show ?thesis by simp
next
case False
with dead `ts t = ⌊(x, ln)⌋` `0 < lnf n` s
obtain l t' where "0 < lnf l" "t ≠ t'"
and "has_lock (lsf l) t'"
by -(erule deadlocked.cases, fastsimp+)
hence "¬ may_acquire_all ls t ln"
by(auto elim: may_acquire_allE dest: has_lock_may_lock_t_eq)
with `may_acquire_all ls t ln` show ?thesis by contradiction
qed
qed
qed
lemma deadlocked'_no_red:
"[| s -t\<triangleright>ta-> s'; deadlocked' s |] ==> False"
apply(rule red_no_deadlock)
apply(assumption)
apply(erule deadlocked'D2)
by(rule red_not_final_thread)
lemma not_final_thread_deadlocked_final_thread [simp, iff]:
"thr s t = ⌊xln⌋ ==> not_final_thread s t ∨ deadlocked s t ∨ final_thread s t"
by(auto simp add: not_final_thread_final_thread_conv[symmetric])
lemma all_waiting_deadlocked:
assumes "not_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 |]
==> ⟨x, shr s⟩ \<wrong> ∧ (∀LT. ⟨x, shr s⟩ LT \<wrong> --> (∃t'. thr s t' ≠ None ∧ (∃lt∈LT. must_wait s t lt t')))"
and acquire: "!!t x ln l. [| thr s t = ⌊(x, ln)⌋; wset s t = None; lnf l > 0 |] ==> ∃l'. lnf l' > 0 ∧ ¬ may_lock ((locks s)f l') t"
shows "deadlocked s t"
proof -
obtain ls ts m ws where s [simp]: "s = (ls, (ts, m), ws)"
by (cases s, auto)
from `not_final_thread s t` show ?thesis
proof(coinduct)
case (deadlocked z)
then obtain x' ln' where "thr s z = ⌊(x', ln')⌋" by(fastsimp elim!: not_final_thread_existsE)
hence "ts z = ⌊(x', ln')⌋" by simp
{ assume "ws z = None" "¬ final x'"
and [simp]: "ln' = no_wait_locks"
with `ts z = ⌊(x', ln')⌋`
have "⟨x', m⟩ \<wrong> ∧ (∀LT. ⟨x', m⟩ LT \<wrong> --> (∃t'. thr s t' ≠ None ∧ (∃lt ∈ LT. must_wait s z lt t')))"
by(auto dest: normal[simplified])
then obtain "⟨x', m⟩ \<wrong>"
and clnml: "!!LT. ⟨x', m⟩ LT \<wrong> ==> ∃t'. thr s t' ≠ None ∧ (∃lt ∈ LT. must_wait s z lt t')" by(blast)
{ fix LT
assume "⟨x', m⟩ LT \<wrong>"
then obtain t' where "thr s t' ≠ None" "∃lt ∈ LT. must_wait s z lt t'"
by(blast dest: clnml)
from `thr s t' ≠ None` obtain xln where "thr s t' = ⌊xln⌋" by auto
hence "not_final_thread s t' ∨ deadlocked s t' ∨ final_thread s t'"
by(rule not_final_thread_deadlocked_final_thread)
with `∃lt ∈ LT. must_wait s z lt t'`
have "∃t'. (not_final_thread s t' ∨ deadlocked s t' ∨ final_thread s t') ∧ (∃lt ∈ LT. must_wait s z lt t')"
by blast }
with `⟨x', m⟩ \<wrong>` `ts z = ⌊(x', ln')⌋` `ws z = None` have ?case by(simp) }
note c1 = this
{ assume "ws z = None"
and "ln' ≠ no_wait_locks"
from `ln' ≠ no_wait_locks` obtain l where "0 < ln'f l"
by(auto simp add: neq_no_wait_locks_conv)
with `ws z = None` `ts z = ⌊(x', ln')⌋`
obtain l' where "0 < ln'f l'" "¬ may_lock (lsf l') z"
by(blast dest: acquire[simplified])
then obtain t'' where "t'' ≠ z" "has_lock (lsf l') t''"
unfolding not_may_lock_conv by blast
with `lock_thread_ok (locks s) (thr s)`
obtain x'' ln'' where "ts t'' = ⌊(x'', ln'')⌋"
by(auto elim!: lock_thread_ok_has_lockE)
hence "(not_final_thread s t'' ∨ deadlocked s t'') ∨ final_thread s t''"
by(clarsimp simp add: not_final_thread_iff final_thread_def)
with `ws z = None` `0 < ln'f l'` `ts z = ⌊(x', ln')⌋` `t'' ≠ z` `has_lock (lsf l') t''`
have ?case by(simp)(blast) }
note c2 = this
{ fix w
assume "ws z = ⌊w⌋"
with `ts z = ⌊(x', ln')⌋` s have ?case
by -(rule disjI2, clarsimp simp add: all_final_except_def not_final_thread_iff) }
note c3 = this
from `not_final_thread s z` `thr s z = ⌊(x', ln')⌋` show ?case
proof(induct rule: not_final_thread_cases2)
case final show ?thesis
proof(cases "ws z")
case None show ?thesis
proof(cases "ln' = no_wait_locks")
case True with None final show ?thesis by(rule c1)
next
case False with None show ?thesis by(rule c2)
qed
next
case (Some w) thus ?thesis by(rule c3)
qed
next
case wait_locks show ?thesis
proof(cases "ws z")
case None thus ?thesis using wait_locks by(rule c2)
next
case (Some w) thus ?thesis by(rule c3)
qed
next
case (wait_set w)
hence "ws z = ⌊w⌋" by simp
thus ?thesis by(rule c3)
qed
qed
qed
text {* Equivalence proof for both notions of deadlock *}
lemma deadlock_implies_deadlocked':
assumes dead: "deadlock s"
shows "deadlocked' s"
proof -
from dead obtain TT where "not_final_thread s TT" by(rule deadlockE)
thus ?thesis
proof(rule deadlocked'I)
fix t
assume "not_final_thread s t"
thus "deadlocked s t"
proof(coinduct)
case (deadlocked t'')
then obtain x'' ln'' where tst'': "thr s t'' = ⌊(x'', ln'')⌋"
by(rule not_final_thread_existsE)
{ fix w''
assume "wset s t'' = ⌊w''⌋"
moreover
with tst'' have nfine: "not_final_thread s t''"
by(blast intro: not_final_thread.intros)
ultimately have ?case using tst''
by(blast intro: all_final_exceptI not_final_thread_final) }
note c1 = this
{ assume wst'': "wset s t'' = None"
and "ln'' ≠ no_wait_locks"
then obtain l where l: "ln''f l > 0"
by(auto simp add: neq_no_wait_locks_conv)
with dead wst'' tst'' obtain l' T
where "ln''f l' > 0" "t'' ≠ T"
and hl: "has_lock ((locks s)f l') T"
and tsT: "thr s T ≠ None"
by - (erule deadlockD2)
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)
moreover hence "not_final_thread s T ∨ final_thread s T"
by(auto simp add: final_thread_def not_final_thread_iff)
ultimately have ?case using wst'' tst'' by blast }
note c2 = this
{ assume "wset s t'' = None"
and [simp]: "ln'' = no_wait_locks"
moreover
with `not_final_thread s t''` tst''
have "¬ final x''" by(auto)
ultimately obtain "⟨x'', shr s⟩ \<wrong>"
and clnml: "!!LT. ⟨x'', shr s⟩ LT \<wrong> ==> ∃t'. thr s t' ≠ None ∧ (∃lt∈LT. must_wait s t'' lt t')"
using `thr s t'' = ⌊(x'', ln'')⌋` `deadlock s`
by(blast elim: deadlockD1)
{ fix LT
assume "⟨x'', shr s⟩ LT \<wrong>"
then obtain t' where "thr s t' ≠ None"
and mw: "∃lt∈LT. must_wait s t'' lt t'" by(blast dest: clnml)
from `thr s t' ≠ None` have "not_final_thread s t' ∨ final_thread s t'"
by(auto simp add: final_thread_def not_final_thread_iff)
with mw have "∃t'.(not_final_thread s t' ∨ deadlocked s t' ∨ final_thread s t') ∧ (∃lt∈LT. must_wait s t'' lt t')"
by fastsimp }
with `⟨x'', shr s⟩ \<wrong>` tst'' `wset s t'' = None` have ?case by(simp) }
note c3 = this
from `not_final_thread s t''` tst'' show ?case
proof(induct rule: not_final_thread_cases2)
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 with None show ?thesis by(rule c2)
qed
next
case (Some w) thus ?thesis by(rule c1)
qed
next
case wait_locks show ?thesis
proof(cases "wset s t''")
case None thus ?thesis using wait_locks by(rule c2)
next
case (Some w) thus ?thesis by(rule c1)
qed
next
case (wait_set w) thus ?thesis by(rule c1)
qed
qed
qed
qed
lemma deadlocked'_implies_deadlock:
assumes dead: "deadlocked' s"
shows "deadlock s"
proof -
from dead obtain TT where "not_final_thread s TT"
by(rule deadlocked'D1E)
have deadlocked: "!!t. not_final_thread s t ==> deadlocked s t"
using dead by(rule deadlocked'D2)
show ?thesis
proof(rule deadlockI)
from `not_final_thread s TT` show "not_final_thread s TT" .
next
fix t' x'
assume "thr s t' = ⌊(x', no_wait_locks)⌋"
and "¬ final x'"
and "wset s t' = None"
hence "not_final_thread s t'" by(auto intro: not_final_thread_final)
hence "deadlocked s t'" by(rule deadlocked)
thus "⟨x', shr s⟩ \<wrong> ∧ (∀LT. ⟨x', shr s⟩ LT \<wrong> --> (∃t''. thr s t'' ≠ None ∧ (∃lt ∈ LT. must_wait s t' lt t'')))"
proof(cases rule: deadlocked_elims)
case (lock x'')
hence lock: "!!LT. ⟨x'', shr s⟩ LT \<wrong> ==> ∃T. (deadlocked s T ∨ final_thread s T) ∧ (∃lt ∈ LT. must_wait s t' lt T)"
by blast
from `thr s t' = ⌊(x'', no_wait_locks)⌋` `thr s t' = ⌊(x', no_wait_locks)⌋`
have [simp]: "x' = x''" by auto
have "!!LT. ⟨x'', shr s⟩ LT \<wrong> ==> ∃t''. thr s t'' ≠ None ∧ (∃lt ∈ LT. must_wait s t' lt t'')"
by -(drule lock, auto elim!: deadlocked_thread_exists final_threadE)
with `⟨x'', shr s⟩ \<wrong>` show ?thesis by(auto)
next
case (wait x'' ln'' w'')
from `wset s t' = None` `wset s t' = ⌊w''⌋`
have False by simp
thus ?thesis ..
next
case (acquire x'' ln'' l'' T)
from `thr s t' = ⌊(x'', ln'')⌋` `thr s t' = ⌊(x', no_wait_locks)⌋` `0 < ln''f l''`
have False by(auto)
thus ?thesis ..
qed
next
fix t' x' ln' l
assume "thr s t' = ⌊(x', ln')⌋"
and "0 < ln'f l"
and "wset s t' = None"
hence "not_final_thread s t'" by(auto intro: not_final_thread_wait_locks)
hence "deadlocked s t'" by(rule deadlocked)
thus "∃l T. 0 < ln'f l ∧ t' ≠ T ∧ thr s T ≠ None ∧ has_lock ((locks s)f l) T"
proof(cases rule: deadlocked_elims)
case (lock x'')
from `thr s t' = ⌊(x', ln')⌋` `thr s t' = ⌊(x'', no_wait_locks)⌋` `0 < ln'f l`
have False by auto
thus ?thesis ..
next
case (wait x' ln' w')
from `wset s t' = None` `wset s t' = ⌊w'⌋`
have False by simp
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
moreover from `deadlocked s t'' ∨ final_thread s t''`
have "thr s t'' ≠ None"
by(auto elim: deadlocked_thread_exists simp add: final_thread_def)
with `0 < ln''f l''` `has_lock ((locks s)f l'') t''` `t' ≠ t''` `thr s t' = ⌊(x'', ln'')⌋`
show ?thesis by auto
qed
qed
qed
lemma deadlock_eq_deadlocked':
"deadlock = deadlocked'"
by(rule ext)(auto intro: deadlock_implies_deadlocked' deadlocked'_implies_deadlock)
lemma deadlock_no_red:
"[| s -t\<triangleright>ta-> s'; deadlock s |] ==> False"
unfolding deadlock_eq_deadlocked'
by(rule deadlocked'_no_red)
end
end