Definitions of RA and SRA


Require Import Classical List Relations Peano_dec.
Require Import Vbase ExtraRelations cactions.
Set Implicit Arguments.
Remove Hints plus_n_O.

Consistency axioms


Definition fence_loc := 0.

Section Consistency.

An execution contains:
  • a sequence of events (actions identifiers), acts,
  • a labeling function, lab, mapping action identifiers to the actions,
  • the "sequence before" order, sb,
  • the "reads from" map, rf, and
  • the modification order, mo.
In the SRArmw model, an execution also contains:
  • the "atomicity" relation, rmw, which relates atomic read and write events belonging to the same successful read-modify-write.

Variable acts : list actid.
Variable lab : actid → act.
Variable sb : actid → actid → Prop.
Variable rf : actid → option actid.
Variable rmw : actid → actid → Prop.
Variable mo : actid → actid → Prop.

Definition happens_before :=
  clos_trans (fun a b ⇒ sb a b ∨ rf b = Some a).

We require executions to have a finite domain:
  • Every action not in the domain must be a Askip 0 action.
  • sb cannot relate any events outside the domain.

Definition ExecutionFinite :=
  << CLOlab: ∀ a, lab a ≠ Askip 0 → In a acts >> ∧
  << CLOsb : ∀ a b, sb a b → In a acts ∧ In b acts >>.

Definition CompleteRF :=
  ∀ a (RF: rf a = None)
         (READ: is_read (lab a)), False.

The reads-from map is consistent iff it relates only reads and writes to the same location and with the same values.

Definition ConsistentRF_dom :=
  ∀ a b (RF: rf a = Some b),
  ∃ l v,
    << READ: is_readLV (lab a) l v >> ∧
    << WRITE: is_writeLV (lab b) l v >>.

Definition BasicConsistency :=
  << FIN : ExecutionFinite >> ∧
  << CsbT: transitive sb >> ∧
  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >>.

Properties of the modification order:

Definition ConsistentMO_dom :=
  ∀ a b (MO: mo a b), ∃ l, is_writeL (lab a) l ∧ is_writeL (lab b) l.

Definition ConsistentMO_big_dom :=
  ∀ a b (MO: mo a b), is_write (lab a) ∧ is_write (lab b).

Definition ConsistentRMW_dom :=
  ∀ a b (RF: rmw a b),
  << PO: sb a b >> ∧
  << POI: ∀ c (SB: sb c b) (NEQ: c ≠ a), sb c a >> ∧
  << POI': ∀ c (SB: sb a c) (NEQ: c ≠ b), sb b c >> ∧
  << NORMWa: is_rmw (lab a) = false >> ∧
  << NORMWb: is_rmw (lab b) = false >> ∧
  ∃ l,
    << READ: is_readL (lab a) l >> ∧
    << WRITE: is_writeL (lab b) l >>.

We move on to the various coherence axioms:
  • CoherentWW: the modification order cannot contradict happens-before
  • CoherentWR: a read cannot read from an overwritten write.

Definition CoherentWW :=
  ∀ a b (HB: happens_before a b) (MO: mo b a),
    False.

Definition CoherentWRplain :=
  ∀ a b (MO: mo a b) c (RF: rf c = Some a) (HB: happens_before b c),
    False.

Definition CoherentWR :=
  ∀ a b (MO: mo a b) c (RF: rf c = Some a) (HB: happens_before b c)
             (LOC: loc (lab a) = loc (lab b)),
    False.

Definition CoherentWRatom :=
  ∀ a b (MO: mo a b) c (RF: rf c = Some a) (MO': mo b c)
             (LOC: loc (lab a) = loc (lab b)),
    False.

Definition CoherentWRrmw :=
  ∀ a b (MO: mo a b) c d (RMW: rmw c d) (RF: rf c = Some a) (MO': mo b d)
             (LOC: loc (lab a) = loc (lab b)),
    False.

Definition ConsistentRA :=
  << FIN : ExecutionFinite >> ∧
  << CsbT: transitive sb >> ∧
  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >> ∧
  << ACYC: irreflexive happens_before >> ∧
  << CmoD: ConsistentMO_dom >> ∧
  << CmoF: ∀ l, is_total (fun a ⇒ is_writeL (lab a) l) mo >> ∧
  << CmoT: transitive mo >> ∧
  << CmoI: irreflexive mo >> ∧
  << Cww : CoherentWW >> ∧
  << Cwr : CoherentWRplain >> ∧
  << Cat : CoherentWRatom >>.

Definition ConsistentSRA :=
  << FIN : ExecutionFinite >> ∧
  << CsbT: transitive sb >> ∧
  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >> ∧
  << ACYC: irreflexive happens_before >> ∧
  << CmoD: ConsistentMO_big_dom >> ∧
  << CmoF: is_total (fun a ⇒ is_write (lab a)) mo >> ∧
  << CmoT: transitive mo >> ∧
  << CmoI: irreflexive mo >> ∧
  << Cww : CoherentWW >> ∧
  << Cwr : CoherentWR >> ∧
  << Cat : CoherentWRatom >>.

Definition ConsistentSRArmw :=
  << FIN : ExecutionFinite >> ∧
  << CsbT: transitive sb >> ∧
  << NOU : ∀ x (RMW: is_rmw (lab x)), False >> ∧
  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >> ∧
  << Crmw: ConsistentRMW_dom >> ∧
  << ACYC: irreflexive happens_before >> ∧
  << CmoD: ConsistentMO_big_dom >> ∧
  << CmoF: is_total (fun a ⇒ is_write (lab a)) mo >> ∧
  << CmoT: transitive mo >> ∧
  << CmoI: irreflexive mo >> ∧
  << Cww : CoherentWW >> ∧
  << Cwr : CoherentWR >> ∧
  << Cat : CoherentWRrmw >>.

An alternative, much more compact, coherence axiom.

Definition mofr l x y :=
  mo x y ∧ is_writeL (lab x) l ∧ is_writeL (lab y) l
  ∨ ∃ z, rf x = Some z ∧ mo z y ∧ x ≠ y
               ∧ is_readL (lab x) l ∧ is_writeL (lab y) l.

Definition ConsistentRAalt :=
  << FIN : ExecutionFinite >> ∧
  << CsbT: transitive sb >> ∧
  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >> ∧
  << CmoD: ConsistentMO_dom >> ∧
  << CmoF: ∀ l, is_total (fun a ⇒ is_writeL (lab a) l) mo >> ∧
  << CmoT: transitive mo >> ∧
  << CmoI: irreflexive mo >> ∧
  << CO : ∀ l, acyclic (fun x y ⇒ sb x y ∨ rf y = Some x ∨ mofr l x y) >>.

Definition no_ww_races :=
  ∀ a l (Wa: is_writeL (lab a) l) b (Wb: is_writeL (lab b) l) (NEQ: a ≠ b) ,
    happens_before a b ∨ happens_before b a.

Definition writes_beforeSRA a b :=
  is_write (lab a) ∧ is_write (lab b) ∧ a ≠ b ∧
  loc (lab a) = loc (lab b) ∧ ∃ c, happens_before a c ∧ rf c = Some b.

Definition ConsistentSRAwb :=
  << FIN : ExecutionFinite >> ∧
  << CsbT: transitive sb >> ∧
  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >> ∧
  << ACYC: acyclic (fun x y ⇒ sb x y ∨ rf y = Some x ∨ writes_beforeSRA x y) >>.

Definition CoherentWRsc sc :=
  ∀ a b (SC: sc a b) c (RF: rf c = Some a) (SC': sc b c)
         (W: is_write (lab b)) (LOC: loc (lab a) = loc (lab b)),
    False.

Definition ConsistentSCalt sc :=
  << FIN : ExecutionFinite >> ∧
  << CsbT: transitive sb >> ∧
  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >> ∧
  << CscF: is_total (fun a ⇒ In a acts) sc >> ∧
  << CscT: transitive sc >> ∧
  << CscI: irreflexive sc >> ∧
  << CrfIN: ∀ a b (RF: rf b = Some a), sc a b >> ∧
  << CpoIN: ∀ a b (SB: sb a b), sc a b >> ∧
  << Cwr : CoherentWRsc sc >>.

Definition ConsistentSC :=
  << FIN : ExecutionFinite >> ∧
  << CsbT: transitive sb >> ∧
  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >> ∧
  << CmoD: ConsistentMO_dom >> ∧
  << CmoF: ∀ l, is_total (fun a ⇒ is_writeL (lab a) l) mo >> ∧
  << CmoT: transitive mo >> ∧
  << CmoI: irreflexive mo >> ∧
  << CO : acyclic (fun x y ⇒ sb x y ∨ rf y = Some x ∨ ∃ l, mofr l x y) >>.

Definition wellformed_fences :=
  ∀ x (WRI: is_writeL (lab x) fence_loc),
    is_rmw (lab x) ∨
    ∀ y (WRI': is_writeL (lab y) fence_loc),
      sb x y.

Definition races_with a b :=
  << NEQ: a ≠ b >> ∧
  << Aa: is_access (lab a) >> ∧
  << Ab: is_access (lab b) >> ∧
  << LOC: loc (lab a) = loc (lab b) >> ∧
  << WRI: is_write (lab a) ∨ is_write (lab b) >> ∧
  << NHB1 : ¬ happens_before a b >> ∧
  << NHB2 : ¬ happens_before b a >>.

Definition racy a := ∃ b, races_with a b.

End Consistency.

Lemma racy_access lab sb rf a : racy lab sb rf a → is_access (lab a).
Proof. by unfold racy, races_with; ins; desf. Qed.

Hint Resolve racy_access : caccess.

Basic properties of the definitions


Lemma sb_in_hb :
  ∀ (sb : relation actid) rf x y,
    sb x y →
    happens_before sb rf x y.
Proof.
  vauto.
Qed.

Lemma rf_in_hb :
  ∀ sb rf x y,
    rf y = Some x →
    happens_before sb rf x y.
Proof.
  vauto.
Qed.

Lemma hb_trans :
  ∀ sb rf x y z,
    happens_before sb rf x y →
    happens_before sb rf y z →
    happens_before sb rf x z.
Proof.
  vauto.
Qed.

Hint Resolve hb_trans sb_in_hb rf_in_hb : hb.

Lemma loceq_mo :
  ∀ lab mo (C: ConsistentMO_dom lab mo) x y (H: mo x y),
    loc (lab x) = loc (lab y).
Proof.
  ins; specialize (C _ _ H); destruct (lab x); ins; destruct (lab y); ins; desf.
Qed.

Lemma loceq_rf :
  ∀ lab rf (C: ConsistentRF_dom lab rf) x y (H: rf x = Some y),
    loc (lab x) = loc (lab y).
Proof.
  ins; specialize (C _ _ H); destruct (lab x); ins; destruct (lab y); ins; desf.
Qed.

Lemma loceq_com :
  ∀ lab rf mo l x y (H: mofr lab rf mo l x y),
    loc (lab x) = loc (lab y).
Proof.
  unfold mofr; ins; desf; destruct (lab x); ins; destruct (lab y); ins; desf.
Qed.

Lemma finiteRF :
  ∀ acts lab sb
    (FIN: ExecutionFinite acts lab sb) rf
    (Crf: ConsistentRF_dom lab rf) a b,
    rf a = Some b → In a acts ∧ In b acts.
Proof.
  unfold ExecutionFinite; ins; desf.
  apply Crf in H; desf.
  generalize (CLOlab a); destruct (lab a); ins;
  generalize (CLOlab b); destruct (lab b); ins; intuition congruence.
Qed.

Lemma finiteMO :
  ∀ acts lab sb
    (FIN: ExecutionFinite acts lab sb) mo
    (Cmo: ConsistentMO_dom lab mo) a b,
    mo a b → In a acts ∧ In b acts.
Proof.
  unfold ExecutionFinite; ins; desf.
  apply Cmo in H; desf.
  generalize (CLOlab a); destruct (lab a); ins;
  generalize (CLOlab b); destruct (lab b); ins; intuition congruence.
Qed.

Lemma finiteHB :
  ∀ acts lab sb
    (FIN: ExecutionFinite acts lab sb) rf
    (Crf: ConsistentRF_dom lab rf) a b,
    happens_before sb rf a b → In a acts ∧ In b acts.
Proof.
  induction 3; desf; [apply FIN in H|eapply finiteRF in H]; desf; eauto.
Qed.

Lemma hb_mo :
  ∀ acts lab sb rf mo
    (CONS: ConsistentRA acts lab sb rf mo) a b
    (HB : happens_before sb rf a b)
    (Wa : is_write (lab a))
    (Wb : is_write (lab b))
    (LOC: loc (lab a) = loc (lab b)),
    mo a b.
Proof.
  ins; red in CONS; desf.
  destruct (eqP a b) as [|N]; [|eapply (CmoF (loc (lab a))) in N]; desf; eauto;
    try by exfalso; eauto.
  by destruct (lab a); ins.
  by destruct (lab b); ins.
Qed.

Lemma hb_in_tot_ext acts sb rf mo a b :
  happens_before sb rf a b →
  tot_ext acts (fun x y ⇒ sb x y ∨ rf y = Some x ∨ mo x y) a b.
Proof.
  ins; eapply clos_trans_of_transitive, (clos_trans_mon _ H);
  eauto using tot_ext_trans; ins; eapply tot_ext_extends; desf; eauto.
Qed.

SRA-coherence is stronger than RA-coherence.

Proposition ConsistentSRA_RA acts lab sb rf mo :
  ConsistentSRA acts lab sb rf mo →
  ConsistentRA acts lab sb rf (fun x y ⇒ mo x y ∧ loc (lab x) = loc (lab y)).
Proof.
  unfold ConsistentSRA, ConsistentRA; ins; desf; unnw; intuition;
  red; ins; desf; eauto.
  by ∃ (loc (lab a)); eapply CmoD in MO; desf; destruct (lab a); ins;
     destruct (lab b); ins.
  by eapply CmoF in NEQ; eauto with caccess; desf; [left|right]; split; ins;
     destruct (lab a); ins; destruct (lab b); ins; desf.
  split; eauto; congruence.
Qed.

Lemma ConsistentSRA_ac acts lab sb rf mo :
  ConsistentSRA acts lab sb rf mo →
  acyclic (fun x y ⇒ sb x y ∨ rf y = Some x ∨ mo x y ∧ loc (lab x) = loc (lab y)).
Proof.
  unfold ConsistentSRA; ins; desf.
  intros x H.
  eapply clos_trans_mon in H;
  [ eapply cycle_utd with (r := fun a b ⇒ sb a b ∨ rf b = Some a) (r':=mo) in H;
    eauto; desf; eauto |]; instantiate; ins; tauto.
Qed.

Lemma ConsistentSRA_alt2 acts lab sb rf mo
  (C: ConsistentRA acts lab sb rf mo)
  (A: acyclic (fun x y ⇒ sb x y ∨ rf y = Some x ∨ mo x y)) :
  ∃ mo',
    inclusion mo mo' ∧
    ConsistentSRA acts lab sb rf mo'.
Proof.
  unfold ConsistentRA, ConsistentSRA in *; desf; unnw.
  ∃ (restr_rel (fun x ⇒ is_write (lab x))
                    (tot_ext acts (fun x y ⇒ sb x y ∨ rf y = Some x ∨ mo x y)));
    intuition; unfold restr_rel; repeat red; ins; desf; intuition;
      eauto using tot_ext_extends;
        try (by eapply CmoD in H; desf; eauto with caccess).
    by eapply tot_ext_total with (dom:=acts) in NEQ; desf; eauto;
       apply FIN; intro X; rewrite X in ×.
   eby eapply tot_ext_trans.
   eby eapply tot_ext_irr.
   by eapply tot_ext_irr, tot_ext_trans, hb_in_tot_ext; eauto.
   destruct (eqP a b) as [|NEQ]; desf; [eby eapply tot_ext_irr|].
   eapply CmoF with (l := loc (lab a)) in NEQ; desf; eauto.
   by eapply tot_ext_irr, tot_ext_trans;
     eauto using tot_ext_trans; ins; eapply tot_ext_extends; desf; eauto.
   by (destruct (lab a); ins).
   by (destruct (lab b); ins).

   destruct (eqP a b) as [|NEQ]; desf; [eby eapply tot_ext_irr|].
   eapply CmoF with (l := loc (lab a)) in NEQ; desf; eauto;
     try solve [destruct (lab a); ins|destruct (lab b); ins].
   destruct (eqP b c) as [|NEQ']; desf; [eby eapply tot_ext_irr|].
   eapply CmoF with (l := loc (lab a)) in NEQ'; desf; eauto;
     try solve [destruct (lab b); ins|
                eapply CrfD in RF; desf;
                destruct (lab a); ins; destruct (lab c); ins; desf].
   by eapply tot_ext_irr with (x := c), tot_ext_trans;
     eauto using tot_ext_trans; ins; eapply tot_ext_extends; desf; eauto.
   by eapply tot_ext_irr with (x := a), tot_ext_trans;
     eauto using tot_ext_trans; ins; eapply tot_ext_extends; desf; eauto.
Qed.

SRA-coherence is equivalent to RA-coherence plus acyclicity po U rf U mo.

Theorem ConsistentSRA_alt acts lab sb rf :
  (∃ mo, ConsistentSRA acts lab sb rf mo) ↔
  (∃ mo, ConsistentRA acts lab sb rf mo ∧
   acyclic (fun x y ⇒ sb x y ∨ rf y = Some x ∨ mo x y)).
Proof.
  split; ins; desf.
    ∃ (fun x y ⇒ mo x y ∧ loc (lab x) = loc (lab y));
    eauto using ConsistentSRA_RA, ConsistentSRA_ac.
  edestruct ConsistentSRA_alt2; desf; eauto.
Qed.

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

Theorem ConsistentRA_no_ww_races :
  ∀ acts lab sb rf (NORACE: no_ww_races lab sb rf),
  (∃ mo, ConsistentSRA acts lab sb rf mo) ↔
  (∃ mo, ConsistentRA acts lab sb rf mo).
Proof.
  ins; rewrite ConsistentSRA_alt; split; ins; desf; ∃ mo; intuition.
  red in H; desc; eapply acyclic_mon; [eapply (trans_irr_acyclic ACYC); vauto|].
  red; ins; desf; vauto.
  edestruct CmoD; eauto; desf.
  destruct (eqP x y) as [|NEQ]; desf; [exfalso; eauto|].
  eapply NORACE in NEQ; desf; eauto with caccess; exfalso; eauto.
Qed.

In the absence of updates, SRA-coherence is equivalent to the writes-before definition.

Theorem ConsistentSRA_wb :
  ∀ acts lab sb rf (NORMW: ∀ a, ¬ is_rmw (lab a)),
  (∃ mo, ConsistentSRA acts lab sb rf mo) ↔
  ConsistentSRAwb acts lab sb rf.
Proof.
  split; ins; desf.
    assert (A := ConsistentSRA_ac H).
    unfold ConsistentSRAwb, ConsistentSRA in *; desf; unnw; intuition.
    eapply acyclic_mon; eauto; red; ins; desf; eauto.
    right; right; red in H; desf; split; ins.
    by eapply CmoF in H1; eauto; desf; exfalso; eauto.
  ∃ (restr_rel (fun x ⇒ is_write (lab x))
                    (tot_ext acts (fun x y ⇒ sb x y ∨ rf y = Some x
                                              ∨ writes_beforeSRA lab sb rf x y))).
    unfold ConsistentSRAwb, ConsistentSRA in *; desf; unnw; intuition;
    eauto using tot_ext_trans, restr_rel_trans.
  by eapply acyclic_mon; eauto; red; ins; desf; vauto.
  by unfold restr_rel; red; ins; desf.
  by eapply is_total_restr; red; ins; eapply tot_ext_total; eauto;
     apply FIN; intro X; rewrite X in ×.
  by unfold restr_rel; red; ins; desf; eapply tot_ext_irr; eauto.
  by unfold restr_rel; red; ins; desf;
     eapply tot_ext_irr, tot_ext_trans, hb_in_tot_ext; eauto.

  unfold restr_rel; red; ins; desf.
  eapply tot_ext_irr with (x:=a), tot_ext_trans, tot_ext_extends; eauto;
  instantiate; ins; right; right; repeat split; eauto;
  eby intro; desf; eapply tot_ext_irr.

  unfold restr_rel; red; ins; desf.
  by eapply (NORMW c); eapply CrfD in RF; desf; destruct (lab c); ins.
Qed.

This page has been generated by coqdoc