Definitions of RA and SRA

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

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

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.

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

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.

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

Lemma loceq_rf :
  ∀ lab rf (C: ConsistentRF_dom lab rf) x y (H: rf x = Some y),
    loc (lab x) = loc (lab y).

Lemma loceq_com :
  ∀ lab rf mo l x y (H: mofr lab rf mo l x y),
    loc (lab x) = loc (lab y).

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.

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.

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.

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.

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.

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

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

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

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

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

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.

This page has been generated by coqdoc