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 : actid → option 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 y ⇒ happens_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 y ⇒ happens_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 x ⇒ is_accessL (lab x) l ∨ ¬ is_access (lab x))
(fun x y ⇒ happens_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 y ⇒ happens_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 y ⇒ happens_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 x ⇒ is_accessL (lab x) l ∨ ¬ is_access (lab x))
(fun x y ⇒ happens_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 y ⇒ happens_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 y ⇒ happens_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 y ⇒ happens_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.
Lemma cycle_hbcom_rev :
∀ mt2 lab sb asw rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
(T: acyclic
(fun x y ⇒ happens_before mt2 lab sb asw rf mo x y
∧ loc (lab x) = loc (lab y)
∨ com rf mo x y)),
≪ 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 ≫.
In total, we show that the Coherence axiom is equivalent to the
conjunction of the other six axioms, assuming ConsistentRF and ConsistentMO
both hold.
Theorem Coherence_alt :
∀ mt2 lab sb asw rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo),
Coherence mt2 lab sb asw rf 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 ≫.
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.
This page has been generated by coqdoc