Theory FWDeadlock
section ‹Deadlock formalisation›
theory FWDeadlock
imports
FWProgressAux
begin
context final_thread 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"
by(auto simp add: all_final_except_def)
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"
by(auto simp add: all_final_except_def)
lemma all_final_exceptD:
"⟦ all_final_except s Ts; not_final_thread s t ⟧ ⟹ t ∈ Ts"
by(auto simp add: all_final_except_def)
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
"⟦ has_lock (locks s $ l) t'; t' ≠ t; t' ∈ Ts ⟧ ⟹ must_wait s t (Inl l) Ts"
|
"⟦ not_final_thread s t'; t' ∈ Ts ⟧ ⟹ must_wait s t (Inr (Inl t')) Ts"
|
"⟦ 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
text‹Deadlock as a system-wide property›
context multithreaded_base begin
definition
deadlock :: "('l,'t,'x,'m,'w) state ⇒ bool"
where
"deadlock s
≡ (∀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⌋)"
lemma deadlockI:
"⟦ ⋀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⌋ ⟧
⟹ deadlock s"
by(auto simp add: deadlock_def)
lemma deadlockE:
assumes "deadlock s"
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⌋"
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 "t ⊢ ⟨x, shr s⟩ ≀"
and "∀LT. t ⊢ ⟨x, shr s⟩ LT ≀ ⟶ (∃lt ∈ LT. must_wait s t lt (dom (thr s)))"
using assms unfolding deadlock_def by(blast)
lemma deadlockD2:
fixes ln
assumes "deadlock s"
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
lemma deadlockD3:
assumes "deadlock s"
and "thr s t = ⌊(x, no_wait_locks)⌋"
shows "∀w. wset s t ≠ ⌊PostWS w⌋"
using assms unfolding deadlock_def by blast
lemma deadlock_def2:
"deadlock s ⟷
(∀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(blast dest: deadlockD1)
apply(blast dest: deadlockD1)
apply(blast elim: deadlockD2)
apply(blast dest: deadlockD3)
apply(blast dest: deadlockD3)
apply(elim conjE exE)
apply(rule deadlockI)
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
lemma all_waiting_implies_deadlock:
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⌋"
shows "deadlock s"
proof(rule deadlockI)
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)
lemma mfinal_deadlock:
"mfinal s ⟹ deadlock s"
unfolding mfinal_def2
by(rule deadlockI)(auto simp add: final_thread_def)
text ‹Now deadlock for single threads›
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
context multithreaded_base begin
coinductive_set deadlocked :: "('l,'t,'x,'m,'w) state ⇒ 't set"
for s :: "('l,'t,'x,'m,'w) state" where
deadlockedLock:
"⟦ 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) ⟧
⟹ t ∈ deadlocked s"
| deadlockedWait:
"⋀ln. ⟦ thr s t = ⌊(x, ln)⌋; all_final_except s (deadlocked s); waiting (wset s t) ⟧ ⟹ t ∈ deadlocked s"
| deadlockedAcquire:
"⋀ln. ⟦ thr s t = ⌊(x, ln)⌋; ¬ waiting (wset s t); ln $ l > 0; has_lock (locks s $ l) t'; t' ≠ t;
t' ∈ deadlocked s ∨ final_thread s t' ⟧
⟹ t ∈ deadlocked s"
monos must_wait_mono UN_mono
lemma deadlockedAcquire_must_wait:
"⋀ln. ⟦ thr s t = ⌊(x, ln)⌋; ¬ waiting (wset s t); ln $ l > 0; must_wait s t (Inl l) (deadlocked s ∪ final_threads s) ⟧
⟹ t ∈ deadlocked s"
apply(erule must_wait_elims)
apply(erule (2) deadlockedAcquire)
apply auto
done
lemma deadlocked_elims [consumes 1, case_names lock wait acquire]:
assumes "t ∈ deadlocked s"
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';
t' ∈ deadlocked s ∨ final_thread s t' ⟧ ⟹ thesis"
shows thesis
using assms by cases blast+
lemma deadlocked_coinduct
[consumes 1, case_names deadlocked, case_conclusion deadlocked Lock Wait Acquire, coinduct set: deadlocked]:
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'))"
shows "t ∈ deadlocked s"
using major
proof(coinduct)
case (deadlocked t)
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
"deadlocked' s ≡ (∀t. not_final_thread s t ⟶ t ∈ deadlocked s)"
lemma deadlocked'I:
"(⋀t. not_final_thread s t ⟹ t ∈ deadlocked s) ⟹ deadlocked' s"
by(auto simp add: deadlocked'_def)
lemma deadlocked'D2:
"⟦ deadlocked' s; not_final_thread s t; t ∈ deadlocked s ⟹ thesis ⟧ ⟹ thesis"
by(auto simp add: deadlocked'_def)
lemma not_deadlocked'I:
"⟦ not_final_thread s t; t ∉ deadlocked s ⟧ ⟹ ¬ deadlocked' s"
by(auto dest: deadlocked'D2)
lemma deadlocked'_intro:
"⟦ ∀t. not_final_thread s t ⟶ t ∈ deadlocked s ⟧ ⟹ deadlocked' s"
by(rule deadlocked'I)(blast)+
lemma deadlocked_thread_exists:
assumes "t ∈ deadlocked s"
and "⋀x ln. thr s t = ⌊(x, ln)⌋ ⟹ thesis"
shows thesis
using assms
by cases blast+
end
context multithreaded begin
lemma red_no_deadlock:
assumes P: "s -t▹ta→ s'"
and dead: "t ∈ deadlocked 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
with dead tst
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))"
by(cases, auto simp add: waiting_def)+
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)"
by(blast dest: cledead[rule_format])
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
by(auto simp add: not_waiting_iff)
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'"
by(cases)(fastforce simp add: waiting_def)+
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
lemma deadlocked'_no_red:
"⟦ s -t▹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 [iff]:
"thr s t = ⌊xln⌋ ⟹ not_final_thread s t ∨ t ∈ deadlocked s ∨ 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 ⟧
⟹ 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⌋"
shows "t ∈ deadlocked s"
proof -
from ‹not_final_thread s t›
have "t ∈ {t. not_final_thread s t}" by simp
thus ?thesis
proof(coinduct)
case (deadlocked z)
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"
by(auto simp add: neq_no_wait_locks_conv)
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'')⌋"
by(auto elim!: lock_thread_ok_has_lockE)
hence "(not_final_thread s t'' ∨ t'' ∈ deadlocked s) ∨ final_thread s t''"
by(clarsimp simp add: not_final_thread_iff final_thread_def)
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
proof(cases rule: not_final_thread_cases2)
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›
lemma deadlock_implies_deadlocked':
assumes dead: "deadlock s"
shows "deadlocked' s"
proof -
show ?thesis
proof(rule deadlocked'I)
fix t
assume "not_final_thread s t"
hence "t ∈ {t. not_final_thread s t}" ..
thus "t ∈ deadlocked s"
proof(coinduct)
case (deadlocked t'')
hence "not_final_thread s t''" ..
then obtain x'' ln'' where tst'': "thr s t'' = ⌊(x'', ln'')⌋"
by(rule not_final_thread_existsE)
{ assume "waiting (wset s t'')"
moreover
with tst'' have nfine: "not_final_thread s t''"
unfolding waiting_def
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'': "¬ waiting (wset s t'')"
and "ln'' ≠ no_wait_locks"
then obtain l where l: "ln'' $ l > 0"
by(auto simp add: neq_no_wait_locks_conv)
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"
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 "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›
by(blast elim: deadlockD1)
{ 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
also have "dom (thr s) = {t. not_final_thread s t} ∪ deadlocked s ∪ final_threads s"
by(auto simp add: not_final_thread_conv dest: deadlocked_thread_exists elim: final_threadE)
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
proof(cases 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
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''
have "ln'' ≠ no_wait_locks" by(auto dest: deadlockD3[OF dead])
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
by(simp add: not_waiting_iff)
moreover from PostWS wait_set tst''
have "ln'' ≠ no_wait_locks" by(auto dest: deadlockD3[OF dead])
ultimately show ?thesis by(rule c2)
qed
qed
qed
qed
qed
lemma deadlocked'_implies_deadlock:
assumes dead: "deadlocked' s"
shows "deadlock s"
proof -
have deadlocked: "⋀t. not_final_thread s t ⟹ t ∈ deadlocked s"
using dead by(rule deadlocked'D2)
show ?thesis
proof(rule deadlockI)
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 "t' ∈ deadlocked s" by(rule deadlocked)
thus "t' ⊢ ⟨x', shr s⟩ ≀ ∧ (∀LT. t' ⊢ ⟨x', shr s⟩ LT ≀ ⟶ (∃lt ∈ LT. must_wait s t' lt (dom (thr s))))"
proof(cases rule: deadlocked_elims)
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
have "deadlocked s ∪ final_threads s ⊆ dom (thr s)"
by(auto elim: final_threadE dest: deadlocked_thread_exists)
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')›
have False by(simp add: waiting_def)
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')"
hence "not_final_thread s t'" by(auto intro: not_final_thread_wait_locks)
hence "t' ∈ deadlocked s" by(rule deadlocked)
thus "∃l T. 0 < ln' $ l ∧ t' ≠ T ∧ thr s T ≠ None ∧ has_lock (locks s $ 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' $ l›
have False by auto
thus ?thesis ..
next
case (wait x' ln')
from wst' ‹waiting (wset s t')›
have False by contradiction
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 ‹t'' ∈ deadlocked s ∨ final_thread s t''›
have "thr s t'' ≠ None"
by(auto elim: deadlocked_thread_exists simp add: final_thread_def)
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"
by(auto simp add: not_final_thread_iff)
hence "t ∈ deadlocked s" by(rule deadlocked)
ultimately show False using tst
by(auto elim: deadlocked.cases simp add: waiting_def)
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▹ta→ s'; deadlock s ⟧ ⟹ False"
unfolding deadlock_eq_deadlocked'
by(rule deadlocked'_no_red)
lemma deadlock_no_active_threads:
assumes dead: "deadlock s"
shows "active_threads s = {}"
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)
thus False using dead by(rule deadlock_no_red)
qed
end
locale preserve_deadlocked = multithreaded final r convert_RA
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
lemma redT_deadlocked_subset:
assumes wfs: "s ∈ wf_state"
and Red: "s -t▹ta→ s'"
shows "deadlocked s ⊆ deadlocked s'"
proof
fix t'
assume t'dead: "t' ∈ deadlocked s"
from Red have tndead: "t ∉ deadlocked s"
by(auto dest: red_no_deadlock)
with t'dead have t't: "t' ≠ t" by auto
{ fix t'
assume "final_thread s 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"
by(auto elim: final_threadE)
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'›
by(auto simp add: final_thread_def) }
hence subset: "deadlocked s ∪ final_threads s ⊆ deadlocked s ∪ deadlocked s' ∪ final_threads s'" by(auto)
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)
with tndead tst have nafe: "¬ all_final_except s (deadlocked s)"
by(fastforce simp add: all_final_except_def not_final_thread_iff)
from t'dead show ?thesis
proof(coinduct)
case (deadlocked t'')
note t''dead = this
with Red have t''t: "t'' ≠ t"
by(auto dest: red_no_deadlock)
from t''dead show ?case
proof(cases rule: deadlocked_elims)
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
with csexdead obtain lt
where lt: "lt ∈ LT" and mw: "must_wait s t'' lt (deadlocked s ∪ final_threads s)"
by blast
from mw have "must_wait s' t'' lt (deadlocked s ∪ deadlocked s' ∪ final_threads s')"
proof(cases rule: must_wait_elims)
case (lock l t')
from ‹t' ∈ deadlocked s ∪ final_threads s› Red have tt': "t ≠ t'"
by(auto dest: red_no_deadlock final_no_redT elim: final_threadE)
from aok have "lock_actions_ok (locks s $ l) t (⦃ta⦄⇘l⇙ $ l)"
by(auto simp add: lock_ok_las_def)
with tt' ‹has_lock (locks s $ l) t'› s'
have hl't': "has_lock (locks s' $ l) t'" by(auto)
moreover note ‹t' ≠ t''›
moreover from ‹t' ∈ deadlocked s ∪ final_threads s›
have "t' ∈ (deadlocked s ∪ deadlocked s' ∪ final_threads s')"
using subset by blast
ultimately show ?thesis unfolding ‹lt = Inl l› ..
next
case (join t')
note t'dead = ‹t' ∈ deadlocked s ∪ final_threads s›
with Red have tt': "t ≠ t'"
by(auto dest: red_no_deadlock final_no_redT elim: final_threadE)
note nftt' = ‹not_final_thread s t'›
from t'dead Red aok s' tt' have ts't': "thr s' t' = thr s t'"
by(auto elim!: deadlocked_thread_exists final_threadE intro: redT_updTs_Some)
from nftt' have "thr s t' ≠ None" by auto
with nftt' t'dead have "t' ∈ deadlocked s"
by(simp add: not_final_thread_final_thread_conv[symmetric])
hence "not_final_thread s' t'"
proof(cases rule: deadlocked_elims)
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
by(auto intro: not_final_thread.intros)
next
case (wait x'' ln'')
from ‹¬ final x› tst ‹all_final_except s (deadlocked s)›
have "t ∈ deadlocked s" by(fastforce dest: all_final_exceptD simp add: not_final_thread_iff)
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'
show ?thesis by(auto intro: not_final_thread.intros(2))
qed
moreover from t'dead subset have "t' ∈ deadlocked s ∪ deadlocked s' ∪ final_threads s'" ..
ultimately show ?thesis unfolding ‹lt = Inr (Inl t')› ..
next
case (interrupt t')
from tst red aok have "not_final_thread s t"
by(auto simp add: wset_actions_ok_def not_final_thread_iff split: if_split_asm dest: final_no_red)
with ‹all_final_except s (deadlocked s ∪ final_threads s)›
have "t ∈ deadlocked s ∪ final_threads s" by(rule all_final_exceptD)
moreover have "t ∉ deadlocked s" using Red by(blast dest: red_no_deadlock)
moreover have "¬ final_thread s t" using red tst by(auto simp add: final_thread_def dest: final_no_red)
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
from ‹T ∈ deadlocked s ∨ final_thread s T›
have "T ≠ t"
proof(rule disjE)
assume "T ∈ deadlocked s"
with Red show ?thesis by(auto dest: red_no_deadlock)
next
assume "final_thread s T"
with Red show ?thesis
by(auto dest!: final_no_redT simp add: final_thread_def)
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
hence "final_thread s T ⟹ final_thread s' T"
by(auto simp add: final_thread_def intro: wset)
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
from t'dead show ?thesis
proof(coinduct)
case (deadlocked t'')
note t''dead = this
with Red have t''t: "t'' ≠ t"
by(auto dest: red_no_deadlock)
from t''dead show ?case
proof(cases rule: deadlocked_elims)
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)
from hlnft have "must_wait s' t'' lt (deadlocked s ∪ deadlocked s' ∪ final_threads s')"
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''›
moreover from ‹T ∈ deadlocked s ∪ final_threads s›
have "T ∈ deadlocked s ∪ deadlocked s' ∪ final_threads s'" using subset by blast
ultimately show ?thesis unfolding ‹lt = Inl l'› ..
next
case (join T)
from ‹not_final_thread s T› have "thr s T ≠ None"
by(auto simp add: not_final_thread_iff)
moreover
from ‹T ∈ deadlocked s ∪ final_threads s›
have "T ≠ t"
proof
assume "T ∈ deadlocked s"
with Red show ?thesis by(auto dest: red_no_deadlock)
next
assume "T ∈ final_threads s"
with ‹0 < ln $ n› tst show ?thesis
by(auto simp add: final_thread_def)
qed
ultimately have "not_final_thread s' T" using ‹not_final_thread s T› s'
by(auto simp add: not_final_thread_iff)
moreover from ‹T ∈ deadlocked s ∪ final_threads s›
have "T ∈ deadlocked s ∪ deadlocked s' ∪ final_threads s'" using subset by blast
ultimately show ?thesis unfolding ‹lt = Inr (Inl T)› ..
next
case (interrupt T)
from tst wst ‹0 < ln $ n› have "not_final_thread s t"
by(auto simp add: waiting_def not_final_thread_iff)
with ‹all_final_except s (deadlocked s ∪ final_threads s)›
have "t ∈ deadlocked s ∪ final_threads s" by(rule all_final_exceptD)
moreover have "t ∉ deadlocked s" using Red by(blast dest: red_no_deadlock)
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)
have "all_final_except s' (deadlocked s)"
proof(rule all_final_exceptI)
fix T
assume "not_final_thread s' T"
hence "not_final_thread s T" using wst tst s'
by(auto simp add: not_final_thread_iff split: if_split_asm)
with ‹all_final_except s (deadlocked s)› ‹thr s t = ⌊(x, ln)⌋›
show "T ∈ deadlocked s" by-(erule all_final_exceptD)
qed
hence "all_final_except s' (deadlocked s ∪ deadlocked s')"
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
have "T ∈ deadlocked s ∨ final_thread s' T"
by(clarsimp simp add: final_thread_def)
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
corollary RedT_deadlocked_subset:
assumes wfs: "s ∈ wf_state"
and Red: "s -▹ttas→* s'"
shows "deadlocked s ⊆ deadlocked s'"
using Red
apply(induct rule: RedT_induct')
apply(unfold RedT_def)
apply(blast dest: invariant3p_rtrancl3p[OF invariant3p_wf_state _ wfs] redT_deadlocked_subset)+
done
end
end