Theory HB_Completion
section ‹Happens-before consistent completion of executions in the JMM›
theory HB_Completion imports
Non_Speculative
begin
coinductive ta_hb_consistent :: "'m prog ⇒ ('thread_id × ('addr, 'thread_id) obs_event action) list ⇒ ('thread_id × ('addr, 'thread_id) obs_event action) llist ⇒ bool"
for P :: "'m prog"
where
LNil: "ta_hb_consistent P obs LNil"
| LCons:
"⟦ ta_hb_consistent P (obs @ [ob]) obs';
case ob of (t, NormalAction (ReadMem ad al v))
⇒ (∃w. w ∈ write_actions (llist_of (obs @ [ob])) ∧ (ad, al) ∈ action_loc P (llist_of (obs @ [ob])) w ∧
value_written P (llist_of (obs @ [ob])) w (ad, al) = v ∧
P,llist_of (obs @ [ob]) ⊢ w ≤hb length obs ∧
(∀w'∈write_actions (llist_of (obs @ [ob])). (ad, al) ∈ action_loc P (llist_of (obs @ [ob])) w' ⟶
(P,llist_of (obs @ [ob]) ⊢ w ≤hb w' ∧ P,llist_of (obs @ [ob]) ⊢ w' ≤hb length obs ∨
is_volatile P al ∧ P,llist_of (obs @ [ob]) ⊢ w ≤so w' ∧ P,llist_of (obs @ [ob]) ⊢ w' ≤so length obs) ⟶
w' = w))
| _ ⇒ True ⟧
⟹ ta_hb_consistent P obs (LCons ob obs')"
inductive_simps ta_hb_consistent_LNil [simp]:
"ta_hb_consistent P obs LNil"
inductive_simps ta_hb_consistent_LCons:
"ta_hb_consistent P obs (LCons ob obs')"
lemma ta_hb_consistent_into_non_speculative:
"ta_hb_consistent P obs0 obs
⟹ non_speculative P (w_values P (λ_. {}) (map snd obs0)) (lmap snd obs)"
proof(coinduction arbitrary: obs0 obs)
case (non_speculative obs0 obs)
let ?vs = "w_values P (λ_. {}) (map snd obs0)"
let ?CH = "λvs obs'. ∃obs0 obs. vs = w_values P (λ_. {}) (map snd obs0) ∧ obs' = lmap snd obs ∧ ta_hb_consistent P obs0 obs"
from non_speculative show ?case
proof(cases)
case LNil hence ?LNil by simp
thus ?thesis ..
next
case (LCons tob obs'')
note obs = ‹obs = LCons tob obs''›
obtain t ob where tob: "tob = (t, ob)" by(cases tob)
from ‹ta_hb_consistent P (obs0 @ [tob]) obs''› tob obs
have "?CH (w_value P ?vs ob) (lmap snd obs'')" by(auto intro!: exI)
moreover {
fix ad al v
assume ob: "ob = NormalAction (ReadMem ad al v)"
with LCons tob obtain w where w: "w ∈ write_actions (llist_of (obs0 @ [tob]))"
and adal: "(ad, al) ∈ action_loc P (llist_of (obs0 @ [tob])) w"
and v: "value_written P (llist_of (obs0 @ [tob])) w (ad, al) = v" by auto
from w obtain "is_write_action (action_obs (llist_of (obs0 @ [tob])) w)"
and w_actions: "w ∈ actions (llist_of (obs0 @ [tob]))" by cases
hence "v ∈ ?vs (ad, al)"
proof(cases)
case (WriteMem ad' al' v')
hence "NormalAction (WriteMem ad al v) ∈ set (map snd obs0)"
using adal ob tob v w_actions unfolding in_set_conv_nth
by(auto simp add: action_obs_def nth_append value_written.simps actions_def cong: conj_cong split: if_split_asm)
thus ?thesis by(rule w_values_WriteMemD)
next
case (NewHeapElem ad' hT)
hence "NormalAction (NewHeapElem ad hT) ∈ set (map snd obs0)"
using adal ob tob v w_actions unfolding in_set_conv_nth
by(auto simp add: action_obs_def nth_append value_written.simps actions_def cong: conj_cong split: if_split_asm)
thus ?thesis using NewHeapElem adal unfolding v[symmetric]
by(fastforce simp add: value_written.simps intro!: w_values_new_actionD intro: rev_image_eqI)
qed }
hence "case ob of NormalAction (ReadMem ad al v) ⇒ v ∈ ?vs (ad, al) | _ ⇒ True"
by(simp split: action.split obs_event.split)
ultimately have ?LCons using obs tob by simp
thus ?thesis ..
qed
qed
lemma ta_hb_consistent_lappendI:
assumes hb1: "ta_hb_consistent P E E'"
and hb2: "ta_hb_consistent P (E @ list_of E') E''"
and fin: "lfinite E'"
shows "ta_hb_consistent P E (lappend E' E'')"
using fin hb1 hb2
proof(induction arbitrary: E)
case lfinite_LNil thus ?case by simp
next
case (lfinite_LConsI E' tob)
from ‹ta_hb_consistent P E (LCons tob E')›
have "ta_hb_consistent P (E @ [tob]) E'" by cases
moreover from ‹ta_hb_consistent P (E @ list_of (LCons tob E')) E''› ‹lfinite E'›
have "ta_hb_consistent P ((E @ [tob]) @ list_of E') E''" by simp
ultimately have "ta_hb_consistent P (E @ [tob]) (lappend E' E'')" by(rule lfinite_LConsI.IH)
thus ?case unfolding lappend_code apply(rule ta_hb_consistent.LCons)
using ‹ta_hb_consistent P E (LCons tob E')›
by cases (simp split: prod.split_asm action.split_asm obs_event.split_asm)
qed
lemma ta_hb_consistent_coinduct_append
[consumes 1, case_names ta_hb_consistent, case_conclusion ta_hb_consistent LNil lappend]:
assumes major: "X E tobs"
and step: "⋀E tobs. X E tobs
⟹ tobs = LNil ∨
(∃tobs' tobs''. tobs = lappend tobs' tobs'' ∧ tobs' ≠ LNil ∧ ta_hb_consistent P E tobs' ∧
(lfinite tobs' ⟶ (X (E @ list_of tobs') tobs''∨
ta_hb_consistent P (E @ list_of tobs') tobs'')))"
(is "⋀E tobs. _ ⟹ _ ∨ ?step E tobs")
shows "ta_hb_consistent P E tobs"
proof -
from major
have "∃tobs' tobs''. tobs = lappend (llist_of tobs') tobs'' ∧ ta_hb_consistent P E (llist_of tobs') ∧
X (E @ tobs') tobs''"
by(auto intro: exI[where x="[]"])
thus ?thesis
proof(coinduct)
case (ta_hb_consistent E tobs)
then obtain tobs' tobs''
where tobs: "tobs = lappend (llist_of tobs') tobs''"
and hb_tobs': "ta_hb_consistent P E (llist_of tobs')"
and X: "X (E @ tobs') tobs''" by blast
show ?case
proof(cases tobs')
case Nil
with X have "X E tobs''" by simp
from step[OF this] show ?thesis
proof
assume "tobs'' = LNil"
with Nil tobs show ?thesis by simp
next
assume "?step E tobs''"
then obtain tobs''' tobs''''
where tobs'': "tobs'' = lappend tobs''' tobs''''" and "tobs''' ≠ LNil"
and sc_obs''': "ta_hb_consistent P E tobs'''"
and fin: "lfinite tobs''' ⟹ X (E @ list_of tobs''') tobs'''' ∨
ta_hb_consistent P (E @ list_of tobs''') tobs''''"
by blast
from ‹tobs''' ≠ LNil› obtain t ob tobs''''' where tobs''': "tobs''' = LCons (t, ob) tobs'''''"
unfolding neq_LNil_conv by auto
with Nil tobs'' tobs have concl1: "tobs = LCons (t, ob) (lappend tobs''''' tobs'''')" by simp
have ?LCons
proof(cases "lfinite tobs'''")
case False
hence "lappend tobs''''' tobs'''' = tobs'''''" using tobs''' by(simp add: lappend_inf)
hence "ta_hb_consistent P (E @ [(t, ob)]) (lappend tobs''''' tobs'''')"
using sc_obs''' tobs''' by(simp add: ta_hb_consistent_LCons)
with concl1 show ?LCons apply(simp)
using sc_obs'''[unfolded tobs'''] by cases simp
next
case True
with tobs''' obtain tobs'''''' where tobs''''': "tobs''''' = llist_of tobs''''''"
by simp(auto simp add: lfinite_eq_range_llist_of)
from fin[OF True]
have "ta_hb_consistent P (E @ [(t, ob)]) (llist_of tobs'''''') ∧ X (E @ (t, ob) # tobs'''''') tobs'''' ∨
ta_hb_consistent P (E @ [(t, ob)]) (lappend (llist_of tobs'''''') tobs'''')"
proof
assume X: "X (E @ list_of tobs''') tobs''''"
hence "X (E @ (t, ob) # tobs'''''') tobs''''" using tobs''''' tobs''' by simp
moreover have "ta_hb_consistent P (E @ [(t, ob)]) (llist_of tobs'''''')"
using sc_obs''' tobs''' tobs''''' by(simp add: ta_hb_consistent_LCons)
ultimately show ?thesis by simp
next
assume "ta_hb_consistent P (E @ list_of tobs''') tobs''''"
with sc_obs''' tobs''''' tobs'''
have "ta_hb_consistent P (E @ [(t, ob)]) (lappend (llist_of tobs'''''') tobs'''')"
by(simp add: ta_hb_consistent_LCons ta_hb_consistent_lappendI)
thus ?thesis ..
qed
hence "((∃tobs' tobs''. lappend (llist_of tobs'''''') tobs'''' = lappend (llist_of tobs') tobs'' ∧
ta_hb_consistent P (E @ [(t, ob)]) (llist_of tobs') ∧ X (E @ (t, ob) # tobs') tobs'') ∨
ta_hb_consistent P (E @ [(t, ob)]) (lappend (llist_of tobs'''''') tobs''''))"
by auto
thus "?LCons" using concl1 tobs''''' apply(simp)
using sc_obs'''[unfolded tobs'''] by cases simp
qed
thus ?thesis ..
qed
next
case (Cons tob tobs''')
with X tobs hb_tobs' show ?thesis by(auto simp add: ta_hb_consistent_LCons)
qed
qed
qed
lemma ta_hb_consistent_coinduct_append_wf
[consumes 2, case_names ta_hb_consistent, case_conclusion ta_hb_consistent LNil lappend]:
assumes major: "X E obs a"
and wf: "wf R"
and step: "⋀E obs a. X E obs a
⟹ obs = LNil ∨
(∃obs' obs'' a'. obs = lappend obs' obs'' ∧ ta_hb_consistent P E obs' ∧ (obs' = LNil ⟶ (a', a) ∈ R) ∧
(lfinite obs' ⟶ X (E @ list_of obs') obs'' a' ∨
ta_hb_consistent P (E @ list_of obs') obs''))"
(is "⋀E obs a. _ ⟹ _ ∨ ?step E obs a")
shows "ta_hb_consistent P E obs"
proof -
{ fix E obs a
assume "X E obs a"
with wf
have "obs = LNil ∨ (∃obs' obs''. obs = lappend obs' obs'' ∧ obs' ≠ LNil ∧ ta_hb_consistent P E obs' ∧
(lfinite obs' ⟶ (∃a. X (E @ list_of obs') obs'' a) ∨
ta_hb_consistent P (E @ list_of obs') obs''))"
(is "_ ∨ ?step_concl E obs")
proof(induction a arbitrary: E obs rule: wf_induct[consumes 1, case_names wf])
case (wf a)
note IH = wf.IH[rule_format]
from step[OF ‹X E obs a›]
show ?case
proof
assume "obs = LNil" thus ?thesis ..
next
assume "?step E obs a"
then obtain obs' obs'' a'
where obs: "obs = lappend obs' obs''"
and sc_obs': "ta_hb_consistent P E obs'"
and decr: "obs' = LNil ⟹ (a', a) ∈ R"
and fin: "lfinite obs' ⟹
X (E @ list_of obs') obs'' a' ∨
ta_hb_consistent P (E @ list_of obs') obs''"
by blast
show ?case
proof(cases "obs' = LNil")
case True
hence "lfinite obs'" by simp
from fin[OF this] show ?thesis
proof
assume X: "X (E @ list_of obs') obs'' a'"
from True have "(a', a) ∈ R" by(rule decr)
from IH[OF this X] show ?thesis
proof
assume "obs'' = LNil"
with True obs have "obs = LNil" by simp
thus ?thesis ..
next
assume "?step_concl (E @ list_of obs') obs''"
hence "?step_concl E obs" using True obs by simp
thus ?thesis ..
qed
next
assume "ta_hb_consistent P (E @ list_of obs') obs''"
thus ?thesis using obs True
by cases (auto 4 3 cong: action.case_cong obs_event.case_cong intro: exI[where x="LCons x LNil" for x] simp add: ta_hb_consistent_LCons)
qed
next
case False
with obs sc_obs' fin show ?thesis by auto
qed
qed
qed }
note step' = this
from major show ?thesis
proof(coinduction arbitrary: E obs a rule: ta_hb_consistent_coinduct_append)
case (ta_hb_consistent E obs)
thus ?case by simp(rule step')
qed
qed
lemma ta_hb_consistent_lappendD2:
assumes hb: "ta_hb_consistent P E (lappend E' E'')"
and fin: "lfinite E'"
shows "ta_hb_consistent P (E @ list_of E') E''"
using fin hb
by(induct arbitrary: E)(fastforce simp add: ta_hb_consistent_LCons)+
lemma ta_hb_consistent_Read_hb:
fixes E E' defines "E'' ≡ lappend (llist_of E') E"
assumes hb: "ta_hb_consistent P E' E"
and tsa: "thread_start_actions_ok E''"
and E'': "is_write_seen P (llist_of E') ws'"
and new_actions_for_fun:
"⋀w w' adal. ⟦ w ∈ new_actions_for P E'' adal;
w' ∈ new_actions_for P E'' adal ⟧ ⟹ w = w'"
shows "∃ws. P ⊢ (E'', ws) √ ∧ (∀n. n ∈ read_actions E'' ⟶ length E' ≤ n ⟶ P,E'' ⊢ ws n ≤hb n) ∧
(∀n. n < length E' ⟶ ws n = ws' n)"
proof(intro exI conjI strip)
let ?P =
"λn w. case lnth E'' n of
(t, NormalAction (ReadMem ad al v)) ⇒
(w ∈ write_actions E'' ∧ (ad, al) ∈ action_loc P E'' w ∧ value_written P E'' w (ad, al) = v ∧
P,E'' ⊢ w ≤hb n ∧
(∀w'∈write_actions E''. (ad, al) ∈ action_loc P E'' w' ⟶
(P,E'' ⊢ w ≤hb w' ∧ P,E'' ⊢ w' ≤hb n ∨
is_volatile P al ∧ P,E'' ⊢ w ≤so w' ∧ P,E'' ⊢ w' ≤so n) ⟶
w' = w))"
let ?ws = "λn. if n < length E' then ws' n else Eps (?P n)"
have "⋀n. n < length E' ⟹ ?ws n = ws' n" by simp
moreover
have "P ⊢ (E'', ?ws) √ ∧
(∀n ad al v. n ∈ read_actions E'' ⟶ length E' ≤ n ⟶ action_obs E'' n = NormalAction (ReadMem ad al v) ⟶ P,E'' ⊢ ?ws n ≤hb n)"
proof(intro conjI wf_execI strip is_write_seenI)
fix a' ad al v
assume read: "a' ∈ read_actions E''"
and aobs: "action_obs E'' a' = NormalAction (ReadMem ad al v)"
then obtain t where a': "enat a' < llength E''"
and lnth'': "lnth E'' a' = (t, NormalAction (ReadMem ad al v))"
by(cases)(cases "lnth E'' a'", clarsimp simp add: actions_def action_obs_def)
have "?ws a' ∈ write_actions E'' ∧
(ad, al) ∈ action_loc P E'' (?ws a') ∧
value_written P E'' (?ws a') (ad, al) = v ∧
(length E' ≤ a' ⟶ P,E'' ⊢ ?ws a' ≤hb a') ∧
¬ P,E'' ⊢ a' ≤hb ?ws a' ∧
(is_volatile P al ⟶ ¬ P,E'' ⊢ a' ≤so ?ws a') ∧
(∀a''. a'' ∈ write_actions E'' ⟶ (ad, al) ∈ action_loc P E'' a'' ⟶
(P,E'' ⊢ ?ws a' ≤hb a'' ∧ P,E'' ⊢ a'' ≤hb a' ∨ is_volatile P al ∧ P,E'' ⊢ ?ws a' ≤so a'' ∧ P,E'' ⊢ a'' ≤so a')
⟶ a'' = ?ws a')"
proof(cases "a' < length E'", safe del: notI disjE conjE)
assume a'_E': "a' < length E'"
with read aobs have a': "a' ∈ read_actions (llist_of E')"
and aobs': "action_obs (llist_of E') a' = NormalAction (ReadMem ad al v)"
by(auto simp add: E''_def action_obs_def lnth_lappend1 actions_def elim: read_actions.cases intro: read_actions.intros)
have sim: "ltake (enat (length E')) (llist_of E') [≈] ltake (enat (length E')) (lappend (llist_of E') E)"
by(rule eq_into_sim_actions)(simp add: ltake_all ltake_lappend1)
from tsa have tsa': "thread_start_actions_ok (llist_of E')"
by(rule thread_start_actions_ok_prefix)(simp add: E''_def lprefix_lappend)
from is_write_seenD[OF E'' a' aobs'] a'_E'
show "?ws a' ∈ write_actions E''"
and "(ad, al) ∈ action_loc P E'' (?ws a')"
and "value_written P E'' (?ws a') (ad, al) = v"
and "¬ P,E'' ⊢ a' ≤hb ?ws a'"
and "is_volatile P al ⟹ ¬ P,E'' ⊢ a' ≤so ?ws a'"
by(auto elim!: write_actions.cases intro!: write_actions.intros simp add: E''_def lnth_lappend1 actions_def action_obs_def value_written_def enat_less_enat_plusI dest: happens_before_change_prefix[OF _ tsa' sim[symmetric]] sync_order_change_prefix[OF _ sim[symmetric]])
{ assume "length E' ≤ a'"
thus "P,E'' ⊢ ?ws a' ≤hb a'" using a'_E' by simp }
{ fix w
assume w: "w ∈ write_actions E''" "(ad, al) ∈ action_loc P E'' w"
and hbso: "P,E'' ⊢ ?ws a' ≤hb w ∧ P,E'' ⊢ w ≤hb a' ∨ is_volatile P al ∧ P,E'' ⊢ ?ws a' ≤so w ∧ P,E'' ⊢ w ≤so a'"
show "w = ?ws a'"
proof(cases "w < length E'")
case True
with is_write_seenD[OF E'' a' aobs'] a'_E' w hbso show ?thesis
by(auto 4 3 elim!: write_actions.cases intro!: write_actions.intros simp add: E''_def lnth_lappend1 actions_def action_obs_def value_written_def enat_less_enat_plusI dest: happens_before_change_prefix[OF _ tsa[unfolded E''_def] sim] happens_before_change_prefix[OF _ tsa' sim[symmetric]] sync_order_change_prefix[OF _ sim, simplified] sync_order_change_prefix[OF _ sim[symmetric], simplified] bspec[where x=w])
next
case False
from hbso have "E'' ⊢ w ≤a a'" by(auto intro: happens_before_into_action_order elim: sync_orderE)
moreover from w(1) read have "w ≠ a'" by(auto dest: read_actions_not_write_actions)
ultimately have new_w: "is_new_action (action_obs E'' w)" using False aobs a'_E'
by(cases rule: action_orderE) auto
moreover from hbso a'_E' have "E'' ⊢ ws' a' ≤a w"
by(auto intro: happens_before_into_action_order elim: sync_orderE)
hence new_a': "is_new_action (action_obs E'' (?ws a'))" using new_w a'_E'
by(cases rule: action_orderE) auto
ultimately have "w ∈ new_actions_for P E'' (ad, al)" "?ws a' ∈ new_actions_for P E'' (ad, al)"
using w is_write_seenD[OF E'' a' aobs'] a'_E'
by(auto simp add: new_actions_for_def actions_def action_obs_def lnth_lappend1 E''_def enat_less_enat_plusI elim!: write_actions.cases)
thus ?thesis by(rule new_actions_for_fun)
qed }
next
assume "¬ a' < length E'"
hence a'_E': "length E' ≤ a'" by simp
define a where "a = a' - length E'"
with a' a'_E' have a: "enat a < llength E"
by(simp add: E''_def) (metis enat_add_mono le_add_diff_inverse plus_enat_simps(1))
from a_def aobs lnth'' a'_E'
have aobs: "action_obs E a = NormalAction (ReadMem ad al v)"
and lnth: "lnth E a = (t, NormalAction (ReadMem ad al v))"
by(simp_all add: E''_def lnth_lappend2 action_obs_def)
define E''' where "E''' = lappend (llist_of E') (ltake (enat a) E)"
let ?E'' = "lappend E''' (LCons (t, NormalAction (ReadMem ad al v)) LNil)"
note hb also
have E_unfold1: "E = lappend (ltake (enat a) E) (ldropn a E)" by simp
also have E_unfold2: "ldropn a E = LCons (t, NormalAction (ReadMem ad al v)) (ldropn (Suc a) E)"
using a lnth by (metis ldropn_Suc_conv_ldropn)
finally
have "ta_hb_consistent P (E' @ list_of (ltake (enat a) E))
(LCons (t, NormalAction (ReadMem ad al v)) (ldropn (Suc a) E))"
by(rule ta_hb_consistent_lappendD2) simp
with a a'_E' a_def obtain w where w: "w ∈ write_actions ?E''"
and adal_w: "(ad, al) ∈ action_loc P ?E'' w"
and written: "value_written P ?E'' w (ad, al) = v"
and hb: "P,?E'' ⊢ w ≤hb a'"
and in_between_so:
"⋀w'. ⟦ w' ∈ write_actions ?E''; (ad, al) ∈ action_loc P ?E'' w';
is_volatile P al; P,?E'' ⊢ w ≤so w'; P,?E'' ⊢ w' ≤so a' ⟧
⟹ w' = w"
and in_between_hb:
"⋀w'. ⟦ w' ∈ write_actions ?E''; (ad, al) ∈ action_loc P ?E'' w';
P,?E'' ⊢ w ≤hb w'; P,?E'' ⊢ w' ≤hb a' ⟧
⟹ w' = w"
by(auto simp add: ta_hb_consistent_LCons length_list_of_conv_the_enat min_def lnth_ltake lappend_llist_of_llist_of[symmetric] E'''_def lappend_assoc simp del: lappend_llist_of_llist_of nth_list_of split: if_splits)
from a' a'_E' a
have eq: "ltake (enat (Suc a')) ?E'' = ltake (enat (Suc a')) E''" (is "?lhs = ?rhs")
unfolding E''_def E'''_def lappend_assoc
apply(subst (2) E_unfold1)
apply(subst E_unfold2)
apply(subst (1 2) ltake_lappend2)
apply(simp)
apply(rule arg_cong) back
apply(subst (1 2) ltake_lappend2)
apply(simp add: min_def)
apply (metis Suc_diff_le a_def le_Suc_eq order_le_less)
apply(rule arg_cong) back
apply(auto simp add: min_def a_def)
apply(auto simp add: eSuc_enat[symmetric] zero_enat_def[symmetric])
done
hence sim: "?lhs [≈] ?rhs" by(rule eq_into_sim_actions)
from tsa have tsa': "thread_start_actions_ok ?E''" unfolding E''_def E'''_def lappend_assoc
by(rule thread_start_actions_ok_prefix)(subst (2) E_unfold1, simp add: E_unfold2)
from w a a' a_def a'_E' have w_a': "w < Suc a'"
by cases(simp add: actions_def E'''_def min_def zero_enat_def eSuc_enat split: if_split_asm)
from w sim have "w ∈ write_actions E''" by(rule write_actions_change_prefix)(simp add: w_a')
moreover
from adal_w action_loc_change_prefix[OF sim, of w P] w_a'
have "(ad, al) ∈ action_loc P E'' w" by simp
moreover
from written value_written_change_prefix[OF eq, of w P] w_a'
have "value_written P E'' w (ad, al) = v" by simp
moreover
from hb tsa sim have "P,E'' ⊢ w ≤hb a'" by(rule happens_before_change_prefix)(simp_all add: w_a')
moreover {
fix w'
assume w': "w' ∈ write_actions E''"
and adal: "(ad, al) ∈ action_loc P E'' w'"
and hbso: "P,E'' ⊢ w ≤hb w' ∧ P,E'' ⊢ w' ≤hb a' ∨ is_volatile P al ∧ P,E'' ⊢ w ≤so w' ∧ P,E'' ⊢ w' ≤so a'"
(is "?hbso E''")
from hbso have ao: "E'' ⊢ w ≤a w'" "E'' ⊢ w' ≤a a'"
by(auto dest: happens_before_into_action_order elim: sync_orderE)
have "w' = w"
proof(cases "is_new_action (action_obs E'' w')")
case True
hence "w' ∈ new_actions_for P E'' (ad, al)" using w' adal by(simp add: new_actions_for_def)
moreover from ao True have "is_new_action (action_obs E'' w)" by(cases rule: action_orderE) simp_all
with ‹w ∈ write_actions E''› ‹(ad, al) ∈ action_loc P E'' w›
have "w ∈ new_actions_for P E'' (ad, al)" by(simp add: new_actions_for_def)
ultimately show "w' = w" by(rule new_actions_for_fun)
next
case False
with ao have "w' ≤ a'" by(auto elim: action_orderE)
hence w'_a: "enat w' < enat (Suc a')" by simp
with hbso w_a' have "?hbso ?E''"
by(auto 4 3 elim: happens_before_change_prefix[OF _ tsa' sim[symmetric]] sync_order_change_prefix[OF _ sim[symmetric]] del: disjCI intro: disjI1 disjI2)
moreover from w' ‹w' ≤ a'› a' a lnth a'_E' have "w' ∈ write_actions ?E''"
by(cases)(cases "w' < a'", auto intro!: write_actions.intros simp add: E'''_def actions_def action_obs_def lnth_lappend min_def zero_enat_def eSuc_enat lnth_ltake a_def E''_def not_le not_less)
moreover from adal ‹w' ≤ a'› a a' lnth w' a'_E' have "(ad, al) ∈ action_loc P ?E'' w'"
by(cases "w' < a'")(cases "w' < length E'", auto simp add: E'''_def action_obs_def lnth_lappend lappend_assoc[symmetric] min_def lnth_ltake less_trans[where y="enat a"] a_def E''_def lnth_ltake elim: write_actions.cases)
ultimately show "w' = w" by(blast dest: in_between_so in_between_hb)
qed }
ultimately have "?P a' w" using a'_E' lnth unfolding E''_def a_def by(simp add: lnth_lappend)
hence P: "?P a' (Eps (?P a'))" by(rule someI[where P="?P a'"])
from P lnth'' a'_E'
show "?ws a' ∈ write_actions E''"
and "(ad, al) ∈ action_loc P E'' (?ws a')"
and "value_written P E'' (?ws a') (ad, al) = v"
and "P,E'' ⊢ ?ws a' ≤hb a'" by simp_all
show "¬ P,E'' ⊢ a' ≤hb ?ws a'"
proof
assume "P,E'' ⊢ a' ≤hb ?ws a'"
with ‹P,E'' ⊢ ?ws a' ≤hb a'› have "a' = ?ws a'"
by(blast dest: antisymPD[OF antisym_action_order] happens_before_into_action_order)
with read ‹?ws a' ∈ write_actions E''› show False
by(auto dest: read_actions_not_write_actions)
qed
show "¬ P,E'' ⊢ a' ≤so ?ws a'"
proof
assume "P,E'' ⊢ a' ≤so ?ws a'"
hence "E'' ⊢ a' ≤a ?ws a'" by(blast elim: sync_orderE)
with ‹P,E'' ⊢ ?ws a' ≤hb a'› have "a' = ?ws a'"
by(blast dest: antisymPD[OF antisym_action_order] happens_before_into_action_order)
with read ‹?ws a' ∈ write_actions E''› show False
by(auto dest: read_actions_not_write_actions)
qed
fix a''
assume "a'' ∈ write_actions E''" "(ad, al) ∈ action_loc P E'' a''"
and "P,E'' ⊢ ?ws a' ≤hb a'' ∧ P,E'' ⊢ a'' ≤hb a' ∨
is_volatile P al ∧ P,E'' ⊢ ?ws a' ≤so a'' ∧ P,E'' ⊢ a'' ≤so a'"
thus "a'' = ?ws a'" using lnth'' P a'_E' by -(erule disjE, clarsimp+)
qed
thus "?ws a' ∈ write_actions E''"
and "(ad, al) ∈ action_loc P E'' (?ws a')"
and "value_written P E'' (?ws a') (ad, al) = v"
and "length E' ≤ a' ⟹ P,E'' ⊢ ?ws a' ≤hb a'"
and "¬ P,E'' ⊢ a' ≤hb ?ws a'"
and "is_volatile P al ⟹ ¬ P,E'' ⊢ a' ≤so ?ws a'"
and "⋀a''. ⟦ a'' ∈ write_actions E''; (ad, al) ∈ action_loc P E'' a''; P,E'' ⊢ ?ws a' ≤hb a''; P,E'' ⊢ a'' ≤hb a' ⟧ ⟹ a'' = ?ws a'"
and "⋀a''. ⟦ a'' ∈ write_actions E''; (ad, al) ∈ action_loc P E'' a''; is_volatile P al; P,E'' ⊢ ?ws a' ≤so a''; P,E'' ⊢ a'' ≤so a' ⟧ ⟹ a'' = ?ws a'"
by blast+
qed(assumption|rule tsa)+
thus "P ⊢ (E'', ?ws) √"
and "⋀n. ⟦ n ∈ read_actions E''; length E' ≤ n ⟧ ⟹ P,E'' ⊢ ?ws n ≤hb n"
by(blast elim: read_actions.cases intro: read_actions.intros)+
fix n
assume "n < length E'"
thus "?ws n = ws' n" by simp
qed
lemma ta_hb_consistent_not_ReadI:
"(⋀t ad al v. (t, NormalAction (ReadMem ad al v)) ∉ lset E) ⟹ ta_hb_consistent P E' E"
proof(coinduction arbitrary: E' E)
case (ta_hb_consistent E' E)
thus ?case by(cases E)(auto split: action.split obs_event.split, blast)
qed
context jmm_multithreaded begin
definition complete_hb :: "('l,'thread_id,'x,'m,'w) state ⇒ ('thread_id × ('addr, 'thread_id) obs_event action) list
⇒ ('thread_id × ('l, 'thread_id, 'x, 'm, 'w, ('addr, 'thread_id) obs_event action) thread_action) llist"
where
"complete_hb s E = unfold_llist
(λ(s, E). ∀t ta s'. ¬ s -t▹ta→ s')
(λ(s, E). fst (SOME ((t, ta), s'). s -t▹ta→ s' ∧ ta_hb_consistent P E (llist_of (map (Pair t) ⦃ta⦄⇘o⇙))))
(λ(s, E). let ((t, ta), s') = SOME ((t, ta), s'). s -t▹ta→ s' ∧ ta_hb_consistent P E (llist_of (map (Pair t) ⦃ta⦄⇘o⇙))
in (s', E @ map (Pair t) ⦃ta⦄⇘o⇙))
(s, E)"
definition hb_completion ::
"('l, 'thread_id, 'x, 'm, 'w) state ⇒ ('thread_id × ('addr, 'thread_id) obs_event action) list ⇒ bool"
where
"hb_completion s E ⟷
(∀ttas s' t x ta x' m' i.
s -▹ttas→* s' ⟶
non_speculative P (w_values P (λ_. {}) (map snd E)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) ⟶
thr s' t = ⌊(x, no_wait_locks)⌋ ⟶ t ⊢ (x, shr s') -ta→ (x', m') ⟶ actions_ok s' t ta ⟶
non_speculative P (w_values P (w_values P (λ_. {}) (map snd E)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙)) ⟶
(∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧
ta_hb_consistent P
(E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas) @ map (Pair t) (take i ⦃ta⦄⇘o⇙))
(llist_of (map (Pair t) (drop i ⦃ta'⦄⇘o⇙))) ∧
(i < length ⦃ta⦄⇘o⇙ ⟶ i < length ⦃ta'⦄⇘o⇙) ∧
(if ∃ad al v. ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta⦄⇘o⇙ ! i) (⦃ta'⦄⇘o⇙ ! i)))"
lemma hb_completionD:
"⟦ hb_completion s E; s -▹ttas→* s';
non_speculative P (w_values P (λ_. {}) (map snd E)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)));
thr s' t = ⌊(x, no_wait_locks)⌋; t ⊢ (x, shr s') -ta→ (x', m'); actions_ok s' t ta;
non_speculative P (w_values P (w_values P (λ_. {}) (map snd E)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙)) ⟧
⟹ ∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧
ta_hb_consistent P (E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas) @ map (Pair t) (take i ⦃ta⦄⇘o⇙))
(llist_of (map (Pair t) (drop i ⦃ta'⦄⇘o⇙))) ∧
(i < length ⦃ta⦄⇘o⇙ ⟶ i < length ⦃ta'⦄⇘o⇙) ∧
(if ∃ad al v. ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta⦄⇘o⇙ ! i) (⦃ta'⦄⇘o⇙ ! i)"
unfolding hb_completion_def by blast
lemma hb_completionI [intro?]:
"(⋀ttas s' t x ta x' m' i.
⟦ s -▹ttas→* s'; non_speculative P (w_values P (λ_. {}) (map snd E)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)));
thr s' t = ⌊(x, no_wait_locks)⌋; t ⊢ (x, shr s') -ta→ (x', m'); actions_ok s' t ta;
non_speculative P (w_values P (w_values P (λ_. {}) (map snd E)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙)) ⟧
⟹ ∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧ take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧
ta_hb_consistent P (E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas) @ map (Pair t) (take i ⦃ta⦄⇘o⇙)) (llist_of (map (Pair t) (drop i ⦃ta'⦄⇘o⇙))) ∧
(i < length ⦃ta⦄⇘o⇙ ⟶ i < length ⦃ta'⦄⇘o⇙) ∧
(if ∃ad al v. ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta⦄⇘o⇙ ! i) (⦃ta'⦄⇘o⇙ ! i))
⟹ hb_completion s E"
unfolding hb_completion_def by blast
lemma hb_completion_shift:
assumes hb_c: "hb_completion s E"
and τRed: "s -▹ttas→* s'"
and sc: "non_speculative P (w_values P (λ_. {}) (map snd E)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
(is "non_speculative _ ?vs _")
shows "hb_completion s' (E @ (concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas)))"
(is "hb_completion _ ?E")
proof(rule hb_completionI)
fix ttas' s'' t x ta x' m' i
assume τRed': "s' -▹ttas'→* s''"
and sc': "non_speculative P (w_values P (λ_. {}) (map snd ?E)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')))"
and red: "thr s'' t = ⌊(x, no_wait_locks)⌋" "t ⊢ ⟨x, shr s''⟩ -ta→ ⟨x', m'⟩" "actions_ok s'' t ta"
and ns: "non_speculative P (w_values P (w_values P (λ_. {}) (map snd ?E)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) (llist_of (take i ⦃ta⦄⇘o⇙))"
from τRed τRed' have "s -▹ttas @ ttas'→* s''" unfolding RedT_def by(rule rtrancl3p_trans)
moreover from sc sc' have "non_speculative P ?vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (ttas @ ttas'))))"
unfolding map_append concat_append lappend_llist_of_llist_of[symmetric] map_concat
by(simp add: non_speculative_lappend o_def split_def del: lappend_llist_of_llist_of)
ultimately
show "∃ta' x'' m''. t ⊢ ⟨x, shr s''⟩ -ta'→ ⟨x'', m''⟩ ∧ actions_ok s'' t ta' ∧ take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧
ta_hb_consistent P (?E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas') @ map (Pair t) (take i ⦃ta⦄⇘o⇙))
(llist_of (map (Pair t) (drop i ⦃ta'⦄⇘o⇙))) ∧
(i < length ⦃ta⦄⇘o⇙ ⟶ i < length ⦃ta'⦄⇘o⇙) ∧
(if ∃ad al v. ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta⦄⇘o⇙ ! i) (⦃ta'⦄⇘o⇙ ! i)"
using red ns unfolding append_assoc
apply(subst (2) append_assoc[symmetric])
unfolding concat_append[symmetric] map_append[symmetric] foldr_append[symmetric]
by(rule hb_completionD[OF hb_c])(simp_all add: map_concat o_def split_def)
qed
lemma hb_completion_shift1:
assumes hb_c: "hb_completion s E"
and Red: "s -t▹ta→ s'"
and sc: "non_speculative P (w_values P (λ_. {}) (map snd E)) (llist_of ⦃ta⦄⇘o⇙)"
shows "hb_completion s' (E @ map (Pair t) ⦃ta⦄⇘o⇙)"
using hb_completion_shift[OF hb_c, of "[(t, ta)]" s'] Red sc
by(simp add: RedT_def rtrancl3p_Cons rtrancl3p_Nil del: split_paired_Ex)
lemma complete_hb_in_Runs:
assumes hb_c: "hb_completion s E"
and ta_hb_consistent_convert_RA: "⋀t E ln. ta_hb_consistent P E (llist_of (map (Pair t) (convert_RA ln)))"
shows "mthr.Runs s (complete_hb s E)"
using hb_c
proof(coinduction arbitrary: s E)
case (Runs s E)
let ?P = "λ((t, ta), s'). s -t▹ta→ s' ∧ ta_hb_consistent P E (llist_of (map (Pair t) ⦃ta⦄⇘o⇙))"
show ?case
proof(cases "∃t ta s'. s -t▹ta→ s'")
case False
then have ?Stuck by(simp add: complete_hb_def)
thus ?thesis ..
next
case True
let ?t = "fst (fst (Eps ?P))" and ?ta = "snd (fst (Eps ?P))" and ?s' = "snd (Eps ?P)"
from True obtain t ta s' where red: "s -t▹ta→ s'" by blast
hence "∃x. ?P x"
proof(cases)
case (redT_normal x x' m')
from hb_completionD[OF Runs _ _ ‹thr s t = ⌊(x, no_wait_locks)⌋› ‹t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩› ‹actions_ok s t ta›, of "[]" 0]
obtain ta' x'' m'' where "t ⊢ ⟨x, shr s⟩ -ta'→ ⟨x'', m''⟩"
and "actions_ok s t ta'" "ta_hb_consistent P E (llist_of (map (Pair t) ⦃ta'⦄⇘o⇙))"
by fastforce
moreover obtain ws' where "redT_updWs t (wset s) ⦃ta'⦄⇘w⇙ ws'" by (metis redT_updWs_total)
ultimately show ?thesis using ‹thr s t = ⌊(x, no_wait_locks)⌋›
by(cases ta')(auto intro!: exI redT.redT_normal)
next
case (redT_acquire x n ln)
thus ?thesis using ta_hb_consistent_convert_RA[of E t ln]
by(auto intro!: exI redT.redT_acquire)
qed
hence "?P (Eps ?P)" by(rule someI_ex)
hence red: "s -?t▹?ta→ ?s'"
and hb: "ta_hb_consistent P E (llist_of (map (Pair ?t) ⦃?ta⦄⇘o⇙))"
by(simp_all add: split_beta)
moreover
from ta_hb_consistent_into_non_speculative[OF hb]
have "non_speculative P (w_values P (λ_. {}) (map snd E)) (llist_of ⦃?ta⦄⇘o⇙)" by(simp add: o_def)
with Runs red have "hb_completion ?s' (E @ map (Pair ?t) ⦃?ta⦄⇘o⇙)" by(rule hb_completion_shift1)
ultimately have ?Step using True
unfolding complete_hb_def by(fastforce simp del: split_paired_Ex simp add: split_def)
thus ?thesis ..
qed
qed
lemma complete_hb_ta_hb_consistent:
assumes "hb_completion s E"
and ta_hb_consistent_convert_RA: "⋀E t ln. ta_hb_consistent P E (llist_of (map (Pair t) (convert_RA ln)))"
shows "ta_hb_consistent P E (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (complete_hb s E)))"
(is "ta_hb_consistent _ _ (?obs (complete_hb s E))")
proof -
define obs a where "obs = ?obs (complete_hb s E)" and "a = complete_hb s E"
with ‹hb_completion s E› have "∃s. hb_completion s E ∧ obs = ?obs (complete_hb s E) ∧ a = complete_hb s E" by blast
moreover have "wf (inv_image {(m, n). m < n} (llength ∘ ltakeWhile (λ(t, ta). ⦃ta⦄⇘o⇙ = [])))"
(is "wf ?R") by(rule wf_inv_image)(rule wellorder_class.wf)
ultimately show "ta_hb_consistent P E obs"
proof(coinduct E obs a rule: ta_hb_consistent_coinduct_append_wf)
case (ta_hb_consistent E obs a)
then obtain s where hb_c: "hb_completion s E"
and obs: "obs = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (complete_hb s E))"
and a: "a = complete_hb s E"
by blast
let ?P = "λ((t, ta), s'). s -t▹ta→ s' ∧ ta_hb_consistent P E (llist_of (map (Pair t) ⦃ta⦄⇘o⇙))"
show ?case
proof(cases "∃t ta s'. s -t▹ta→ s'")
case False
with obs have ?LNil by(simp add: complete_hb_def)
thus ?thesis ..
next
case True
let ?t = "fst (fst (Eps ?P))" and ?ta = "snd (fst (Eps ?P))" and ?s' = "snd (Eps ?P)"
from True obtain t ta s' where red: "s -t▹ta→ s'" by blast
hence "∃x. ?P x"
proof(cases)
case (redT_normal x x' m')
from hb_completionD[OF hb_c _ _ ‹thr s t = ⌊(x, no_wait_locks)⌋› ‹t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩› ‹actions_ok s t ta›, of "[]" 0]
obtain ta' x'' m'' where "t ⊢ ⟨x, shr s⟩ -ta'→ ⟨x'', m''⟩"
and "actions_ok s t ta'" "ta_hb_consistent P E (llist_of (map (Pair t) ⦃ta'⦄⇘o⇙))"
by fastforce
moreover obtain ws' where "redT_updWs t (wset s) ⦃ta'⦄⇘w⇙ ws'" by (metis redT_updWs_total)
ultimately show ?thesis using ‹thr s t = ⌊(x, no_wait_locks)⌋›
by(cases ta')(auto intro!: exI redT.redT_normal)
next
case (redT_acquire x n ln)
thus ?thesis using ta_hb_consistent_convert_RA[of E t ln]
by(auto intro!: exI redT.redT_acquire)
qed
hence "?P (Eps ?P)" by(rule someI_ex)
hence red': "s -?t▹?ta→ ?s'"
and hb: "ta_hb_consistent P E (llist_of (map (Pair ?t) ⦃?ta⦄⇘o⇙))"
by(simp_all add: split_beta)
moreover
from ta_hb_consistent_into_non_speculative[OF hb]
have "non_speculative P (w_values P (λ_. {}) (map snd E)) (llist_of ⦃?ta⦄⇘o⇙)" by(simp add: o_def)
with hb_c red' have hb_c': "hb_completion ?s' (E @ map (Pair ?t) ⦃?ta⦄⇘o⇙)"
by(rule hb_completion_shift1)
show ?thesis
proof(cases "lnull obs")
case True thus ?thesis unfolding lnull_def by simp
next
case False
have eq: "(∀t ta s'. ¬ s -t▹ta→ s') = False" using True by auto
{ assume "⦃?ta⦄⇘o⇙ = []"
moreover from obs False
have "lfinite (ltakeWhile (λ(t, ta). ⦃ta⦄⇘o⇙ = []) (complete_hb s E))"
unfolding lfinite_ltakeWhile by(fastforce simp add: split_def lconcat_eq_LNil)
ultimately have "(complete_hb ?s' (E @ map (Pair ?t) ⦃?ta⦄⇘o⇙), a) ∈ ?R"
using red unfolding a complete_hb_def
apply(subst (2) unfold_llist.code)
apply(subst (asm) unfold_llist.code)
apply(auto simp add: split_beta simp del: split_paired_Ex split_paired_All split: if_split_asm)
apply(auto simp add: lfinite_eq_range_llist_of)
done }
hence ?lappend using red hb hb_c' unfolding obs complete_hb_def
apply(subst unfold_llist.code)
apply(simp add: split_beta eq del: split_paired_Ex split_paired_All split del: if_split)
apply(intro exI conjI impI refl disjI1|rule refl|assumption|simp_all add: llist_of_eq_LNil_conv)+
done
thus ?thesis ..
qed
qed
qed
qed
lemma hb_completion_Runs:
assumes "hb_completion s E"
and "⋀E t ln. ta_hb_consistent P E (llist_of (map (Pair t) (convert_RA ln)))"
shows "∃ttas. mthr.Runs s ttas ∧ ta_hb_consistent P E (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas))"
using complete_hb_in_Runs[OF assms] complete_hb_ta_hb_consistent[OF assms]
by blast
end
end