Theory SC_Legal
section ‹Sequentially consistent executions are legal›
theory SC_Legal imports
JMM_Spec
begin
context executions_base begin
primrec commit_for_sc :: "'m prog ⇒ ('addr, 'thread_id) execution × write_seen ⇒ ('addr, 'thread_id) justification"
where
"commit_for_sc P (E, ws) n =
(if enat n ≤ llength E then
let (E', ws') = SOME (E', ws'). E' ∈ ℰ ∧ P ⊢ (E', ws') √ ∧ enat n ≤ llength E' ∧
ltake (enat (n - 1)) E = ltake (enat (n - 1)) E' ∧
(n > 0 ⟶ action_tid E' (n - 1) = action_tid E (n - 1) ∧
(if n - 1 ∈ read_actions E then sim_action else (=))
(action_obs E' (n - 1)) (action_obs E (n - 1)) ∧
(∀i < n - 1. i ∈ read_actions E ⟶ ws' i = ws i)) ∧
(∀r ∈ read_actions E'. n - 1 ≤ r ⟶ P,E' ⊢ ws' r ≤hb r)
in ⦇committed = {..<n}, justifying_exec = E', justifying_ws = ws', action_translation = id⦈
else ⦇committed = actions E, justifying_exec = E, justifying_ws = ws, action_translation = id⦈)"
end
context sc_legal begin
lemma commit_for_sc_correct:
assumes E: "E ∈ ℰ"
and wf: "P ⊢ (E, ws) √"
and sc: "sequentially_consistent P (E, ws)"
shows wf_action_translation_commit_for_sc:
"⋀n. wf_action_translation E (commit_for_sc P (E, ws) n)" (is "⋀n. ?thesis1 n")
and commit_for_sc_in_ℰ:
"⋀n. justifying_exec (commit_for_sc P (E, ws) n) ∈ ℰ" (is "⋀n. ?thesis2 n")
and commit_for_sc_wf:
"⋀n. P ⊢ (justifying_exec (commit_for_sc P (E, ws) n), justifying_ws (commit_for_sc P (E, ws) n)) √"
(is "⋀n. ?thesis3 n")
and commit_for_sc_justification:
"P ⊢ (E, ws) justified_by commit_for_sc P (E, ws)" (is ?thesis4)
proof -
let ?φ = "commit_for_sc P (E, ws)"
note [simp] = split_beta
from wf have tsok: "thread_start_actions_ok E" by simp
let ?P = "λn (E', ws'). E' ∈ ℰ ∧ P ⊢ (E', ws') √ ∧ (enat n ≤ llength E ⟶ enat n ≤ llength E') ∧
ltake (enat (n - 1)) E = ltake (enat (n - 1)) E' ∧
(n > 0 ⟶ action_tid E' (n - 1) = action_tid E (n - 1) ∧
(if n - 1 ∈ read_actions E then sim_action else (=))
(action_obs E' (n - 1)) (action_obs E (n - 1)) ∧
(∀i < n - 1. i ∈ read_actions E ⟶ ws' i = ws i)) ∧
(∀r ∈ read_actions E'. n - 1 ≤ r ⟶ P,E' ⊢ ws' r ≤hb r)"
define E' ws' where "E' n = fst (Eps (?P n))" and "ws' n = snd (Eps (?P n))" for n
hence [simp]:
"⋀n. commit_for_sc P (E, ws) n =
(if enat n ≤ llength E
then ⦇committed = {..<n}, justifying_exec = E' n, justifying_ws = ws' n, action_translation = id⦈
else ⦇committed = actions E, justifying_exec = E, justifying_ws = ws, action_translation = id⦈)"
by simp
note [simp del] = commit_for_sc.simps
have "(∀n. ?thesis1 n) ∧ (∀n. ?thesis2 n) ∧ (∀n. ?thesis3 n) ∧ ?thesis4"
unfolding is_justified_by.simps is_commit_sequence_def justification_well_formed_def committed_subset_actions_def
happens_before_committed_def sync_order_committed_def value_written_committed_def uncommitted_reads_see_hb_def
committed_reads_see_committed_writes_def external_actions_committed_def wf_action_translations_def
write_seen_committed_def
proof(intro conjI strip LetI)
show "committed (?φ 0) = {}"
by(auto simp add: actions_def zero_enat_def[symmetric])
show actions_E: "actions E = (⋃n. action_translation (?φ n) ` committed (?φ n))"
by(auto simp add: actions_def less_le_trans[where y="enat n" for n] split: if_split_asm)
hence committed_subset_E: "⋀n. action_translation (?φ n) ` committed (?φ n) ⊆ actions E" by fastforce
{ fix n
have "?P n (Eps (?P n))"
proof(cases n)
case 0
from ℰ_hb_completion[OF E wf, of 0] have "∃Ews. ?P 0 Ews"
by(fastforce simp add: zero_enat_def[symmetric])
thus ?thesis unfolding 0 by(rule someI_ex)
next
case (Suc n')
moreover
from sc have sc': "⋀a. ⟦ a < n'; a ∈ read_actions E ⟧ ⟹ P,E ⊢ a ↝mrw ws a"
by(simp add: sequentially_consistent_def)
from ℰ_hb_completion[OF E wf this, of n']
obtain E' ws' where "E' ∈ ℰ" and "P ⊢ (E', ws') √"
and eq: "ltake (enat n') E = ltake (enat n') E'"
and hb: "∀a∈read_actions E'. if a < n' then ws' a = ws a else P,E' ⊢ ws' a ≤hb a"
and n_sim: "action_tid E' n' = action_tid E n'"
"(if n' ∈ read_actions E then sim_action else (=)) (action_obs E' n') (action_obs E n')"
and n: "n' ∈ actions E ⟹ n' ∈ actions E'" by blast
moreover {
assume "enat n ≤ llength E"
with n Suc have "enat n ≤ llength E'"
by(simp add: actions_def Suc_ile_eq) }
moreover {
fix i
assume "i ∈ read_actions E"
moreover from eq have "ltake (enat n') E [≈] ltake (enat n') E'"
by(rule eq_into_sim_actions)
moreover assume "i < n'"
hence "enat i < enat n'" by simp
ultimately have "i ∈ read_actions E'" by(rule read_actions_change_prefix)
with hb[rule_format, OF this] ‹i < n'›
have "ws' i = ws i" by simp }
ultimately have "?P n (E', ws')" by simp
thus ?thesis by(rule someI)
qed }
hence P [simplified]: "⋀n. ?P n (E' n, ws' n)" by(simp add: E'_def ws'_def)
{ fix n
assume n_E: "enat n ≤ llength E"
have "ltake (enat n) (E' n) [≈] ltake (enat n) E" unfolding sim_actions_def
proof(rule llist_all2_all_lnthI)
show "llength (ltake (enat n) (E' n)) = llength (ltake (enat n) E)"
using n_E P[of n] by(clarsimp simp add: min_def)
next
fix n'
assume n': "enat n' < llength (ltake (enat n) (E' n))"
show "(λ(t, a) (t', a'). t = t' ∧ a ≈ a') (lnth (ltake (enat n) (E' n)) n') (lnth (ltake (enat n) E) n')"
proof(cases "n = Suc n'")
case True
with P[of n] show ?thesis
by(simp add: action_tid_def action_obs_def lnth_ltake split: if_split_asm)
next
case False
with n' have "n' < n - 1" by auto
moreover from P[of n] have "lnth (ltake (enat (n - 1)) (E' n)) n' = lnth (ltake (enat (n - 1)) E) n'" by simp
ultimately show ?thesis by(simp add: lnth_ltake)
qed
qed }
note sim = this
note len_eq = llist_all2_llengthD[OF this[unfolded sim_actions_def]]
{ fix n
show "wf_action_translation E (?φ n)"
proof(cases "enat n ≤ llength E")
case False thus ?thesis by(simp add: wf_action_translation_on_def)
next
case True
hence "{..<n} ⊆ actions E"
by(auto simp add: actions_def min_def less_le_trans[where y="enat n"] split: if_split_asm)
moreover
from True len_eq[OF True] have "{..<n} ⊆ actions (E' n)"
by(auto simp add: actions_def min_def less_le_trans[where y="enat n"] split: if_split_asm)
moreover {
fix a assume "a < n"
moreover from sim[OF True]
have "action_tid (ltake (enat n) (E' n)) a = action_tid (ltake (enat n) E) a"
"action_obs (ltake (enat n) (E' n)) a ≈ action_obs (ltake (enat n) E) a"
by(rule sim_actions_action_tidD sim_actions_action_obsD)+
ultimately have "action_tid (E' n) a = action_tid E a" "action_obs (E' n) a ≈ action_obs E a"
by(simp_all add: action_tid_def action_obs_def lnth_ltake) }
ultimately show ?thesis by(auto simp add: wf_action_translation_on_def del: subsetI)
qed
thus "wf_action_translation E (?φ n)" . }
note wfa = this
{ fix n from P E show "justifying_exec (?φ n) ∈ ℰ"
by(cases "enat n ≤ llength E") simp_all }
note En = this
{ fix n from P wf show "P ⊢ (justifying_exec (?φ n), justifying_ws (?φ n)) √"
by(cases "enat n ≤ llength E") simp_all
thus "P ⊢ (justifying_exec (?φ n), justifying_ws (?φ n)) √" . }
note wfn = this
{ fix n show "action_translation (?φ n) ` committed (?φ n) ⊆ action_translation (?φ (Suc n)) ` committed (?φ (Suc n))"
by(auto simp add: actions_def less_le_trans[where y="enat n"]) (metis Suc_ile_eq order_less_imp_le) }
note committed_subset = this
{ fix n
from len_eq[of n] have "enat n ≤ llength E ⟹ {..<n} ⊆ actions (E' n)"
by(auto simp add: E'_def actions_def min_def less_le_trans[where y="enat n"] split: if_split_asm)
thus "committed (?φ n) ⊆ actions (justifying_exec (?φ n))"
by(simp add: actions_def E'_def) }
note committed_actions = this
fix n
show "happens_before P (justifying_exec (?φ n)) |` committed (?φ n) =
inv_imageP (happens_before P E) (action_translation (?φ n)) |` committed (?φ n)"
proof(cases "enat n ≤ llength E")
case False thus ?thesis by simp
next
case True thus ?thesis
proof(safe intro!: ext)
fix a b
assume hb: "P,justifying_exec (?φ n) ⊢ a ≤hb b"
and a: "a ∈ committed (?φ n)"
and b: "b ∈ committed (?φ n)"
from hb True have "P,E' n ⊢ a ≤hb b" by(simp add: E'_def)
moreover note tsok sim[OF True]
moreover from a b True
have "enat a < enat n" "enat b < enat n" by simp_all
ultimately have "P,E ⊢ a ≤hb b" by(rule happens_before_change_prefix)
thus "P,E ⊢ action_translation (?φ n) a ≤hb action_translation (?φ n) b" by simp
next
fix a b
assume a: "a ∈ committed (?φ n)"
and b: "b ∈ committed (?φ n)"
and hb: "P,E ⊢ action_translation (?φ n) a ≤hb action_translation (?φ n) b"
from hb True have "P,E ⊢ a ≤hb b" by simp
moreover from wfn[of n] True have "thread_start_actions_ok (E' n)" by(simp)
moreover from sim[OF True] have "ltake (enat n) E [≈] ltake (enat n) (E' n)"
by(rule sim_actions_sym)
moreover from a b True have "enat a < enat n" "enat b < enat n" by simp_all
ultimately have "P,E' n ⊢ a ≤hb b" by(rule happens_before_change_prefix)
thus "P,justifying_exec (?φ n) ⊢ a ≤hb b" using True by(simp add: E'_def)
qed
qed
show "sync_order P (justifying_exec (?φ n)) |` committed (?φ n) =
inv_imageP (sync_order P E) (action_translation (?φ n)) |` committed (?φ n)"
proof(cases "enat n ≤ llength E")
case False thus ?thesis by simp
next
case True thus ?thesis
proof(safe intro!: ext)
fix a b
assume hb: "P,justifying_exec (?φ n) ⊢ a ≤so b"
and a: "a ∈ committed (?φ n)"
and b: "b ∈ committed (?φ n)"
from hb True have "P,E' n ⊢ a ≤so b" by(simp add: E'_def)
moreover note sim[OF True]
moreover from a b True
have "enat a < enat n" "enat b < enat n" by simp_all
ultimately have "P,E ⊢ a ≤so b" by(rule sync_order_change_prefix)
thus "P,E ⊢ action_translation (?φ n) a ≤so action_translation (?φ n) b" by simp
next
fix a b
assume a: "a ∈ committed (?φ n)"
and b: "b ∈ committed (?φ n)"
and hb: "P,E ⊢ action_translation (?φ n) a ≤so action_translation (?φ n) b"
from hb True have "P,E ⊢ a ≤so b" by simp
moreover from sim[OF True] have "ltake (enat n) E [≈] ltake (enat n) (E' n)"
by(rule sim_actions_sym)
moreover from a b True have "enat a < enat n" "enat b < enat n" by simp_all
ultimately have "P,E' n ⊢ a ≤so b" by(rule sync_order_change_prefix)
thus "P,justifying_exec (?φ n) ⊢ a ≤so b" using True by(simp add: E'_def)
qed
qed
{ fix w w' adal
assume w: "w ∈ write_actions (justifying_exec (?φ n)) ∩ committed (?φ n)"
and w': "w' = action_translation (?φ n) w"
and adal: "adal ∈ action_loc P E w'"
show "value_written P (justifying_exec (?φ n)) w adal = value_written P E w' adal"
proof(cases "enat n ≤ llength E")
case False thus ?thesis using w' by simp
next
case True
note n_E = this
have "action_obs E w = action_obs (E' n) w"
proof(cases "w < n - 1")
case True
with P[of n] w' n_E show ?thesis
by(clarsimp simp add: action_obs_change_prefix_eq)
next
case False
with w True have "w = n - 1" "n > 0" by auto
moreover
with True have "w ∈ actions E"
by(simp add: actions_def)(metis Suc_ile_eq Suc_pred)
with True w wf_action_translation_on_actionD[OF wfa, of w n] w'
have "w' ∈ write_actions E"
by(auto intro!: write_actions.intros elim!: write_actions.cases is_write_action.cases)
hence "w' ∉ read_actions E" by(blast dest: read_actions_not_write_actions)
ultimately show ?thesis using P[of n] w' True by clarsimp
qed
with True w' show ?thesis by(cases adal)(simp add: value_written.simps)
qed }
{ fix r' r r''
assume r': "r' ∈ read_actions (justifying_exec (commit_for_sc P (E, ws) n)) ∩ committed (?φ n)"
and r: "r = action_translation (?φ n) r'"
and r'': "r'' = inv_into (actions (justifying_exec (?φ (Suc n)))) (action_translation (?φ (Suc n))) r"
from r' r committed_subset[of n] have "r ∈ actions E"
by(auto split: if_split_asm elim!: read_actions.cases simp add: actions_def Suc_ile_eq less_trans[where y="enat n"])
with r' r have r_actions: "r ∈ read_actions E"
by(fastforce dest: wf_action_translation_on_actionD[OF wfa] split: if_split_asm elim!: read_actions.cases intro: read_actions.intros)
moreover from r' committed_subset[of n] committed_actions[of "Suc n"]
have "r' ∈ actions (justifying_exec (?φ (Suc n)))" by(auto split: if_split_asm elim: read_actions.cases)
ultimately have "r'' = r'" using r' r r'' by(cases "enat (Suc n) ≤ llength E") simp_all
moreover from r' have "r' < n"
by(simp add: actions_def split: if_split_asm)(metis enat_ord_code(2) linorder_linear order_less_le_trans)
ultimately show "action_translation (?φ (Suc n)) (justifying_ws (?φ (Suc n)) r'') = ws r"
using P[of "Suc n"] r' r r_actions by(clarsimp split: if_split_asm) }
{ fix r'
assume r': "r' ∈ read_actions (justifying_exec (?φ (Suc n)))"
show "action_translation (?φ (Suc n)) r' ∈ action_translation (?φ n) ` committed (?φ n) ∨
P,justifying_exec (?φ (Suc n)) ⊢ justifying_ws (?φ (Suc n)) r' ≤hb r'" (is "?committed ∨ ?hb")
proof(cases "r' < n")
case True
hence "?committed" using r'
by(auto elim!: actionsE split: if_split_asm dest!: read_actions_actions)(metis Suc_ile_eq linorder_not_le not_less_iff_gr_or_eq)
thus ?thesis ..
next
case False
hence "r' ≥ n" by simp
hence "enat (Suc n) ≤ llength E" using False r'
by(auto split: if_split_asm dest!: read_actions_actions elim!: actionsE) (metis Suc_ile_eq enat_ord_code(2) not_le_imp_less order_less_le_trans)
hence ?hb using P[of "Suc n"] r' ‹r' ≥ n› by simp
thus ?thesis ..
qed }
{ fix r' r C_n
assume r': "r' ∈ read_actions (justifying_exec (?φ (Suc n))) ∩ committed (?φ (Suc n))"
and r: "r = action_translation (?φ (Suc n)) r'"
and C_n: "C_n = action_translation (?φ n) ` committed (?φ n)"
show "r ∈ C_n ∨ action_translation (?φ (Suc n)) (justifying_ws (?φ (Suc n)) r') ∈ C_n ∧ ws r ∈ C_n"
(is "_ ∨ (?C_ws_n ∧ ?C_ws)")
proof(cases "r ∈ C_n")
case True thus ?thesis ..
next
case False
with r' r C_n have [simp]: "r' = n"
apply(auto split: if_split_asm dest!: read_actions_actions elim!: actionsE)
apply(metis enat_ord_code(1) less_SucI less_eq_Suc_le not_less_eq_eq order_trans)
by (metis Suc_ile_eq enat_ord_code(1) leD leI linorder_cases)
from r' have len_E: "enat (Suc n) ≤ llength E"
by(clarsimp simp add: actions_def Suc_ile_eq split: if_split_asm)
with r' P[of "Suc n"] have "P,justifying_exec (?φ (Suc n)) ⊢ ws' (Suc n) r' ≤hb r'" by(simp)
hence "justifying_exec (?φ (Suc n)) ⊢ ws' (Suc n) r' ≤a r'" by(rule happens_before_into_action_order)
moreover from r' have "r' ∈ read_actions (justifying_exec (?φ (Suc n)))" by simp
moreover then obtain ad al v where "action_obs (justifying_exec (?φ (Suc n))) r' = NormalAction (ReadMem ad al v)"
by cases auto
with wfn[of "Suc n"] ‹r' ∈ read_actions _› len_E obtain adal
where "ws' (Suc n) r' ∈ write_actions (justifying_exec (?φ (Suc n)))"
and "adal ∈ action_loc P (justifying_exec (?φ (Suc n))) r'"
and "adal ∈ action_loc P (justifying_exec (?φ (Suc n))) (ws' (Suc n) r')"
by(clarsimp)(auto dest: is_write_seenD)
moreover {
from En[of "Suc n"] len_E have "E' (Suc n) ∈ ℰ" by simp
moreover
fix a assume "a ∈ read_actions (justifying_exec (?φ (Suc n)))" and "a < r'"
hence "a ∈ read_actions (E' (Suc n))" "enat a < enat (Suc n)" using len_E by simp_all
with sim[OF len_E] have a: "a ∈ read_actions E" by -(rule read_actions_change_prefix)
with ‹a < r'› have mrw: "P,E ⊢ a ↝mrw ws a" using sc by(simp add: sequentially_consistent_def)
from P[of "Suc n"] ‹a < r'› a len_E have "ws a = ws' (Suc n) a" by simp
with mrw have mrw': "P,E ⊢ a ↝mrw ws' (Suc n) a" by simp
moreover from wfn[of "Suc n"] wf len_E have "thread_start_actions_ok (E' (Suc n))" by(simp)
moreover note sim[OF len_E, symmetric]
moreover from E wf mrw' have "ws' (Suc n) a < a"
by(rule mrw_before)(erule sequentially_consistentE[OF sc])
with ‹a < r'› have "ws' (Suc n) a < r'" by simp
ultimately have "P,E' (Suc n) ⊢ a ↝mrw ws' (Suc n) a" using ‹a < r'›
by -(rule mrw_change_prefix, simp+)
hence "P,justifying_exec (?φ (Suc n)) ⊢ a ↝mrw justifying_ws (?φ (Suc n)) a" using len_E by simp
}
ultimately have "ws' (Suc n) r' < r'" by(rule action_order_read_before_write[OF En wfn])
with len_E C_n have "?C_ws_n" by clarsimp (metis Suc_ile_eq linorder_le_cases order_less_irrefl order_trans)
moreover
from r' have "r' ∈ committed (?φ (Suc n))" by blast
with r' r len_E wf_action_translation_on_actionD[OF wfa this] committed_subset_E[of "Suc n"]
have "r ∈ read_actions E" by(fastforce elim!: read_actions.cases intro: read_actions.intros split: if_split_asm)
with sc obtain "P,E ⊢ r ↝mrw ws r" by(rule sequentially_consistentE)
with E wf have "ws r < r" by(rule mrw_before)(rule sequentially_consistentE[OF sc])
with C_n len_E r have ?C_ws by(auto simp add: Suc_ile_eq)
ultimately show ?thesis by simp
qed }
{ fix a a'
assume a: "a ∈ external_actions (justifying_exec (?φ n))"
and a': "a' ∈ committed (?φ n)"
and hb: "P,justifying_exec (?φ n) ⊢ a ≤hb a'"
from hb have "justifying_exec (?φ n) ⊢ a ≤a a'"
by(rule happens_before_into_action_order)
with a have "a ≤ a'" by(auto elim!: action_orderE dest: external_actions_not_new)
with a' a show "a ∈ committed (?φ n)" by(auto elim: external_actions.cases) }
qed
thus "⋀n. ?thesis1 n" "⋀n. ?thesis2 n" "⋀n. ?thesis3 n" "?thesis4"
by blast+
qed
theorem SC_is_legal:
assumes E: "E ∈ ℰ"
and wf: "P ⊢ (E, ws) √"
and sc: "sequentially_consistent P (E, ws)"
shows "legal_execution P ℰ (E, ws)"
using E wf
apply(rule legal_executionI)
apply(rule commit_for_sc_correct[OF assms])
apply clarify
apply(unfold o_apply)
apply(rule commit_for_sc_in_ℰ[OF assms])
done
end
context jmm_consistent begin
theorem consistent:
assumes "E ∈ ℰ" "P ⊢ (E, ws) √"
shows "∃E ∈ ℰ. ∃ws. legal_execution P ℰ (E, ws)"
proof -
from ℰ_sequential_completion[OF assms, of 0]
obtain E' ws' where "E'∈ℰ" "P ⊢ (E', ws') √" "sequentially_consistent P (E', ws')" by auto
moreover hence "legal_execution P ℰ (E', ws')" by(rule SC_is_legal)
ultimately show ?thesis by blast
qed
end
end