# Alternative coherence axioms

Require Import List Vbase Relations ExtraRelations actions c11.
Set Implicit Arguments.

We start with some lemmas showing that small cycles involving happens-before and mo/sc/rf cannot occur in a consistent execution.

Lemma cycle_hbmo :
mt2 lab sb asw rf mo (Cmo: ConsistentMO lab mo)
(Chbmo: ConsistentMOhb mt2 lab sb asw rf mo) x y
(MO: mo x y) (HB: happens_before mt2 lab sb asw rf mo y x),
False.

Lemma cycle_hbsc :
mt2 lab sb asw rf mo sc (Csc: ConsistentSC mt2 lab sb asw rf mo sc) x y
(SC: sc x y) (HB: happens_before mt2 lab sb asw rf mo y x),
False.

Lemma cycle_hbrf :
mt2 lab sb asw rf mo (CrfH: ConsistentRFhb mt2 lab sb asw rf mo) x y
(RF: rf y = Some x) (HB: happens_before mt2 lab sb asw rf mo y x),
False.

Lemma cycle_hbfr :
mt2 lab sb asw rf mo
(Cwr: CoherentWR mt2 lab sb asw rf mo) x y
(RF: rf y = Some x) z (MO: mo x z)
(HB: happens_before mt2 lab sb asw rf mo z y),
False.

Lemma cycle_rf :
lab rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
(Crmw: AtomicRMW lab rf mo) b
(T: rf b = Some b),
False.

The first theorem states that the CoherentWW axiom is equivalent to the ConsistentMOhb axiom.

Theorem CoherentWW_eq_ConsistentMOhb :
mt2 lab sb asw rf mo
(IRR: irreflexive (happens_before mt2 lab sb asw rf mo))
(Cmo: ConsistentMO lab mo),
CoherentWW mt2 lab sb asw rf mo ConsistentMOhb mt2 lab sb asw rf mo.

In the remainder of this section, we work towards the main theorem of this file, namely that the Coherence axiom is equivalent to the conjunction of the six other axioms.

Definition is_accessLminusRfNone lab (rf : actidoption actid) l (x : actid) :=
is_writeL (lab x) l
is_readL (lab x) l ¬ is_writeL (lab x) l rf x None.

Lemma is_accessL_split :
a l,
is_accessL a l
is_writeL a l is_readL a l ¬ is_writeL a l.

Lemma is_accessL_com1 :
lab rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo) x y
(C: com rf mo x y) l
(A: is_accessL (lab x) l),
is_accessLminusRfNone lab rf l x.

Lemma is_accessL_com2 :
lab rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo) x y
(C: com rf mo x y) l
(A: is_accessL (lab y) l),
is_accessLminusRfNone lab rf l y.

Lemma is_rmw_rfmo1 :
lab rf
(Crf: ConsistentRF lab rf) mo
(Cmo: ConsistentMO lab mo)
x y (RF: rf x = Some y)
z (MO: mo x z),
is_rmw (lab x).

Lemma is_rmw_rfmo2 :
lab rf
(Crf: ConsistentRF lab rf) mo
(Cmo: ConsistentMO lab mo)
x y (RF: rf x = Some y)
z (MO: mo z x),
is_rmw (lab x).

Lemma is_rmw_rfrf :
lab rf
(Crf: ConsistentRF lab rf)
x y (RF: rf x = Some y)
z (RF': rf z = Some x),
is_rmw (lab x).

Lemma is_rmw_rfmo3 :
lab rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
(Crmw : AtomicRMW lab rf mo)
x y (RF: rf x = Some y)
z (MO: mo z x),
mo z y z = y.

Lemma path_com :
lab rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
(Crmw: AtomicRMW lab rf mo) a b
(T: clos_trans _ (com rf mo) a b),
mo a b
rf b = Some a
( z, mo a z rf b = Some z)
( z, rf a = Some z mo z b a b)
( z w, rf a = Some z mo z w rf b = Some w).

Lemma cycle_com :
lab rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
(Crmw: AtomicRMW lab rf mo) a
(T: clos_trans _ (com rf mo) a a),
False.

Lemma path_hbcom_restrLminusRfNone :
mt2 lab sb asw rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
(CmoH: ConsistentMOhb mt2 lab sb asw rf mo)
(CrfH: ConsistentRFhb mt2 lab sb asw rf mo)
(Crr: CoherentRR mt2 lab sb asw rf mo)
(Crw: CoherentRW mt2 lab sb asw rf mo)
(Cwr: CoherentWR mt2 lab sb asw rf mo)
(Crmw: AtomicRMW lab rf mo) l a b
(T: clos_trans _
(restr_rel (is_accessLminusRfNone lab rf l)
(fun x yhappens_before mt2 lab sb asw rf mo x y
com rf mo x y)) a b),
restr_rel (is_accessLminusRfNone lab rf l)
(fun a b
( z w,
¬ is_writeL (lab a) l ¬ is_writeL (lab b) l
happens_before mt2 lab sb asw rf mo a b
rf a = Some z is_writeL (lab z) l
rf b = Some w is_writeL (lab w) l)
(is_writeL (lab a) l is_writeL (lab b) l mo a b)
(is_writeL (lab a) l ¬ is_writeL (lab b) l rf b = Some a)
( z, is_writeL (lab a) l ¬ is_writeL (lab b) l
mo a z rf b = Some z is_writeL (lab z) l)
( z, ¬ is_writeL (lab a) l is_writeL (lab b) l
rf a = Some z mo z b is_writeL (lab z) l)
( z w, ¬ is_writeL (lab a) l ¬ is_writeL (lab b) l
rf a = Some z mo z w rf b = Some w
is_writeL (lab z) l
is_writeL (lab w) l)) a b.

Lemma cycle_hbcom_restrLminusRfNone :
mt2 lab sb asw rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
(IRR: irreflexive (happens_before mt2 lab sb asw rf mo))
(CmoH: ConsistentMOhb mt2 lab sb asw rf mo)
(CrfH: ConsistentRFhb mt2 lab sb asw rf mo)
(Crr: CoherentRR mt2 lab sb asw rf mo)
(Crw: CoherentRW mt2 lab sb asw rf mo)
(Cwr: CoherentWR mt2 lab sb asw rf mo)
(Crmw: AtomicRMW lab rf mo) l a
(T: clos_trans _
(restr_rel (is_accessLminusRfNone lab rf l)
(fun x yhappens_before mt2 lab sb asw rf mo x y
com rf mo x y)) a a),
False.

Lemma path_hbcom1 :
mt2 lab sb asw rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
(IRR: irreflexive (happens_before mt2 lab sb asw rf mo))
(CmoH: ConsistentMOhb mt2 lab sb asw rf mo)
(CrfH: ConsistentRFhb mt2 lab sb asw rf mo)
(Crr: CoherentRR mt2 lab sb asw rf mo)
(Crw: CoherentRW mt2 lab sb asw rf mo)
(Cwr: CoherentWR mt2 lab sb asw rf mo)
(Crmw: AtomicRMW lab rf mo) l a b
(T: clos_trans _
(restr_rel (fun xis_accessL (lab x) l ¬ is_access (lab x))
(fun x yhappens_before mt2 lab sb asw rf mo x y com rf mo x y)) a b),
happens_before mt2 lab sb asw rf mo a b
c d,
(a = c happens_before mt2 lab sb asw rf mo a c)
clos_trans _
(restr_rel (is_accessLminusRfNone lab rf l)
(fun x yhappens_before mt2 lab sb asw rf mo x y com rf mo x y)) c d
(d = b happens_before mt2 lab sb asw rf mo d b).

Lemma path_hbcom2 :
mt2 lab sb asw rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo) a b
(T: clos_trans _
(fun x yhappens_before mt2 lab sb asw rf mo x y
loc (lab x) = loc (lab y)
com rf mo x y) a b),
l, clos_trans _
(restr_rel (fun xis_accessL (lab x) l ¬ is_access (lab x))
(fun x yhappens_before mt2 lab sb asw rf mo x y
com rf mo x y)) a b.

Lemma path_hbcom :
mt2 lab sb asw rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
(IRR: irreflexive (happens_before mt2 lab sb asw rf mo))
(CmoH: ConsistentMOhb mt2 lab sb asw rf mo)
(CrfH: ConsistentRFhb mt2 lab sb asw rf mo)
(Crr: CoherentRR mt2 lab sb asw rf mo)
(Crw: CoherentRW mt2 lab sb asw rf mo)
(Cwr: CoherentWR mt2 lab sb asw rf mo)
(Crmw: AtomicRMW lab rf mo) a b
(T: clos_trans _
(fun x yhappens_before mt2 lab sb asw rf mo x y
loc (lab x) = loc (lab y)
com rf mo x y) a b),
happens_before mt2 lab sb asw rf mo a b
l c d,
(a = c happens_before mt2 lab sb asw rf mo a c)
clos_trans _
(restr_rel (is_accessLminusRfNone lab rf l)
(fun x yhappens_before mt2 lab sb asw rf mo x y
com rf mo x y)) c d
(d = b happens_before mt2 lab sb asw rf mo d b).

Packaging everything to get the one direction of the equivalence theorem.

Lemma cycle_hbcom :
mt2 lab sb asw rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
(IRR: irreflexive (happens_before mt2 lab sb asw rf mo))
(CmoH: ConsistentMOhb mt2 lab sb asw rf mo)
(CrfH: ConsistentRFhb mt2 lab sb asw rf mo)
(Crr: CoherentRR mt2 lab sb asw rf mo)
(Crw: CoherentRW mt2 lab sb asw rf mo)
(Cwr: CoherentWR mt2 lab sb asw rf mo)
(Crmw: AtomicRMW lab rf mo) a
(T: clos_trans _
(fun x yhappens_before mt2 lab sb asw rf mo x y
loc (lab x) = loc (lab y)
com rf mo x y) a a),
False.

The other direction is actually much easier to show.
In total, we show that the Coherence axiom is equivalent to the conjunction of the other six axioms, assuming ConsistentRF and ConsistentMO both hold.
As a corollary of the previous theorem, the two different consistency formulations are equivalent.

Corollary Consistent_alt :
mt mt2 mtsc acts lab sb dsb asw rf mo sc,
Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc
ConsistentAlt mt mt2 mtsc acts lab sb dsb asw rf mo sc.

Corollary Semiconsistent_alt :
mt mt2 mtsc acts lab sb dsb asw rf mo sc,
Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc
SemiconsistentAlt mt mt2 mtsc acts lab sb dsb asw rf mo sc.