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