Theory FWLTS
section ‹The multithreaded semantics as a labelled transition system›
theory FWLTS
imports
FWProgressAux
FWLifting
LTS
begin
sublocale multithreaded_base < trsys "r t" for t .
sublocale multithreaded_base < mthr: trsys redT .
definition redT_upd_ε :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ 'x ⇒ 'm ⇒ ('l,'t,'x,'m,'w) state"
where [simp]: "redT_upd_ε s t x' m' = (locks s, ((thr s)(t ↦ (x', snd (the (thr s t)))), m'), wset s, interrupts s)"
lemma redT_upd_ε_redT_upd:
"redT_upd s t ε x' m' (redT_upd_ε s t x' m')"
by(auto simp add: redT_updLns_def redT_updWs_def)
context multithreaded begin
sublocale trsys "r t" for t .
sublocale mthr: trsys redT .
end
subsection ‹The multithreaded semantics with internal actions›
type_synonym
('l,'t,'x,'m,'w,'o) τmoves =
"'x × 'm ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'x × 'm ⇒ bool"
text ‹pretty printing for ‹τmoves››
print_translation ‹
let
fun tr' [(Const (@{type_syntax "prod"}, _) $ x1 $ m1),
(Const (@{type_syntax "fun"}, _) $
(Const (@{type_syntax "prod"}, _) $
(Const (@{type_syntax "finfun"}, _) $ l $
(Const (@{type_syntax "list"}, _) $ Const (@{type_syntax "lock_action"}, _))) $
(Const (@{type_syntax "prod"},_) $
(Const (@{type_syntax "list"}, _) $ (Const (@{type_syntax "new_thread_action"}, _) $ t1 $ x2 $ m2)) $
(Const (@{type_syntax "prod"}, _) $
(Const (@{type_syntax "list"}, _) $ (Const (@{type_syntax "conditional_action"}, _) $ t2)) $
(Const (@{type_syntax "prod"}, _) $
(Const (@{type_syntax "list"}, _) $ (Const (@{type_syntax "wait_set_action"}, _) $ t3 $ w)) $
(Const (@{type_syntax prod}, _) $
(Const (@{type_syntax list}, _) $ (Const (@{type_syntax "interrupt_action"}, _) $ t4)) $
(Const (@{type_syntax "list"}, _) $ o1)))))) $
(Const (@{type_syntax "fun"}, _) $
(Const (@{type_syntax "prod"}, _) $ x3 $ m3) $
(Const (@{type_syntax "bool"}, _))))] =
if x1 = x2 andalso x1 = x3 andalso m1 = m2 andalso m1 = m3 andalso t1 = t2 andalso t2 = t3 andalso t3 = t4
then Syntax.const (@{type_syntax "τmoves"}) $ l $ t1 $ x1 $ m1 $ w $ o1
else raise Match;
in [(@{type_syntax "fun"}, K tr')]
end
›
typ "('l,'t,'x,'m,'w,'o) τmoves"
locale τmultithreaded = multithreaded_base +
constrains final :: "'x ⇒ bool"
and r :: "('l,'t,'x,'m,'w,'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"
fixes τmove :: "('l,'t,'x,'m,'w,'o) τmoves"
sublocale τmultithreaded < τtrsys "r t" τmove for t .
context τmultithreaded begin
inductive mτmove :: "(('l,'t,'x,'m,'w) state, 't × ('l,'t,'x,'m,'w,'o) thread_action) trsys"
where
"⟦ thr s t = ⌊(x, no_wait_locks)⌋; thr s' t = ⌊(x', ln')⌋; τmove (x, shr s) ta (x', shr s') ⟧
⟹ mτmove s (t, ta) s'"
end
sublocale τmultithreaded < mthr: τtrsys redT mτmove .
context τmultithreaded begin
abbreviation τmredT :: "('l,'t,'x,'m,'w) state ⇒ ('l,'t,'x,'m,'w) state ⇒ bool"
where "τmredT == mthr.silent_move"
end
lemma (in multithreaded_base) τrtrancl3p_redT_thread_not_disappear:
assumes "τtrsys.τrtrancl3p redT τmove s ttas s'" "thr s t ≠ None"
shows "thr s' t ≠ None"
proof -
interpret T: τtrsys redT τmove .
show ?thesis
proof
assume "thr s' t = None"
with ‹τtrsys.τrtrancl3p redT τmove s ttas s'› have "thr s t = None"
by(induct rule: T.τrtrancl3p.induct)(auto simp add: split_paired_all dest: redT_thread_not_disappear)
with ‹thr s t ≠ None› show False by contradiction
qed
qed
lemma mτmove_False: "τmultithreaded.mτmove (λs ta s'. False) = (λs ta s'. False)"
by(auto intro!: ext elim: τmultithreaded.mτmove.cases)
declare split_paired_Ex [simp del]
locale τmultithreaded_wf =
τmultithreaded _ _ _ τmove +
multithreaded final r convert_RA
for τmove :: "('l,'t,'x,'m,'w,'o) τmoves" +
assumes τmove_heap: "⟦ t ⊢ (x, m) -ta→ (x', m'); τmove (x, m) ta (x', m') ⟧ ⟹ m = m'"
assumes silent_tl: "τmove s ta s' ⟹ ta = ε"
begin
lemma mτmove_silentD: "mτmove s (t, ta) s' ⟹ ta = (K$ [], [], [], [], [], [])"
by(auto elim!: mτmove.cases dest: silent_tl)
lemma mτmove_heap:
assumes redT: "redT s (t, ta) s'"
and mτmove: "mτmove s (t, ta) s'"
shows "shr s' = shr s"
using mτmove redT
by cases(auto dest: τmove_heap elim!: redT.cases)
lemma τmredT_thread_preserved:
"τmredT s s' ⟹ thr s t = None ⟷ thr s' t = None"
by(auto simp add: mthr.silent_move_iff elim!: redT.cases dest!: mτmove_silentD split: if_split_asm)
lemma τmRedT_thread_preserved:
"τmredT^** s s' ⟹ thr s t = None ⟷ thr s' t = None"
by(induct rule: rtranclp.induct)(auto dest: τmredT_thread_preserved[where t=t])
lemma τmtRedT_thread_preserved:
"τmredT^++ s s' ⟹ thr s t = None ⟷ thr s' t = None"
by(induct rule: tranclp.induct)(auto dest: τmredT_thread_preserved[where t=t])
lemma τmredT_add_thread_inv:
assumes τred: "τmredT s s'" and tst: "thr s t = None"
shows "τmredT (locks s, ((thr s)(t ↦ xln), shr s), wset s, interrupts s) (locks s', ((thr s')(t ↦ xln), shr s'), wset s', interrupts s')"
proof -
obtain ls ts m ws "is" where s: "s = (ls, (ts, m), ws, is)" by(cases s) fastforce
obtain ls' ts' m' ws' is' where s': "s' = (ls', (ts', m'), ws', is')" by(cases s') fastforce
from τred s s' obtain t' where red: "(ls, (ts, m), ws, is) -t'▹ε→ (ls', (ts', m'), ws', is')"
and τ: "mτmove (ls, (ts, m), ws, is) (t', ε) (ls', (ts', m'), ws', is')"
by(auto simp add: mthr.silent_move_iff dest: mτmove_silentD)
from red have "(ls, (ts(t ↦ xln), m), ws, is) -t'▹ε→ (ls', (ts'(t ↦ xln), m'), ws', is')"
proof(cases rule: redT_elims)
case (normal x x' m') with tst s show ?thesis
by-(rule redT_normal, auto simp add: fun_upd_twist elim!: rtrancl3p_cases)
next
case (acquire x ln n)
with tst s show ?thesis
unfolding ‹ε = (K$ [], [], [], [], [], convert_RA ln)›
by -(rule redT_acquire, auto intro: fun_upd_twist)
qed
moreover from red tst s have tt': "t ≠ t'" by(cases) auto
have "(λt''. (ts(t ↦ xln)) t'' ≠ None ∧ (ts(t ↦ xln)) t'' ≠ (ts'(t ↦ xln)) t'') =
(λt''. ts t'' ≠ None ∧ ts t'' ≠ ts' t'')" using tst s by(auto simp add: fun_eq_iff)
with τ tst tt' have "mτmove (ls, (ts(t ↦ xln), m), ws, is) (t', ε) (ls', (ts'(t ↦ xln), m'), ws', is')"
by cases(rule mτmove.intros, auto)
ultimately show ?thesis unfolding s s' by auto
qed
lemma τmRedT_add_thread_inv:
"⟦ τmredT^** s s'; thr s t = None ⟧
⟹ τmredT^** (locks s, ((thr s)(t ↦ xln), shr s), wset s, interrupts s) (locks s', ((thr s')(t ↦ xln), shr s'), wset s', interrupts s')"
apply(induct rule: rtranclp_induct)
apply(blast dest: τmRedT_thread_preserved[where t=t] τmredT_add_thread_inv[where xln=xln] intro: rtranclp.rtrancl_into_rtrancl)+
done
lemma τmtRed_add_thread_inv:
"⟦ τmredT^++ s s'; thr s t = None ⟧
⟹ τmredT^++ (locks s, ((thr s)(t ↦ xln), shr s), wset s, interrupts s) (locks s', ((thr s')(t ↦ xln), shr s'), wset s', interrupts s')"
apply(induct rule: tranclp_induct)
apply(blast dest: τmtRedT_thread_preserved[where t=t] τmredT_add_thread_inv[where xln=xln] intro: tranclp.trancl_into_trancl)+
done
lemma silent_move_into_RedT_τ_inv:
assumes move: "silent_move t (x, shr s) (x', m')"
and state: "thr s t = ⌊(x, no_wait_locks)⌋" "wset s t = None"
shows "τmredT s (redT_upd_ε s t x' m')"
proof -
from move obtain red: "t ⊢ (x, shr s) -ε→ (x', m')" and τ: "τmove (x, shr s) ε (x', m')"
by(auto simp add: silent_move_iff dest: silent_tl)
from red state have "s -t▹ε→ redT_upd_ε s t x' m'"
by -(rule redT_normal, auto simp add: redT_updLns_def o_def finfun_Diag_const2 redT_updWs_def)
moreover from τ red state have "mτmove s (t, ε) (redT_upd_ε s t x' m')"
by -(rule mτmove.intros, auto dest: τmove_heap simp add: redT_updLns_def)
ultimately show ?thesis by auto
qed
lemma silent_moves_into_RedT_τ_inv:
assumes major: "silent_moves t (x, shr s) (x', m')"
and state: "thr s t = ⌊(x, no_wait_locks)⌋" "wset s t = None"
shows "τmredT^** s (redT_upd_ε s t x' m')"
using major
proof(induct rule: rtranclp_induct2)
case refl with state show ?case by(cases s)(auto simp add: fun_upd_idem)
next
case (step x' m' x'' m'')
from ‹silent_move t (x', m') (x'', m'')› state
have "τmredT (redT_upd_ε s t x' m') (redT_upd_ε (redT_upd_ε s t x' m') t x'' m'')"
by -(rule silent_move_into_RedT_τ_inv, auto)
hence "τmredT (redT_upd_ε s t x' m') (redT_upd_ε s t x'' m'')" by(simp)
with ‹τmredT^** s (redT_upd_ε s t x' m')› show ?case ..
qed
lemma red_rtrancl_τ_heapD_inv:
"⟦ silent_moves t s s'; wfs t s ⟧ ⟹ snd s' = snd s"
proof(induct rule: rtranclp_induct)
case base show ?case ..
next
case (step s' s'')
thus ?case by(cases s, cases s', cases s'')(auto dest: τmove_heap)
qed
lemma red_trancl_τ_heapD_inv:
"⟦ silent_movet t s s'; wfs t s ⟧ ⟹ snd s' = snd s"
proof(induct rule: tranclp_induct)
case (base s') thus ?case by(cases s')(cases s, auto simp add: silent_move_iff dest: τmove_heap)
next
case (step s' s'')
thus ?case by(cases s, cases s', cases s'')(auto simp add: silent_move_iff dest: τmove_heap)
qed
lemma red_trancl_τ_into_RedT_τ_inv:
assumes major: "silent_movet t (x, shr s) (x', m')"
and state: "thr s t = ⌊(x, no_wait_locks)⌋" "wset s t = None"
shows "τmredT^++ s (redT_upd_ε s t x' m')"
using major
proof(induct rule: tranclp_induct2)
case (base x' m')
thus ?case using state
by -(rule tranclp.r_into_trancl, rule silent_move_into_RedT_τ_inv, auto)
next
case (step x' m' x'' m'')
hence "τmredT^++ s (redT_upd_ε s t x' m')" by blast
moreover from ‹silent_move t (x', m') (x'', m'')› state
have "τmredT (redT_upd_ε s t x' m') (redT_upd_ε (redT_upd_ε s t x' m') t x'' m'')"
by -(rule silent_move_into_RedT_τ_inv, auto simp add: redT_updLns_def)
hence "τmredT (redT_upd_ε s t x' m') (redT_upd_ε s t x'' m'')"
by(simp add: redT_updLns_def)
ultimately show ?case ..
qed
lemma τdiverge_into_τmredT:
assumes "τdiverge t (x, shr s)"
and "thr s t = ⌊(x, no_wait_locks)⌋" "wset s t = None"
shows "mthr.τdiverge s"
using assms
proof(coinduction arbitrary: s x)
case (τdiverge s x)
note tst = ‹thr s t = ⌊(x, no_wait_locks)⌋›
from ‹τdiverge t (x, shr s)› obtain x' m' where "silent_move t (x, shr s) (x', m')"
and "τdiverge t (x', m')" by cases auto
from ‹silent_move t (x, shr s) (x', m')› tst ‹wset s t = None›
have "τmredT s (redT_upd_ε s t x' m')" by(rule silent_move_into_RedT_τ_inv)
moreover have "thr (redT_upd_ε s t x' m') t = ⌊(x', no_wait_locks)⌋"
using tst by(auto simp add: redT_updLns_def)
moreover have "wset (redT_upd_ε s t x' m') t = None" using ‹wset s t = None› by simp
moreover from ‹τdiverge t (x', m')› have "τdiverge t (x', shr (redT_upd_ε s t x' m'))" by simp
ultimately show ?case using ‹τdiverge t (x', m')› by blast
qed
lemma τdiverge_τmredTD:
assumes div: "mthr.τdiverge s"
and fin: "finite (dom (thr s))"
shows "∃t x. thr s t = ⌊(x, no_wait_locks)⌋ ∧ wset s t = None ∧ τdiverge t (x, shr s)"
using fin div
proof(induct A≡"dom (thr s)" arbitrary: s rule: finite_induct)
case empty
from ‹mthr.τdiverge s› obtain s' where "τmredT s s'" by cases auto
with ‹{} = dom (thr s)›[symmetric] have False by(auto elim!: mthr.silent_move.cases redT.cases)
thus ?case ..
next
case (insert t A)
note IH = ‹⋀s. ⟦ A = dom (thr s); mthr.τdiverge s ⟧
⟹ ∃t x. thr s t = ⌊(x, no_wait_locks)⌋ ∧ wset s t = None ∧ τdiverge t (x, shr s)›
from ‹insert t A = dom (thr s)›
obtain x ln where tst: "thr s t = ⌊(x, ln)⌋" by(fastforce simp add: dom_def)
define s' where "s' = (locks s, ((thr s)(t := None), shr s), wset s, interrupts s)"
show ?case
proof(cases "ln = no_wait_locks ∧ τdiverge t (x, shr s) ∧ wset s t = None")
case True
with tst show ?thesis by blast
next
case False
define xm where "xm = (x, shr s)"
define xm' where "xm' = (x, shr s)"
have "A = dom (thr s')" using ‹t ∉ A› ‹insert t A = dom (thr s)›
unfolding s'_def by auto
moreover {
from xm'_def tst ‹mthr.τdiverge s› False
have "∃s x. thr s t = ⌊(x, ln)⌋ ∧ (ln ≠ no_wait_locks ∨ wset s t ≠ None ∨ ¬ τdiverge t xm') ∧
s' = (locks s, ((thr s)(t := None), shr s), wset s, interrupts s) ∧ xm = (x, shr s) ∧
mthr.τdiverge s ∧ silent_moves t xm' xm"
unfolding s'_def xm_def by blast
moreover
from False have "wfP (if τdiverge t xm' then (λs s'. False) else flip (silent_move_from t xm'))"
using τdiverge_neq_wfP_silent_move_from[of t "(x, shr s)"] unfolding xm'_def by(auto)
ultimately have "mthr.τdiverge s'"
proof(coinduct s' xm rule: mthr.τdiverge_trancl_measure_coinduct)
case (τdiverge s' xm)
then obtain s x where tst: "thr s t = ⌊(x, ln)⌋"
and blocked: "ln ≠ no_wait_locks ∨ wset s t ≠ None ∨ ¬ τdiverge t xm'"
and s'_def: "s' = (locks s, ((thr s)(t := None), shr s), wset s, interrupts s)"
and xm_def: "xm = (x, shr s)"
and xmxm': "silent_moves t xm' (x, shr s)"
and "mthr.τdiverge s" by blast
from ‹mthr.τdiverge s› obtain s'' where "τmredT s s''" "mthr.τdiverge s''" by cases auto
from ‹τmredT s s''› obtain t' ta where "s -t'▹ta→ s''" and "mτmove s (t', ta) s''" by auto
then obtain x' x'' m'' where red: "t' ⊢ ⟨x', shr s⟩ -ta→ ⟨x'', m''⟩"
and tst': "thr s t' = ⌊(x', no_wait_locks)⌋"
and aoe: "actions_ok s t' ta"
and s'': "redT_upd s t' ta x'' m'' s''"
by cases(fastforce elim: mτmove.cases)+
from ‹mτmove s (t', ta) s''› have [simp]: "ta = ε"
by(auto elim!: mτmove.cases dest!: silent_tl)
hence wst': "wset s t' = None" using aoe by auto
from ‹mτmove s (t', ta) s''› tst' s''
have "τmove (x', shr s) ε (x'', m'')" by(auto elim: mτmove.cases)
show ?case
proof(cases "t' = t")
case False
with tst' wst' have "thr s' t' = ⌊(x', no_wait_locks)⌋"
"wset s' t' = None" "shr s' = shr s" unfolding s'_def by auto
with red have "s' -t'▹ε→ redT_upd_ε s' t' x'' m''"
by -(rule redT_normal, auto simp add: redT_updLns_def o_def finfun_Diag_const2 redT_updWs_def)
moreover from ‹τmove (x', shr s) ε (x'', m'')› ‹thr s' t' = ⌊(x', no_wait_locks)⌋› ‹shr s' = shr s›
have "mτmove s' (t', ta) (redT_upd_ε s' t' x'' m'')"
by -(rule mτmove.intros, auto)
ultimately have "τmredT s' (redT_upd_ε s' t' x'' m'')"
unfolding ‹ta = ε› by(rule mthr.silent_move.intros)
hence "τmredT^++ s' (redT_upd_ε s' t' x'' m'')" ..
moreover have "thr s'' t = ⌊(x, ln)⌋"
using tst ‹t' ≠ t› s'' by auto
moreover from ‹τmove (x', shr s) ε (x'', m'')› red
have [simp]: "m'' = shr s" by(auto dest: τmove_heap)
hence "shr s = shr s''" using s'' by(auto)
have "ln ≠ no_wait_locks ∨ wset s'' t ≠ None ∨ ¬ τdiverge t xm'"
using blocked s'' by(auto simp add: redT_updWs_def elim!: rtrancl3p_cases)
moreover have "redT_upd_ε s' t' x'' m'' = (locks s'', ((thr s'')(t := None), shr s''), wset s'', interrupts s'')"
unfolding s'_def using tst s'' ‹t' ≠ t›
by(auto intro: ext elim!: rtrancl3p_cases simp add: redT_updLns_def redT_updWs_def)
ultimately show ?thesis using ‹mthr.τdiverge s''› xmxm'
unfolding ‹shr s = shr s''› by blast
next
case True
with tst tst' wst' blocked have "¬ τdiverge t xm'"
and [simp]: "x' = x" by auto
moreover from red ‹τmove (x', shr s) ε (x'', m'')› True
have "silent_move t (x, shr s) (x'', m'')" by auto
with xmxm' have "silent_move_from t xm' (x, shr s) (x'', m'')"
by(rule silent_move_fromI)
ultimately have "(if τdiverge t xm' then λs s'. False else flip (silent_move_from t xm')) (x'', m'') xm"
by(auto simp add: flip_conv xm_def)
moreover have "thr s'' t = ⌊(x'', ln)⌋" using tst True s''
by(auto simp add: redT_updLns_def)
moreover from ‹τmove (x', shr s) ε (x'', m'')› red
have [simp]: "m'' = shr s" by(auto dest: τmove_heap)
hence "shr s = shr s''" using s'' by auto
have "s' = (locks s'', ((thr s'')(t := None), shr s''), wset s'', interrupts s'')"
using True s'' unfolding s'_def
by(auto intro: ext elim!: rtrancl3p_cases simp add: redT_updLns_def redT_updWs_def)
moreover have "(x'', m'') = (x'', shr s'')" using s'' by auto
moreover from xmxm' ‹silent_move t (x, shr s) (x'', m'')›
have "silent_moves t xm' (x'', shr s'')"
unfolding ‹m'' = shr s› ‹shr s = shr s''› by auto
ultimately show ?thesis using ‹¬ τdiverge t xm'› ‹mthr.τdiverge s''› by blast
qed
qed }
ultimately have "∃t x. thr s' t = ⌊(x, no_wait_locks)⌋ ∧ wset s' t = None ∧ τdiverge t (x, shr s')" by(rule IH)
then obtain t' x' where "thr s' t' = ⌊(x', no_wait_locks)⌋"
and "wset s' t' = None" and "τdiverge t' (x', shr s')" by blast
moreover with False have "t' ≠ t" by(auto simp add: s'_def)
ultimately have "thr s t' = ⌊(x', no_wait_locks)⌋" "wset s t' = None" "τdiverge t' (x', shr s)"
unfolding s'_def by auto
thus ?thesis by blast
qed
qed
lemma τmredT_preserves_final_thread:
"⟦ τmredT s s'; final_thread s t ⟧ ⟹ final_thread s' t"
by(auto elim: mthr.silent_move.cases intro: redT_preserves_final_thread)
lemma τmRedT_preserves_final_thread:
"⟦ τmredT^** s s'; final_thread s t ⟧ ⟹ final_thread s' t"
by(induct rule: rtranclp.induct)(blast intro: τmredT_preserves_final_thread)+
lemma silent_moves2_silentD:
assumes "rtrancl3p mthr.silent_move2 s ttas s'"
and "(t, ta) ∈ set ttas"
shows "ta = ε"
using assms
by(induct)(auto simp add: mthr.silent_move2_def dest: mτmove_silentD)
lemma inf_step_silentD:
assumes step: "trsys.inf_step mthr.silent_move2 s ttas"
and lset: "(t, ta) ∈ lset ttas"
shows "ta = ε"
using lset step
by(induct arbitrary: s rule: lset_induct)(fastforce elim: trsys.inf_step.cases simp add: mthr.silent_move2_def dest: mτmove_silentD)+
end
subsection ‹The multithreaded semantics with a well-founded relation on states›
locale multithreaded_base_measure = multithreaded_base +
constrains final :: "'x ⇒ bool"
and r :: "('l,'t,'x,'m,'w,'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"
fixes μ :: "('x × 'm) ⇒ ('x × 'm) ⇒ bool"
begin
inductive mμt :: "'m ⇒ ('l,'t,'x) thread_info ⇒ ('l,'t,'x) thread_info ⇒ bool"
for m and ts and ts'
where
mμtI:
"⋀ln. ⟦ finite (dom ts); ts t = ⌊(x, ln)⌋; ts' t = ⌊(x', ln')⌋; μ (x, m) (x', m); ⋀t'. t' ≠ t ⟹ ts t' = ts' t' ⟧
⟹ mμt m ts ts'"
definition mμ :: "('l,'t,'x,'m,'w) state ⇒ ('l,'t,'x,'m,'w) state ⇒ bool"
where "mμ s s' ⟷ shr s = shr s' ∧ mμt (shr s) (thr s) (thr s')"
lemma mμt_thr_dom_eq: "mμt m ts ts' ⟹ dom ts = dom ts'"
apply(erule mμt.cases)
apply(rule equalityI)
apply(rule subsetI)
apply(case_tac "xa = t")
apply(auto)[2]
apply(rule subsetI)
apply(case_tac "xa = t")
apply auto
done
lemma mμ_finite_thrD:
assumes "mμt m ts ts'"
shows "finite (dom ts)" "finite (dom ts')"
using assms
by(simp_all add: mμt_thr_dom_eq[symmetric])(auto elim: mμt.cases)
end
locale multithreaded_base_measure_wf = multithreaded_base_measure +
constrains final :: "'x ⇒ bool"
and r :: "('l,'t,'x,'m,'w,'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"
and μ :: "('x × 'm) ⇒ ('x × 'm) ⇒ bool"
assumes wf_μ: "wfP μ"
begin
lemma wf_mμt: "wfP (mμt m)"
unfolding wfP_eq_minimal
proof(intro strip)
fix Q :: "('l,'t,'x) thread_info set" and ts
assume "ts ∈ Q"
show "∃z∈Q. ∀y. mμt m y z ⟶ y ∉ Q"
proof(cases "finite (dom ts)")
case False
hence "∀y. mμt m y ts ⟶ y ∉ Q" by(auto dest: mμ_finite_thrD)
thus ?thesis using ‹ts ∈ Q› by blast
next
case True
thus ?thesis using ‹ts ∈ Q›
proof(induct A≡"dom ts" arbitrary: ts Q rule: finite_induct)
case empty
hence "dom ts = {}" by simp
with ‹ts ∈ Q› show ?case by(auto elim: mμt.cases)
next
case (insert t A)
note IH = ‹⋀ts Q. ⟦A = dom ts; ts ∈ Q⟧ ⟹ ∃z∈Q. ∀y. mμt m y z ⟶ y ∉ Q›
define Q' where "Q' = {ts. ts t = None ∧ (∃xln. ts(t ↦ xln) ∈ Q)}"
let ?ts' = "ts(t := None)"
from ‹insert t A = dom ts› ‹t ∉ A› have "A = dom ?ts'" by auto
moreover from ‹insert t A = dom ts› obtain xln where "ts t = ⌊xln⌋" by(cases "ts t") auto
hence "ts(t ↦ xln) = ts" by(auto simp add: fun_eq_iff)
with ‹ts ∈ Q› have "ts(t ↦ xln) ∈ Q" by(auto)
hence "?ts' ∈ Q'" unfolding Q'_def by(auto simp del: split_paired_Ex)
ultimately have "∃z∈Q'. ∀y. mμt m y z ⟶ y ∉ Q'" by(rule IH)
then obtain ts' where "ts' ∈ Q'"
and min: "⋀ts''. mμt m ts'' ts' ⟹ ts'' ∉ Q'" by blast
from ‹ts' ∈ Q'› obtain x' ln' where "ts' t = None" "ts'(t ↦ (x', ln')) ∈ Q"
unfolding Q'_def by auto
define Q'' where "Q'' = {(x, m)|x. ∃ln. ts'(t ↦ (x, ln)) ∈ Q}"
from ‹ts'(t ↦ (x', ln')) ∈ Q› have "(x', m) ∈ Q''" unfolding Q''_def by blast
hence "∃xm''∈Q''. ∀xm'''. μ xm''' xm'' ⟶ xm''' ∉ Q''" by(rule wf_μ[unfolded wfP_eq_minimal, rule_format])
then obtain xm'' where "xm'' ∈ Q''" and min': "⋀xm'''. μ xm''' xm'' ⟹ xm''' ∉ Q''" by blast
from ‹xm'' ∈ Q''› obtain x'' ln'' where "xm'' = (x'', m)" "ts'(t ↦ (x'', ln'')) ∈ Q" unfolding Q''_def by blast
moreover {
fix ts''
assume "mμt m ts'' (ts'(t ↦ (x'', ln'')))"
then obtain T X'' LN'' X' LN'
where "finite (dom ts'')" "ts'' T = ⌊(X'', LN'')⌋"
and "(ts'(t ↦ (x'', ln''))) T = ⌊(X', LN')⌋" "μ (X'', m) (X', m)"
and eq: "⋀t'. t' ≠ T ⟹ ts'' t' = (ts'(t ↦ (x'', ln''))) t'" by(cases) blast
have "ts'' ∉ Q"
proof(cases "T = t")
case True
from True ‹(ts'(t ↦ (x'', ln''))) T = ⌊(X', LN')⌋› have "X' = x''" by simp
with ‹μ (X'', m) (X', m)› have "(X'', m) ∉ Q''" by(auto dest: min'[unfolded ‹xm'' = (x'', m)›])
hence "∀ln. ts'(t ↦ (X'', ln)) ∉ Q" by(simp add: Q''_def)
moreover from ‹ts' t = None› eq True
have "ts''(t := None) = ts'" by(auto simp add: fun_eq_iff)
with ‹ts'' T = ⌊(X'', LN'')⌋› True
have ts'': "ts'' = ts'(t ↦ (X'', LN''))" by(auto intro!: ext)
ultimately show ?thesis by blast
next
case False
from ‹finite (dom ts'')› have "finite (dom (ts''(t := None)))" by simp
moreover from ‹ts'' T = ⌊(X'', LN'')⌋› False
have "(ts''(t := None)) T = ⌊(X'', LN'')⌋" by simp
moreover from ‹(ts'(t ↦ (x'', ln''))) T = ⌊(X', LN')⌋› False
have "ts' T = ⌊(X', LN')⌋" by simp
ultimately have "mμt m (ts''(t := None)) ts'" using ‹μ (X'', m) (X', m)›
proof(rule mμtI)
fix t'
assume "t' ≠ T"
with eq[OF False[symmetric]] eq[OF this] ‹ts' t = None›
show "(ts''(t := None)) t' = ts' t'" by auto
qed
hence "ts''(t := None) ∉ Q'" by(rule min)
thus ?thesis
proof(rule contrapos_nn)
assume "ts'' ∈ Q"
from eq[OF False[symmetric]] have "ts'' t = ⌊(x'', ln'')⌋" by simp
hence ts'': "ts''(t ↦ (x'', ln'')) = ts''" by(auto simp add: fun_eq_iff)
from ‹ts'' ∈ Q› have "ts''(t ↦ (x'', ln'')) ∈ Q" unfolding ts'' .
thus "ts''(t := None) ∈ Q'" unfolding Q'_def by auto
qed
qed
}
ultimately show ?case by blast
qed
qed
qed
lemma wf_mμ: "wfP mμ"
proof -
have "wf (inv_image (same_fst (λm. True) (λm. {(ts, ts'). mμt m ts ts'})) (λs. (shr s, thr s)))"
by(rule wf_inv_image)(rule wf_same_fst, rule wf_mμt[unfolded wfP_def])
also have "inv_image (same_fst (λm. True) (λm. {(ts, ts'). mμt m ts ts'})) (λs. (shr s, thr s)) = {(s, s'). mμ s s'}"
by(auto simp add: mμ_def same_fst_def)
finally show ?thesis by(simp add: wfP_def)
qed
end
end