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

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).

Lemma ModelSRA_ac lab sb rf mo :
  ModelSRA lab sb rf mo →
  acyclic (sb +++ rf_external sb rf +++ mo).

Lemma inclusion_hb_tot_ext_nat sb rf mo :
  inclusion (happens_before sb rf)
            (tot_ext_nat (sb +++ rf_external sb rf +++ mo)).

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'.

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)).

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).