Theory JMM_DRF
section ‹The data race free guarantee of the JMM›
theory JMM_DRF
imports
JMM_Spec
begin
context drf begin
lemma drf_lemma:
assumes wf: "P ⊢ (E, ws) √"
and E: "E ∈ ℰ"
and sync: "correctly_synchronized P ℰ"
and read_before: "⋀r. r ∈ read_actions E ⟹ P,E ⊢ ws r ≤hb r"
shows "sequentially_consistent P (E, ws)"
proof(rule ccontr)
let ?Q = "{r. r ∈ read_actions E ∧ ¬ P,E ⊢ r ↝mrw ws r}"
assume "¬ ?thesis"
then obtain r where "r ∈ read_actions E" "¬ P,E ⊢ r ↝mrw ws r"
by(auto simp add: sequentially_consistent_def)
hence "r ∈ ?Q" by simp
with wf_action_order[of E] obtain r'
where "r' ∈ ?Q"
and "(action_order E)⇧≠⇧≠^** r' r"
and r'_min: "⋀a. (action_order E)⇧≠⇧≠ a r' ⟹ a ∉ ?Q"
by(rule wfP_minimalE) blast
from ‹r' ∈ ?Q› have r': "r' ∈ read_actions E"
and not_mrw: "¬ P,E ⊢ r' ↝mrw ws r'" by blast+
from r' obtain ad al v where obs_r': "action_obs E r' = NormalAction (ReadMem ad al v)"
by(cases) auto
from wf have ws: "is_write_seen P E ws"
and tsa_ok: "thread_start_actions_ok E"
by(rule wf_exec_is_write_seenD wf_exec_thread_start_actions_okD)+
from is_write_seenD[OF ws r' obs_r']
have ws_r: "ws r' ∈ write_actions E"
and adal: "(ad, al) ∈ action_loc P E (ws r')"
and v: "v = value_written P E (ws r') (ad, al)"
and not_hb: "¬ P,E ⊢ r' ≤hb ws r'" by auto
from r' have "P,E ⊢ ws r' ≤hb r'" by(rule read_before)
hence "E ⊢ ws r' ≤a r'" by(rule happens_before_into_action_order)
from not_mrw
have "∃w'. w' ∈ write_actions E ∧ (ad, al) ∈ action_loc P E w' ∧
¬ P,E ⊢ w' ≤hb ws r' ∧ ¬ P,E ⊢ w' ≤so ws r' ∧
¬ P,E ⊢ r' ≤hb w' ∧ ¬ P,E ⊢ r' ≤so w' ∧ E ⊢ w' ≤a r'"
proof(rule contrapos_np)
assume inbetween: "¬ ?thesis"
note r'
moreover from obs_r' have "(ad, al) ∈ action_loc P E r'" by simp
moreover note ‹E ⊢ ws r' ≤a r'› ws_r adal
moreover
{ fix w'
assume "w' ∈ write_actions E" "(ad, al) ∈ action_loc P E w'"
with inbetween have "P,E ⊢ w' ≤hb ws r' ∨ P,E ⊢ w' ≤so ws r' ∨ P,E ⊢ r' ≤hb w' ∨ P,E ⊢ r' ≤so w' ∨ ¬ E ⊢ w' ≤a r'" by simp
moreover from total_onPD[OF total_action_order, of w' E r'] ‹w' ∈ write_actions E› r'
have "E ⊢ w' ≤a r' ∨ E ⊢ r' ≤a w'" by(auto dest: read_actions_not_write_actions)
ultimately have "E ⊢ w' ≤a ws r' ∨ E ⊢ r' ≤a w'" unfolding sync_order_def
by(blast intro: happens_before_into_action_order) }
ultimately show "P,E ⊢ r' ↝mrw ws r'" by(rule most_recent_write_for.intros)
qed
then obtain w' where w': "w' ∈ write_actions E"
and adal_w': "(ad, al) ∈ action_loc P E w'"
and "¬ P,E ⊢ w' ≤hb ws r'" "¬ P,E ⊢ r' ≤hb w'" "E ⊢ w' ≤a r'"
and so: "¬ P,E ⊢ w' ≤so ws r'" "¬ P,E ⊢ r' ≤so w'" by blast
have "ws r' ≠ w'" using ‹¬ P,E ⊢ w' ≤hb ws r'› ws_r
by(auto intro: happens_before_refl)
have vol: "¬ is_volatile P al"
proof
assume vol_al: "is_volatile P al"
with r' obs_r' have "r' ∈ sactions P E" by cases(rule sactionsI, simp_all)
moreover from w' vol_al adal_w' have "w' ∈ sactions P E"
by(cases)(auto intro: sactionsI elim!: is_write_action.cases)
ultimately have "P,E ⊢ w' ≤so r' ∨ w' = r' ∨ P,E ⊢ r' ≤so w'"
using total_sync_order[of P E] by(blast dest: total_onPD)
moreover have "w' ≠ r'" using w' r' by(auto dest: read_actions_not_write_actions)
ultimately have "P,E ⊢ w' ≤so r'" using ‹¬ P,E ⊢ r' ≤so w'› by simp
moreover from ws_r vol_al adal have "ws r' ∈ sactions P E"
by(cases)(auto intro: sactionsI elim!: is_write_action.cases)
with total_sync_order[of P E] ‹w' ∈ sactions P E› ‹¬ P,E ⊢ w' ≤so ws r'› ‹ws r' ≠ w'›
have "P,E ⊢ ws r' ≤so w'" by(blast dest: total_onPD)
ultimately show False
using is_write_seenD[OF ws r' obs_r'] w' adal_w' vol_al ‹ws r' ≠ w'› by auto
qed
{ fix a
assume "a < r'" and "a ∈ read_actions E"
hence "(action_order E)⇧≠⇧≠ a r'" using r' obs_r' by(auto intro: action_orderI)
from r'_min[OF this] ‹a ∈ read_actions E›
have "P,E ⊢ a ↝mrw ws a" by simp }
from ℰ_sequential_completion[OF E wf this, of r'] r'
obtain E' ws' where "E' ∈ ℰ" "P ⊢ (E', ws') √"
and eq: "ltake (enat r') E = ltake (enat r') E'"
and sc': "sequentially_consistent P (E', ws')"
and r'': "action_tid E r' = action_tid E' r'" "action_obs E r' ≈ action_obs E' r'"
and "r' ∈ actions E'"
by auto
from ‹P ⊢ (E', ws') √› have tsa_ok': "thread_start_actions_ok E'"
by(rule wf_exec_thread_start_actions_okD)
from ‹r' ∈ read_actions E› have "enat r' < llength E" by(auto elim: read_actions.cases actionsE)
moreover from ‹r' ∈ actions E'› have "enat r' < llength E'" by(auto elim: actionsE)
ultimately have eq': "ltake (enat (Suc r')) E [≈] ltake (enat (Suc r')) E'"
using eq[THEN eq_into_sim_actions] r''
by(auto simp add: ltake_Suc_conv_snoc_lnth sim_actions_def split_beta action_tid_def action_obs_def intro!: llist_all2_lappendI)
from r' have r'': "r' ∈ read_actions E'"
by(rule read_actions_change_prefix[OF _eq']) simp
from obs_r' have "(ad, al) ∈ action_loc P E r'" by simp
hence adal_r'': "(ad, al) ∈ action_loc P E' r'"
by(subst (asm) action_loc_change_prefix[OF eq']) simp
from ‹¬ P,E ⊢ w' ≤hb ws r'›
have "¬ is_new_action (action_obs E w')"
proof(rule contrapos_nn)
assume new_w': "is_new_action (action_obs E w')"
show "P,E ⊢ w' ≤hb ws r'"
proof(cases "is_new_action (action_obs E (ws r'))")
case True
with adal new_w' adal_w' w' ws_r
have "ws r' ∈ new_actions_for P E (ad, al)" "w' ∈ new_actions_for P E (ad, al)"
by(auto simp add: new_actions_for_def)
with ‹E ∈ ℰ› have "ws r' = w'" by(rule ℰ_new_actions_for_fun)
thus ?thesis using w' by(auto intro: happens_before_refl)
next
case False
with tsa_ok w' ws_r new_w'
show ?thesis by(auto intro: happens_before_new_not_new)
qed
qed
with ‹E ⊢ w' ≤a r'› have "w' ≤ r'" by(auto elim!: action_orderE)
moreover from w' r' have "w' ≠ r'" by(auto intro: read_actions_not_write_actions)
ultimately have "w' < r'" by simp
with w' have "w' ∈ write_actions E'"
by(auto intro: write_actions_change_prefix[OF _ eq'])
hence "w' ∈ actions E'" by simp
from adal_w' ‹w' < r'›
have "(ad, al) ∈ action_loc P E' w'"
by(subst action_loc_change_prefix[symmetric, OF eq']) simp_all
from vol ‹r' ∈ read_actions E'› ‹w' ∈ write_actions E'› ‹(ad, al) ∈ action_loc P E' w'› adal_r''
have "P,E' ⊢ r' † w'" unfolding non_volatile_conflict_def by auto
with sync ‹E' ∈ ℰ› ‹P ⊢ (E', ws') √› sc' ‹r' ∈ actions E'› ‹w' ∈ actions E'›
have hb'_r'_w': "P,E' ⊢ r' ≤hb w' ∨ P,E' ⊢ w' ≤hb r'"
by(rule correctly_synchronizedD[rule_format])
hence "P,E ⊢ r' ≤hb w' ∨ P,E ⊢ w' ≤hb r'" using ‹w' < r'›
by(auto intro: happens_before_change_prefix[OF _ tsa_ok eq'[symmetric]])
with ‹¬ P,E ⊢ r' ≤hb w'› have "P,E ⊢ w' ≤hb r'" by simp
have "P,E ⊢ ws r' ≤hb w'"
proof(cases "is_new_action (action_obs E (ws r'))")
case False
with ‹E ⊢ ws r' ≤a r'› have "ws r' ≤ r'" by(auto elim!: action_orderE)
moreover from ws_r r' have "ws r' ≠ r'" by(auto dest: read_actions_not_write_actions)
ultimately have "ws r' < r'" by simp
with ws_r have "ws r' ∈ write_actions E'"
by(auto intro: write_actions_change_prefix[OF _ eq'])
hence "ws r' ∈ actions E'" by simp
from adal ‹ws r' < r'›
have "(ad, al) ∈ action_loc P E' (ws r')"
by(subst action_loc_change_prefix[symmetric, OF eq']) simp_all
hence "P,E' ⊢ ws r' † w'"
using ‹ws r' ∈ write_actions E'› ‹w' ∈ write_actions E'› ‹(ad, al) ∈ action_loc P E' w'› vol
unfolding non_volatile_conflict_def by auto
with sync ‹E' ∈ ℰ› ‹P ⊢ (E', ws') √› sc' ‹ws r' ∈ actions E'› ‹w' ∈ actions E'›
have "P,E' ⊢ ws r' ≤hb w' ∨ P,E' ⊢ w' ≤hb ws r'"
by(rule correctly_synchronizedD[rule_format])
thus "P,E ⊢ ws r' ≤hb w'" using ‹w' < r'› ‹ws r' < r'› ‹¬ P,E ⊢ w' ≤hb ws r'›
by(auto dest: happens_before_change_prefix[OF _ tsa_ok eq'[symmetric]])
next
case True
with tsa_ok ws_r w' ‹¬ is_new_action (action_obs E w')›
show "P,E ⊢ ws r' ≤hb w'" by(auto intro: happens_before_new_not_new)
qed
moreover
from wf have "is_write_seen P E ws" by(rule wf_exec_is_write_seenD)
ultimately have "w' = ws r'"
using is_write_seenD[OF ‹is_write_seen P E ws› ‹r' ∈ read_actions E› obs_r']
‹w' ∈ write_actions E› ‹(ad, al) ∈ action_loc P E w'› ‹P,E ⊢ w' ≤hb r'›
by auto
with porder_happens_before[of E P] ‹¬ P,E ⊢ w' ≤hb ws r'› ws_r show False
by(auto dest: refl_onPD[where a="ws r'"] elim!: porder_onE)
qed
lemma justified_action_committedD:
assumes justified: "P ⊢ (E, ws) weakly_justified_by J"
and a: "a ∈ actions E"
obtains n a' where "a = action_translation (J n) a'" "a' ∈ committed (J n)"
proof(atomize_elim)
from justified have "actions E = (⋃n. action_translation (J n) ` committed (J n))"
by(simp add: is_commit_sequence_def)
with a show "∃n a'. a = action_translation (J n) a' ∧ a' ∈ committed (J n)" by auto
qed
theorem drf_weak:
assumes sync: "correctly_synchronized P ℰ"
and legal: "weakly_legal_execution P ℰ (E, ws)"
shows "sequentially_consistent P (E, ws)"
using legal_wf_execD[OF legal] legal_ℰD[OF legal] sync
proof(rule drf_lemma)
fix r
assume "r ∈ read_actions E"
from legal obtain J where E: "E ∈ ℰ"
and wf_exec: "P ⊢ (E, ws) √"
and J: "P ⊢ (E, ws) weakly_justified_by J"
and range_J: "range (justifying_exec ∘ J) ⊆ ℰ"
by(rule legal_executionE)
let ?E = "λn. justifying_exec (J n)"
and ?ws = "λn. justifying_ws (J n)"
and ?C = "λn. committed (J n)"
and ?φ = "λn. action_translation (J n)"
from ‹r ∈ read_actions E› have "r ∈ actions E" by simp
with J obtain n r' where r: "r = action_translation (J n) r'"
and r': "r' ∈ ?C n" by(rule justified_action_committedD)
note ‹r ∈ read_actions E›
moreover from J have wfan: "wf_action_translation_on (?E n) E (?C n) (?φ n)"
by(simp add: wf_action_translations_def)
hence "action_obs (?E n) r' ≈ action_obs E r" using r' unfolding r
by(blast dest: wf_action_translation_on_actionD)
moreover from J r' have "r' ∈ actions (?E n)"
by(auto simp add: committed_subset_actions_def)
ultimately have "r' ∈ read_actions (?E n)" unfolding r
by cases(auto intro: read_actions.intros)
hence "P,E ⊢ ws (?φ n r') ≤hb ?φ n r'" using ‹r' ∈ ?C n›
proof(induct n arbitrary: r')
case 0
from J have "?C 0 = {}" by(simp add: is_commit_sequence_def)
with 0 have False by simp
thus ?case ..
next
case (Suc n r)
note r = ‹r ∈ read_actions (?E (Suc n))›
from J have wfan: "wf_action_translation_on (?E n) E (?C n) (?φ n)"
and wfaSn: "wf_action_translation_on (?E (Suc n)) E (?C (Suc n)) (?φ (Suc n))"
by(simp_all add: wf_action_translations_def)
from wfaSn have injSn: "inj_on (?φ (Suc n)) (actions (?E (Suc n)))"
by(rule wf_action_translation_on_inj_onD)
from J have C_sub_A: "?C (Suc n) ⊆ actions (?E (Suc n))"
by(simp add: committed_subset_actions_def)
from J have wf: "P ⊢ (?E (Suc n), ?ws (Suc n)) √" by(simp add: justification_well_formed_def)
moreover from range_J have "?E (Suc n) ∈ ℰ" by auto
ultimately have sc: "sequentially_consistent P (?E (Suc n), ?ws (Suc n))" using sync
proof(rule drf_lemma)
fix r'
assume r': "r' ∈ read_actions (?E (Suc n))"
hence "r' ∈ actions (?E (Suc n))" by simp
show "P,?E (Suc n) ⊢ ?ws (Suc n) r' ≤hb r'"
proof(cases "?φ (Suc n) r' ∈ ?φ n ` ?C n")
case True
then obtain r'' where r'': "r'' ∈ ?C n"
and r'_r'': "?φ (Suc n) r' = ?φ n r''" by(auto)
from r'' wfan have "action_tid (?E n) r'' = action_tid E (?φ n r'')"
and "action_obs (?E n) r'' ≈ action_obs E (?φ n r'')"
by(blast dest: wf_action_translation_on_actionD)+
moreover from J have "?φ n ` ?C n ⊆ ?φ (Suc n) ` ?C (Suc n)"
by(simp add: is_commit_sequence_def)
with r'' have "?φ (Suc n) r' ∈ ?φ (Suc n) ` ?C (Suc n)"
unfolding r'_r'' by auto
hence "r' ∈ ?C (Suc n)"
unfolding inj_on_image_mem_iff[OF injSn ‹r' ∈ actions (?E (Suc n))› C_sub_A] .
with wfaSn have "action_tid (?E (Suc n)) r' = action_tid E (?φ (Suc n) r')"
and "action_obs (?E (Suc n)) r' ≈ action_obs E (?φ (Suc n) r')"
by(blast dest: wf_action_translation_on_actionD)+
ultimately have tid: "action_tid (?E n) r'' = action_tid (?E (Suc n)) r'"
and obs: "action_obs (?E n) r'' ≈ action_obs (?E (Suc n)) r'"
unfolding r'_r'' by(auto intro: sim_action_trans sim_action_sym)
from J have "?C n ⊆ actions (?E n)" by(simp add: committed_subset_actions_def)
with r'' have "r'' ∈ actions (?E n)" by blast
with r' obs have "r'' ∈ read_actions (?E n)"
by cases(auto intro: read_actions.intros)
hence hb'': "P,E ⊢ ws (?φ n r'') ≤hb ?φ n r''"
using ‹r'' ∈ ?C n› by(rule Suc)
have r_conv_inv: "r' = inv_into (actions (?E (Suc n))) (?φ (Suc n)) (?φ n r'')"
using ‹r' ∈ actions (?E (Suc n))› unfolding r'_r''[symmetric]
by(simp add: inv_into_f_f[OF injSn])
with ‹r'' ∈ ?C n› r' J ‹r'' ∈ read_actions (?E n)›
have ws_eq[symmetric]: "?φ (Suc n) (?ws (Suc n) r') = ws (?φ n r'')"
by(simp add: write_seen_committed_def)
with r'_r''[symmetric] hb'' have "P,E ⊢ ?φ (Suc n) (?ws (Suc n) r') ≤hb ?φ (Suc n) r'" by simp
moreover
from J r' ‹r' ∈ committed (J (Suc n))›
have "ws (?φ (Suc n) r') ∈ ?φ (Suc n) ` ?C (Suc n)"
by(rule weakly_justified_write_seen_hb_read_committed)
then obtain w' where w': "ws (?φ (Suc n) r') = ?φ (Suc n) w'"
and committed_w': "w' ∈ ?C (Suc n)" by blast
with C_sub_A have w'_action: "w' ∈ actions (?E (Suc n))" by auto
hence w'_def: "w' = inv_into (actions (?E (Suc n))) (?φ (Suc n)) (ws (?φ (Suc n) r'))"
using injSn unfolding w' by simp
from J r' ‹r' ∈ committed (J (Suc n))›
have hb_eq: "P,E ⊢ ws (?φ (Suc n) r') ≤hb ?φ (Suc n) r' ⟷ P,?E (Suc n) ⊢ w' ≤hb r'"
unfolding w'_def by(simp add: happens_before_committed_weak_def)
from r' obtain ad al v where "action_obs (?E (Suc n)) r' = NormalAction (ReadMem ad al v)" by(cases)
from is_write_seenD[OF wf_exec_is_write_seenD[OF wf] r' this]
have "?ws (Suc n) r' ∈ actions (?E (Suc n))" by(auto)
with injSn have "w' = ?ws (Suc n) r'"
unfolding w'_def ws_eq[folded r'_r''] by(rule inv_into_f_f)
thus ?thesis using hb'' hb_eq w'_action r'_r''[symmetric] w' injSn by simp
next
case False
with J r' show ?thesis by(auto simp add: uncommitted_reads_see_hb_def)
qed
qed
from r have "r ∈ actions (?E (Suc n))" by simp
let ?w = "inv_into (actions (?E (Suc n))) (?φ (Suc n)) (ws (?φ (Suc n) r))"
from J r ‹r ∈ ?C (Suc n)› have ws_rE_comm: "ws (?φ (Suc n) r) ∈ ?φ (Suc n) ` ?C (Suc n)"
by(rule weakly_justified_write_seen_hb_read_committed)
hence "?w ∈ ?C (Suc n)" using C_sub_A by(auto simp add: inv_into_f_f[OF injSn])
with C_sub_A have w: "?w ∈ actions (?E (Suc n))" by blast
from ws_rE_comm C_sub_A have w_eq: "?φ (Suc n) ?w = ws (?φ (Suc n) r)"
by(auto simp: f_inv_into_f[where f="?φ (Suc n)"])
from r obtain ad al v
where obsr: "action_obs (?E (Suc n)) r = NormalAction (ReadMem ad al v)" by cases
hence adal_r: "(ad, al) ∈ action_loc P (?E (Suc n)) r" by simp
from J wfaSn ‹r ∈ ?C (Suc n)›
have obs_sim: "action_obs (?E (Suc n)) r ≈ action_obs E (?φ (Suc n) r)" "?φ (Suc n) r ∈ actions E"
by(auto dest: wf_action_translation_on_actionD simp add: committed_subset_actions_def is_commit_sequence_def)
with obsr have rE: "?φ (Suc n) r ∈ read_actions E" by(fastforce intro: read_actions.intros)
from obs_sim obsr obtain v'
where obsrE: "action_obs E (?φ (Suc n) r) = NormalAction (ReadMem ad al v')" by auto
from wf_exec have "is_write_seen P E ws" by(rule wf_exec_is_write_seenD)
from is_write_seenD[OF this rE obsrE]
have "ws (?φ (Suc n) r) ∈ write_actions E"
and "(ad, al) ∈ action_loc P E (ws (?φ (Suc n) r))"
and nhb: "¬ P,E ⊢ ?φ (Suc n) r ≤hb ws (?φ (Suc n) r)"
and vol: "is_volatile P al ⟹ ¬ P,E ⊢ ?φ (Suc n) r ≤so ws (?φ (Suc n) r)" by simp_all
show ?case
proof(cases "is_volatile P al")
case False
from wf_action_translation_on_actionD[OF wfaSn ‹?w ∈ ?C (Suc n)›]
have "action_obs (?E (Suc n)) ?w ≈ action_obs E (?φ (Suc n) ?w)" by simp
with w_eq have obs_sim_w: "action_obs (?E (Suc n)) ?w ≈ action_obs E (ws (?φ (Suc n) r))" by simp
with ‹ws (?φ (Suc n) r) ∈ write_actions E› ‹?w ∈ actions (?E (Suc n))›
have "?w ∈ write_actions (?E (Suc n))"
by cases(fastforce intro: write_actions.intros is_write_action.intros elim!: is_write_action.cases)
from ‹(ad, al) ∈ action_loc P E (ws (?φ (Suc n) r))› obs_sim_w
have "(ad, al) ∈ action_loc P (?E (Suc n)) ?w" by cases(auto intro: action_loc_aux_intros)
with r adal_r ‹?w ∈ write_actions (?E (Suc n))› False
have "P,?E (Suc n) ⊢ r † ?w" by(auto simp add: non_volatile_conflict_def)
with sc ‹r ∈ actions (?E (Suc n))› w
have "P,?E (Suc n) ⊢ r ≤hb ?w ∨ P,?E (Suc n) ⊢ ?w ≤hb r"
by(rule correctly_synchronizedD[rule_format, OF sync ‹?E (Suc n) ∈ ℰ› wf])
moreover from J r ‹r ∈ ?C (Suc n)›
have "P,?E (Suc n) ⊢ ?w ≤hb r ⟷ P,E ⊢ ws (?φ (Suc n) r) ≤hb ?φ (Suc n) r"
and "¬ P,?E (Suc n) ⊢ r ≤hb ?w"
by(simp_all add: happens_before_committed_weak_def)
ultimately show ?thesis by auto
next
case True
with rE obsrE have "?φ (Suc n) r ∈ sactions P E" by cases (auto intro: sactionsI)
moreover from ‹ws (?φ (Suc n) r) ∈ write_actions E› ‹(ad, al) ∈ action_loc P E (ws (?φ (Suc n) r))› True
have "ws (?φ (Suc n) r) ∈ sactions P E" by cases(auto intro!: sactionsI elim: is_write_action.cases)
moreover have "?φ (Suc n) r ≠ ws (?φ (Suc n) r)"
using ‹ws (?φ (Suc n) r) ∈ write_actions E› rE by(auto dest: read_actions_not_write_actions)
ultimately have "P,E ⊢ ws (?φ (Suc n) r) ≤so ?φ (Suc n) r"
using total_sync_order[of P E] vol[OF True] by(auto dest: total_onPD)
moreover from ‹ws (?φ (Suc n) r) ∈ write_actions E› ‹(ad, al) ∈ action_loc P E (ws (?φ (Suc n) r))› True
have "P ⊢ (action_tid E (ws (?φ (Suc n) r)), action_obs E (ws (?φ (Suc n) r))) ↝sw
(action_tid E (?φ (Suc n) r), action_obs E (?φ (Suc n) r))"
by cases(fastforce elim!: is_write_action.cases intro: synchronizes_with.intros addr_locsI simp add: obsrE)
ultimately have "P,E ⊢ ws (?φ (Suc n) r) ≤sw ?φ (Suc n) r" by(rule sync_withI)
thus ?thesis unfolding po_sw_def by blast
qed
qed
thus "P,E ⊢ ws r ≤hb r" unfolding r .
qed
corollary drf:
"⟦ correctly_synchronized P ℰ; legal_execution P ℰ (E, ws) ⟧
⟹ sequentially_consistent P (E, ws)"
by(erule drf_weak)(rule legal_imp_weakly_legal_execution)
end
end