Theory SC_Completion
section ‹Sequentially consistent completion of executions in the JMM›
theory SC_Completion
imports
Non_Speculative
begin
subsection ‹Most recently written values›
fun mrw_value ::
"'m prog ⇒ (('addr × addr_loc) ⇀ ('addr val × bool)) ⇒ ('addr, 'thread_id) obs_event action
⇒ (('addr × addr_loc) ⇀ ('addr val × bool))"
where
"mrw_value P vs (NormalAction (WriteMem ad al v)) = vs((ad, al) ↦ (v, True))"
| "mrw_value P vs (NormalAction (NewHeapElem ad hT)) =
(λ(ad', al). if ad = ad' ∧ al ∈ addr_locs P hT ∧ (case vs (ad, al) of None ⇒ True | Some (v, b) ⇒ ¬ b)
then Some (addr_loc_default P hT al, False)
else vs (ad', al))"
| "mrw_value P vs _ = vs"
lemma mrw_value_cases:
obtains ad al v where "x = NormalAction (WriteMem ad al v)"
| ad hT where "x = NormalAction (NewHeapElem ad hT)"
| ad M vs v where "x = NormalAction (ExternalCall ad M vs v)"
| ad al v where "x = NormalAction (ReadMem ad al v)"
| t where "x = NormalAction (ThreadStart t)"
| t where "x = NormalAction (ThreadJoin t)"
| ad where "x = NormalAction (SyncLock ad)"
| ad where "x = NormalAction (SyncUnlock ad)"
| t where "x = NormalAction (ObsInterrupt t)"
| t where "x = NormalAction (ObsInterrupted t)"
| "x = InitialThreadAction"
| "x = ThreadFinishAction"
by pat_completeness
abbreviation mrw_values ::
"'m prog ⇒ (('addr × addr_loc) ⇀ ('addr val × bool)) ⇒ ('addr, 'thread_id) obs_event action list
⇒ (('addr × addr_loc) ⇀ ('addr val × bool))"
where "mrw_values P ≡ foldl (mrw_value P)"
lemma mrw_values_eq_SomeD:
assumes mrw: "mrw_values P vs0 obs (ad, al) = ⌊(v, b)⌋"
and "vs0 (ad, al) = ⌊(v, b)⌋ ⟹ ∃wa. wa ∈ set obs ∧ is_write_action wa ∧ (ad, al) ∈ action_loc_aux P wa ∧ (b ⟶ ¬ is_new_action wa)"
shows "∃obs' wa obs''. obs = obs' @ wa # obs'' ∧ is_write_action wa ∧ (ad, al) ∈ action_loc_aux P wa ∧
value_written_aux P wa al = v ∧ (is_new_action wa ⟷ ¬ b) ∧
(∀ob∈set obs''. is_write_action ob ⟶ (ad, al) ∈ action_loc_aux P ob ⟶ is_new_action ob ∧ b)"
(is "?concl obs")
using assms
proof(induct obs rule: rev_induct)
case Nil thus ?case by simp
next
case (snoc ob obs)
note mrw = ‹mrw_values P vs0 (obs @ [ob]) (ad, al) = ⌊(v, b)⌋›
show ?case
proof(cases "is_write_action ob ∧ (ad, al) ∈ action_loc_aux P ob ∧ (is_new_action ob ⟶ ¬ b)")
case True thus ?thesis using mrw
by(fastforce elim!: is_write_action.cases intro: action_loc_aux_intros split: if_split_asm)
next
case False
with mrw have "mrw_values P vs0 obs (ad, al) = ⌊(v, b)⌋"
by(cases "ob" rule: mrw_value_cases)(auto split: if_split_asm simp add: addr_locs_def split: htype.split_asm)
moreover
{ assume "vs0 (ad, al) = ⌊(v, b)⌋"
hence "∃wa. wa ∈ set (obs @ [ob]) ∧ is_write_action wa ∧ (ad, al) ∈ action_loc_aux P wa ∧ (b ⟶ ¬ is_new_action wa)"
by(rule snoc)
with False have "∃wa. wa ∈ set obs ∧ is_write_action wa ∧ (ad, al) ∈ action_loc_aux P wa ∧ (b ⟶ ¬ is_new_action wa)"
by auto }
ultimately have "?concl obs" by(rule snoc)
thus ?thesis using False mrw by fastforce
qed
qed
lemma mrw_values_WriteMemD:
assumes "NormalAction (WriteMem ad al v') ∈ set obs"
shows "∃v. mrw_values P vs0 obs (ad, al) = Some (v, True)"
using assms
apply(induct obs rule: rev_induct)
apply simp
apply clarsimp
apply(erule disjE)
apply clarsimp
apply clarsimp
apply(case_tac x rule: mrw_value_cases)
apply simp_all
done
lemma mrw_values_new_actionD:
assumes "w ∈ set obs" "is_new_action w" "adal ∈ action_loc_aux P w"
shows "∃v b. mrw_values P vs0 obs adal = Some (v, b)"
using assms
apply(induct obs rule: rev_induct)
apply simp
apply clarsimp
apply(erule disjE)
apply(fastforce simp add: split_beta elim!: action_loc_aux_cases is_new_action.cases)
apply clarsimp
apply(rename_tac w' obs' v b)
apply(case_tac w' rule: mrw_value_cases)
apply(auto simp add: split_beta)
done
lemma mrw_value_dom_mono:
"dom vs ⊆ dom (mrw_value P vs ob)"
by(cases ob rule: mrw_value_cases) auto
lemma mrw_values_dom_mono:
"dom vs ⊆ dom (mrw_values P vs obs)"
by(induct obs arbitrary: vs)(auto intro: subset_trans[OF mrw_value_dom_mono] del: subsetI)
lemma mrw_values_eq_NoneD:
assumes "mrw_values P vs0 obs adal = None"
and "w ∈ set obs" and "is_write_action w" and "adal ∈ action_loc_aux P w"
shows False
using assms
apply -
apply(erule is_write_action.cases)
apply(fastforce dest: mrw_values_WriteMemD[where ?vs0.0=vs0 and P=P] mrw_values_new_actionD[where ?vs0.0=vs0] elim: action_loc_aux_cases)+
done
lemma mrw_values_mrw:
assumes mrw: "mrw_values P vs0 (map snd obs) (ad, al) = ⌊(v, b)⌋"
and initial: "vs0 (ad, al) = ⌊(v, b)⌋ ⟹ ∃wa. wa ∈ set (map snd obs) ∧ is_write_action wa ∧ (ad, al) ∈ action_loc_aux P wa ∧ (b ⟶ ¬ is_new_action wa)"
shows "∃i. i < length obs ∧ P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) ⊢ length obs ↝mrw i ∧ value_written P (llist_of obs) i (ad, al) = v"
proof -
from mrw_values_eq_SomeD[OF mrw initial]
obtain obs' wa obs'' where obs: "map snd obs = obs' @ wa # obs''"
and wa: "is_write_action wa"
and adal: "(ad, al) ∈ action_loc_aux P wa"
and written: "value_written_aux P wa al = v"
and new: "is_new_action wa ⟷ ¬ b"
and last: "⋀ob. ⟦ ob ∈ set obs''; is_write_action ob; (ad, al) ∈ action_loc_aux P ob ⟧ ⟹ is_new_action ob ∧ b"
by blast
let ?i = "length obs'"
let ?E = "llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])"
from obs have len: "length (map snd obs) = Suc (length obs') + length obs''" by simp
hence "?i < length obs" by simp
moreover
hence obs_i: "action_obs ?E ?i = wa" using len obs
by(auto simp add: action_obs_def map_eq_append_conv)
have "P,?E ⊢ length obs ↝mrw ?i"
proof(rule most_recent_write_for.intros)
show "length obs ∈ read_actions ?E"
by(auto intro: read_actions.intros simp add: actions_def action_obs_def)
show "(ad, al) ∈ action_loc P ?E (length obs)"
by(simp add: action_obs_def lnth_llist_of)
show "?E ⊢ length obs' ≤a length obs" using len
by-(rule action_orderI, auto simp add: actions_def action_obs_def nth_append)
show "?i ∈ write_actions ?E" using len obs wa
by-(rule write_actions.intros, auto simp add: actions_def action_obs_def nth_append map_eq_append_conv)
show "(ad, al) ∈ action_loc P ?E ?i" using obs_i adal by simp
fix wa'
assume wa': "wa' ∈ write_actions ?E"
and adal': "(ad, al) ∈ action_loc P ?E wa'"
from wa' ‹?i ∈ write_actions ?E›
have "wa' ∈ actions ?E" "?i ∈ actions ?E" by simp_all
hence "?E ⊢ wa' ≤a ?i"
proof(rule action_orderI)
assume new_wa': "is_new_action (action_obs ?E wa')"
and new_i: "is_new_action (action_obs ?E ?i)"
from new_i obs_i new have b: "¬ b" by simp
show "wa' ≤ ?i"
proof(rule ccontr)
assume "¬ ?thesis"
hence "?i < wa'" by simp
hence "snd (obs ! wa') ∈ set obs''" using obs wa' unfolding in_set_conv_nth
by -(rule exI[where x="wa' - Suc (length obs')"], auto elim!: write_actions.cases actionsE simp add: action_obs_def lnth_llist_of actions_def nth_append map_eq_append_conv nth_Cons' split: if_split_asm)
moreover from wa' have "is_write_action (snd (obs ! wa'))"
by cases(auto simp add: action_obs_def nth_append actions_def split: if_split_asm)
moreover from adal' wa' have "(ad, al) ∈ action_loc_aux P (snd (obs ! wa'))"
by(auto simp add: action_obs_def nth_append nth_Cons' actions_def split: if_split_asm elim!: write_actions.cases)
ultimately show False using last[of "snd (obs ! wa')"] b by simp
qed
next
assume new_wa': "¬ is_new_action (action_obs ?E wa')"
with wa' adal' obtain v' where "NormalAction (WriteMem ad al v') ∈ set (map snd obs)"
unfolding in_set_conv_nth
by (fastforce elim!: write_actions.cases is_write_action.cases simp add: action_obs_def actions_def nth_append split: if_split_asm intro!: exI[where x=wa'])
from mrw_values_WriteMemD[OF this, of P vs0] mrw have b by simp
with new obs_i have "¬ is_new_action (action_obs ?E ?i)" by simp
moreover
have "wa' ≤ ?i"
proof(rule ccontr)
assume "¬ ?thesis"
hence "?i < wa'" by simp
hence "snd (obs ! wa') ∈ set obs''" using obs wa' unfolding in_set_conv_nth
by -(rule exI[where x="wa' - Suc (length obs')"], auto elim!: write_actions.cases actionsE simp add: action_obs_def lnth_llist_of actions_def nth_append map_eq_append_conv nth_Cons' split: if_split_asm)
moreover from wa' have "is_write_action (snd (obs ! wa'))"
by cases(auto simp add: action_obs_def nth_append actions_def split: if_split_asm)
moreover from adal' wa' have "(ad, al) ∈ action_loc_aux P (snd (obs ! wa'))"
by(auto simp add: action_obs_def nth_append nth_Cons' actions_def split: if_split_asm elim!: write_actions.cases)
ultimately have "is_new_action (snd (obs ! wa'))" using last[of "snd (obs ! wa')"] by simp
moreover from new_wa' wa' have "¬ is_new_action (snd (obs ! wa'))"
by(auto elim!: write_actions.cases simp add: action_obs_def nth_append actions_def split: if_split_asm)
ultimately show False by contradiction
qed
ultimately
show "¬ is_new_action (action_obs ?E ?i) ∧ wa' ≤ ?i" by blast
qed
thus "?E ⊢ wa' ≤a ?i ∨ ?E ⊢ length obs ≤a wa'" ..
qed
moreover from written ‹?i < length obs› obs_i
have "value_written P (llist_of obs) ?i (ad, al) = v"
by(simp add: value_written_def action_obs_def nth_append)
ultimately show ?thesis by blast
qed
lemma mrw_values_no_write_unchanged:
assumes no_write: "⋀w. ⟦ w ∈ set obs; is_write_action w; adal ∈ action_loc_aux P w ⟧
⟹ case vs adal of None ⇒ False | Some (v, b) ⇒ b ∧ is_new_action w"
shows "mrw_values P vs obs adal = vs adal"
using assms
proof(induct obs arbitrary: vs)
case Nil show ?case by simp
next
case (Cons ob obs)
from Cons.prems[of ob]
have "mrw_value P vs ob adal = vs adal"
apply(cases adal)
apply(cases ob rule: mrw_value_cases, fastforce+)
apply(auto simp add: addr_locs_def split: htype.split_asm)
apply blast+
done
moreover
have "mrw_values P (mrw_value P vs ob) obs adal = mrw_value P vs ob adal"
proof(rule Cons.hyps)
fix w
assume "w ∈ set obs" "is_write_action w" "adal ∈ action_loc_aux P w"
with Cons.prems[of w] ‹mrw_value P vs ob adal = vs adal›
show "case mrw_value P vs ob adal of None ⇒ False | ⌊(v, b)⌋ ⇒ b ∧ is_new_action w" by simp
qed
ultimately show ?case by simp
qed
subsection ‹Coinductive version of sequentially consistent prefixes›
coinductive ta_seq_consist ::
"'m prog ⇒ ('addr × addr_loc ⇀ 'addr val × bool) ⇒ ('addr, 'thread_id) obs_event action llist ⇒ bool"
for P :: "'m prog"
where
LNil: "ta_seq_consist P vs LNil"
| LCons:
"⟦ case ob of NormalAction (ReadMem ad al v) ⇒ ∃b. vs (ad, al) = ⌊(v, b)⌋ | _ ⇒ True;
ta_seq_consist P (mrw_value P vs ob) obs ⟧
⟹ ta_seq_consist P vs (LCons ob obs)"
inductive_simps ta_seq_consist_simps [simp]:
"ta_seq_consist P vs LNil"
"ta_seq_consist P vs (LCons ob obs)"
lemma ta_seq_consist_lappend:
assumes "lfinite obs"
shows "ta_seq_consist P vs (lappend obs obs') ⟷
ta_seq_consist P vs obs ∧ ta_seq_consist P (mrw_values P vs (list_of obs)) obs'"
(is "?concl vs obs")
using assms
proof(induct arbitrary: vs)
case lfinite_LNil thus ?case by simp
next
case (lfinite_LConsI obs ob)
have "?concl (mrw_value P vs ob) obs" by fact
thus ?case using ‹lfinite obs› by(simp split: action.split add: list_of_LCons)
qed
lemma
assumes "ta_seq_consist P vs obs"
shows ta_seq_consist_ltake: "ta_seq_consist P vs (ltake n obs)" (is ?thesis1)
and ta_seq_consist_ldrop: "ta_seq_consist P (mrw_values P vs (list_of (ltake n obs))) (ldrop n obs)" (is ?thesis2)
proof -
note assms
also have "obs = lappend (ltake n obs) (ldrop n obs)" by(simp add: lappend_ltake_ldrop)
finally have "?thesis1 ∧ ?thesis2"
by(cases n)(simp_all add: ta_seq_consist_lappend del: lappend_ltake_enat_ldropn)
thus ?thesis1 ?thesis2 by blast+
qed
lemma ta_seq_consist_coinduct_append [consumes 1, case_names ta_seq_consist, case_conclusion ta_seq_consist LNil lappend]:
assumes major: "X vs obs"
and step: "⋀vs obs. X vs obs
⟹ obs = LNil ∨
(∃obs' obs''. obs = lappend obs' obs'' ∧ obs' ≠ LNil ∧ ta_seq_consist P vs obs' ∧
(lfinite obs' ⟶ (X (mrw_values P vs (list_of obs')) obs'' ∨
ta_seq_consist P (mrw_values P vs (list_of obs')) obs'')))"
(is "⋀vs obs. _ ⟹ _ ∨ ?step vs obs")
shows "ta_seq_consist P vs obs"
proof -
from major
have "∃obs' obs''. obs = lappend (llist_of obs') obs'' ∧ ta_seq_consist P vs (llist_of obs') ∧
X (mrw_values P vs obs') obs''"
by(auto intro: exI[where x="[]"])
thus ?thesis
proof(coinduct)
case (ta_seq_consist vs obs)
then obtain obs' obs''
where obs: "obs = lappend (llist_of obs') obs''"
and sc_obs': "ta_seq_consist P vs (llist_of obs')"
and X: "X (mrw_values P vs obs') obs''" by blast
show ?case
proof(cases obs')
case Nil
with X have "X vs obs''" by simp
from step[OF this] show ?thesis
proof
assume "obs'' = LNil"
with Nil obs show ?thesis by simp
next
assume "?step vs obs''"
then obtain obs''' obs''''
where obs'': "obs'' = lappend obs''' obs''''" and "obs''' ≠ LNil"
and sc_obs''': "ta_seq_consist P vs obs'''"
and fin: "lfinite obs''' ⟹ X (mrw_values P vs (list_of obs''')) obs'''' ∨
ta_seq_consist P (mrw_values P vs (list_of obs''')) obs''''"
by blast
from ‹obs''' ≠ LNil› obtain ob obs''''' where obs''': "obs''' = LCons ob obs'''''"
unfolding neq_LNil_conv by blast
with Nil obs'' obs have concl1: "obs = LCons ob (lappend obs''''' obs'''')" by simp
have concl2: "case ob of NormalAction (ReadMem ad al v) ⇒ ∃b. vs (ad, al) = ⌊(v, b)⌋ | _ ⇒ True"
using sc_obs''' obs''' by simp
show ?thesis
proof(cases "lfinite obs'''")
case False
hence "lappend obs''''' obs'''' = obs'''''" using obs''' by(simp add: lappend_inf)
hence "ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')"
using sc_obs''' obs''' by simp
with concl1 concl2 have ?LCons by blast
thus ?thesis by simp
next
case True
with obs''' obtain obs'''''' where obs''''': "obs''''' = llist_of obs''''''"
by simp(auto simp add: lfinite_eq_range_llist_of)
from fin[OF True] have "?LCons"
proof
assume X: "X (mrw_values P vs (list_of obs''')) obs''''"
hence "X (mrw_values P (mrw_value P vs ob) obs'''''') obs''''"
using obs''''' obs''' by simp
moreover from obs'''''
have "lappend obs''''' obs'''' = lappend (llist_of obs'''''') obs''''" by simp
moreover have "ta_seq_consist P (mrw_value P vs ob) (llist_of obs'''''')"
using sc_obs''' obs''' obs''''' by simp
ultimately show ?thesis using concl1 concl2 by blast
next
assume "ta_seq_consist P (mrw_values P vs (list_of obs''')) obs''''"
with sc_obs''' obs''''' obs'''
have "ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')"
by(simp add: ta_seq_consist_lappend)
with concl1 concl2 show ?thesis by blast
qed
thus ?thesis by simp
qed
qed
next
case (Cons ob obs''')
hence "obs = LCons ob (lappend (llist_of obs''') obs'')"
using obs by simp
moreover from sc_obs' Cons
have "case ob of NormalAction (ReadMem ad al v) ⇒ ∃b. vs (ad, al) = ⌊(v, b)⌋ | _ ⇒ True"
and "ta_seq_consist P (mrw_value P vs ob) (llist_of obs''')" by simp_all
moreover from X Cons have "X (mrw_values P (mrw_value P vs ob) obs''') obs''" by simp
ultimately show ?thesis by blast
qed
qed
qed
lemma ta_seq_consist_coinduct_append_wf
[consumes 2, case_names ta_seq_consist, case_conclusion ta_seq_consist LNil lappend]:
assumes major: "X vs obs a"
and wf: "wf R"
and step: "⋀vs obs a. X vs obs a
⟹ obs = LNil ∨
(∃obs' obs'' a'. obs = lappend obs' obs'' ∧ ta_seq_consist P vs obs' ∧ (obs' = LNil ⟶ (a', a) ∈ R) ∧
(lfinite obs' ⟶ X (mrw_values P vs (list_of obs')) obs'' a' ∨
ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))"
(is "⋀vs obs a. _ ⟹ _ ∨ ?step vs obs a")
shows "ta_seq_consist P vs obs"
proof -
{ fix vs obs a
assume "X vs obs a"
with wf
have "obs = LNil ∨ (∃obs' obs''. obs = lappend obs' obs'' ∧ obs' ≠ LNil ∧ ta_seq_consist P vs obs' ∧
(lfinite obs' ⟶ (∃a. X (mrw_values P vs (list_of obs')) obs'' a) ∨
ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))"
(is "_ ∨ ?step_concl vs obs")
proof(induct a arbitrary: vs obs rule: wf_induct[consumes 1, case_names wf])
case (wf a)
note IH = wf.hyps[rule_format]
from step[OF ‹X vs obs a›]
show ?case
proof
assume "obs = LNil" thus ?thesis ..
next
assume "?step vs obs a"
then obtain obs' obs'' a'
where obs: "obs = lappend obs' obs''"
and sc_obs': "ta_seq_consist P vs obs'"
and decr: "obs' = LNil ⟹ (a', a) ∈ R"
and fin: "lfinite obs' ⟹
X (mrw_values P vs (list_of obs')) obs'' a' ∨
ta_seq_consist P (mrw_values P vs (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 (mrw_values P vs (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 (mrw_values P vs (list_of obs')) obs''"
hence "?step_concl vs obs" using True obs by simp
thus ?thesis ..
qed
next
assume "ta_seq_consist P (mrw_values P vs (list_of obs')) obs''"
thus ?thesis using obs True
by cases(auto cong: action.case_cong obs_event.case_cong intro: exI[where x="LCons x LNil" for x])
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: vs obs a rule: ta_seq_consist_coinduct_append)
case (ta_seq_consist vs obs a)
thus ?case by simp(rule step')
qed
qed
lemma ta_seq_consist_nthI:
"(⋀i ad al v. ⟦ enat i < llength obs; lnth obs i = NormalAction (ReadMem ad al v);
ta_seq_consist P vs (ltake (enat i) obs) ⟧
⟹ ∃b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = ⌊(v, b)⌋)
⟹ ta_seq_consist P vs obs"
proof(coinduction arbitrary: vs obs)
case (ta_seq_consist vs obs)
hence nth:
"⋀i ad al v. ⟦ enat i < llength obs; lnth obs i = NormalAction (ReadMem ad al v);
ta_seq_consist P vs (ltake (enat i) obs) ⟧
⟹ ∃b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = ⌊(v, b)⌋" by blast
show ?case
proof(cases obs)
case LNil thus ?thesis by simp
next
case (LCons ob obs')
{ fix ad al v
assume "ob = NormalAction (ReadMem ad al v)"
with nth[of 0 ad al v] LCons
have "∃b. vs (ad, al) = ⌊(v, b)⌋"
by(simp add: zero_enat_def[symmetric]) }
note base = this
moreover {
fix i ad al v
assume "enat i < llength obs'" "lnth obs' i = NormalAction (ReadMem ad al v)"
and "ta_seq_consist P (mrw_value P vs ob) (ltake (enat i) obs')"
with LCons nth[of "Suc i" ad al v] base
have "∃b. mrw_values P (mrw_value P vs ob) (list_of (ltake (enat i) obs')) (ad, al) = ⌊(v, b)⌋"
by(clarsimp simp add: eSuc_enat[symmetric] split: obs_event.split action.split) }
ultimately have ?LCons using LCons by(simp split: action.split obs_event.split)
thus ?thesis ..
qed
qed
lemma ta_seq_consist_into_non_speculative:
"⟦ ta_seq_consist P vs obs; ∀adal. set_option (vs adal) ⊆ vs' adal × UNIV ⟧
⟹ non_speculative P vs' obs"
proof(coinduction arbitrary: vs' obs vs)
case (non_speculative vs' obs vs)
thus ?case
apply cases
apply(auto split: action.split_asm obs_event.split_asm)
apply(rule exI, erule conjI, auto)+
done
qed
lemma llist_of_list_of_append:
"lfinite xs ⟹ llist_of (list_of xs @ ys) = lappend xs (llist_of ys)"
unfolding lfinite_eq_range_llist_of by(clarsimp simp add: lappend_llist_of_llist_of)
lemma ta_seq_consist_most_recent_write_for:
assumes sc: "ta_seq_consist P Map.empty (lmap snd E)"
and read: "r ∈ read_actions E"
and new_actions_for_fun: "⋀adal a a'. ⟦ a ∈ new_actions_for P E adal; a' ∈ new_actions_for P E adal ⟧ ⟹ a = a'"
shows "∃i. P,E ⊢ r ↝mrw i ∧ i < r"
proof -
from read obtain t v ad al
where nth_r: "lnth E r = (t, NormalAction (ReadMem ad al v))"
and r: "enat r < llength E"
by(cases)(cases "lnth E r", auto simp add: action_obs_def actions_def)
from nth_r r
have E_unfold: "E = lappend (ltake (enat r) E) (LCons (t, NormalAction (ReadMem ad al v)) (ldropn (Suc r) E))"
by (metis lappend_ltake_enat_ldropn ldropn_Suc_conv_ldropn)
from sc obtain b where sc': "ta_seq_consist P Map.empty (ltake (enat r) (lmap snd E))"
and mrw': "mrw_values P Map.empty (map snd (list_of (ltake (enat r) E))) (ad, al) = ⌊(v, b)⌋"
by(subst (asm) (3) E_unfold)(auto simp add: ta_seq_consist_lappend lmap_lappend_distrib)
from mrw_values_mrw[OF mrw', of t] r
obtain E' w'
where E': "E' = llist_of (list_of (ltake (enat r) E) @ [(t, NormalAction (ReadMem ad al v))])"
and v: "v = value_written P (ltake (enat r) E) w' (ad, al)"
and mrw'': "P,E' ⊢ r ↝mrw w'"
and w': "w' < r" by(fastforce simp add: length_list_of_conv_the_enat min_def split: if_split_asm)
from E' r have sim: "ltake (enat (Suc r)) E' [≈] ltake (enat (Suc r)) E"
by(subst E_unfold)(simp add: ltake_lappend llist_of_list_of_append min_def, auto simp add: eSuc_enat[symmetric] zero_enat_def[symmetric] eq_into_sim_actions)
from nth_r have adal_r: "(ad, al) ∈ action_loc P E r" by(simp add: action_obs_def)
from E' r have nth_r': "lnth E' r = (t, NormalAction (ReadMem ad al v))"
by(auto simp add: nth_append length_list_of_conv_the_enat min_def)
with mrw'' w' r adal_r obtain "E ⊢ w' ≤a r" "w' ∈ write_actions E" "(ad, al) ∈ action_loc P E w'"
by cases(fastforce simp add: action_obs_def action_loc_change_prefix[OF sim[symmetric], simplified action_obs_def] intro: action_order_change_prefix[OF _ sim] write_actions_change_prefix[OF _ sim])
with read adal_r have "P,E ⊢ r ↝mrw w'"
proof(rule most_recent_write_for.intros)
fix wa'
assume write': "wa' ∈ write_actions E"
and adal_wa': "(ad, al) ∈ action_loc P E wa'"
show "E ⊢ wa' ≤a w' ∨ E ⊢ r ≤a wa'"
proof(cases "r ≤ wa'")
assume "r ≤ wa'"
show ?thesis
proof(cases "is_new_action (action_obs E wa')")
case False
with ‹r ≤ wa'› have "E ⊢ r ≤a wa'" using read write'
by(auto simp add: action_order_def elim!: read_actions.cases)
thus ?thesis ..
next
case True
with write' adal_wa' have "wa' ∈ new_actions_for P E (ad, al)"
by(simp add: new_actions_for_def)
hence "w' ∉ new_actions_for P E (ad, al)" using r w' ‹r ≤ wa'›
by(auto dest: new_actions_for_fun)
with ‹w' ∈ write_actions E› ‹(ad, al) ∈ action_loc P E w'›
have "¬ is_new_action (action_obs E w')" by(simp add: new_actions_for_def)
with write' True ‹w' ∈ write_actions E› have "E ⊢ wa' ≤a w'" by(simp add: action_order_def)
thus ?thesis ..
qed
next
assume "¬ r ≤ wa'"
hence "wa' < r" by simp
with write' adal_wa'
have "wa' ∈ write_actions E'" "(ad, al) ∈ action_loc P E' wa'"
by(auto intro: write_actions_change_prefix[OF _ sim[symmetric]] simp add: action_loc_change_prefix[OF sim])
from most_recent_write_recent[OF mrw'' _ this] nth_r'
have "E' ⊢ wa' ≤a w' ∨ E' ⊢ r ≤a wa'" by(simp add: action_obs_def)
thus ?thesis using ‹wa' < r› w'
by(auto 4 3 del: disjCI intro: disjI1 disjI2 action_order_change_prefix[OF _ sim])
qed
qed
with w' show ?thesis by blast
qed
lemma ta_seq_consist_mrw_before:
assumes sc: "ta_seq_consist P Map.empty (lmap snd E)"
and new_actions_for_fun: "⋀adal a a'. ⟦ a ∈ new_actions_for P E adal; a' ∈ new_actions_for P E adal ⟧ ⟹ a = a'"
and mrw: "P,E ⊢ r ↝mrw w"
shows "w < r"
proof -
from mrw have "r ∈ read_actions E" by cases
with sc new_actions_for_fun obtain w' where "P,E ⊢ r ↝mrw w'" "w' < r"
by(auto dest: ta_seq_consist_most_recent_write_for)
with mrw show ?thesis by(auto dest: most_recent_write_for_fun)
qed
lemma ta_seq_consist_imp_sequentially_consistent:
assumes tsa_ok: "thread_start_actions_ok E"
and new_actions_for_fun: "⋀adal a a'. ⟦ a ∈ new_actions_for P E adal; a' ∈ new_actions_for P E adal ⟧ ⟹ a = a'"
and seq: "ta_seq_consist P Map.empty (lmap snd E)"
shows "∃ws. sequentially_consistent P (E, ws) ∧ P ⊢ (E, ws) √"
proof(intro exI conjI)
define ws where "ws i = (THE w. P,E ⊢ i ↝mrw w)" for i
from seq have ns: "non_speculative P (λ_. {}) (lmap snd E)"
by(rule ta_seq_consist_into_non_speculative) simp
show "sequentially_consistent P (E, ws)" unfolding ws_def
proof(rule sequentially_consistentI)
fix r
assume "r ∈ read_actions E"
with seq new_actions_for_fun
obtain w where "P,E ⊢ r ↝mrw w" by(auto dest: ta_seq_consist_most_recent_write_for)
thus "P,E ⊢ r ↝mrw THE w. P,E ⊢ r ↝mrw w" by(simp add: THE_most_recent_writeI)
qed
show "P ⊢ (E, ws) √"
proof(rule wf_execI)
show "is_write_seen P E ws"
proof(rule is_write_seenI)
fix a ad al v
assume a: "a ∈ read_actions E"
and adal: "action_obs E a = NormalAction (ReadMem ad al v)"
from ns have seq': "non_speculative P (λ_. {}) (ltake (enat a) (lmap snd E))" by(rule non_speculative_ltake)
from seq a seq new_actions_for_fun
obtain w where mrw: "P,E ⊢ a ↝mrw w"
and "w < a" by(auto dest: ta_seq_consist_most_recent_write_for)
hence w: "ws a = w" by(simp add: ws_def THE_most_recent_writeI)
with mrw adal
show "ws a ∈ write_actions E"
and "(ad, al) ∈ action_loc P E (ws a)"
and "¬ P,E ⊢ a ≤hb ws a"
by(fastforce elim!: most_recent_write_for.cases dest: happens_before_into_action_order antisymPD[OF antisym_action_order] read_actions_not_write_actions)+
let ?between = "ltake (enat (a - Suc w)) (ldropn (Suc w) E)"
let ?prefix = "ltake (enat w) E"
let ?vs_prefix = "mrw_values P Map.empty (map snd (list_of ?prefix))"
{ fix v'
assume new: "is_new_action (action_obs E w)"
and vs': "?vs_prefix (ad, al) = ⌊(v', True)⌋"
from mrw_values_eq_SomeD[OF vs']
obtain obs' wa obs'' where split: "map snd (list_of ?prefix) = obs' @ wa # obs''"
and wa: "is_write_action wa"
and adal': "(ad, al) ∈ action_loc_aux P wa"
and new_wa: "¬ is_new_action wa" by blast
from split have "length (map snd (list_of ?prefix)) = Suc (length obs' + length obs'')" by simp
hence len_prefix: "llength ?prefix = enat …" by(simp add: length_list_of_conv_the_enat min_enat1_conv_enat)
with split have "nth (map snd (list_of ?prefix)) (length obs') = wa"
and "enat (length obs') < llength ?prefix" by simp_all
hence "snd (lnth ?prefix (length obs')) = wa" by(simp add: list_of_lmap[symmetric] del: list_of_lmap)
hence wa': "action_obs E (length obs') = wa" and "enat (length obs') < llength E"
using ‹enat (length obs') < llength ?prefix› by(auto simp add: action_obs_def lnth_ltake)
with wa have "length obs' ∈ write_actions E" by(auto intro: write_actions.intros simp add: actions_def)
from most_recent_write_recent[OF mrw _ this, of "(ad, al)"] adal adal' wa'
have "E ⊢ length obs' ≤a w ∨ E ⊢ a ≤a length obs'" by simp
hence False using new_wa new wa' adal len_prefix ‹w < a›
by(auto elim!: action_orderE simp add: min_enat1_conv_enat split: enat.split_asm)
}
hence mrw_value_w: "mrw_value P ?vs_prefix (snd (lnth E w)) (ad, al) =
⌊(value_written P E w (ad, al), ¬ is_new_action (action_obs E w))⌋"
using ‹ws a ∈ write_actions E› ‹(ad, al) ∈ action_loc P E (ws a)› w
by(cases "snd (lnth E w)" rule: mrw_value_cases)(fastforce elim: write_actions.cases simp add: value_written_def action_obs_def)+
have "mrw_values P (mrw_value P ?vs_prefix (snd (lnth E w))) (list_of (lmap snd ?between)) (ad, al) = ⌊(value_written P E w (ad, al), ¬ is_new_action (action_obs E w))⌋"
proof(subst mrw_values_no_write_unchanged)
fix wa
assume "wa ∈ set (list_of (lmap snd ?between))"
and write_wa: "is_write_action wa"
and adal_wa: "(ad, al) ∈ action_loc_aux P wa"
hence wa: "wa ∈ lset (lmap snd ?between)" by simp
from wa obtain i_wa where "wa = lnth (lmap snd ?between) i_wa"
and i_wa: "enat i_wa < llength (lmap snd ?between)"
unfolding lset_conv_lnth by blast
moreover hence i_wa_len: "enat (Suc (w + i_wa)) < llength E" by(cases "llength E") auto
ultimately have wa': "wa = action_obs E (Suc (w + i_wa))"
by(simp_all add: lnth_ltake action_obs_def ac_simps)
with write_wa i_wa_len have "Suc (w + i_wa) ∈ write_actions E"
by(auto intro: write_actions.intros simp add: actions_def)
from most_recent_write_recent[OF mrw _ this, of "(ad, al)"] adal adal_wa wa'
have "E ⊢ Suc (w + i_wa) ≤a w ∨ E ⊢ a ≤a Suc (w + i_wa)" by(simp)
hence "is_new_action wa ∧ ¬ is_new_action (action_obs E w)"
using adal i_wa wa' by(auto elim: action_orderE)
thus "case (mrw_value P ?vs_prefix (snd (lnth E w)) (ad, al)) of None ⇒ False | Some (v, b) ⇒ b ∧ is_new_action wa"
unfolding mrw_value_w by simp
qed(simp add: mrw_value_w)
moreover
from a have "a ∈ actions E" by simp
hence "enat a < llength E" by(rule actionsE)
with ‹w < a› have "enat (a - Suc w) < llength E - enat (Suc w)"
by(cases "llength E") simp_all
hence "E = lappend (lappend ?prefix (LCons (lnth E w) ?between)) (LCons (lnth (ldropn (Suc w) E) (a - Suc w)) (ldropn (Suc (a - Suc w)) (ldropn (Suc w) E)))"
using ‹w < a› ‹enat a < llength E› unfolding lappend_assoc lappend_code
apply(subst ldropn_Suc_conv_ldropn, simp)
apply(subst lappend_ltake_enat_ldropn)
apply(subst ldropn_Suc_conv_ldropn, simp add: less_trans[where y="enat a"])
by simp
hence E': "E = lappend (lappend ?prefix (LCons (lnth E w) ?between)) (LCons (lnth E a) (ldropn (Suc a) E))"
using ‹w < a› ‹enat a < llength E› by simp
from seq have "ta_seq_consist P (mrw_values P Map.empty (list_of (lappend (lmap snd ?prefix) (LCons (snd (lnth E w)) (lmap snd ?between))))) (lmap snd (LCons (lnth E a) (ldropn (Suc a) E)))"
by(subst (asm) E')(simp add: lmap_lappend_distrib ta_seq_consist_lappend)
ultimately show "value_written P E (ws a) (ad, al) = v" using adal w
by(clarsimp simp add: action_obs_def list_of_lappend list_of_LCons)
show "¬ P,E ⊢ a ≤so ws a" using ‹w < a› w adal by(auto elim!: action_orderE sync_orderE)
fix a'
assume a': "a' ∈ write_actions E" "(ad, al) ∈ action_loc P E a'"
{
presume "E ⊢ ws a ≤a a'" "E ⊢ a' ≤a a"
with mrw adal a' have "a' = ws a" unfolding w
by cases(fastforce dest: antisymPD[OF antisym_action_order] read_actions_not_write_actions elim!: meta_allE[where x=a'])
thus "a' = ws a" "a' = ws a" by -
next
assume "P,E ⊢ ws a ≤hb a'" "P,E ⊢ a' ≤hb a"
thus "E ⊢ ws a ≤a a'" "E ⊢ a' ≤a a" using a' by(blast intro: happens_before_into_action_order)+
next
assume "is_volatile P al" "P,E ⊢ ws a ≤so a'" "P,E ⊢ a' ≤so a"
thus "E ⊢ ws a ≤a a'" "E ⊢ a' ≤a a" by(auto elim: sync_orderE)
}
qed
qed(rule tsa_ok)
qed
subsection ‹Cut-and-update and sequentially consistent completion›
inductive foldl_list_all2 ::
"('b ⇒ 'c ⇒ 'a ⇒ 'a) ⇒ ('b ⇒ 'c ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'c ⇒ 'a ⇒ bool) ⇒ 'b list ⇒ 'c list ⇒ 'a ⇒ bool"
for f and P and Q
where
"foldl_list_all2 f P Q [] [] s"
| "⟦ Q x y s; P x y s ⟹ foldl_list_all2 f P Q xs ys (f x y s) ⟧ ⟹ foldl_list_all2 f P Q (x # xs) (y # ys) s"
inductive_simps foldl_list_all2_simps [simp]:
"foldl_list_all2 f P Q [] ys s"
"foldl_list_all2 f P Q xs [] s"
"foldl_list_all2 f P Q (x # xs) (y # ys) s"
inductive_simps foldl_list_all2_Cons1:
"foldl_list_all2 f P Q (x # xs) ys s"
inductive_simps foldl_list_all2_Cons2:
"foldl_list_all2 f P Q xs (y # ys) s"
definition eq_upto_seq_inconsist ::
"'m prog ⇒ ('addr, 'thread_id) obs_event action list ⇒ ('addr, 'thread_id) obs_event action list
⇒ ('addr × addr_loc ⇀ 'addr val × bool) ⇒ bool"
where
"eq_upto_seq_inconsist P =
foldl_list_all2 (λob ob' vs. mrw_value P vs ob)
(λob ob' vs. case ob of NormalAction (ReadMem ad al v) ⇒ ∃b. vs (ad, al) = Some (v, b) | _ ⇒ True)
(λob ob' vs. if (case ob of NormalAction (ReadMem ad al v) ⇒ ∃b. vs (ad, al) = Some (v, b) | _ ⇒ True) then ob = ob' else ob ≈ ob')"
lemma eq_upto_seq_inconsist_simps:
"eq_upto_seq_inconsist P [] obs' vs ⟷ obs' = []"
"eq_upto_seq_inconsist P obs [] vs ⟷ obs = []"
"eq_upto_seq_inconsist P (ob # obs) (ob' # obs') vs ⟷
(case ob of NormalAction (ReadMem ad al v) ⇒
if (∃b. vs (ad, al) = ⌊(v, b)⌋)
then ob = ob' ∧ eq_upto_seq_inconsist P obs obs' (mrw_value P vs ob)
else ob ≈ ob'
| _ ⇒ ob = ob' ∧ eq_upto_seq_inconsist P obs obs' (mrw_value P vs ob))"
by(auto simp add: eq_upto_seq_inconsist_def split: action.split obs_event.split)
lemma eq_upto_seq_inconsist_Cons1:
"eq_upto_seq_inconsist P (ob # obs) obs' vs ⟷
(∃ob' obs''. obs' = ob' # obs'' ∧
(case ob of NormalAction (ReadMem ad al v) ⇒
if (∃b. vs (ad, al) = ⌊(v, b)⌋)
then ob' = ob ∧ eq_upto_seq_inconsist P obs obs'' (mrw_value P vs ob)
else ob ≈ ob'
| _ ⇒ ob' = ob ∧ eq_upto_seq_inconsist P obs obs'' (mrw_value P vs ob)))"
unfolding eq_upto_seq_inconsist_def
by(auto split: obs_event.split action.split simp add: foldl_list_all2_Cons1)
lemma eq_upto_seq_inconsist_appendD:
assumes "eq_upto_seq_inconsist P (obs @ obs') obs'' vs"
and "ta_seq_consist P vs (llist_of obs)"
shows "length obs ≤ length obs''" (is ?thesis1)
and "take (length obs) obs'' = obs" (is ?thesis2)
and "eq_upto_seq_inconsist P obs' (drop (length obs) obs'') (mrw_values P vs obs)" (is ?thesis3)
using assms
by(induct obs arbitrary: obs'' vs)(auto split: action.split_asm obs_event.split_asm simp add: eq_upto_seq_inconsist_Cons1)
lemma ta_seq_consist_imp_eq_upto_seq_inconsist_refl:
"ta_seq_consist P vs (llist_of obs) ⟹ eq_upto_seq_inconsist P obs obs vs"
apply(induct obs arbitrary: vs)
apply(auto simp add: eq_upto_seq_inconsist_simps split: action.split obs_event.split)
done
context notes split_paired_Ex [simp del] eq_upto_seq_inconsist_simps [simp] begin
lemma eq_upto_seq_inconsist_appendI:
"⟦ eq_upto_seq_inconsist P obs OBS vs;
⟦ ta_seq_consist P vs (llist_of obs) ⟧ ⟹ eq_upto_seq_inconsist P obs' OBS' (mrw_values P vs OBS) ⟧
⟹ eq_upto_seq_inconsist P (obs @ obs') (OBS @ OBS') vs"
apply(induct obs arbitrary: vs OBS)
apply simp
apply(auto simp add: eq_upto_seq_inconsist_Cons1)
apply(simp split: action.split obs_event.split)
apply auto
done
lemma eq_upto_seq_inconsist_trans:
"⟦ eq_upto_seq_inconsist P obs obs' vs; eq_upto_seq_inconsist P obs' obs'' vs ⟧
⟹ eq_upto_seq_inconsist P obs obs'' vs"
apply(induction obs arbitrary: obs' obs'' vs)
apply(clarsimp simp add: eq_upto_seq_inconsist_Cons1)+
apply(auto split!: action.split obs_event.split if_split_asm)
done
lemma eq_upto_seq_inconsist_append2:
"⟦ eq_upto_seq_inconsist P obs obs' vs; ¬ ta_seq_consist P vs (llist_of obs) ⟧
⟹ eq_upto_seq_inconsist P obs (obs' @ obs'') vs"
apply(induction obs arbitrary: obs' vs)
apply(clarsimp simp add: eq_upto_seq_inconsist_Cons1)+
apply(auto split!: action.split obs_event.split if_split_asm)
done
end
context executions_sc_hb begin
lemma ta_seq_consist_mrwI:
assumes E: "E ∈ ℰ"
and wf: "P ⊢ (E, ws) √"
and mrw: "⋀a. ⟦ enat a < r; a ∈ read_actions E ⟧ ⟹ P,E ⊢ a ↝mrw ws a"
shows "ta_seq_consist P Map.empty (lmap snd (ltake r E))"
proof(rule ta_seq_consist_nthI)
fix i ad al v
assume i_len: "enat i < llength (lmap snd (ltake r E))"
and E_i: "lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v)"
and sc: "ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))"
from i_len have "enat i < r" by simp
with sc have "ta_seq_consist P Map.empty (ltake (enat i) (lmap snd E))"
by(simp add: min_def split: if_split_asm)
hence ns: "non_speculative P (λ_. {}) (ltake (enat i) (lmap snd E))"
by(rule ta_seq_consist_into_non_speculative) simp
from i_len have "i ∈ actions E" by(simp add: actions_def)
moreover from E_i i_len have obs_i: "action_obs E i = NormalAction (ReadMem ad al v)"
by(simp add: action_obs_def lnth_ltake)
ultimately have read: "i ∈ read_actions E" ..
with i_len have mrw_i: "P,E ⊢ i ↝mrw ws i" by(auto intro: mrw)
with E have "ws i < i" using ns by(rule mrw_before)
from mrw_i obs_i obtain adal_w: "(ad, al) ∈ action_loc P E (ws i)"
and adal_r: "(ad, al) ∈ action_loc P E i"
and "write": "ws i ∈ write_actions E" by cases auto
from wf have "is_write_seen P E ws" by(rule wf_exec_is_write_seenD)
from is_write_seenD[OF this read obs_i]
have vw_v: "value_written P E (ws i) (ad, al) = v" by simp
let ?vs = "mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))"
from ‹ws i < i› i_len have "enat (ws i) < llength (ltake (enat i) E)"
by(simp add: less_trans[where y="enat i"])
hence "ltake (enat i) E = lappend (ltake (enat (ws i)) (ltake (enat i) E)) (LCons (lnth (ltake (enat i) E) (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))"
by(simp only: ldropn_Suc_conv_ldropn lappend_ltake_enat_ldropn)
also have "… = lappend (ltake (enat (ws i)) E) (LCons (lnth E (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))"
using ‹ws i < i› i_len ‹enat (ws i) < llength (ltake (enat i) E)›
by (simp add: lnth_ltake)
finally have r_E: "ltake (enat i) E = …" .
have "mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al)
= mrw_values P Map.empty (map snd (list_of (ltake (enat i) E))) (ad, al)"
using ‹enat i < r› by(auto simp add: min_def)
also have "… = mrw_values P (mrw_value P ?vs (snd (lnth E (ws i)))) (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))) (ad, al)"
by(subst r_E)(simp add: list_of_lappend)
also have "… = mrw_value P ?vs (snd (lnth E (ws i))) (ad, al)"
proof(rule mrw_values_no_write_unchanged)
fix wa
assume wa: "wa ∈ set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))))"
and "is_write_action wa" "(ad, al) ∈ action_loc_aux P wa"
from wa obtain w where "w < length (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))))"
and "map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))) ! w = wa"
unfolding in_set_conv_nth by blast
moreover hence "Suc (ws i + w) < i" (is "?w < _") using i_len
by(cases "llength E")(simp_all add: length_list_of_conv_the_enat)
ultimately have obs_w': "action_obs E ?w = wa" using i_len
by(simp add: action_obs_def lnth_ltake less_trans[where y="enat i"] ac_simps)
from ‹?w < i› i_len have "?w ∈ actions E"
by(simp add: actions_def less_trans[where y="enat i"])
with ‹is_write_action wa› obs_w' ‹(ad, al) ∈ action_loc_aux P wa›
have write': "?w ∈ write_actions E"
and adal': "(ad, al) ∈ action_loc P E ?w"
by(auto intro: write_actions.intros)
from ‹?w < i› ‹i ∈ read_actions E› ‹?w ∈ actions E›
have "E ⊢ ?w ≤a i" by(auto simp add: action_order_def elim: read_actions.cases)
from mrw_i adal_r write' adal'
have "E ⊢ ?w ≤a ws i ∨ E ⊢ i ≤a ?w" by(rule most_recent_write_recent)
hence "E ⊢ ?w ≤a ws i"
proof
assume "E ⊢ i ≤a ?w"
with ‹E ⊢ ?w ≤a i› have "?w = i" by(rule antisymPD[OF antisym_action_order])
with write' read have False by(auto dest: read_actions_not_write_actions)
thus ?thesis ..
qed
from adal_w "write" have "mrw_value P ?vs (snd (lnth E (ws i))) (ad, al) ≠ None"
by(cases "snd (lnth E (ws i))" rule: mrw_value_cases)
(auto simp add: action_obs_def split: if_split_asm elim: write_actions.cases)
then obtain b v where vb: "mrw_value P ?vs (snd (lnth E (ws i))) (ad, al) = Some (v, b)" by auto
moreover
from ‹E ⊢ ?w ≤a ws i› obs_w'
have "is_new_action wa" "¬ is_new_action (action_obs E (ws i))" by(auto elim!: action_orderE)
from ‹¬ is_new_action (action_obs E (ws i))› "write" adal_w
obtain v' where "action_obs E (ws i) = NormalAction (WriteMem ad al v')"
by(auto elim!: write_actions.cases is_write_action.cases)
with vb have b by(simp add: action_obs_def)
with ‹is_new_action wa› vb
show "case mrw_value P ?vs (snd (lnth E (ws i))) (ad, al) of None ⇒ False | ⌊(v, b)⌋ ⇒ b ∧ is_new_action wa" by simp
qed
also {
fix v
assume "?vs (ad, al) = Some (v, True)"
and "is_new_action (action_obs E (ws i))"
from mrw_values_eq_SomeD[OF this(1)]
obtain wa where "wa ∈ set (map snd (list_of (ltake (enat (ws i)) E)))"
and "is_write_action wa"
and "(ad, al) ∈ action_loc_aux P wa"
and "¬ is_new_action wa" by(fastforce simp del: set_map)
moreover then obtain w where w: "w < ws i" and wa: "wa = snd (lnth E w)"
unfolding in_set_conv_nth by(cases "llength E")(auto simp add: lnth_ltake length_list_of_conv_the_enat)
ultimately have "w ∈ write_actions E" "action_obs E w = wa" "(ad, al) ∈ action_loc P E w"
using ‹ws i ∈ write_actions E›
by(auto intro!: write_actions.intros simp add: actions_def less_trans[where y="enat (ws i)"] action_obs_def elim!: write_actions.cases)
with mrw_i adal_r have "E ⊢ w ≤a ws i ∨ E ⊢ i ≤a w" by -(rule most_recent_write_recent)
hence False
proof
assume "E ⊢ w ≤a ws i"
moreover from ‹¬ is_new_action wa› ‹is_new_action (action_obs E (ws i))› "write" w wa ‹w ∈ write_actions E›
have "E ⊢ ws i ≤a w" by(auto simp add: action_order_def action_obs_def)
ultimately have "w = ws i" by(rule antisymPD[OF antisym_action_order])
with ‹w < ws i› show False by simp
next
assume "E ⊢ i ≤a w"
moreover from ‹w ∈ write_actions E› ‹w < ws i› ‹ws i < i› read
have "E ⊢ w ≤a i" by(auto simp add: action_order_def elim: read_actions.cases)
ultimately have "i = w" by(rule antisymPD[OF antisym_action_order])
with ‹w < ws i› ‹ws i < i› show False by simp
qed }
then obtain b where "… = Some (v, b)" using vw_v "write" adal_w
apply(atomize_elim)
apply(auto simp add: action_obs_def value_written_def write_actions_iff)
apply(erule is_write_action.cases)
apply auto
done
finally show "∃b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = ⌊(v, b)⌋"
by blast
qed
end
context jmm_multithreaded begin
definition complete_sc :: "('l,'thread_id,'x,'m,'w) state ⇒ ('addr × addr_loc ⇀ 'addr val × bool) ⇒
('thread_id × ('l, 'thread_id, 'x, 'm, 'w, ('addr, 'thread_id) obs_event action) thread_action) llist"
where
"complete_sc s vs = unfold_llist
(λ(s, vs). ∀t ta s'. ¬ s -t▹ta→ s')
(λ(s, vs). fst (SOME ((t, ta), s'). s -t▹ta→ s' ∧ ta_seq_consist P vs (llist_of ⦃ta⦄⇘o⇙)))
(λ(s, vs). let ((t, ta), s') = SOME ((t, ta), s'). s -t▹ta→ s' ∧ ta_seq_consist P vs (llist_of ⦃ta⦄⇘o⇙)
in (s', mrw_values P vs ⦃ta⦄⇘o⇙))
(s, vs)"
definition sc_completion :: "('l, 'thread_id, 'x, 'm, 'w) state ⇒ ('addr × addr_loc ⇀ 'addr val × bool) ⇒ bool"
where
"sc_completion s vs ⟷
(∀ttas s' t x ta x' m'.
s -▹ttas→* s' ⟶ ta_seq_consist P vs (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 ⟶
(∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
ta_seq_consist P (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of ⦃ta'⦄⇘o⇙)))"
lemma sc_completionD:
"⟦ sc_completion s vs; s -▹ttas→* s'; ta_seq_consist P vs (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 ⟧
⟹ ∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
ta_seq_consist P (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of ⦃ta'⦄⇘o⇙)"
unfolding sc_completion_def by blast
lemma sc_completionI:
"(⋀ttas s' t x ta x' m'.
⟦ s -▹ttas→* s'; ta_seq_consist P vs (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 ⟧
⟹ ∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
ta_seq_consist P (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of ⦃ta'⦄⇘o⇙))
⟹ sc_completion s vs"
unfolding sc_completion_def by blast
lemma sc_completion_shift:
assumes sc_c: "sc_completion s vs"
and τRed: "s -▹ttas→* s'"
and sc: "ta_seq_consist P vs (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) (llist_of ttas)))"
shows "sc_completion s' (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
proof(rule sc_completionI)
fix ttas' s'' t x ta x' m'
assume τRed': "s' -▹ttas'→* s''"
and sc': "ta_seq_consist P (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (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"
from τRed τRed' have "s -▹ttas @ ttas'→* s''" unfolding RedT_def by(rule rtrancl3p_trans)
moreover from sc sc' have "ta_seq_consist P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (ttas @ ttas'))))"
apply(simp add: lappend_llist_of_llist_of[symmetric] ta_seq_consist_lappend del: lappend_llist_of_llist_of)
apply(simp add: lconcat_llist_of[symmetric] lmap_llist_of[symmetric] llist.map_comp o_def split_def del: lmap_llist_of)
done
ultimately
show "∃ta' x'' m''. t ⊢ ⟨x, shr s''⟩ -ta'→ ⟨x'', m''⟩ ∧ actions_ok s'' t ta' ∧
ta_seq_consist P (mrw_values P (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) (llist_of ⦃ta'⦄⇘o⇙)"
using red unfolding foldl_append[symmetric] concat_append[symmetric] map_append[symmetric]
by(rule sc_completionD[OF sc_c])
qed
lemma complete_sc_in_Runs:
assumes cau: "sc_completion s vs"
and ta_seq_consist_convert_RA: "⋀vs ln. ta_seq_consist P vs (llist_of (convert_RA ln))"
shows "mthr.Runs s (complete_sc s vs)"
proof -
let ?ttas' = "λttas' :: ('thread_id × ('l,'thread_id,'x,'m,'w, ('addr, 'thread_id) obs_event action) thread_action) list.
concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')"
let "?vs ttas'" = "mrw_values P vs (?ttas' ttas')"
define s' vs'
and ttas :: "('thread_id × ('l,'thread_id,'x,'m,'w, ('addr, 'thread_id) obs_event action) thread_action) list"
where "s' = s" and "vs' = vs" and "ttas = []"
hence "s -▹ttas→* s'" "ta_seq_consist P vs (llist_of (?ttas' ttas))" by auto
hence "mthr.Runs s' (complete_sc s' (?vs ttas))"
proof(coinduction arbitrary: s' ttas rule: mthr.Runs.coinduct)
case (Runs s' ttas')
note Red = ‹s -▹ttas'→* s'›
and sc = ‹ta_seq_consist P vs (llist_of (?ttas' ttas'))›
show ?case
proof(cases "∃t' ta' s''. s' -t'▹ta'→ s''")
case False
hence ?Stuck by(simp add: complete_sc_def)
thus ?thesis ..
next
case True
let ?proceed = "λ((t', ta'), s''). s' -t'▹ta'→ s'' ∧ ta_seq_consist P (?vs ttas') (llist_of ⦃ta'⦄⇘o⇙)"
from True obtain t' ta' s'' where red: "s' -t'▹ta'→ s''" by(auto)
then obtain ta'' s''' where "s' -t'▹ta''→ s'''"
and "ta_seq_consist P (?vs ttas') (llist_of ⦃ta''⦄⇘o⇙)"
proof(cases)
case (redT_normal x x' m')
note red = ‹t' ⊢ ⟨x, shr s'⟩ -ta'→ ⟨x', m'⟩›
and ts''t' = ‹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 sc_completionD[OF cau Red sc ts''t' red aok]
obtain ta'' x'' m'' where red': "t' ⊢ ⟨x, shr s'⟩ -ta''→ ⟨x'', m''⟩"
and aok': "actions_ok s' t' ta''"
and sc': "ta_seq_consist P (?vs ttas') (llist_of ⦃ta''⦄⇘o⇙)" by blast
from redT_updWs_total obtain ws' where "redT_updWs t' (wset s') ⦃ta''⦄⇘w⇙ ws'" ..
then obtain s''' where "redT_upd s' t' ta'' x'' m'' s'''" by fastforce
with red' ts''t' aok' have "s' -t'▹ta''→ s'''" ..
thus thesis using sc' by(rule that)
next
case redT_acquire
thus thesis by(simp add: that[OF red] ta_seq_consist_convert_RA)
qed
hence "?proceed ((t', ta''), s''')" using Red by(auto)
hence *: "?proceed (Eps ?proceed)" by(rule someI)
moreover from Red * have "s -▹ttas' @ [fst (Eps ?proceed)]→* snd (Eps ?proceed)"
by(auto simp add: split_beta RedT_def intro: rtrancl3p_step)
moreover from True
have "complete_sc s' (?vs ttas') = LCons (fst (Eps ?proceed)) (complete_sc (snd (Eps ?proceed)) (?vs (ttas' @ [fst (Eps ?proceed)])))"
unfolding complete_sc_def by(simp add: split_def)
moreover from sc ‹?proceed (Eps ?proceed)›
have "ta_seq_consist P vs (llist_of (?ttas' (ttas' @ [fst (Eps ?proceed)])))"
unfolding map_append concat_append lappend_llist_of_llist_of[symmetric]
by(subst ta_seq_consist_lappend)(auto simp add: split_def)
ultimately have ?Step
by(fastforce intro: exI[where x="ttas' @ [fst (Eps ?proceed)]"] simp del: split_paired_Ex)
thus ?thesis by simp
qed
qed
thus ?thesis by(simp add: s'_def ttas_def)
qed
lemma complete_sc_ta_seq_consist:
assumes cau: "sc_completion s vs"
and ta_seq_consist_convert_RA: "⋀vs ln. ta_seq_consist P vs (llist_of (convert_RA ln))"
shows "ta_seq_consist P vs (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) (complete_sc s vs)))"
proof -
define vs' where "vs' = vs"
let ?obs = "λttas. lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) ttas)"
define obs where "obs = ?obs (complete_sc s vs)"
define a where "a = complete_sc s vs'"
let ?ttas' = "λttas' :: ('thread_id × ('l,'thread_id,'x,'m,'w,('addr, 'thread_id) obs_event action) thread_action) list.
concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')"
let ?vs = "λttas'. mrw_values P vs (?ttas' ttas')"
from vs'_def obs_def
have "s -▹[]→* s" "ta_seq_consist P vs (llist_of (?ttas' []))" "vs' = ?vs []" by(auto)
hence "∃s' ttas'. obs = ?obs (complete_sc s' vs') ∧ s -▹ttas'→* s' ∧
ta_seq_consist P vs (llist_of (?ttas' ttas')) ∧ vs' = ?vs ttas' ∧
a = complete_sc s' vs'"
unfolding obs_def vs'_def a_def by metis
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_seq_consist P vs' obs"
proof(coinduct vs' obs a rule: ta_seq_consist_coinduct_append_wf)
case (ta_seq_consist vs' obs a)
then obtain s' ttas' where obs_def: "obs = ?obs (complete_sc s' (?vs ttas'))"
and Red: "s -▹ttas'→* s'"
and sc: "ta_seq_consist P vs (llist_of (?ttas' ttas'))"
and vs'_def: "vs' = ?vs ttas'"
and a_def: "a = complete_sc s' vs'" by blast
show ?case
proof(cases "∃t' ta' s''. s' -t'▹ta'→ s''")
case False
hence "obs = LNil" unfolding obs_def complete_sc_def by simp
hence ?LNil unfolding obs_def by auto
thus ?thesis ..
next
case True
let ?proceed = "λ((t', ta'), s''). s' -t'▹ta'→ s'' ∧ ta_seq_consist P (?vs ttas') (llist_of ⦃ta'⦄⇘o⇙)"
let ?tta = "fst (Eps ?proceed)"
let ?s' = "snd (Eps ?proceed)"
from True obtain t' ta' s'' where red: "s' -t'▹ta'→ s''" by blast
then obtain ta'' s''' where "s' -t'▹ta''→ s'''"
and "ta_seq_consist P (?vs ttas') (llist_of ⦃ta''⦄⇘o⇙)"
proof(cases)
case (redT_normal x x' m')
note red = ‹t' ⊢ ⟨x, shr s'⟩ -ta'→ ⟨x', m'⟩›
and ts''t' = ‹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 sc_completionD[OF cau Red sc ts''t' red aok]
obtain ta'' x'' m'' where red': "t' ⊢ ⟨x, shr s'⟩ -ta''→ ⟨x'', m''⟩"
and aok': "actions_ok s' t' ta''"
and sc': "ta_seq_consist P (?vs ttas') (llist_of ⦃ta''⦄⇘o⇙)" by blast
from redT_updWs_total obtain ws' where "redT_updWs t' (wset s') ⦃ta''⦄⇘w⇙ ws'" ..
then obtain s''' where "redT_upd s' t' ta'' x'' m'' s'''" by fastforce
with red' ts''t' aok' have "s' -t'▹ta''→ s'''" ..
thus thesis using sc' by(rule that)
next
case redT_acquire
thus thesis by(simp add: that[OF red] ta_seq_consist_convert_RA)
qed
hence "?proceed ((t', ta''), s''')" by auto
hence "?proceed (Eps ?proceed)" by(rule someI)
show ?thesis
proof(cases "obs = LNil")
case True thus ?thesis ..
next
case False
from True
have csc_unfold: "complete_sc s' (?vs ttas') = LCons ?tta (complete_sc ?s' (?vs (ttas' @ [?tta])))"
unfolding complete_sc_def by(simp add: split_def)
hence "obs = lappend (llist_of ⦃snd ?tta⦄⇘o⇙) (?obs (complete_sc ?s' (?vs (ttas' @ [?tta]))))"
using obs_def by(simp add: split_beta)
moreover have "ta_seq_consist P vs' (llist_of ⦃snd ?tta⦄⇘o⇙)"
using ‹?proceed (Eps ?proceed)› vs'_def by(clarsimp simp add: split_beta)
moreover {
assume "llist_of ⦃snd ?tta⦄⇘o⇙ = LNil"
moreover from obs_def ‹obs ≠ LNil›
have "lfinite (ltakeWhile (λ(t, ta). ⦃ta⦄⇘o⇙ = []) (complete_sc s' (?vs ttas')))"
unfolding lfinite_ltakeWhile by(fastforce simp add: split_def lconcat_eq_LNil)
ultimately have "(complete_sc ?s' (?vs (ttas' @ [?tta])), a) ∈ ?R"
unfolding a_def vs'_def csc_unfold
by(clarsimp simp add: split_def llist_of_eq_LNil_conv)(auto simp add: lfinite_eq_range_llist_of) }
moreover have "?obs (complete_sc ?s' (?vs (ttas' @ [?tta]))) = ?obs (complete_sc ?s' (mrw_values P vs' (list_of (llist_of ⦃snd ?tta⦄⇘o⇙))))"
unfolding vs'_def by(simp add: split_def)
moreover from ‹?proceed (Eps ?proceed)› Red
have "s -▹ttas' @ [?tta]→* ?s'" by(auto simp add: RedT_def split_def intro: rtrancl3p_step)
moreover from sc ‹?proceed (Eps ?proceed)›
have "ta_seq_consist P vs (llist_of (?ttas' (ttas' @ [?tta])))"
by(clarsimp simp add: split_def ta_seq_consist_lappend lappend_llist_of_llist_of[symmetric] simp del: lappend_llist_of_llist_of)
moreover have "mrw_values P vs' (list_of (llist_of ⦃snd ?tta⦄⇘o⇙)) = ?vs (ttas' @ [?tta])"
unfolding vs'_def by(simp add: split_def)
moreover have "complete_sc ?s' (?vs (ttas' @ [?tta])) = complete_sc ?s' (mrw_values P vs' (list_of (llist_of ⦃snd ?tta⦄⇘o⇙)))"
unfolding vs'_def by(simp add: split_def)
ultimately have "?lappend" by blast
thus ?thesis ..
qed
qed
qed
qed
lemma sequential_completion_Runs:
assumes "sc_completion s vs"
and "⋀vs ln. ta_seq_consist P vs (llist_of (convert_RA ln))"
shows "∃ttas. mthr.Runs s ttas ∧ ta_seq_consist P vs (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) ttas))"
using complete_sc_ta_seq_consist[OF assms] complete_sc_in_Runs[OF assms]
by blast
definition cut_and_update :: "('l, 'thread_id, 'x, 'm, 'w) state ⇒ ('addr × addr_loc ⇀ 'addr val × bool) ⇒ bool"
where
"cut_and_update s vs ⟷
(∀ttas s' t x ta x' m'.
s -▹ttas→* s' ⟶ ta_seq_consist P vs (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 ⟶
(∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
ta_seq_consist P (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of ⦃ta'⦄⇘o⇙) ∧
eq_upto_seq_inconsist P ⦃ta⦄⇘o⇙ ⦃ta'⦄⇘o⇙ (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))))"
lemma cut_and_updateI[intro?]:
"(⋀ttas s' t x ta x' m'.
⟦ s -▹ttas→* s'; ta_seq_consist P vs (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 ⟧
⟹ ∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
ta_seq_consist P (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of ⦃ta'⦄⇘o⇙) ∧
eq_upto_seq_inconsist P ⦃ta⦄⇘o⇙ ⦃ta'⦄⇘o⇙ (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))))
⟹ cut_and_update s vs"
unfolding cut_and_update_def by blast
lemma cut_and_updateD:
"⟦ cut_and_update s vs; s -▹ttas→* s'; ta_seq_consist P vs (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 ⟧
⟹ ∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
ta_seq_consist P (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of ⦃ta'⦄⇘o⇙) ∧
eq_upto_seq_inconsist P ⦃ta⦄⇘o⇙ ⦃ta'⦄⇘o⇙ (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
unfolding cut_and_update_def by blast
lemma cut_and_update_imp_sc_completion:
"cut_and_update s vs ⟹ sc_completion s vs"
apply(rule sc_completionI)
apply(drule (5) cut_and_updateD)
apply blast
done
lemma sequential_completion:
assumes cut_and_update: "cut_and_update s vs"
and ta_seq_consist_convert_RA: "⋀vs ln. ta_seq_consist P vs (llist_of (convert_RA ln))"
and Red: "s -▹ttas→* s'"
and sc: "ta_seq_consist P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
and red: "s' -t▹ta→ s''"
shows
"∃ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') ∧
ta_seq_consist P vs (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) ∧
eq_upto_seq_inconsist P ⦃ta⦄⇘o⇙ ⦃ta'⦄⇘o⇙ (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
proof -
from red obtain ta' s'''
where red': "redT s' (t, ta') s'''"
and sc': "ta_seq_consist P vs (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) (lappend (llist_of ttas) (LCons (t, ta') LNil))))"
and eq: "eq_upto_seq_inconsist P ⦃ta⦄⇘o⇙ ⦃ta'⦄⇘o⇙ (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
proof cases
case (redT_normal x x' m')
note ts't = ‹thr s' t = ⌊(x, no_wait_locks)⌋›
and red = ‹t ⊢ ⟨x, shr s'⟩ -ta→ ⟨x', m'⟩›
and aok = ‹actions_ok s' t ta›
and s'' = ‹redT_upd s' t ta x' m' s''›
from cut_and_updateD[OF cut_and_update, OF Red sc ts't red aok]
obtain ta' x'' m'' where red: "t ⊢ ⟨x, shr s'⟩ -ta'→ ⟨x'', m''⟩"
and sc': "ta_seq_consist P (mrw_values P vs (concat (map (λ(t, y). ⦃y⦄⇘o⇙) ttas))) (llist_of ⦃ta'⦄⇘o⇙)"
and eq: "eq_upto_seq_inconsist P ⦃ta⦄⇘o⇙ ⦃ta'⦄⇘o⇙ (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
and aok: "actions_ok s' t ta'" by blast
obtain ws''' where "redT_updWs t (wset s') ⦃ta'⦄⇘w⇙ ws'''"
using redT_updWs_total ..
then obtain s''' where s''': "redT_upd s' t ta' x'' m'' s'''" by fastforce
with red ‹thr s' t = ⌊(x, no_wait_locks)⌋› aok have "s' -t▹ta'→ s'''" by(rule redT.redT_normal)
moreover from sc sc'
have "ta_seq_consist P vs (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) (lappend (llist_of ttas) (LCons (t, ta') LNil))))"
by(auto simp add: lmap_lappend_distrib ta_seq_consist_lappend split_def lconcat_llist_of[symmetric] o_def list_of_lconcat)
ultimately show thesis using eq by(rule that)
next
case (redT_acquire x ln n)
hence "ta_seq_consist P vs (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) (lappend (llist_of ttas) (LCons (t, ta) LNil))))"
and "eq_upto_seq_inconsist P ⦃ta⦄⇘o⇙ ⦃ta⦄⇘o⇙ (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
using sc
by(simp_all add: lmap_lappend_distrib ta_seq_consist_lappend split_def lconcat_llist_of[symmetric] o_def list_of_lconcat ta_seq_consist_convert_RA ta_seq_consist_imp_eq_upto_seq_inconsist_refl)
with red show thesis by(rule that)
qed
txt ‹Now, find a sequentially consistent completion from @{term "s'''"} onwards.›
from Red red' have Red': "s -▹ttas @ [(t, ta')]→* s'''"
unfolding RedT_def by(auto intro: rtrancl3p_step)
from sc sc'
have "ta_seq_consist P vs (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) (llist_of (ttas @ [(t, ta')]))))"
by(simp add: o_def split_def lappend_llist_of_llist_of[symmetric])
with cut_and_update_imp_sc_completion[OF cut_and_update] Red'
have "sc_completion s''' (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (ttas @ [(t, ta')]))))"
by(rule sc_completion_shift)
from sequential_completion_Runs[OF this ta_seq_consist_convert_RA]
obtain ttas' where τRuns: "mthr.Runs s''' ttas'"
and sc'': "ta_seq_consist P (mrw_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (ttas @ [(t, ta')]))))
(lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) ttas'))"
by blast
from red' τRuns have "mthr.Runs s' (LCons (t, ta') ttas')" ..
moreover from sc sc' sc''
have "ta_seq_consist P vs (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) (lappend (llist_of ttas) (LCons (t, ta') ttas'))))"
unfolding lmap_lappend_distrib lconcat_lappend by(simp add: o_def ta_seq_consist_lappend split_def list_of_lconcat)
ultimately show ?thesis using eq by blast
qed
end
end