Require Import Classical List Relations.
Require Import Vbase ExtraRelations cactions RAmodels.
Set Implicit Arguments.

Definition TSO_read_maximal lab sb rf (tso : relation actid) :=
  ∀ a b (TSO: tso a b) c (RF: rf c = Some a)
         (HB: sb b c ∨ tso b c) (W: is_write (lab b))
         (LOC: loc (lab a) = loc (lab b)),
    False.

Definition ConsistentTSO acts lab sb rf tso :=
  << FIN : ExecutionFinite acts lab sb >> ∧
  << CsbT: transitive sb >> ∧
  << CrfD: ConsistentRF_dom lab rf >> ∧
  << COrf: CompleteRF lab rf >> ∧
  << CsbI: irreflexive sb >> ∧
  << CtsoF: is_total (fun a ⇒ is_write (lab a)) tso >> ∧
  << CtsoT: transitive tso >> ∧
  << CtsoI: irreflexive tso >> ∧
  << CpoIN: ∀ a b (PO: sb a b) (Aa: is_access (lab a)) (Ab: is_access (lab b)),
              tso a b ∨ is_write_only (lab a) ∧ is_read_only (lab b) >> ∧
  << CrfIN: ∀ a b (PO: rf b = Some a), tso a b ∨ sb a b >> ∧
  << Cwr : TSO_read_maximal lab sb rf tso >>.

Definition TSO_alt_coherence_condition lab sb rf (mo: relation actid) :=
  ∀ a b (TSO: mo a b) c (RF: rf c = Some a)
         (HB: happens_before sb rf b c ∨ mo b c ∨
              (∃ m n, mo b m ∧ rf n = Some m ∧ ¬ sb m n ∧ sb n c) ∨
              (∃ m, mo b m ∧ is_rmw (lab m) ∧ sb m c))
         (LOC: loc (lab a) = loc (lab b)),
    False.

Definition ConsistentTSOalt acts lab sb rf mo :=
  << FIN : ExecutionFinite acts lab sb >> ∧
  << CsbT: transitive sb >> ∧
  << CrfD: ConsistentRF_dom lab rf >> ∧
  << COrf: CompleteRF lab rf >> ∧
  << ACYC: irreflexive (happens_before sb rf) >> ∧
  << CmoD: ConsistentMO_big_dom lab mo >> ∧
  << CmoF: is_total (fun a ⇒ is_write (lab a)) mo >> ∧
  << CmoT: transitive mo >> ∧
  << CmoI: irreflexive mo >> ∧
  << Cww : CoherentWW sb rf mo >> ∧
  << Cwr : TSO_alt_coherence_condition lab sb rf mo >>.

Lemma ConsistentTSO_hb :
  ∀ acts lab sb rf tso (C : ConsistentTSO acts lab sb rf tso)
         a b (HB: happens_before sb rf a b)
         (A: is_access (lab a)) (B: is_access (lab b)),
    tso a b ∨ sb a b ∧ is_write_only (lab a) ∧ is_read_only (lab b).
Proof.
  unfold ConsistentTSO; ins; desf.
  assert (∀ a b,
            clos_trans
              (fun x y ⇒ sb x y ∧ is_write (lab y) ∨ rf y = Some x ∧ ¬ sb x y) a b →
            is_access (lab a) →
            tso a b).
  { clear a b HB A B; ins; apply clos_trans_t1n in H.
    induction H; desf; eauto.
    × by exploit CpoIN; eauto with caccess; ins; desf; eauto; destruct (lab y).
    × by exploit CrfIN; eauto; ins; desf.
    × assert (is_access (lab y)) by (destruct (lab y); ins).
      by exploit CpoIN; eauto with caccess; ins; desf; eauto; destruct (lab y).
    × assert (is_access (lab y)) by (apply CrfD in H; desc; destruct (lab y); ins).
      by exploit CrfIN; eauto; ins; desf; eauto.
  }
  eapply clos_trans_mon
    with (r':= fun x y ⇒ sb x y ∨ rf y = Some x ∧ ¬ sb x y) in HB.
  2: by ins; destruct (classic (sb a0 b0)); desf; eauto.
  eapply path_tur with
    (adom := fun x ⇒ is_write (lab x))
    (bdom := fun x ⇒ is_read (lab x)) in HB; ins;
  try (by desc; apply CrfD in R; desc; eauto with caccess).
  desf; eauto.
    by edestruct CpoIN; eauto.
    by edestruct CpoIN; desc; eauto; destruct (lab z).
Qed.

Lemma ConsistentTSO_hb_no_access :
  ∀ acts lab sb rf tso (C : ConsistentTSO acts lab sb rf tso)
         a b (HB: happens_before sb rf a b)
         (A: is_access (lab b) = false),
  sb a b ∨
  (∃ d, tso a d ∧ is_write (lab a) ∧ is_read (lab d) ∧ sb d b) ∨
  ∃ c d, sb a c ∧ is_write (lab c) ∧ is_read (lab d) ∧ tso c d ∧ sb d b.
Proof.
  ins; red in C; desc.
  apply clos_trans_t1n in HB; induction HB; desf; eauto;
    try (by apply CrfD in H; desc; destruct (lab y));
    try (by apply CrfD in H; desc; destruct (lab z));
    intuition; desf; eauto 10;
      exploit CrfD; eauto; ins; desc;
      apply CrfIN in H; desf; eauto 12 with caccess.
  by eapply CpoIN in H0; eauto with caccess; desf; eauto 12 with caccess;
     destruct (lab c).
Qed.

Lemma ConsistentTSOalt_hb :
  ∀ acts lab sb rf mo (C : ConsistentTSOalt acts lab sb rf mo) a b
    (HB : clos_trans (fun a b ⇒ mo a b ∨ sb a b ∧ is_read (lab a)
                                ∨ rf b = Some a ∧ ¬ sb a b) a b)
    (W : is_write (lab a)),
  happens_before sb rf a b ∨
  mo a b ∨
  (∃ m : actid, mo a m ∧ rf b = Some m ∧ ¬ sb m b) ∨
  (∃ m n : actid, mo a m ∧ rf n = Some m ∧ ¬ sb m n ∧ sb n b) ∨
  (∃ m : actid, mo a m ∧ is_rmw (lab m) ∧ sb m b).
Proof.
  ins; assert (K:=C); red in K; desc.
  assert (AA: acyclic (fun a b ⇒
          mo a b ∨
          sb a b ∧ is_read (lab a) ∨ rf b = Some a ∧ ¬ sb a b)).
    by intros ? H; eapply clos_trans_mon with
         (r' := fun a b ⇒ (sb a b ∨ rf b = Some a) ∨ mo a b) in H;
       ins; desf; eauto; eapply cycle_utd in H; eauto; desf; eauto.

  apply clos_trans_tn1 in HB.
  induction HB; [by desf; eauto with hb|].
  apply clos_tn1_trans in HB.
  case_eq (is_write (lab z)) as Wz.
    destruct (eqP a z) as [|NEQ].
      by subst; exfalso; eauto using clos_trans.
    apply CmoF in NEQ; eauto; destruct NEQ; eauto.
    by subst; exfalso; eauto 8 using clos_trans.

  destruct H; [by eapply CmoD in H; desf|].
  desf; eauto with hb; eauto 12.

  by assert (is_rmw (lab y)); [by apply CmoD in IHHB; desc; destruct (lab y)|eauto 8].

  destruct (eqP a y) as [|NEQ]; subst; [by exfalso; eauto|].
  exploit CrfD; try exact H; ins; desc.
  by eapply CmoF in NEQ; eauto with caccess; desf; eauto 10; exfalso; eauto using clos_trans.

  destruct (eqP a y) as [|NEQ]; subst; [by exfalso; eauto|].
  exploit CrfD; try exact H; ins; desc.
  by eapply CmoF in NEQ; eauto with caccess; desf; eauto 10; exfalso; eauto using clos_trans.

  destruct (eqP a y) as [|NEQ]; subst; [by exfalso; eauto|].
  exploit CrfD; try exact H; ins; desc.
  by eapply CmoF in NEQ; eauto with caccess; desf; eauto 10; exfalso; eauto using clos_trans.
Qed.

Theorem ConsistentTSO_alt1 :
  ∀ acts lab sb rf tso (C : ConsistentTSO acts lab sb rf tso),
    ConsistentTSOalt acts lab sb rf (restr_rel (fun x ⇒ is_write (lab x)) tso).
Proof.
  ins; assert (K:=C); red in K; red; desc; unnw; intuition;
  eauto using is_total_restr, restr_rel_trans, restr_rel;
    red; unfold restr_rel; ins; desf; eauto.
  {
    case_eq (is_access (lab x)) as A.
      by eapply ConsistentTSO_hb in H; eauto; desf; eauto.
    eapply ConsistentTSO_hb_no_access in H; eauto; desf; eauto.
    destruct (lab x); ins.
    exploit (CpoIN d c); eauto with caccess; ins; desf; eauto.
    destruct (lab c); ins.
  }
  by eapply ConsistentTSO_hb in HB; eauto with caccess;
     desf; eauto; destruct (lab b).
  by exploit CrfD; eauto; ins; desc;
     eapply ConsistentTSO_hb in HB; desf; eauto with caccess.
  by exploit CrfD; try exact RF; ins; desc; exploit CrfD; try exact HB0; ins; desc;
     eapply CpoIN in HB2; desf; eauto with caccess;
     [|by apply CrfD in HB0; desc; destruct (lab n)];
     eapply CrfIN in HB0; desf; eauto.
  by exploit CrfD; try exact RF; ins; desc; eapply CpoIN in HB1; desf;
     eauto with caccess; destruct (lab m).
Qed.

Theorem ConsistentTSO_alt2 :
  ∀ acts lab sb rf mo (C : ConsistentTSOalt acts lab sb rf mo),
    ConsistentTSO acts lab sb rf
      (clos_trans (fun a b ⇒ mo a b ∨ sb a b ∧ is_read (lab a)
                              ∨ rf b = Some a ∧ ¬ sb a b)).
Proof.
  ins; assert (K:=C); red in K; red; desc; unnw.

  assert (AA: acyclic (fun a b ⇒
          mo a b ∨
          sb a b ∧ is_read (lab a) ∨ rf b = Some a ∧ ¬ sb a b)).
    by intros ? H; eapply clos_trans_mon with
         (r' := fun a b ⇒ (sb a b ∨ rf b = Some a) ∨ mo a b) in H;
       ins; desf; eauto; eapply cycle_utd in H; eauto; desf; eauto.

  repeat (split; try done); try red; ins; eauto using clos_trans with hb.
  by apply CmoF in NEQ; desf; eauto using clos_trans.
  { case_eq (is_write_only (lab a)) as Wa; [|by left; apply t_step; destruct (lab a); ins; vauto].
    case_eq (is_write (lab b)) as Wb; [|by right; split; ins; destruct (lab b); ins].
    destruct (eqP a b) as [|NEQ]; [by exfalso; desf; eauto with hb|].
    by eapply CmoF in NEQ; desf; eauto using clos_trans; try (by destruct (lab a));
       exfalso; eauto with hb.
  }
  by destruct (classic (sb a b)); eauto 6 using clos_trans.

  exploit CrfD; eauto; ins; desc.
  destruct (eqP a b) as [|NEQ]; [by desf; eauto with hb|].
  eapply CmoF in NEQ; eauto with caccess.
  desf; eauto using clos_trans with hb.
  eapply Cwr; eauto.

  eapply ConsistentTSOalt_hb in HB; desf; eauto 10.
  exfalso; eauto.
Qed.

Theorem ConsistentTSO_alternative :
  ∀ acts lab sb rf,
    (∃ tso, ConsistentTSO acts lab sb rf tso) ↔
    (∃ mo, ConsistentTSOalt acts lab sb rf mo).
Proof.
  split; ins; desf; eauto using ConsistentTSO_alt1, ConsistentTSO_alt2.
Qed.

Definition tso_protected_events lab sb rf (B : actid → Prop) :=
  << PhbF : is_total B (happens_before sb rf) >> ∧
  << Prace: ∀ a b (RACE: races_with lab sb rf a b), B a ∨ B b >> ∧
  << Prfe : ∀ a b (RF: rf b = Some a) (NPO: ¬ sb a b), B a ∨ B b >>.

Theorem tso_protected_sc_reduction :
  ∀ acts lab sb rf mo
    (CONS: ConsistentRA acts lab sb rf mo)
    (WF: wellformed_fences lab sb)
    (NOUPD: ∀ a, ¬ is_rmw (lab a))
    (NOWW: no_ww_races lab sb rf) B
    (PR: tso_protected_events lab sb rf B),
  ∃ tso, ConsistentTSO acts lab sb rf tso.
Proof.
  ins; eapply ConsistentTSO_alternative.
  assert (KK := CONS); red in KK; desc.

  assert (A: acyclic
     (pref_union (happens_before sb rf)
        (fun x y : actid ⇒
         B x ∧ is_read (lab x) ∧ is_write (lab y) ∧ ¬ B y))).
    by red in PR; desc; eapply acyclic_pref_union with (dom:=B);
       try red; ins; desc; eauto with hb.

  assert (A': acyclic
     (fun x y ⇒ happens_before sb rf x y
                 ∨ B x ∧ ∃ d, rf x = Some d ∧ mo d y)).
    eapply acyclic_mon; eauto.
    repeat red; ins; desf; eauto.
    destruct (classic (B y)).
      destruct (eqP x y) as [|N]; [|eapply PR in N]; desf; eauto with hb.
      by exploit CmoD; eauto; exploit CrfD; eauto; ins; desc;
         destruct (NOUPD y), (lab y).
      by exfalso; eauto with hb.
    by exploit CmoD; eauto; exploit CrfD; eauto; ins; desc;
       right; repeat split; eauto with caccess.
  clear A.

  assert (HBI: ∀ a b,
      tot_ext acts
     (fun x y ⇒ happens_before sb rf x y
                 ∨ B x ∧ ∃ d, rf x = Some d ∧ mo d y) a b →
      is_write (lab a) →
      is_write (lab b) →
      loc (lab a) = loc (lab b) →
      happens_before sb rf a b).
    ins; destruct (eqP a b) as [|N]; [|eapply NOWW in N]; desf; eauto.
      by edestruct tot_ext_irr; eauto.
      by exfalso; eapply tot_ext_irr, tot_ext_trans; eauto;
         apply tot_ext_extends; vauto.
      by instantiate (1 := loc (lab a)); destruct (lab a).
      by destruct (lab b); ins; desf.

  ∃ (restr_rel (fun x ⇒ is_write (lab x))
            (tot_ext acts (fun x y ⇒ happens_before sb rf x y
                             ∨ B x ∧ ∃ d, rf x = Some d ∧ mo d y))).

  red; unnw; intuition.

  by unfold restr_rel; red; ins; desf.

  by eapply is_total_restr; red; ins; eapply tot_ext_total; ins;
     apply FIN; intro X; rewrite X in ×.

  by eapply restr_rel_trans, tot_ext_trans.

  by unfold restr_rel; red; ins; desc; eapply tot_ext_irr in H.

  by unfold restr_rel; red; ins; desc;
     eapply tot_ext_irr, tot_ext_trans, MO; ins;
     apply tot_ext_extends; vauto.

  unfold restr_rel; red; ins; desf; eauto.
    by eapply HBI in TSO; eauto;
       eapply Cwr; eauto; eapply hb_mo; eauto.

  by eapply CrfD in RF; desc; apply (NOUPD c); destruct (lab c).

    eapply HBI in TSO; eauto.
    assert (mo a b) by (eapply hb_mo; eauto).
    assert (¬ B c).
      intro; eapply tot_ext_irr, tot_ext_trans, HB; eauto.
      eapply tot_ext_trans, tot_ext_trans; eauto 6 using tot_ext_extends with hb.
    assert (J: ¬ happens_before sb rf b c) by eauto.
    destruct(classic (happens_before sb rf c b)).
      eapply tot_ext_irr, tot_ext_trans, HB; eauto.
      by eapply tot_ext_trans, tot_ext_trans; eauto 6 using tot_ext_extends with hb.

    assert (R: races_with lab sb rf b c).
      generalize (CrfD _ _ RF); exploit loceq_rf; try exact RF; eauto; ins; desc.
      red; unnw; repeat split; try done; eauto 2 with caccess; try congruence.
      by intro; desf; eapply (NOUPD c); destruct (lab c).
    apply PR in R; desf.

    apply PR in HB1; desf.
    destruct (eqP b m) as [|N]; [|eapply PR in N]; desf.
      by eapply tot_ext_irr, HB.
      by destruct J; eauto with hb.
      by eapply tot_ext_irr, tot_ext_trans, HB; eauto using tot_ext_extends.

    destruct (eqP b n) as [|N]; [|eapply PR in N]; desf.
      by eapply tot_ext_irr, tot_ext_trans, HB; eauto using tot_ext_extends with hb.
      by destruct J; eauto with hb.
      by eapply tot_ext_irr, tot_ext_trans, tot_ext_trans, HB;
         eauto using tot_ext_extends with hb.
Qed.