Memory model definitions


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

Section Consistency.

A (full) 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.

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

Derived relations

Definition rf_external x y :=
  rf y = Some x ¬ sb x y.

Definition happens_before :=
  clos_trans (sb +++ rf_external).

Definition reads_before x y :=
   z l, rf x = Some z mo z y x y
               is_readL (lab x) l is_writeL (lab y) l.

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.

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 In a acts >>
  << CLOsb : a b, sb a b In a acts In b acts >>.

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

In a complete execution, every read has an incoming rf-edge.

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

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

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
  • CoherentWRsc: under SC we read from the last sc-previous same-location write
  • CoherentWRatom: updates must read from their immediate mo-predecessors

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 CoherentWRsc :=
   a b (SC: mo a b) c (RF: rf c = Some a) (SC': mo b c)
         (W: is_write (lab b)) (LOC: loc (lab a) = loc (lab b)),
    False.

Minimal memory model

Definition MinimalReq :=
  << FIN : ExecutionFinite >>
  << NDA : NoDup acts >>
  << CsbT: transitive sb >>
  << CsbI: irreflexive sb >>.

Sequential consistency (SC)


Definition ModelSC_total :=
  << CrfD: ConsistentRF_dom >>
  << COrf: CompleteRF >>
  << CscF: is_total (fun ais_access (lab a)) mo >>
  << CscT: transitive mo >>
  << CscI: irreflexive mo >>
  << CrfIN: inclusion rf_external mo >>
  << CpoIN: inclusion sb mo >>
  << Cwr : CoherentWRsc >>.

Definition ModelSC_mo :=
  << CrfD: ConsistentRF_dom >>
  << COrf: CompleteRF >>
  << CmoD: ConsistentMO_dom >>
  << CmoF: l, is_total (fun ais_writeL (lab a) l) mo >>
  << CmoT: transitive mo >>
  << CmoI: irreflexive mo >>
  << CO : acyclic (sb +++ rf_external +++ mo +++ reads_before) >>.

Definition ModelSC_bigmo :=
  << CrfD: ConsistentRF_dom >>
  << COrf: CompleteRF >>
  << CmoD: ConsistentMO_big_dom >>
  << CmoF: is_total (fun ais_write (lab a)) mo >>
  << CmoT: transitive mo >>
  << CmoI: irreflexive mo >>
  << ChbI: irreflexive happens_before >>
  << Cww : irreflexive (mo ;; happens_before) >>
  << Cwr : irreflexive (reads_before ;; happens_before) >>
  << Cat : irreflexive (reads_before ;; mo) >>
  << CwrS: irreflexive (reads_before ;; mo ;; happens_before) >>.

Definition ModelSC_bigmo_simpl :=
  << CrfD: ConsistentRF_dom >>
  << COrf: CompleteRF >>
  << CmoD: ConsistentMO_big_dom >>
  << CmoF: is_total (fun ais_write (lab a)) mo >>
  << CmoT: transitive mo >>
  << CmoI: irreflexive mo >>
  << ChbI: irreflexive happens_before >>
  << Cww : irreflexive (mo ;; happens_before) >>
  << Cwr : irreflexive (reads_before ;; happens_before) >>
  << Cat : irreflexive (reads_before ;; mo) >>
  << CwrE: irreflexive (reads_before ;; mo ;; rf_external ;; sb) >>
  << CwrI: irreflexive (reads_before ;; mo ;; sb) >>.

Release-acquire (RA)


Definition ModelRA :=
  << CrfD: ConsistentRF_dom >>
  << COrf: CompleteRF >>
  << CmoD: ConsistentMO_dom >>
  << CmoF: l, is_total (fun ais_writeL (lab a) l) mo >>
  << CmoT: transitive mo >>
  << CmoI: irreflexive mo >>
  << ChbI: irreflexive happens_before >>
  << Cww : irreflexive (mo ;; happens_before) >>
  << Cwr : irreflexive (reads_before ;; happens_before) >>
  << Cat : irreflexive (reads_before ;; mo) >>.

Definition ModelRA_coh :=
  << CrfD: ConsistentRF_dom >>
  << COrf: CompleteRF >>
  << CmoD: ConsistentMO_dom >>
  << CmoF: l, is_total (fun ais_writeL (lab a) l) mo >>
  << CmoT: transitive mo >>
  << CmoI: irreflexive mo >>
  << CO : l, acyclic (sb +++ rf_external +++ mofr l) >>.

Strong release-acquire (SRA)

Total store order (TSO)

Plain executions


Record plain_exec :=
  PlainExec { pe_inits : list actid ;
              pe_threads : list (list actid) ;
              pe_lab : actid act }.

Definition pe_wellformed (pe : plain_exec) :=
  << TP: NoDup (pe.(pe_inits) ++ concat pe.(pe_threads)) >>
  << RNG: a, pe.(pe_lab) a Askip
                    In a (pe.(pe_inits) ++ concat pe.(pe_threads)) >>
  << MAIN: x, In x (concat pe.(pe_threads))
                     is_access (pe.(pe_lab) x) >>.

Definition Consistent model pe :=
   (rf : actid option actid) (mo: relation actid),
    model (pe.(pe_lab))
          (mk_po pe.(pe_inits) pe.(pe_threads))
          rf mo.

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.
  ins; destruct (classic (sb x y)); vauto.
Qed.

Lemma rf_external_in_hb :
   sb rf x y,
    rf_external sb rf x y
    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_external_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_rfe :
   lab sb rf (C: ConsistentRF_dom lab rf) x y (H: rf_external sb rf x y),
    loc (lab x) = loc (lab y).
Proof.
  unfold rf_external; ins; desc; eauto using eq_sym, loceq_rf.
Qed.

Lemma loceq_rb :
   lab rf mo x y (H: reads_before lab rf mo x y),
    loc (lab x) = loc (lab y).
Proof.
  unfold reads_before; ins; desf; 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 finiteRFE :
   acts lab sb
    (FIN: ExecutionFinite acts lab sb) rf
    (Crf: ConsistentRF_dom lab rf) a b,
    rf_external sb rf a b In a acts In b acts.
Proof.
  unfold rf_external; ins; desc; eapply finiteRF in H; desc; eauto.
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 finiteMO2 :
   acts lab sb
    (FIN: ExecutionFinite acts lab sb) mo
    (Cmo: ConsistentMO_big_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; unfold union in *; desf; [apply FIN in H|eapply finiteRFE in H];
  desf; eauto.
Qed.

Lemma finiteRB :
   acts lab sb mo
    (FIN: ExecutionFinite acts lab sb) rf a b,
    reads_before lab rf mo a b In a acts In b acts.
Proof.
  by unfold reads_before; ins; desf; split; apply FIN; intro X; rewrite X in ×.
Qed.

Finally, we add support for rewriting.

Add Parametric Morphism : ExecutionFinite with signature
  (@Permutation _) ==> eq ==> same_relation ==> iff as ExecutionFinite_more.
Proof.
  unfold ExecutionFinite, same_relation; split; ins; desf; unnw;
  split; ins; try rewrite H in *; eauto; rewrite <- H in *; eauto.
Qed.

Add Parametric Morphism : rf_external with signature
  same_relation ==> eq ==> same_relation as rf_external_more.
Proof.
  unfold same_relation, inclusion, rf_external; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : happens_before with signature
  same_relation ==> eq ==> same_relation as happens_before_more.
Proof.
  unfold happens_before; ins; rewrite H; reflexivity.
Qed.

Add Parametric Morphism : reads_before with signature
  eq ==> eq ==> same_relation ==> same_relation as reads_before_more.
Proof.
  unfold same_relation, inclusion, reads_before; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : ConsistentMO_big_dom with signature
  eq ==> same_relation ==> iff as ConsistentMO_big_dom_more.
Proof.
  unfold ConsistentMO_big_dom, same_relation; split; ins; desf; eauto.
Qed.

Add Parametric Morphism : ModelTSO with signature
  eq ==> same_relation ==> eq ==> same_relation ==> iff as ModelTSO_more.
Proof.
  by unfold ModelTSO; unnw; ins; rewrite H, H0.
Qed.

Add Parametric Morphism : ModelTSO_simpl with signature
  eq ==> same_relation ==> eq ==> same_relation ==> iff as ModelTSO_simpl_more.
Proof.
  by unfold ModelTSO_simpl; unnw; ins; rewrite H, H0.
Qed.

Add Parametric Morphism : reads_before with signature
  eq ==> eq ==> inclusion ==> inclusion as reads_before_mori.
Proof.
  unfold inclusion, reads_before; intuition; desf; eauto 8.
Qed.


This page has been generated by coqdoc