Equivalence between SRArmw and Power-RA

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

In this file, we prove that the compilation of SRA to Power is correct (soundness) and optimal (completeness).

Definition of Power-RA

We start by defining a simplified version of the Power model resulting from placing a lwsync fence before every write access and control-dependent isync fence after every read access.

Section PowerModel.

Variable acts : list actid.
Variable lab : actid → act.
Variable po : actid → actid → Prop.
Variable rf : actid → option actid.
Variable rmw : actid → actid → Prop.
Variable co : actid → actid → Prop.

Definition ctrlisync x y := po x y ∧ is_read_only (lab x).

Definition lwsync x y := ∃ z, po x z ∧ clos_refl po z y ∧ is_write_only (lab z).

Definition rfe x y := rf y = Some x ∧ ¬ po x y.

Definition fr x y := ∃ z, rf x = Some z ∧ co z y.

Definition fre x y := ∃ z, rf x = Some z ∧ co z y ∧ ¬ po x y.

Definition coe x y := co x y ∧ ¬ po x y.

Definition ppo := ctrlisync.

Definition fence :=
  union (fun x y ⇒ is_read_only (lab x) ∧ lwsync x y)
        (fun x y ⇒ is_write_only (lab y) ∧ po x y).

Definition hb_power := union ppo (union fence rfe).

Definition prop_base :=
  (seq (clos_refl rfe) (seq fence (clos_refl_trans hb_power))).

Definition prop :=
  restr_rel (fun x ⇒ is_write_only (lab x)) prop_base.

Definition eqloc rel x y :=
  rel x y ∧ is_access (lab x) ∧ is_access (lab y) ∧ loc (lab x) = loc (lab y).

Definition uniproc_condition :=
  ∀ l, acyclic (union (restr_rel (fun x ⇒ is_access (lab x) ∧
                                                loc (lab x) = l) po)
                           (union (fun x y ⇒ rf y = Some x) (union co fr))).

Definition uniproc_condition_eqloc :=
  acyclic (union (eqloc po) (union (fun x y ⇒ rf y = Some x) (union co fr))).

Definition ConsistentPowerRA :=
  ≪ FIN : ExecutionFinite acts lab po ≫ ∧
  ≪ NOU : ∀ x (RMW: is_rmw (lab x)), False ≫ ∧
  ≪ CsbT: transitive po ≫ ∧
  ≪ CsbI: irreflexive po ≫ ∧
  ≪ CrfD: ConsistentRF_dom lab rf ≫ ∧
  ≪ COrf: CompleteRF lab rf ≫ ∧
  ≪ Crmw: ConsistentRMW_dom lab po rmw ≫ ∧
  ≪ CcoD: ConsistentMO_dom lab co ≫ ∧
  ≪ CcoF: ∀ l, is_total (fun a ⇒ is_writeL (lab a) l) co ≫ ∧
  ≪ CcoT: transitive co ≫ ∧
  ≪ CcoI: irreflexive co ≫ ∧
  ≪ LOC_SC : uniproc_condition ≫ ∧
  ≪ ATOM : ∀ x y (RMW: rmw x y) z (FRE: fre x z) (COE: coe z y), False ≫ ∧
  ≪ NTA : acyclic hb_power ≫ ∧
  ≪ OBS : ∀ x y (FRE: fre x y) z (PROP: prop y z)
                  (HB: clos_refl_trans hb_power z x), False ≫ ∧
  ≪ PROP: acyclic (union co prop) ≫.

Lemma uniproc_condition_alt :
  ∀
    (CrfD: ConsistentRF_dom lab rf)
    (CcoD: ConsistentMO_dom lab co),
  uniproc_condition ↔ uniproc_condition_eqloc.

End PowerModel.

Basic properties of Power-RA

Lemma is_read_only_access a : is_read_only a → is_access a.

Lemma is_write_only_access a : is_write_only a → is_access a.

Lemma is_read_only_read a : is_read_only a → is_read a.

Lemma is_write_only_write a : is_write_only a → is_write a.

Hint Resolve is_read_only_read is_read_only_access
     is_write_only_write is_write_only_access : caccess.

Lemma power_rfe_dom :
  ∀ lab po rf
         (NOU : ∀ x (RMW: is_rmw (lab x)), False)
         (CrfD: ConsistentRF_dom lab rf) x y
         (RFE: rfe po rf x y),
  is_write_only (lab x) ∧ is_read_only (lab y).

Lemma power_fre_dom :
  ∀ lab po rf co
         (NOU : ∀ x (RMW: is_rmw (lab x)), False)
         (CrfD: ConsistentRF_dom lab rf)
         (CcoD: ConsistentMO_dom lab co) x y
         (FRE: fre po rf co x y),
  is_read_only (lab x) ∧ is_write_only (lab y).

Lemma ppo_trans lab po (T: transitive po) a b c :
  ppo lab po a b →
  ppo lab po b c →
  ppo lab po a c.

Lemma ppo_in_fence lab po a b :
  ppo lab po a b →
  is_write_only (lab b) →
  fence lab po a b.

Lemma ppo_fence_trans lab po (T: transitive po) a b c :
  ppo lab po a b →
  fence lab po b c →
  fence lab po a c.

Lemma fence_trans lab po (T: transitive po) a b c :
  fence lab po a b →
  fence lab po b c →
  fence lab po a c.

Lemma fence_ppo_trans lab po (T: transitive po) a b c :
  fence lab po a b →
  ppo lab po b c →
  fence lab po a c.

Soundness with respect to SRArmw

Lemma power_hb2 :
  ∀ acts lab po rf rmw co
    (CONS: ConsistentPowerRA acts lab po rf rmw co) a b
    (HB: clos_trans (hb_power lab po rf) a b),
  ppo lab po a b ∧ ¬ is_write_only (lab b) ∨
  seq (rfe po rf) (clos_refl (ppo lab po)) a b ∧ ¬ is_write_only (lab b) ∨
  seq (clos_refl (rfe po rf))
      (seq (fence lab po) (clos_refl_trans (hb_power lab po rf))) a b.

Lemma power_hb_prop :
  ∀ acts lab po rf rmw co
    (CONS: ConsistentPowerRA acts lab po rf rmw co) a b
    (HB: clos_trans (hb_power lab po rf) a b)
    (A : is_write_only (lab a))
    (B : is_write_only (lab b)),
  prop lab po rf a b.

Lemma power_hb :
  ∀ acts lab po rf rmw co
    (CONS: ConsistentPowerRA acts lab po rf rmw co) a b
    (HB: happens_before po rf a b)
    (COND: is_read_only (lab a) ∨ is_write_only (lab b) ∨ ¬ po a b),
  clos_trans (hb_power lab po rf) a b.

Lemma observation :
  ∀ acts lab po rf rmw co
    (CONS: ConsistentPowerRA acts lab po rf rmw co)
    x y (FRE: fre po rf co x y) (PROP: prop_base lab po rf y x),
    False.

Soundness: Every complete PowerRA-coherent execution is also SRArmw-coherent.

Theorem ConsistentPowerRA_SRArmw :
  ∀ acts lab po rf rmw co
    (CONS: ConsistentPowerRA acts lab po rf rmw co),
  ConsistentSRArmw acts lab po rf rmw
    (restr_rel (fun x ⇒ is_write_only (lab x)) (tot_ext acts (union co (prop lab po rf)))).

Completeness with respect to SRArmw

Lemma incl_hb_power_sra lab po (T: transitive po) rf a b :
  hb_power lab po rf a b →
  po a b ∨ rf b = Some a.

Lemma incl_mhb_power_sra lab po (T: transitive po) rf a b :
  clos_refl_trans (hb_power lab po rf) a b →
  clos_refl_trans (fun x y ⇒ po x y ∨ rf y = Some x) a b.

Lemma incl_prop_base_sra lab po (T: transitive po) rf a b :
  prop_base lab po rf a b →
  happens_before po rf a b.

Ltac com_ext_trans_tac CmoF a :=
  let N := fresh in destruct a as [|N]; [|eapply CmoF in N];
  desf; eauto 10 with caccess;
  try (by exfalso; eauto using loceq_mo with hb).

Ltac com_ext_trans_tac' a :=
  destruct a; desf; eauto 9 with caccess;
  try (by exfalso; eauto using loceq_mo with hb).

Ltac add_locs CrfD CmoD :=
    repeat match goal with
      | [H: _ = Some _ |- _] ⇒ generalize (CrfD _ _ H); revert H
      | [H: _ |- _] ⇒ generalize (CmoD _ _ H); revert H
    end; ins; desf;
    repeat match goal with
      | H: is_writeL ?a ?l, H' : context[loc ?a] |- _ ⇒
        let EQ := fresh in assert (EQ: loc a = l) by (destruct a; ins; desf); rewrite EQ in *; clear EQ
      | H: is_readLV ?a ?l _, H' : context[loc ?a] |- _ ⇒
        let EQ := fresh in assert (EQ: loc a = l) by (destruct a; ins; desf); rewrite EQ in *; clear EQ
      | H: is_writeLV ?a ?l _, H' : is_readLV ?a ?l' _ |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
      | H: is_writeL ?a ?l, H' : is_readLV ?a ?l' _ |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
      | H: is_writeL ?a ?l, H' : is_writeLV ?a ?l' _ |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
      | H: is_writeL ?a ?l, H' : is_writeL ?a ?l' |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
      | H: is_readL ?a ?l, H' : is_readLV ?a ?l' _ |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
    end.

We prove some basic properties of com_ext:

transitivity: com_ext; com_ext ≤ com_ext
com_ext; rf ≤ com_ext
com_ext; hb; com_ext ≤ com_ext when the two com_ext are to the same location
po U rf U mo U fr ≤ hb U com_ext

Lemma mofr_trans :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) l a b c,
    mofr lab rf mo l a b →
    mofr lab rf mo l b c →
    mofr lab rf mo l a c.

Lemma mofr_shorten_hb :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) l a b c d,
    mofr lab rf mo l a b →
    happens_before sb rf b c →
    mofr lab rf mo l c d →
    mofr lab rf mo l a d.

Lemma mofr_shorten :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) l a b c d,
    mofr lab rf mo l a b →
    clos_refl_trans (fun x y ⇒ sb x y ∨ rf y = Some x) b c →
    mofr lab rf mo l c d →
    mofr lab rf mo l a d.

Lemma weaken_rmw :
  ∀ acts lab po rf rmw mo
    (CONS: ConsistentSRArmw acts lab po rf rmw mo),
    ConsistentSRA acts lab po rf mo.

Require Import Setoid.
Add Morphism fr with signature
    eq ⇒ same_relation ⇒ same_relation as fr_mor.

Lemma rf_eqloc lab rf (CrfD: ConsistentRF_dom lab rf) :
  (fun x y ⇒ rf y = Some x ) ↔ eqloc lab (fun x y ⇒ rf y = Some x).

Lemma fr_eqloc lab rf mo
    (CrfD: ConsistentRF_dom lab rf) :
  fr rf (eqloc lab mo) ↔ eqloc lab (fr rf mo).

Lemma union_eqloc lab r r' :
  union (eqloc lab r) (eqloc lab r') ↔ eqloc lab (union r r').

Lemma acyclic_eqloc lab r :
  (∀ l, acyclic (restr_rel (fun x ⇒ is_access (lab x) ∧ loc (lab x) = l) r)) →
  acyclic (eqloc lab r).

Lemma mofr_cycle1 :
  ∀ acts lab po rf mo
    (CONS: ConsistentRA acts lab po rf mo) l a b
    (MOFR: mofr lab rf mo l a b)
    (CRT: clos_refl_trans (fun x y ⇒ po x y ∨ rf y = Some x) b a),
  False.

Next, we prove that SRA-coherence implies the absence of uniproc cycles.

Lemma ConsistentSRA_uniproc :
  ∀ acts lab po rf mo
    (CONS: ConsistentSRA acts lab po rf mo)
    (NOU : ∀ x (RMW: is_rmw (lab x)), False),
   uniproc_condition lab po rf
     (fun x y : actid ⇒
      ∃ l : nat , mo x y ∧ is_writeL (lab x) l ∧ is_writeL (lab y) l).

Completeness: Every complete SRArmw-coherent execution is also PowerRA-coherent.

Theorem ConsistentSRArmw_PowerRA :
  ∀ acts lab po rf rmw mo
    (CONS: ConsistentSRArmw acts lab po rf rmw mo),
  ConsistentPowerRA acts lab po rf rmw
     (fun x y ⇒ ∃ l, mo x y ∧ is_writeL (lab x) l ∧ is_writeL (lab y) l).

Equivalence of Power-RA and SRA memory models

Putting the two together, we get equivalence between the two models.

Theorem ConsistentPowerRA_iff_SRArmw :
  ∀ acts lab po rf rmw,
    (∃ co, ConsistentPowerRA acts lab po rf rmw co )
    ↔ (∃ mo, ConsistentSRArmw acts lab po rf rmw mo ).

This page has been generated by coqdoc