Theory Non_Speculative

(*  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