(* Title: JinjaThreads/MM/Non_Speculative.thy Author: Andreas Lochbihler *) section ‹Non-speculative prefixes of executions› theory Non_Speculative imports JMM_Spec "../Framework/FWLTS" begin declare addr_locsI [simp] subsection ‹Previously written values› fun w_value :: "'m prog ⇒ (('addr × addr_loc) ⇒ 'addr val set) ⇒ ('addr, 'thread_id) obs_event action ⇒ (('addr × addr_loc) ⇒ 'addr val set)" where "w_value P vs (NormalAction (WriteMem ad al v)) = vs((ad, al) := insert v (vs (ad, al)))" | "w_value P vs (NormalAction (NewHeapElem ad hT)) = (λ(ad', al). if ad = ad' ∧ al ∈ addr_locs P hT then insert (addr_loc_default P hT al) (vs (ad, al)) else vs (ad', al))" | "w_value P vs _ = vs" lemma w_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 w_values :: "'m prog ⇒ (('addr × addr_loc) ⇒ 'addr val set) ⇒ ('addr, 'thread_id) obs_event action list ⇒ (('addr × addr_loc) ⇒ 'addr val set)" where "w_values P ≡ foldl (w_value P)" lemma in_w_valuesD: assumes w: "v ∈ w_values P vs0 obs (ad, al)" and v: "v ∉ vs0 (ad, al)" 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 "?concl obs") using w proof(induction obs rule: rev_induct) case Nil thus ?case using v by simp next case (snoc ob obs) from snoc.IH show ?case proof(cases "v ∈ w_values P vs0 obs (ad, al)") case False thus ?thesis using ‹v ∈ w_values P vs0 (obs @ [ob]) (ad, al)› by(cases ob rule: w_value_cases)(auto 4 4 intro: action_loc_aux_intros split: if_split_asm simp add: addr_locs_def split: htype.split_asm) qed fastforce qed lemma w_values_WriteMemD: assumes "NormalAction (WriteMem ad al v) ∈ set obs" shows "v ∈ w_values P vs0 obs (ad, al)" using assms apply(induct obs rule: rev_induct) apply simp apply clarsimp apply(erule disjE) apply clarsimp apply clarsimp apply(case_tac x rule: w_value_cases) apply auto done lemma w_values_new_actionD: assumes "NormalAction (NewHeapElem ad hT) ∈ set obs" "(ad, al) ∈ action_loc_aux P (NormalAction (NewHeapElem ad hT))" shows "addr_loc_default P hT al ∈ w_values P vs0 obs (ad, al)" using assms apply(induct obs rule: rev_induct) apply simp apply clarsimp apply(rename_tac w' obs) apply(case_tac w' rule: w_value_cases) apply(auto simp add: split_beta) done lemma w_value_mono: "vs0 adal ⊆ w_value P vs0 ob adal" by(cases ob rule: w_value_cases)(auto split: if_split_asm simp add: split_beta) lemma w_values_mono: "vs0 adal ⊆ w_values P vs0 obs adal" by(induct obs rule: rev_induct)(auto del: subsetI intro: w_value_mono subset_trans) lemma w_value_greater: "vs0 ≤ w_value P vs0 ob" by(rule le_funI)(rule w_value_mono) lemma w_values_greater: "vs0 ≤ w_values P vs0 obs" by(rule le_funI)(rule w_values_mono) lemma w_values_eq_emptyD: assumes "w_values P vs0 obs adal = {}" and "w ∈ set obs" and "is_write_action w" and "adal ∈ action_loc_aux P w" shows False using assms(4) assms(1-3) apply(cases rule: action_loc_aux_cases) apply(auto dest!: w_values_new_actionD[where ?vs0.0=vs0 and P=P] w_values_WriteMemD[where ?vs0.0=vs0 and P=P]) apply blast done subsection ‹Coinductive version of non-speculative prefixes› coinductive non_speculative :: "'m prog ⇒ ('addr × addr_loc ⇒ 'addr val set) ⇒ ('addr, 'thread_id) obs_event action llist ⇒ bool" for P :: "'m prog" where LNil: "non_speculative P vs LNil" | LCons: "⟦ case ob of NormalAction (ReadMem ad al v) ⇒ v ∈ vs (ad, al) | _ ⇒ True; non_speculative P (w_value P vs ob) obs ⟧ ⟹ non_speculative P vs (LCons ob obs)" inductive_simps non_speculative_simps [simp]: "non_speculative P vs LNil" "non_speculative P vs (LCons ob obs)" lemma non_speculative_lappend: assumes "lfinite obs" shows "non_speculative P vs (lappend obs obs') ⟷ non_speculative P vs obs ∧ non_speculative P (w_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 (w_value P vs ob) obs" by fact thus ?case using ‹lfinite obs› by simp qed lemma assumes "non_speculative P vs obs" shows non_speculative_ltake: "non_speculative P vs (ltake n obs)" (is ?thesis1) and non_speculative_ldrop: "non_speculative P (w_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: non_speculative_lappend del: lappend_ltake_enat_ldropn) thus ?thesis1 ?thesis2 by blast+ qed lemma non_speculative_coinduct_append [consumes 1, case_names non_speculative, case_conclusion non_speculative LNil lappend]: assumes major: "X vs obs" and step: "⋀vs obs. X vs obs ⟹ obs = LNil ∨ (∃obs' obs''. obs = lappend obs' obs'' ∧ obs' ≠ LNil ∧ non_speculative P vs obs' ∧ (lfinite obs' ⟶ (X (w_values P vs (list_of obs')) obs'' ∨ non_speculative P (w_values P vs (list_of obs')) obs'')))" (is "⋀vs obs. _ ⟹ _ ∨ ?step vs obs") shows "non_speculative P vs obs" proof - from major have "∃obs' obs''. obs = lappend (llist_of obs') obs'' ∧ non_speculative P vs (llist_of obs') ∧ X (w_values P vs obs') obs''" by(auto intro: exI[where x="[]"]) thus ?thesis proof(coinduct) case (non_speculative vs obs) then obtain obs' obs'' where obs: "obs = lappend (llist_of obs') obs''" and sc_obs': "non_speculative P vs (llist_of obs')" and X: "X (w_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''': "non_speculative P vs obs'''" and fin: "lfinite obs''' ⟹ X (w_values P vs (list_of obs''')) obs'''' ∨ non_speculative P (w_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) ⇒ v ∈ vs (ad, al) | _ ⇒ 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 "non_speculative P (w_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 (w_values P vs (list_of obs''')) obs''''" hence "X (w_values P (w_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 "non_speculative P (w_value P vs ob) (llist_of obs'''''')" using sc_obs''' obs''' obs''''' by simp ultimately show ?thesis using concl1 concl2 by blast next assume "non_speculative P (w_values P vs (list_of obs''')) obs''''" with sc_obs''' obs''''' obs''' have "non_speculative P (w_value P vs ob) (lappend obs''''' obs'''')" by(simp add: non_speculative_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) ⇒ v ∈ vs (ad, al) | _ ⇒ True" and "non_speculative P (w_value P vs ob) (llist_of obs''')" by simp_all moreover from X Cons have "X (w_values P (w_value P vs ob) obs''') obs''" by simp ultimately show ?thesis by blast qed qed qed lemma non_speculative_coinduct_append_wf [consumes 2, case_names non_speculative, case_conclusion non_speculative 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'' ∧ non_speculative P vs obs' ∧ (obs' = LNil ⟶ (a', a) ∈ R) ∧ (lfinite obs' ⟶ X (w_values P vs (list_of obs')) obs'' a' ∨ non_speculative P (w_values P vs (list_of obs')) obs''))" (is "⋀vs obs a. _ ⟹ _ ∨ ?step vs obs a") shows "non_speculative 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 ∧ non_speculative P vs obs' ∧ (lfinite obs' ⟶ (∃a. X (w_values P vs (list_of obs')) obs'' a) ∨ non_speculative P (w_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': "non_speculative P vs obs'" and decr: "obs' = LNil ⟹ (a', a) ∈ R" and fin: "lfinite obs' ⟹ X (w_values P vs (list_of obs')) obs'' a' ∨ non_speculative P (w_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 (w_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 (w_values P vs (list_of obs')) obs''" hence "?step_concl vs obs" using True obs by simp thus ?thesis .. qed next assume "non_speculative P (w_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: non_speculative_coinduct_append) case (non_speculative vs obs) thus ?case by simp(rule step') qed qed lemma non_speculative_nthI: "(⋀i ad al v. ⟦ enat i < llength obs; lnth obs i = NormalAction (ReadMem ad al v); non_speculative P vs (ltake (enat i) obs) ⟧ ⟹ v ∈ w_values P vs (list_of (ltake (enat i) obs)) (ad, al)) ⟹ non_speculative P vs obs" proof(coinduction arbitrary: vs obs rule: non_speculative.coinduct) case (non_speculative vs obs) hence nth: "⋀i ad al v. ⟦ enat i < llength obs; lnth obs i = NormalAction (ReadMem ad al v); non_speculative P vs (ltake (enat i) obs) ⟧ ⟹ v ∈ w_values P vs (list_of (ltake (enat i) obs)) (ad, al)" 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 "v ∈ vs (ad, al)" 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 "non_speculative P (w_value P vs ob) (ltake (enat i) obs')" with LCons nth[of "Suc i" ad al v] base have "v ∈ w_values P (w_value P vs ob) (list_of (ltake (enat i) obs')) (ad, al)" 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 locale executions_sc_hb = executions_base ℰ P for ℰ :: "('addr, 'thread_id) execution set" and P :: "'m prog" + assumes ℰ_new_actions_for_fun: "⟦ E ∈ ℰ; a ∈ new_actions_for P E adal; a' ∈ new_actions_for P E adal ⟧ ⟹ a = a'" and ℰ_ex_new_action: "⟦ E ∈ ℰ; ra ∈ read_actions E; adal ∈ action_loc P E ra; non_speculative P (λ_. {}) (ltake (enat ra) (lmap snd E)) ⟧ ⟹ ∃wa. wa ∈ new_actions_for P E adal ∧ wa < ra" begin lemma ℰ_new_same_addr_singleton: assumes E: "E ∈ ℰ" shows "∃a. new_actions_for P E adal ⊆ {a}" by(blast dest: ℰ_new_actions_for_fun[OF E]) lemma new_action_before_read: assumes E: "E ∈ ℰ" and ra: "ra ∈ read_actions E" and adal: "adal ∈ action_loc P E ra" and new: "wa ∈ new_actions_for P E adal" and sc: "non_speculative P (λ_. {}) (ltake (enat ra) (lmap snd E))" shows "wa < ra" using ℰ_new_same_addr_singleton[OF E, of adal] ℰ_ex_new_action[OF E ra adal sc] new by auto lemma most_recent_write_exists: assumes E: "E ∈ ℰ" and ra: "ra ∈ read_actions E" and sc: "non_speculative P (λ_. {}) (ltake (enat ra) (lmap snd E))" shows "∃wa. P,E ⊢ ra ↝mrw wa" proof - from ra obtain ad al where adal: "(ad, al) ∈ action_loc P E ra" by(rule read_action_action_locE) define Q where "Q = {a. a ∈ write_actions E ∧ (ad, al) ∈ action_loc P E a ∧ E ⊢ a ≤a ra}" let ?A = "new_actions_for P E (ad, al)" let ?B = "{a. a ∈ actions E ∧ (∃v'. action_obs E a = NormalAction (WriteMem ad al v')) ∧ a ≤ ra}" have "Q ⊆ ?A ∪ ?B" unfolding Q_def by(auto elim!: write_actions.cases action_loc_aux_cases simp add: new_actions_for_def elim: action_orderE) moreover from ℰ_new_same_addr_singleton[OF E, of "(ad, al)"] have "finite ?A" by(blast intro: finite_subset) moreover have "finite ?B" by auto ultimately have finQ: "finite Q" by(blast intro: finite_subset) from ℰ_ex_new_action[OF E ra adal sc] ra obtain wa where wa: "wa ∈ Q" unfolding Q_def by(fastforce elim!: new_actionsE is_new_action.cases read_actions.cases intro: write_actionsI action_orderI) define wa' where "wa' = Max_torder (action_order E) Q" from wa have "Q ≠ {}" "Q ⊆ actions E" by(auto simp add: Q_def) with finQ have "wa' ∈ Q" unfolding wa'_def by(rule Max_torder_in_set[OF torder_action_order]) hence "E ⊢ wa' ≤a ra" "wa' ∈ write_actions E" and "(ad, al) ∈ action_loc P E wa'" by(simp_all add: Q_def) with ra adal have "P,E ⊢ ra ↝mrw wa'" proof fix wa'' assume wa'': "wa'' ∈ write_actions E" "(ad, al) ∈ action_loc P E wa''" from ‹wa'' ∈ write_actions E› ra have "ra ≠ wa''" by(auto dest: read_actions_not_write_actions) show "E ⊢ wa'' ≤a wa' ∨ E ⊢ ra ≤a wa''" proof(rule disjCI) assume "¬ E ⊢ ra ≤a wa''" with total_onPD[OF total_action_order, of ra E wa''] ‹ra ≠ wa''› ‹ra ∈ read_actions E› ‹wa'' ∈ write_actions E› have "E ⊢ wa'' ≤a ra" by simp with wa'' have "wa'' ∈ Q" by(simp add: Q_def) with finQ show "E ⊢ wa'' ≤a wa'" using ‹Q ⊆ actions E› unfolding wa'_def by(rule Max_torder_above[OF torder_action_order]) qed qed thus ?thesis .. qed lemma mrw_before: assumes E: "E ∈ ℰ" and mrw: "P,E ⊢ r ↝mrw w" and sc: "non_speculative P (λ_. {}) (ltake (enat r) (lmap snd E))" shows "w < r" using mrw read_actions_not_write_actions[of r E] apply cases apply(erule action_orderE) apply(erule (1) new_action_before_read[OF E]) apply(simp add: new_actions_for_def) apply(rule sc) apply(cases "w = r") apply auto done lemma sequentially_consistent_most_recent_write_for: assumes E: "E ∈ ℰ" and sc: "non_speculative P (λ_. {}) (lmap snd E)" shows "sequentially_consistent P (E, λr. THE w. P,E ⊢ r ↝mrw w)" proof(rule sequentially_consistentI) fix r assume r: "r ∈ read_actions E" from sc have sc': "non_speculative P (λ_. {}) (ltake (enat r) (lmap snd E))" by(rule non_speculative_ltake) from most_recent_write_exists[OF E r this] obtain w where "P,E ⊢ r ↝mrw w" .. thus "P,E ⊢ r ↝mrw THE w. P,E ⊢ r ↝mrw w" by(simp add: THE_most_recent_writeI) qed end locale jmm_multithreaded = multithreaded_base + constrains final :: "'x ⇒ bool" and r :: "('l, 'thread_id, 'x, 'm, 'w, ('addr, 'thread_id) obs_event action) semantics" and convert_RA :: "'l released_locks ⇒ ('addr, 'thread_id) obs_event action list" fixes P :: "'md prog" end