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 a ⇒ is_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 a ⇒ is_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 a ⇒ is_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 a ⇒ is_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 a ⇒ is_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 a ⇒ is_writeL (lab a) l) mo >> ∧
  << CmoT: transitive mo >> ∧
  << CmoI: irreflexive mo >> ∧
  << CO : ∀ l, acyclic (sb +++ rf_external +++ mofr l) >>.

Strong release-acquire (SRA)

Definition ModelSRA :=
  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >> ∧
  << CmoD: ConsistentMO_big_dom >> ∧
  << CmoF: is_total (fun a ⇒ is_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) >>.

Total store order (TSO)

Definition ModelTSO :=
  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >> ∧
  << CmoD: ConsistentMO_big_dom >> ∧
  << CmoF: is_total (fun a ⇒ is_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) >> ∧
  << CwrU: irreflexive (reads_before ;; mo ;; eqv_rel (fun x ⇒ is_rmw (lab x)) ;; sb) >>.

Definition ModelTSO_simpl :=
  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >> ∧
  << CmoD: ConsistentMO_big_dom >> ∧
  << CmoF: is_total (fun a ⇒ is_write (lab a)) mo >> ∧
  << CmoT: transitive mo >> ∧
  << CmoI: irreflexive mo >> ∧
  << CrfI: irreflexive rf_external >> ∧
  << ChbI: irreflexive (clos_refl rf_external ;; sb) >> ∧
  << Cat': irreflexive (mo ;; rf_external) >> ∧
  << Cww : irreflexive (mo ;; clos_refl rf_external ;; sb) >> ∧
  << Cwr : irreflexive (reads_before ;; clos_refl rf_external ;; sb) >> ∧
  << Cat : irreflexive (reads_before ;; mo) >> ∧
  << CwrE: irreflexive (reads_before ;; mo ;; rf_external ;; sb) >> ∧
  << CwrU: irreflexive (reads_before ;; mo ;; eqv_rel (fun x ⇒ is_rmw (lab x)) ;; sb) >>.

End Consistency.

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