Require Import Classical List Permutation Relations Peano_dec Setoid Omega.
Require Import Vbase extralib ExtraRelations cactions WMModels SCresults.
Set Implicit Arguments.
Remove Hints plus_n_O.

Proposition ModelSRA_RA lab sb rf mo :
  ModelSRA lab sb rf mo →
  ModelRA lab sb rf (restr_eq_rel (fun x ⇒ loc (lab x)) mo).
Proof.
  unfold ModelSRA, ModelRA; ins; desf; unnw; rewrite irreflexive_restr_eq.
  intuition; eauto using transitive_restr_eq, ConsistentMO_dom_restr_eq,
                         is_total_restr_eq;
   try (by rewrite inclusion_restr_eq).
Qed.

Lemma ModelSRA_ac lab sb rf mo :
  ModelSRA lab sb rf mo →
  acyclic (sb +++ rf_external sb rf +++ mo).
Proof.
  unfold ModelSRA; ins; desf.
  intros x H; eapply cycle_utd in H; eauto; desf; unfold seq in *; eauto.
Qed.

Lemma inclusion_hb_tot_ext_nat sb rf mo :
  inclusion (happens_before sb rf)
            (tot_ext_nat (sb +++ rf_external sb rf +++ mo)).
Proof.
  unfold inclusion, union, rf_external; ins.
  eapply clos_trans_of_transitive, (clos_trans_mon _ H);
  eauto using tot_ext_nat_trans; ins; eapply tot_ext_nat_extends; desf; eauto.
Qed.

Lemma ModelSRA_alt2 lab sb rf mo
  (C: ModelRA lab sb rf mo)
  (A: acyclic (sb +++ rf_external sb rf +++ mo)) :
  ∃ mo',
    inclusion mo mo' ∧
    ModelSRA lab sb rf mo'.
Proof.
  unfold ModelRA, ModelSRA in *; desf; unnw.
  ∃ (restr_rel (fun x ⇒ is_write (lab x))
                    (tot_ext_nat (sb +++ rf_external sb rf +++ mo)));
    intuition; unfold inclusion, ConsistentMO_big_dom, is_total, transitive;
      ins; desf; repeat match goal with H : restr_rel _ _ _ _ |- _ ⇒ red in H
                                  | |- restr_rel _ _ _ _ ⇒ red end; intuition;
        try (by unfold union; eauto using tot_ext_nat_extends);
        try (by eapply CmoD in H; desf; eauto with caccess).
    by unfold restr_rel; eapply tot_ext_nat_total in NEQ; desf; eauto.
   eby eapply tot_ext_nat_trans.
   eby unfold restr_rel; red; ins; desf; eapply tot_ext_nat_irr.
   by eapply irreflexive_inclusion, tot_ext_nat_irr; eauto;
      eapply inclusion_seq_trans; eauto using tot_ext_nat_trans,
                                  inclusion_hb_tot_ext_nat with inclusion.

   unfold seq, reads_before, restr_rel in *; intros x X; desf.
   exploit CrfD; eauto; intro; desc.
   assert (l0 = l) by (destruct (lab x); ins; desf); subst.
   destruct (eqP z z0) as [|NEQ]; desf; [eby eapply tot_ext_nat_irr|].
   eapply CmoF with (l := l) in NEQ; desf; eauto with caccess.
     by eapply tot_ext_nat_irr, tot_ext_nat_trans, tot_ext_nat_extends; eauto; vauto.
   by eapply Cwr; repeat eexists; eauto.

   unfold seq, reads_before, restr_rel in *; intros x X; desf.
   exploit CrfD; eauto; intro; desc.
   assert (l0 = l) by (destruct (lab x); ins; desf); subst.
   destruct (eqP z z0) as [|NEQ]; desf; [eby eapply tot_ext_nat_irr|].
   eapply CmoF with (l := l) in NEQ; desf; eauto with caccess.
     by eapply tot_ext_nat_irr, tot_ext_nat_trans with z, tot_ext_nat_extends;
        eauto; vauto.
   assert (N: x ≠ z) by done.
   eapply CmoF with (l := l) in N; desf; eauto with caccess.
     by eapply tot_ext_nat_irr, tot_ext_nat_trans with x, tot_ext_nat_extends;
        eauto; vauto.
   eapply Cat; repeat eexists; eauto with caccess.
   by destruct (lab x); ins.
Qed.

Theorem ModelSRA_alt lab sb rf :
  (∃ mo, ModelSRA lab sb rf mo) ↔
  (∃ mo, ModelRA lab sb rf mo ∧
              acyclic (sb +++ rf_external sb rf +++ mo)).
Proof.
  split; ins; desf.
    eexists; split; eauto using ModelSRA_RA.
    eapply acyclic_mon; [by eapply ModelSRA_ac; eauto|].
    red; unfold union, restr_eq_rel; ins; desf; eauto.
  edestruct ModelSRA_alt2; desf; eauto.
Qed.

Definition no_ww_races lab sb rf :=
  ∀ a l (Wa: is_writeL (lab a) l) b (Wb: is_writeL (lab b) l) (NEQ: a ≠ b) ,
    happens_before sb rf a b ∨ happens_before sb rf b a.

Theorem ModelRA_no_ww_races :
  ∀ lab sb rf (NORACE: no_ww_races lab sb rf),
  (∃ mo, ModelSRA lab sb rf mo) ↔
  (∃ mo, ModelRA lab sb rf mo).
Proof.
  ins; rewrite ModelSRA_alt; split; ins; desf; ∃ mo; intuition.
  red in H; desc; eapply acyclic_mon; [eapply (trans_irr_acyclic ChbI); vauto|].
  unfold union; red; ins; desf; vauto.
  edestruct CmoD; eauto; desf.
  destruct (eqP x y) as [|NEQ]; desf; [exfalso; eauto|].
  eapply NORACE in NEQ; desf; eauto with caccess.
  edestruct Cww; vauto.
Qed.