# Results about RA and SRA

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

SRA-coherence is stronger than RA-coherence.

Proposition ModelSRA_RA lab sb rf mo :
ModelSRA lab sb rf mo
ModelRA lab sb rf (restr_eq_rel (fun xloc (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'.

SRA-coherence is equivalent to RA-coherence plus acyclicity po U rf U 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)).

In the absence of WW-races, SRA-coherence and RA-coherence coincide.

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