Theory FWProgressAux
section ‹Auxiliary definitions for the progress theorem for the multithreaded semantics›
theory FWProgressAux
imports
FWSemantics
begin
abbreviation collect_waits :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ ('l + 't + 't) set"
where "collect_waits ta ≡ collect_locks ⦃ta⦄⇘l⇙ <+> collect_cond_actions ⦃ta⦄⇘c⇙ <+> collect_interrupts ⦃ta⦄⇘i⇙"
lemma collect_waits_unfold:
"collect_waits ta = {l. Lock ∈ set (⦃ta⦄⇘l⇙ $ l)} <+> {t. Join t ∈ set ⦃ta⦄⇘c⇙} <+> collect_interrupts ⦃ta⦄⇘i⇙"
by(simp add: collect_locks_def)
context multithreaded_base begin
definition must_sync :: "'t ⇒ 'x ⇒ 'm ⇒ bool" (‹_ ⊢ ⟨_,/ _⟩/ ≀› [50, 0,0] 81) where
"t ⊢ ⟨x, m⟩ ≀ ⟷ (∃ta x' m' s. t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩ ∧ shr s = m ∧ actions_ok s t ta)"
lemma must_sync_def2:
"t ⊢ ⟨x, m⟩ ≀ ⟷ (∃ta x' m' s. t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩ ∧ actions_ok s t ta)"
by(fastforce simp add: must_sync_def intro: cond_action_oks_shr_change)
lemma must_syncI:
"∃ta x' m' s. t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩ ∧ actions_ok s t ta ⟹ t ⊢ ⟨x, m⟩ ≀"
by(fastforce simp add: must_sync_def2)
lemma must_syncE:
"⟦ t ⊢ ⟨x, m⟩ ≀; ⋀ta x' m' s. ⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; actions_ok s t ta; m = shr s ⟧ ⟹ thesis ⟧ ⟹ thesis"
by(fastforce simp only: must_sync_def)
definition can_sync :: "'t ⇒ 'x ⇒ 'm ⇒ ('l + 't + 't) set ⇒ bool" (‹_ ⊢ ⟨_,/ _⟩/ _/ ≀› [50,0,0,0] 81) where
"t ⊢ ⟨x, m⟩ LT ≀ ≡ ∃ta x' m'. t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩ ∧ (LT = collect_waits ta)"
lemma can_syncI:
"⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩;
LT = collect_waits ta ⟧
⟹ t ⊢ ⟨x, m⟩ LT ≀"
by(cases ta)(fastforce simp add: can_sync_def)
lemma can_syncE:
assumes "t ⊢ ⟨x, m⟩ LT ≀"
obtains ta x' m'
where "t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩"
and "LT = collect_waits ta"
using assms
by(clarsimp simp add: can_sync_def)
inductive_set active_threads :: "('l,'t,'x,'m,'w) state ⇒ 't set"
for s :: "('l,'t,'x,'m,'w) state"
where
normal:
"⋀ln. ⟦ thr s t = Some (x, ln);
ln = no_wait_locks;
t ⊢ (x, shr s) -ta→ x'm';
actions_ok s t ta ⟧
⟹ t ∈ active_threads s"
| acquire:
"⋀ln. ⟦ thr s t = Some (x, ln);
ln ≠ no_wait_locks;
¬ waiting (wset s t);
may_acquire_all (locks s) t ln ⟧
⟹ t ∈ active_threads s"
lemma active_threads_iff:
"active_threads s =
{t. ∃x ln. thr s t = Some (x, ln) ∧
(if ln = no_wait_locks
then ∃ta x' m'. t ⊢ (x, shr s) -ta→ (x', m') ∧ actions_ok s t ta
else ¬ waiting (wset s t) ∧ may_acquire_all (locks s) t ln)}"
apply(auto elim!: active_threads.cases intro: active_threads.intros)
apply blast
done
lemma active_thread_ex_red:
assumes "t ∈ active_threads s"
shows "∃ta s'. s -t▹ta→ s'"
using assms
proof cases
case (normal x ta x'm' ln)
with redT_updWs_total[of t "wset s" "⦃ta⦄⇘w⇙"]
show ?thesis
by(cases x'm')(fastforce intro!: redT_normal simp del: split_paired_Ex)
next
case acquire thus ?thesis
by(fastforce intro: redT_acquire simp del: split_paired_Ex simp add: neq_no_wait_locks_conv)
qed
end
text ‹Well-formedness conditions for final›
context final_thread begin
inductive not_final_thread :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ bool"
for s :: "('l,'t,'x,'m,'w) state" and t :: "'t" where
not_final_thread_final: "⋀ln. ⟦ thr s t = ⌊(x, ln)⌋; ¬ final x ⟧ ⟹ not_final_thread s t"
| not_final_thread_wait_locks: "⋀ln. ⟦ thr s t = ⌊(x, ln)⌋; ln ≠ no_wait_locks ⟧ ⟹ not_final_thread s t"
| not_final_thread_wait_set: "⋀ln. ⟦ thr s t = ⌊(x, ln)⌋; wset s t = ⌊w⌋ ⟧ ⟹ not_final_thread s t"
declare not_final_thread.cases [elim]
lemmas not_final_thread_cases = not_final_thread.cases [consumes 1, case_names final wait_locks wait_set]
lemma not_final_thread_cases2 [consumes 2, case_names final wait_locks wait_set]:
"⋀ln. ⟦ not_final_thread s t; thr s t = ⌊(x, ln)⌋;
¬ final x ⟹ thesis; ln ≠ no_wait_locks ⟹ thesis; ⋀w. wset s t = ⌊w⌋ ⟹ thesis ⟧
⟹ thesis"
by(auto)
lemma not_final_thread_iff:
"not_final_thread s t ⟷ (∃x ln. thr s t = ⌊(x, ln)⌋ ∧ (¬ final x ∨ ln ≠ no_wait_locks ∨ (∃w. wset s t = ⌊w⌋)))"
by(auto intro: not_final_thread.intros)
lemma not_final_thread_conv:
"not_final_thread s t ⟷ thr s t ≠ None ∧ ¬ final_thread s t"
by(auto simp add: final_thread_def intro: not_final_thread.intros)
lemma not_final_thread_existsE:
assumes "not_final_thread s t"
and "⋀x ln. thr s t = ⌊(x, ln)⌋ ⟹ thesis"
shows thesis
using assms by blast
lemma not_final_thread_final_thread_conv:
"thr s t ≠ None ⟹ ¬ final_thread s t ⟷ not_final_thread s t"
by(simp add: not_final_thread_iff final_thread_def)
lemma may_join_cond_action_oks:
assumes "⋀t'. Join t' ∈ set cas ⟹ ¬ not_final_thread s t' ∧ t ≠ t'"
shows "cond_action_oks s t cas"
using assms
proof (induct cas)
case Nil thus ?case by clarsimp
next
case (Cons ca cas)
note IH = ‹⟦ ⋀t'. Join t' ∈ set cas ⟹ ¬ not_final_thread s t' ∧ t ≠ t' ⟧
⟹ cond_action_oks s t cas›
note ass = ‹⋀t'. Join t' ∈ set (ca # cas) ⟹ ¬ not_final_thread s t' ∧ t ≠ t'›
hence "⋀t'. Join t' ∈ set cas ⟹ ¬ not_final_thread s t' ∧ t ≠ t'" by simp
hence "cond_action_oks s t cas" by(rule IH)
moreover have "cond_action_ok s t ca"
proof(cases ca)
case (Join t')
with ass have "¬ not_final_thread s t'" "t ≠ t'" by auto
thus ?thesis using Join by(auto simp add: not_final_thread_iff)
next
case Yield thus ?thesis by simp
qed
ultimately show ?case by simp
qed
end
context multithreaded begin
lemma red_not_final_thread:
"s -t▹ta→ s' ⟹ not_final_thread s t"
by(fastforce elim: redT.cases intro: not_final_thread.intros dest: final_no_red)
lemma redT_preserves_final_thread:
"⟦ s -t'▹ta→ s'; final_thread s t ⟧ ⟹ final_thread s' t"
apply(erule redT.cases)
apply(clarsimp simp add: final_thread_def)
apply(auto simp add: final_thread_def dest: redT_updTs_None redT_updTs_Some final_no_red intro: redT_updWs_None_implies_None)
done
end
context multithreaded_base begin
definition wset_Suspend_ok :: "('l,'t,'x,'m,'w) state set ⇒ ('l,'t,'x,'m,'w) state set"
where
"wset_Suspend_ok I =
{s. s ∈ I ∧
(∀t ∈ dom (wset s). ∃s0∈I. ∃s1∈I. ∃ttas x x0 ta w' ln' ln''. s0 -t▹ta→ s1 ∧ s1 -▹ttas→* s ∧
thr s0 t = ⌊(x0, no_wait_locks)⌋ ∧ t ⊢ ⟨x0, shr s0⟩ -ta→ ⟨x, shr s1⟩ ∧ Suspend w' ∈ set ⦃ta⦄⇘w⇙ ∧
actions_ok s0 t ta ∧ thr s1 t = ⌊(x, ln')⌋ ∧ thr s t = ⌊(x, ln'')⌋)}"
lemma wset_Suspend_okI:
"⟦ s ∈ I;
⋀t w. wset s t = ⌊w⌋ ⟹ ∃s0∈I. ∃s1∈I. ∃ttas x x0 ta w' ln' ln''. s0 -t▹ta→ s1 ∧ s1 -▹ttas→* s ∧
thr s0 t = ⌊(x0, no_wait_locks)⌋ ∧ t ⊢ ⟨x0, shr s0⟩ -ta→ ⟨x, shr s1⟩ ∧ Suspend w' ∈ set ⦃ta⦄⇘w⇙ ∧
actions_ok s0 t ta ∧ thr s1 t = ⌊(x, ln')⌋ ∧ thr s t = ⌊(x, ln'')⌋ ⟧
⟹ s ∈ wset_Suspend_ok I"
unfolding wset_Suspend_ok_def by blast
lemma wset_Suspend_okD1:
"s ∈ wset_Suspend_ok I ⟹ s ∈ I"
unfolding wset_Suspend_ok_def by blast
lemma wset_Suspend_okD2:
"⟦ s ∈ wset_Suspend_ok I; wset s t = ⌊w⌋ ⟧
⟹ ∃s0∈I. ∃s1∈I. ∃ttas x x0 ta w' ln' ln''. s0 -t▹ta→ s1 ∧ s1 -▹ttas→* s ∧
thr s0 t = ⌊(x0, no_wait_locks)⌋ ∧ t ⊢ ⟨x0, shr s0⟩ -ta→ ⟨x, shr s1⟩ ∧ Suspend w' ∈ set ⦃ta⦄⇘w⇙ ∧
actions_ok s0 t ta ∧ thr s1 t = ⌊(x, ln')⌋ ∧ thr s t = ⌊(x, ln'')⌋"
unfolding wset_Suspend_ok_def by blast
lemma wset_Suspend_ok_imp_wset_thread_ok:
"s ∈ wset_Suspend_ok I ⟹ wset_thread_ok (wset s) (thr s)"
apply(rule wset_thread_okI)
apply(rule ccontr)
apply(auto dest: wset_Suspend_okD2)
done
lemma invariant3p_wset_Suspend_ok:
assumes I: "invariant3p redT I"
shows "invariant3p redT (wset_Suspend_ok I)"
proof(rule invariant3pI)
fix s tl s'
assume wso: "s ∈ wset_Suspend_ok I"
and "redT s tl s'"
moreover obtain t' ta where tl: "tl = (t', ta)" by(cases tl)
ultimately have red: "s -t'▹ta→ s'" by simp
moreover from wso have "s ∈ I" by(rule wset_Suspend_okD1)
ultimately have "s' ∈ I" by(rule invariant3pD[OF I])
thus "s' ∈ wset_Suspend_ok I"
proof(rule wset_Suspend_okI)
fix t w
assume ws't: "wset s' t = ⌊w⌋"
show "∃s0∈I. ∃s1∈I. ∃ttas x x0 ta w' ln' ln''. s0 -t▹ta→ s1 ∧ s1 -▹ttas→* s' ∧
thr s0 t = ⌊(x0, no_wait_locks)⌋ ∧ t ⊢ ⟨x0, shr s0⟩ -ta→ ⟨x, shr s1⟩ ∧
Suspend w' ∈ set ⦃ta⦄⇘w⇙ ∧ actions_ok s0 t ta ∧
thr s1 t = ⌊(x, ln')⌋ ∧ thr s' t = ⌊(x, ln'')⌋"
proof(cases "t = t'")
case False
with red ws't obtain w' where wst: "wset s t = ⌊w'⌋"
by cases(auto 4 4 dest: redT_updWs_Some_otherD split: wait_set_status.split_asm)
from wset_Suspend_okD2[OF wso this] obtain s0 s1 ttas x x0 ta' w' ln' ln''
where reuse: "s0 ∈ I" "s1 ∈ I" "s0 -t▹ta'→ s1" "thr s0 t = ⌊(x0, no_wait_locks)⌋"
"t ⊢ ⟨x0, shr s0⟩ -ta'→ ⟨x, shr s1⟩" "Suspend w' ∈ set ⦃ta'⦄⇘w⇙" "actions_ok s0 t ta'" "thr s1 t = ⌊(x, ln')⌋"
and step: "s1 -▹ttas→* s" and tst: "thr s t = ⌊(x, ln'')⌋" by blast
from step red have "s1 -▹ttas@[(t', ta)]→* s'" unfolding RedT_def by(rule rtrancl3p_step)
moreover from red tst False have "thr s' t = ⌊(x, ln'')⌋"
by(cases)(auto intro: redT_updTs_Some)
ultimately show ?thesis using reuse by blast
next
case True
from red show ?thesis
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 s' have ws': "redT_updWs t' (wset s) ⦃ta⦄⇘w⇙ (wset s')"
and m: "m = shr s'"
and ts't: "thr s' t' = ⌊(x', redT_updLns (locks s) t' (snd (the (thr s t'))) ⦃ta⦄⇘l⇙)⌋" by auto
from aok have nwait: "¬ waiting (wset s t')"
by(auto simp add: wset_actions_ok_def waiting_def split: if_split_asm)
have "∃w'. Suspend w' ∈ set ⦃ta⦄⇘w⇙"
proof(cases "wset s t")
case None
from redT_updWs_None_SomeD[OF ws', OF ws't None]
show ?thesis ..
next
case (Some w')
with True aok have "Notified ∈ set ⦃ta⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta⦄⇘w⇙"
by(auto simp add: wset_actions_ok_def split: if_split_asm)
with ws' show ?thesis using ws't unfolding True
by(rule redT_updWs_WokenUp_SuspendD)
qed
with tst' ts't aok ‹s ∈ I› ‹s' ∈ I› red red' show ?thesis
unfolding True m by blast
next
case (redT_acquire x n ln)
with ws't True have "wset s t = ⌊w⌋" by auto
from wset_Suspend_okD2[OF wso this] ‹thr s t' = ⌊(x, ln)⌋› True
obtain s0 s1 ttas x0 ta' w' ln' ln''
where reuse: "s0 ∈ I" "s1 ∈ I" "s0 -t▹ta'→ s1" "thr s0 t = ⌊(x0, no_wait_locks)⌋"
"t ⊢ ⟨x0, shr s0⟩ -ta'→ ⟨x, shr s1⟩" "Suspend w' ∈ set ⦃ta'⦄⇘w⇙" "actions_ok s0 t ta'" "thr s1 t = ⌊(x, ln')⌋"
and step: "s1 -▹ttas→* s" by fastforce
from step red have "s1 -▹ttas@[(t', ta)]→* s'" unfolding RedT_def by(rule rtrancl3p_step)
moreover from redT_acquire True have "thr s' t = ⌊(x, no_wait_locks)⌋" by simp
ultimately show ?thesis using reuse by blast
qed
qed
qed
qed
end
end