(* Title: JinjaThreads/MM/JMM_DRF.thy Author: Andreas Lochbihler *) 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