Theory FWProgress
section ‹Progress theorem for the multithreaded semantics›
theory FWProgress
imports
FWDeadlock
begin
locale progress = 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 wf_stateD: "s ∈ wf_state ⟹ lock_thread_ok (locks s) (thr s) ∧ wset_final_ok (wset s) (thr s)"
and wf_red:
"⟦ s ∈ wf_state; thr s t = ⌊(x, no_wait_locks)⌋;
t ⊢ (x, shr s) -ta→ (x', m'); ¬ waiting (wset s t) ⟧
⟹ ∃ta' x' m'. t ⊢ (x, shr s) -ta'→ (x', m') ∧ (actions_ok s t ta' ∨ actions_ok' s t ta' ∧ actions_subset ta' ta)"
and red_wait_set_not_final:
"⟦ s ∈ wf_state; thr s t = ⌊(x, no_wait_locks)⌋;
t ⊢ (x, shr s) -ta→ (x', m'); ¬ waiting (wset s t); Suspend w ∈ set ⦃ta⦄⇘w⇙ ⟧
⟹ ¬ final x'"
and wf_progress:
"⟦ s ∈ wf_state; thr s t = ⌊(x, no_wait_locks)⌋; ¬ final x ⟧
⟹ ∃ta x' m'. t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩"
and ta_Wakeup_no_join_no_lock_no_interrupt:
"⟦ s ∈ wf_state; thr s t = ⌊(x, no_wait_locks)⌋; t ⊢ xm -ta→ xm'; Notified ∈ set ⦃ta⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta⦄⇘w⇙ ⟧
⟹ collect_waits ta = {}"
and ta_satisfiable:
"⟦ s ∈ wf_state; thr s t = ⌊(x, no_wait_locks)⌋; t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩ ⟧
⟹ ∃s'. actions_ok s' t ta"
begin
lemma wf_redE:
assumes "s ∈ wf_state" "thr s t = ⌊(x, no_wait_locks)⌋"
and "t ⊢ ⟨x, shr s⟩ -ta→ ⟨x'', m''⟩" "¬ waiting (wset s t)"
obtains ta' x' m'
where "t ⊢ ⟨x, shr s⟩ -ta'→ ⟨x', m'⟩" "actions_ok' s t ta'" "actions_subset ta' ta"
| ta' x' m' where "t ⊢ ⟨x, shr s⟩ -ta'→ ⟨x', m'⟩" "actions_ok s t ta'"
using wf_red[OF assms] by blast
lemma wf_progressE:
assumes "s ∈ wf_state"
and "thr s t = ⌊(x, no_wait_locks)⌋" "¬ final x"
obtains ta x' m' where "t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩"
using assms
by(blast dest: wf_progress)
lemma wf_progress_satisfiable:
"⟦ s ∈ wf_state; thr s t = ⌊(x, no_wait_locks)⌋; ¬ final x ⟧
⟹ ∃ta x' m' s'. t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩ ∧ actions_ok s' t ta"
apply(frule (2) wf_progress)
apply(blast dest: ta_satisfiable)
done
theorem redT_progress:
assumes wfs: "s ∈ wf_state"
and ndead: "¬ deadlock s"
shows "∃t' ta' s'. s -t'▹ta'→ s'"
proof -
from wfs have lok: "lock_thread_ok (locks s) (thr s)"
and wfin: "wset_final_ok (wset s) (thr s)"
by(auto dest: wf_stateD)
from ndead
have "∃t x ln l. thr s t = ⌊(x, ln)⌋ ∧
(wset s t = None ∧ ln = no_wait_locks ∧ ¬ final x ∧ (∃LT. t ⊢ ⟨x, shr s⟩ LT ≀ ∧ (∀lt ∈ LT. ¬ must_wait s t lt (dom (thr s)))) ∨
¬ waiting (wset s t) ∧ ln $ l > 0 ∧ (∀l. ln $ l > 0 ⟶ may_lock (locks s $ l) t) ∨
(∃w. ln = no_wait_locks ∧ wset s t = ⌊PostWS w⌋))"
by(rule contrapos_np)(blast intro!: all_waiting_implies_deadlock[OF lok] intro: must_syncI[OF wf_progress_satisfiable[OF wfs]])
then obtain t x ln l
where tst: "thr s t = ⌊(x, ln)⌋"
and a: "wset s t = None ∧ ln = no_wait_locks ∧ ¬ final x ∧
(∃LT. t ⊢ ⟨x, shr s⟩ LT ≀ ∧ (∀lt ∈ LT. ¬ must_wait s t lt (dom (thr s)))) ∨
¬ waiting (wset s t) ∧ ln $ l > 0 ∧ (∀l. ln $ l > 0 ⟶ may_lock (locks s $ l) t) ∨
(∃w. ln = no_wait_locks ∧ wset s t = ⌊PostWS w⌋)"
by blast
from a have cases[case_names normal acquire wakeup]:
"⋀thesis.
⟦ ⋀LT. ⟦ wset s t = None; ln = no_wait_locks; ¬ final x; t ⊢ ⟨x, shr s⟩ LT ≀;
⋀lt. lt ∈ LT ⟹ ¬ must_wait s t lt (dom (thr s)) ⟧ ⟹ thesis;
⟦ ¬ waiting (wset s t); ln $ l > 0; ⋀l. ln $ l > 0 ⟹ may_lock (locks s $ l) t ⟧ ⟹ thesis;
⋀w. ⟦ ln = no_wait_locks; wset s t = ⌊PostWS w⌋ ⟧ ⟹ thesis ⟧ ⟹ thesis"
by auto
show ?thesis
proof(cases rule: cases)
case (normal LT)
note [simp] = ‹ln = no_wait_locks›
and nfine' = ‹¬ final x›
and cl' = ‹t ⊢ ⟨x, shr s⟩ LT ≀›
and mw = ‹⋀lt. lt∈LT ⟹ ¬ must_wait s t lt (dom (thr s))›
from tst nfine' obtain x'' m'' ta'
where red: "t ⊢ ⟨x, shr s⟩ -ta'→ ⟨x'', m''⟩"
by(auto intro: wf_progressE[OF wfs])
from cl'
have "∃ta''' x''' m'''. t ⊢ ⟨x, shr s⟩ -ta'''→ ⟨x''', m'''⟩ ∧
LT = collect_waits ta'''"
by (fastforce elim!: can_syncE)
then obtain ta''' x''' m'''
where red'': "t ⊢ ⟨x, shr s⟩ -ta'''→ ⟨x''', m'''⟩"
and L: "LT = collect_waits ta'''"
by blast
from ‹wset s t = None› have "¬ waiting (wset s t)" by(simp add: not_waiting_iff)
with tst obtain ta'' x'' m''
where red': "t ⊢ ⟨x, shr s⟩ -ta''→ ⟨x'', m''⟩"
and aok': "actions_ok s t ta'' ∨ actions_ok' s t ta'' ∧ actions_subset ta'' ta'''"
by -(rule wf_redE[OF wfs _ red''], auto)
from aok' have "actions_ok s t ta''"
proof
assume "actions_ok' s t ta'' ∧ actions_subset ta'' ta'''"
hence aok': "actions_ok' s t ta''" and aos: "actions_subset ta'' ta'''" by simp_all
{ fix l
assume "Inl l ∈ LT"
{ fix t'
assume "t ≠ t'"
have "¬ has_lock (locks s $ l) t'"
proof
assume "has_lock (locks s $ l) t'"
moreover with lok have "thr s t' ≠ None" by(auto dest: lock_thread_okD)
ultimately have "must_wait s t (Inl l) (dom (thr s))" using ‹t ≠ t'› by(auto)
moreover from ‹Inl l ∈ LT› have "¬ must_wait s t (Inl l) (dom (thr s))" by(rule mw)
ultimately show False by contradiction
qed }
hence "may_lock (locks s $ l) t"
by-(rule classical, auto simp add: not_may_lock_conv) }
note mayl = this
{ fix t'
assume t'LT: "Inr (Inl t') ∈ LT"
hence "¬ not_final_thread s t' ∧ t' ≠ t"
proof(cases "t' = t")
case False with t'LT mw L show ?thesis by(fastforce)
next
case True with tst mw[OF t'LT] nfine' L have False
by(auto intro!: must_wait.intros simp add: not_final_thread_iff)
thus ?thesis ..
qed }
note mayj = this
{ fix t'
assume t': "Inr (Inr t') ∈ LT"
from t' have "¬ must_wait s t (Inr (Inr t')) (dom (thr s))" by(rule mw)
hence "t' ∈ interrupts s"
by(rule contrapos_np)(fastforce intro: all_final_exceptI simp add: not_final_thread_iff) }
note interrupt = this
from aos L mayl
have "⋀l. l ∈ collect_locks' ⦃ta''⦄⇘l⇙ ⟹ may_lock (locks s $ l) t" by auto
with aok' have "lock_ok_las (locks s) t ⦃ta''⦄⇘l⇙" by(auto intro: lock_ok_las'_into_lock_on_las)
moreover
from mayj aos L
have "cond_action_oks s t ⦃ta''⦄⇘c⇙"
by(fastforce intro: may_join_cond_action_oks)
moreover
from ta_satisfiable[OF wfs tst[simplified] red']
obtain is' where "interrupt_actions_ok is' ⦃ta''⦄⇘i⇙" by auto
with interrupt aos aok' L have "interrupt_actions_ok (interrupts s) ⦃ta''⦄⇘i⇙"
by(auto 5 2 intro: interrupt_actions_ok'_collect_interrupts_imp_interrupt_actions_ok)
ultimately show "actions_ok s t ta''" using aok' by auto
qed
moreover obtain ws'' where "redT_updWs t (wset s) ⦃ta''⦄⇘w⇙ ws''"
using redT_updWs_total[of t "wset s" "⦃ta''⦄⇘w⇙"] ..
then obtain s' where "redT_upd s t ta'' x'' m'' s'" by fastforce
ultimately have "s -t▹ta''→ s'"
using red' tst ‹wset s t = None› by(auto intro: redT_normal)
thus ?thesis by blast
next
case acquire
hence "may_acquire_all (locks s) t ln" by(auto)
with tst ‹¬ waiting (wset s t)› ‹0 < ln $ l›
show ?thesis by(fastforce intro: redT_acquire)
next
case (wakeup w)
from ‹wset s t = ⌊PostWS w⌋›
have "¬ waiting (wset s t)" by(simp add: not_waiting_iff)
from tst wakeup have tst: "thr s t = ⌊(x, no_wait_locks)⌋" by simp
from wakeup tst wfin have "¬ final x" by(auto dest: wset_final_okD)
from wf_progress[OF wfs tst this]
obtain ta x' m' where red: "t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩" by auto
from wf_red[OF wfs tst red ‹¬ waiting (wset s t)›]
obtain ta' x'' m''
where red': "t ⊢ ⟨x, shr s⟩ -ta'→ ⟨x'', m''⟩"
and aok': "actions_ok s t ta' ∨ actions_ok' s t ta' ∧ actions_subset ta' ta" by blast
from aok' have "actions_ok s t ta'"
proof
assume "actions_ok' s t ta' ∧ actions_subset ta' ta"
hence aok': "actions_ok' s t ta'"
and subset: "actions_subset ta' ta" by simp_all
from wakeup aok' have "Notified ∈ set ⦃ta'⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta'⦄⇘w⇙"
by(auto simp add: wset_actions_ok_def split: if_split_asm)
from ta_Wakeup_no_join_no_lock_no_interrupt[OF wfs tst red' this]
have no_join: "collect_cond_actions ⦃ta'⦄⇘c⇙ = {}"
and no_lock: "collect_locks ⦃ta'⦄⇘l⇙ = {}"
and no_interrupt: "collect_interrupts ⦃ta'⦄⇘i⇙ = {}" by auto
from no_lock have no_lock': "collect_locks' ⦃ta'⦄⇘l⇙ = {}"
using collect_locks'_subset_collect_locks[of "⦃ta'⦄⇘l⇙"] by auto
from aok' have "lock_ok_las' (locks s) t ⦃ta'⦄⇘l⇙" by auto
hence "lock_ok_las (locks s) t ⦃ta'⦄⇘l⇙"
by(rule lock_ok_las'_into_lock_on_las)(simp add: no_lock')
moreover from subset aok' no_join have "cond_action_oks s t ⦃ta'⦄⇘c⇙"
by(auto intro: may_join_cond_action_oks)
moreover from ta_satisfiable[OF wfs tst[simplified] red']
obtain is' where "interrupt_actions_ok is' ⦃ta'⦄⇘i⇙" by auto
with aok' no_interrupt have "interrupt_actions_ok (interrupts s) ⦃ta'⦄⇘i⇙"
by(auto intro: interrupt_actions_ok'_collect_interrupts_imp_interrupt_actions_ok)
ultimately show "actions_ok s t ta'" using aok' by auto
qed
moreover obtain ws'' where "redT_updWs t (wset s) ⦃ta'⦄⇘w⇙ ws''"
using redT_updWs_total[of t "wset s" "⦃ta'⦄⇘w⇙"] ..
then obtain s' where "redT_upd s t ta' x'' m'' s'" by fastforce
ultimately have "s -t▹ta'→ s'" using tst red' wakeup
by(auto intro: redT_normal)
thus ?thesis by blast
qed
qed
end
end