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 :
forall 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.
Proof.
unfold ConsistentMO; ins; desf.
edestruct (CmoD _ _ MO); desf.
eapply Chbmo in HB; eauto.
Qed.
Lemma cycle_hbsc :
forall 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.
Proof.
unfold ConsistentSC; ins; desf.
edestruct (CscD _ _ SC); desf.
eapply Chbsc in HB; eauto.
Qed.
Lemma cycle_hbrf :
forall 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.
Proof.
ins; eapply CrfH in RF; desf.
Qed.
Lemma cycle_hbfr :
forall 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.
Proof.
ins; eapply Cwr; try eassumption.
Qed.
Lemma cycle_rf :
forall lab rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
(Crmw: AtomicRMW lab rf mo) b
(T: rf b = Some b),
False.
Proof.
ins; exploit Crf; eauto; ins; desf.
eapply Crmw, proj1 in T; try eapply Cmo; eauto.
destruct (lab b); ins.
Qed.
The first theorem states that the CoherentWW axiom is equivalent to the
ConsistentMOhb axiom.
Theorem CoherentWW_eq_ConsistentMOhb :
forall 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.
Proof.
split; repeat red; ins; eauto using cycle_hbmo.
destruct (eqP a b) as [|N]; desf.
by exfalso; eauto.
by eapply Cmo in N; eauto; desf; exfalso; eauto.
Qed.
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 :
forall a l,
is_accessL a l ->
is_writeL a l \/ is_readL a l /\ ~ is_writeL a l.
Proof.
destruct a; ins; vauto.
Qed.
Lemma is_accessL_com1 :
forall 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.
Proof.
unfold com; red; ins; desf; rewrite ?C.
by eapply (proj1 Cmo) in C; desf; destruct (lab x); ins; eauto.
by left; eapply Crf in C; desf; destruct (lab x); ins.
by eapply Crf in C; desf;
destruct (lab x); ins; desf; econstructor (econstructor (by vauto)).
Qed.
Lemma is_accessL_com2 :
forall 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.
Proof.
unfold com; red; ins; desf; rewrite ?C.
by eapply (proj1 Cmo) in C; desf; destruct (lab y); ins; eauto.
by eapply Crf in C; desf;
destruct (lab y); ins; desf; econstructor (econstructor (by vauto)).
by eapply (proj1 Cmo) in C0; desf; destruct (lab y); ins; eauto.
Qed.
Lemma is_rmw_rfmo1 :
forall 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).
Proof.
ins; apply Crf in RF;
apply (proj1 Cmo) in MO; desf; destruct (lab x); ins.
Qed.
Lemma is_rmw_rfmo2 :
forall 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).
Proof.
ins; apply Crf in RF;
apply (proj1 Cmo) in MO; desf; destruct (lab x); ins.
Qed.
Lemma is_rmw_rfrf :
forall lab rf
(Crf: ConsistentRF lab rf)
x y (RF: rf x = Some y)
z (RF': rf z = Some x),
is_rmw (lab x).
Proof.
ins; apply Crf in RF; apply Crf in RF'; desf; destruct (lab x); ins.
Qed.
Lemma is_rmw_rfmo3 :
forall 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.
Proof.
ins; destruct (eqP z y) as [|NEQ]; eauto; left.
generalize (proj1 Cmo _ _ MO), (Crf _ _ RF); ins; desf.
assert (l0 = l) by (destruct (lab x); ins; desf); subst.
eapply Cmo in NEQ; desf; eauto.
by exfalso; eapply Crmw, proj2 in RF; eauto using is_rmw_rfmo2.
by destruct (lab y); ins; desf.
Qed.
Lemma path_com :
forall 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 \/
(exists z, mo a z /\ rf b = Some z) \/
(exists z, rf a = Some z /\ mo z b /\ a <> b) \/
(exists z w, rf a = Some z /\ mo z w /\ rf b = Some w).
Proof.
unfold com; ins; dupdes Cmo.
induction T; ins; desf; eauto 14; clear T1 T2;
try (match goal with
| H : rf _ = _ |- _ => by eapply Crmw, proj1 in H;
eauto 14 using is_rmw_rfmo1, is_rmw_rfmo2, is_rmw_rfrf
end).
destruct (eqP x z); desf; eauto 10.
by exfalso; eapply Crmw, proj2 in IHT1; eauto 8 using is_rmw_rfmo1, is_rmw_rfmo2, is_rmw_rfrf.
eapply Crmw, proj1 in IHT3; eauto 8 using is_rmw_rfmo1, is_rmw_rfmo2, is_rmw_rfrf.
destruct (eqP x z); desf; eauto 10.
by exfalso; eapply Crmw, proj2 in IHT1; eauto 8 using is_rmw_rfmo1, is_rmw_rfmo2, is_rmw_rfrf.
destruct (eqP x z); desf; eauto 10.
by exfalso; eapply Crmw, proj2 in IHT2;
eauto 14 using is_rmw_rfmo1, is_rmw_rfmo2, is_rmw_rfrf.
generalize (CmoD _ _ IHT1), (CmoD _ _ IHT0), (Crf _ _ IHT2); ins; desf.
assert (l1 = l) by (destruct (lab y); ins; desf); desf.
assert (l0 = l) by (destruct (lab z0); ins; desf); desf.
eapply CmoF in n; desf; eauto 10.
by exfalso; eapply Crmw, proj2 in IHT2;
eauto 14 using is_rmw_rfmo1, is_rmw_rfmo2, is_rmw_rfrf.
{
generalize (Crf _ _ IHT1), (CmoD _ _ IHT4), (CmoD _ _ IHT0), (Crf _ _ IHT2); ins; desf.
assert (l0 = l) by (destruct (lab z0); ins; desf); desf.
assert (l1 = l) by (destruct (lab y); ins; desf); desf.
assert (l2 = l) by (destruct (lab z1); ins; desf); desf.
eapply Crmw in IHT2; eauto using is_rmw_rfmo1, is_rmw_rfmo2, is_rmw_rfrf;
red in IHT2; desc.
eapply CmoF in IHT3; eauto; desf; try solve[exfalso; eauto].
destruct (eqP x z); desf; eauto 10.
by exfalso; eapply Crmw, proj2 in IHT1; eauto 8 using is_rmw_rfmo1, is_rmw_rfmo2, is_rmw_rfrf.
}
destruct (eqP x z); desf; eauto 10.
by exfalso; eapply Crmw, proj2 in IHT1; eauto 8 using is_rmw_rfmo1, is_rmw_rfmo2, is_rmw_rfrf.
by eapply (is_rmw_rfmo3 Crf Cmo) in IHT2; eauto; desf; eauto 10.
by eapply (is_rmw_rfmo3 Crf Cmo) in IHT2; eauto; desf; eauto 10.
Qed.
Lemma cycle_com :
forall 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.
Proof.
ins; dupdes Cmo; eapply path_com in T; eauto; desf; eauto.
eby eapply cycle_rf.
by eapply Crmw, proj1 in T0; eauto using is_rmw_rfmo1.
Qed.
Lemma path_hbcom_restrLminusRfNone :
forall 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 =>
(exists 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) \/
(exists z, is_writeL (lab a) l /\ ~ is_writeL (lab b) l /\
mo a z /\ rf b = Some z /\ is_writeL (lab z) l) \/
(exists z, ~ is_writeL (lab a) l /\ is_writeL (lab b) l /\
rf a = Some z /\ mo z b /\ is_writeL (lab z) l) \/
(exists 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.
Proof.
unfold is_accessLminusRfNone, com; ins; dupdes Cmo.
induction T; ins.
{
red in H; desc; repeat split; ins; desf; eauto 10.
by eapply CmoH in H; eauto.
by eapply Crmw, proj1 in H; eauto; eapply Crf in H; desc; destruct (lab y); ins.
by eapply CmoF in H3; desf; eauto;
exfalso; eapply Crmw, proj2 in H; eauto;
eapply Crf in H; desc; destruct (lab x); ins.
by case_eq (rf x) as RF;
assert (is_writeL (lab a) l)
by (apply Crf in RF; desf; destruct (lab x); ins; desf;
destruct (lab a); ins; desf);
destruct (eqP y a); desf; [by eapply CrfH in RF|];
eapply CmoF in n; desf; try edone;
try (by exfalso; eauto); eauto 16.
by exfalso; eapply CmoD in H; desf; destruct (lab x); ins.
by exfalso; eapply Crf in H; desf; destruct (lab x); ins.
by assert (is_writeL (lab z) l)
by (apply Crf in H; desf; destruct (lab x); ins; desf;
destruct (lab z); ins; desf); eauto 14.
by case_eq (rf y) as RF;
assert (is_writeL (lab a) l)
by (apply Crf in RF; desf; destruct (lab y); ins; desf;
destruct (lab a); ins; desf);
destruct (eqP x a); desf; eauto 10;
eapply CmoF in n; desf; try edone;
try (by exfalso; eauto); eauto 16.
by exfalso; eapply CmoD in H; desf; destruct (lab y); ins.
by exfalso; eapply CmoD in H4; desf; destruct (lab y); ins.
by case_eq (rf x) as RF;
assert (is_writeL (lab a) l)
by (apply Crf in RF; desf; destruct (lab x); ins; desf;
destruct (lab a); ins; desf);
case_eq (rf y) as RF';
assert (is_writeL (lab a0) l)
by (apply Crf in RF'; desf; destruct (lab y); ins; desf;
destruct (lab a0); ins; desf); eauto 10.
by exfalso; eapply CmoD in H; desf; destruct (lab x); ins.
by exfalso; eapply Crf in H; desf; destruct (lab x); ins.
by exfalso; eapply CmoD in H6; desf; destruct (lab y); ins.
}
clear T1 T2.
destruct IHT1 as (T & A1 & A2).
destruct IHT2 as (S & _ & A3).
repeat split; ins.
clear A1 A2 A3.
desf; eauto 16.
eauto 14 using hb_trans.
by destruct (eqP x w); desf; eauto 14;
eapply CmoF in n; desf; try edone;
try (by exfalso; eauto); eauto 16.
by destruct (eqP z1 w); desf; eauto 14;
eapply CmoF in n; desf; try edone;
try (by exfalso; eauto); eauto 16.
by destruct (eqP w0 w); desf; eauto 14;
eapply CmoF in n; desf; try edone;
try (by exfalso; eauto); eauto 16.
by destruct (eqP z1 w); desf; eauto 14;
eapply CmoF in n; desf; try edone;
try (by exfalso; eauto); eauto 16.
by destruct (eqP z1 w0); desf; eauto 14;
eapply CmoF in n; desf; try edone;
try (by exfalso; eauto); eauto 16.
Qed.
Lemma cycle_hbcom_restrLminusRfNone :
forall 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.
Proof.
ins; dupdes Cmo; eapply path_hbcom_restrLminusRfNone, proj1 in T;
eauto; desf; eauto using t_step.
Qed.
Lemma path_hbcom1 :
forall 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 \/
exists 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).
Proof.
ins; induction T; try clear T1 T2; desf;
eauto 10 using hb_trans, clos_trans, clos_trans_restr_trans_mid.
red in H; desf; eauto;
try by right; eexists x, y; repeat first [eexists | apply t_step];
eauto 8 using is_accessL_com1, is_accessL_com2.
by exfalso; eapply comD in H; eauto; desf; destruct (lab x).
by exfalso; eapply comD in H; eauto; desf; destruct (lab y).
by exfalso; eapply comD in H; eauto; desf; destruct (lab x).
Qed.
Lemma path_hbcom2 :
forall 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),
exists 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.
Proof.
ins; exists (loc (lab a)).
induction T.
desf; apply t_step; repeat split; eauto.
by destruct (lab x); ins; vauto.
by destruct (lab y); ins; vauto.
by eapply comD in H; desf; eauto; destruct (lab x); ins; vauto.
by eapply comD in H; desf; eauto; destruct (lab x); ins; vauto.
assert (EQ: loc (lab x) = loc (lab y)).
clear - Crf Cmo T1.
induction T1; desf; try congruence.
by eapply comD in H; desf; eauto; destruct (lab x); ins;
destruct (lab y); ins; vauto.
by rewrite EQ in *; eauto using clos_trans.
Qed.
Lemma path_hbcom :
forall 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 \/
exists 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).
Proof.
ins; eapply path_hbcom2 in T; desf; eauto.
edestruct path_hbcom1; eauto.
Qed.
Packaging everything to get the one direction of the equivalence theorem.
Lemma cycle_hbcom :
forall 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.
Proof.
ins; eapply path_hbcom in T; eauto; desf; eauto using clos_trans;
[|generalize (clos_trans_restr_trans_cycle _ _ T0 T)
|generalize (clos_trans_restr_trans_cycle _ _ T0 T1)
|generalize (clos_trans_restr_trans_cycle _ _ T0 (hb_trans T1 T))];
eapply cycle_hbcom_restrLminusRfNone; eauto.
Qed.
The other direction is actually much easier to show.
Lemma cycle_hbcom_rev :
forall 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 >>.
Proof.
unfold com; repeat split; repeat intro.
by eapply (T x), t_step; vauto.
destruct (eqP a b) as [|MO]; desf.
by exfalso; eapply (T b), t_step; eauto.
eapply Cmo in MO; desf; eauto.
by exfalso; eapply (T a), t_trans with b; apply t_step;
eauto using loceq_mo, eq_sym.
exploit Crf; eauto; ins; desf.
by exfalso; eapply (T a), t_trans with b; apply t_step;
eauto using loceq_rf, eq_sym.
assert (loc (lab a) = loc (lab b)).
apply (loceq_rf Crf) in RFa;
apply (loceq_rf Crf) in RFb;
apply (loceq_mo Cmo) in MO; congruence.
destruct (eqP c b); desf.
by eapply (T a), t_trans with b; apply t_step; eauto 8.
by eapply (T a), t_trans with b, t_trans with c; apply t_step; eauto 8.
assert (loc (lab a) = loc (lab b)).
apply (loceq_rf Crf) in RF;
apply (loceq_mo Cmo) in MO; congruence.
by eapply (T a), t_trans with b, t_trans with c; apply t_step; eauto 8.
assert (loc (lab a) = loc (lab b)).
apply (loceq_rf Crf) in RF;
apply (loceq_mo Cmo) in MO; congruence.
destruct (eqP b a); desf.
by eapply (T a); apply t_step; eauto 8.
by eapply (T a), t_trans with b; apply t_step; eauto 8.
generalize (Crf _ _ RF); ins; desf.
destruct (eqP b a) as [|MO]; desf.
by exfalso; eapply (T a), t_step; eauto 8.
eapply Cmo in MO; desf; eauto 8 with access.
by exfalso; eapply (T a), t_trans with b; apply t_step; eauto 8.
assert (loc (lab a) = loc (lab b)).
apply (loceq_rf Crf) in RF;
apply (loceq_mo Cmo) in R1;
apply (loceq_mo Cmo) in R2; congruence.
destruct (eqP c a); desf.
by exfalso; eapply (T a); apply t_step; eauto 8.
by eapply (T a), t_trans with c; apply t_step; eauto 8.
Qed.
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 :
forall 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 >>.
Proof.
unfold NW; split; ins; desf.
by apply cycle_hbcom_rev.
repeat red; ins; eapply cycle_hbcom; eauto.
Qed.
As a corollary of the previous theorem, the two different consistency
formulations are equivalent.
Corollary Consistent_alt :
forall 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.
Proof.
unfold Consistent, ConsistentAlt; split; ins; desf; unfold NW.
by intuition; intro; eapply cycle_hbcom; eauto.
by apply cycle_hbcom_rev in Coh; desf; intuition.
Qed.
Corollary Semiconsistent_alt :
forall 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.
Proof.
unfold Semiconsistent, SemiconsistentAlt; split; ins; desf; unfold NW.
by intuition; intro; eapply cycle_hbcom; eauto.
by apply cycle_hbcom_rev in Coh; desf; intuition.
Qed.
This page has been generated by coqdoc