Definition of the Power memory model

In this section, we define the Power memory model of Alglave et al., as well as a variant with a total order on sync fences. In the end, we show that the two models are equivalent.

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

Definition actid := nat.

Inductive act :=
  | Askip
  | Async
  | Alwsync
  | Aload (l : nat) (v : nat)
  | Astore (l : nat) (v : nat).

Definition loc a :=
  match a with
    | Aload l _
    | Astore l _ ⇒ 1
    | _ ⇒ 0
  end.

Definition is_access a :=
  match a with
    | Aload _ _ | Astore _ _ ⇒ true
    | _ ⇒ false
  end.

Definition is_read a :=
  match a with
    | Aload _ _ ⇒ true
    | _ ⇒ false
  end.

Definition is_write a :=
  match a with
    | Astore _ _ ⇒ true
    | _ ⇒ false
  end.

Lemma is_read_access a : is_read a → is_access a.

Lemma is_write_access a : is_write a → is_access a.

Hint Resolve is_read_access is_write_access : access.

Section PowerModel.

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

Definitions of auxiliary relations for the model

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 po_loc_RW x y :=
  po x y ∧ is_read (lab x) ∧ is_write (lab y) ∧ loc (lab x) = loc (lab y).

Definition ppo x y :=
  (deps x y ∨ seq (clos_refl deps) po_loc_RW x y)
  ∧ is_read (lab x) ∧ is_access (lab y).

Definition sync x y :=
  ∃ s, po x s ∧ po s y ∧ lab s = Async ∧
   is_access (lab x) ∧ is_access (lab y).

Definition lwsync x y :=
  (∃ s, po x s ∧ po s y ∧ lab s = Alwsync)
  ∧ (is_read (lab x) ∧ is_access (lab y) ∨
      is_access (lab x) ∧ is_write (lab y)).

Definition fence :=
  union sync lwsync.

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

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

Definition chapo :=
  union rfe (union fre (union coe (union (seq fre rfe) (seq coe rfe)))).

Definition prop :=
  union (restr_rel (fun x ⇒ is_write (lab x)) prop_base)
        (seq (clos_refl chapo)
             (seq (clos_refl_trans prop_base) (seq sync (clos_refl_trans hb_power)))).

The implicit well-formedness axioms

Definition ExecutionFinite :=
  ≪ CLOlab: ∀ a, lab a ≠ Askip → In a acts ≫ ∧
  ≪ CLOsb : ∀ a b, po a b → In a acts ∧ In b acts ≫.

Definition ConsistentRF_dom :=
  ∀ a b (RF: rf b = Some a),
  ∃ l v, ≪WRI: lab a = Astore l v≫ ∧ ≪READ: lab b = Aload l v ≫.

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

Definition ConsistentMO_dom :=
  ∀ a b (MO: co a b),
    is_write (lab a) ∧ is_write (lab b) ∧ loc (lab a) = loc (lab b).

Definition ConsistentRMW_dom :=
  ∀ a b (RF: rmw a b),
  ≪ PO: po a b ≫ ∧
  ≪ POI: ∀ c (SB: po c b) (NEQ: c ≠ a), po c a ≫ ∧
  ≪ POI': ∀ c (SB: po a c) (NEQ: c ≠ b), po b c ≫ ∧
  ≪ READ: is_read (lab a) ≫ ∧
  ≪ WRITE: is_write (lab b) ≫ ∧
  ≪ LOCEQ: loc (lab a) = loc (lab b) ≫.

The Power axioms.

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 observation_condition :=
  ∀ x y (FRE: fre x y) z (PROP: prop y z)
             (HB: clos_refl_trans hb_power z x), False.

Definition ConsistentPower :=
  ≪ FIN : ExecutionFinite ≫ ∧
  ≪ CsbT: transitive po ≫ ∧
  ≪ CsbI: irreflexive po ≫ ∧
  ≪ CrfD: ConsistentRF_dom ≫ ∧
  ≪ COrf: CompleteRF ≫ ∧
  ≪ Crmw: ConsistentRMW_dom ≫ ∧
  ≪ CcoD: ConsistentMO_dom ≫ ∧
  ≪ CcoF: ∀ l, is_total (fun a ⇒ ∃ v, lab a = Astore l v) 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 : observation_condition ≫ ∧
  ≪ PROP: acyclic (union co prop) ≫.

Next, we define an equivalent uniproc condition that is more convenient for proofs.

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_eqloc :=
  acyclic (union (eqloc po) (union (fun x y ⇒ rf y = Some x) (union co fr))).

We also define a simpler equivalent observation condition.

Definition observation_condition_simpl :=
  ∀ x y (FRE: fre x y) (BASE: prop_base y x), False.

We define versions of the fence and hb relations to include only edges that can be ensured without strong synchronization primitives. Specifically, we exclude any write-to-read edges that are ensured by strong sync fences.

Definition fence_weak x y :=
  (∃ s, po x s ∧ po s y ∧ (lab s = Alwsync ∨ lab s = Async))
  ∧ (is_read (lab x) ∧ is_access (lab y) ∨
      is_access (lab x) ∧ is_write (lab y)).

Definition hb_weak := union ppo (union fence_weak rfe).

Using these versions of fence and hb, we can define an equivalent propogation condition:

Definition prop_base_weak :=
  (seq (clos_refl rfe) (seq fence_weak (clos_refl_trans hb_weak))).

Definition prop_weak :=
  union (restr_rel (fun x ⇒ is_write (lab x)) prop_base_weak)
        (seq (clos_refl chapo)
             (seq (clos_refl_trans prop_base_weak)
                  (seq sync (clos_refl_trans hb_weak)))).

and yet another equivalent observation condition.

Definition observation_condition_alt :=
  ∀ x y (FRE: fre x y) (BASE: prop_base_weak y x), False.

We next define an alternative memory model for Power that uses a total order (so) over sync fence events. The alternative model depends on the following auxiliary definitions.

Definition so_step so a b :=
  ∃ f f',
    po a f ∧ so f f' ∧ po f' b ∧ lab f = Async ∧ lab f' = Async.

Definition hb_so so := union hb_weak (so_step so).

Definition fence_so so := union fence_weak (so_step so).

Definition prop_base_so so :=
  (seq (clos_refl rfe) (seq (fence_so so) (clos_refl_trans (hb_so so)))).

Definition prop_so so :=
  (restr_rel (fun x ⇒ is_write (lab x)) (prop_base_so so)).

Definition ConsistentSyncTotal so :=
  ≪ FIN : ExecutionFinite ≫ ∧
  ≪ CsbT: transitive po ≫ ∧
  ≪ CsbI: irreflexive po ≫ ∧
  ≪ CrfD: ConsistentRF_dom ≫ ∧
  ≪ COrf: CompleteRF ≫ ∧
  ≪ Crmw: ConsistentRMW_dom ≫ ∧
  ≪ CcoD: ConsistentMO_dom ≫ ∧
  ≪ CcoF: ∀ l, is_total (fun a ⇒ ∃ v, lab a = Astore l v) co ≫ ∧
  ≪ CcoT: transitive co ≫ ∧
  ≪ CcoI: irreflexive co ≫ ∧
  ≪ CsoF: is_total (fun a ⇒ lab a = Async) so ≫ ∧
  ≪ CsoT: transitive so ≫ ∧
  ≪ CsoI: irreflexive so ≫ ∧
  ≪ LOC_SC : uniproc_condition ≫ ∧
  ≪ ATOM : ∀ x y (RMW: rmw x y) z (FRE: fre x z) (COE: coe z y), False ≫ ∧
  ≪ NTA : acyclic (hb_so so) ≫ ∧
  ≪ OBS : ∀ x y (FRE: fre x y) (PROP: prop_base_so so y x), False ≫ ∧
  ≪ PROP: acyclic (union co (union so (prop_so so))) ≫.

Basic properties of the model


Lemma loceq_rf :
  ∀ (CrfD: ConsistentRF_dom) a b (H: rf b = Some a),
    loc (lab a) = loc (lab b).

Lemma loceq_co :
  ∀ (CcoD: ConsistentMO_dom) a b (H: co a b),
    loc (lab a) = loc (lab b).

Lemma loceq_fr :
  ∀ (CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
         a b (H: fr a b),
    loc (lab a) = loc (lab b).

Lemma fr_dom :
  ∀ (CrfD: ConsistentRF_dom)
         (CcoD: ConsistentMO_dom) x y
         (FR: fr x y),
  is_read (lab x) ∧ is_write (lab y) ∧ loc (lab x) = loc (lab y).

Lemma rfe_dom :
  ∀ (CrfD: ConsistentRF_dom) x y
         (RFE: rfe x y),
  is_write (lab x) ∧ is_read (lab y) ∧ loc (lab x) = loc (lab y).

Lemma fre_dom :
  ∀
         (CrfD: ConsistentRF_dom)
         (CcoD: ConsistentMO_dom) x y
         (FRE: fre x y),
  is_read (lab x) ∧ is_write (lab y) ∧ loc (lab x) = loc (lab y).

Lemma hb_is_access_l (CrfD: ConsistentRF_dom) x y :
  hb_power x y → is_access (lab x).

Lemma hb_is_access_r (CrfD: ConsistentRF_dom) x y :
  hb_power x y → is_access (lab y).

Hint Immediate hb_is_access_l hb_is_access_r : access.

Lemma hbp_is_access_l (CrfD: ConsistentRF_dom) x y :
  clos_trans hb_power x y → is_access (lab x).

Lemma hbp_is_access_r (CrfD: ConsistentRF_dom) x y :
  clos_trans hb_power x y → is_access (lab y).

Hint Immediate hbp_is_access_l hbp_is_access_r : access.

Lemma hb_weak_is_access_l (CrfD: ConsistentRF_dom) x y :
  hb_weak x y → is_access (lab x).

Lemma hb_weak_is_access_r (CrfD: ConsistentRF_dom) x y :
  hb_weak x y → is_access (lab y).

Hint Immediate hb_weak_is_access_l hb_weak_is_access_r : access.

Lemma hb_weakp_is_access_l (CrfD: ConsistentRF_dom) x y :
  clos_trans hb_weak x y → is_access (lab x).

Lemma hb_weakp_is_access_r (CrfD: ConsistentRF_dom) x y :
  clos_trans hb_weak x y → is_access (lab y).

Hint Immediate hb_weakp_is_access_l hb_weakp_is_access_r : access.

Lemma chapo_access
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) a b :
  chapo a b → is_access (lab a) ∧ is_access (lab b).

The two uniproc conditions are equivalent.

Proposition uniproc_condition_alt :
  ∀
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom),
  uniproc_condition ↔ uniproc_condition_eqloc.

Lemma may_chapoE :
  clos_refl chapo ↔ seq (clos_refl (union coe fre)) (clos_refl rfe).

Lemma freE a b : fre a b ↔ fr a b ∧ ¬ po a b.

Lemma fence_weakE x y :
  fence_weak x y ↔ fence x y ∧ ¬ (is_write (lab x) ∧ is_read (lab y)).

Lemma fenceE x y :
  fence x y ↔ fence_weak x y ∨ sync x y ∧ is_write (lab x) ∧ is_read (lab y).

Inclusion lemmas

Lemma inclusion_sync_fence : inclusion sync fence.

Lemma inclusion_fence_hb : inclusion fence hb_power.

Lemma inclusion_fence_hb_weak : inclusion fence_weak hb_weak.

Lemma inclusion_fence_weak_hb : inclusion fence_weak hb_power.

Lemma inclusion_rfe_hb : inclusion rfe hb_power.

Lemma inclusion_rfe_hb_weak : inclusion rfe hb_weak.

Lemma inclusion_hb_weak_hb : inclusion hb_weak hb_power.

Hint Resolve inclusion_sync_fence
     inclusion_fence_hb_weak inclusion_rfe_hb_weak
     inclusion_fence_hb inclusion_fence_weak_hb inclusion_rfe_hb
     inclusion_hb_weak_hb : inclusion.

Lemma inclusion_base_hb : inclusion prop_base (clos_refl_trans hb_power).

Lemma inclusion_base_hb_weak :
  inclusion prop_base_weak (clos_refl_trans hb_weak).

Lemma inclusion_base_weak_hb :
  inclusion prop_base_weak (clos_refl_trans hb_power).

Lemma inclusion_fence_po (T: transitive po) : inclusion fence po.

Lemma ppo_in_po
   (T: transitive po) (INCL: inclusion deps po) x y :
  ppo x y → po x y.

Lemma fr_po_hb :
  ∀ (CrfD: ConsistentRF_dom)
         (CcoD: ConsistentMO_dom) x y,
  fr x y → po x y →
  hb_power x y.

Transitivity lemmas

Lemma base_hb_trans a b c :
  prop_base a b →
  clos_refl_trans hb_power b c →
  prop_base a c.

Lemma rfe_base_trans (CrfD: ConsistentRF_dom) a b c:
  rfe a b →
  prop_base b c →
  prop_base a c.

Lemma rrfe_base_trans (CrfD: ConsistentRF_dom) a b c:
  clos_refl rfe a b →
  prop_base b c →
  prop_base a c.

Lemma base_sync_base a b c:
  clos_refl_trans prop_base a b →
  sync b c →
  prop_base a c.

Hint Resolve base_sync_base rfe_base_trans rrfe_base_trans base_hb_trans : trans.

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

Lemma ppo_weaken (T: transitive po) (INCL : inclusion deps po) a b :
  ppo a b →
  po a b ∧ is_read (lab a) ∧ is_access (lab b).

Lemma ppo_fence_trans (T: transitive po) (INCL : inclusion deps po) a b c :
  ppo a b →
  fence b c →
  fence a c.

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

Lemma fence_ppo_trans (T: transitive po) (INCL : inclusion deps po) a b c :
  fence a b →
  ppo b c →
  fence a c.

Lemma sync_trans (T: transitive po) a b c :
  sync a b →
  sync b c →
  sync a c.

Lemma prop_base_weak_trans a b c :
  prop_base_weak a b →
  prop_base_weak b c →
  prop_base_weak a c.

Lemma prop_base_trans a b c :
  prop_base a b →
  prop_base b c →
  prop_base a c.

Hint Resolve ppo_trans ppo_fence_trans fence_trans fence_ppo_trans : trans.
Hint Resolve sync_trans : trans.

A happens-before path starting from a read either stays in the same thread, or it must go through a write.

Lemma hb_RT :
  ∀ (T: transitive po)
    (INCL : inclusion deps po)
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom) x y
    (P : clos_trans hb_power x y)
    (R : is_read (lab x)),
  po x y ∨
  (∃ m : actid,
     clos_refl_trans hb_power x m ∧ po x m ∧
     clos_refl_trans hb_power m y ∧ is_write (lab m)).

Lemma hb_weak_RT :
  ∀ (T: transitive po)
    (INCL : inclusion deps po)
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom) x y
    (P : clos_trans hb_weak x y)
    (R : is_read (lab x)),
  po x y ∨
  (∃ m : actid,
     clos_refl_trans hb_weak x m ∧ po x m ∧
     clos_refl_trans hb_weak m y ∧ is_write (lab m)).

Lemma hb_weak_TW :
  ∀ (T: transitive po)
    (INCL : inclusion deps po)
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom) x y
    (P : clos_refl_trans hb_weak x y)
    (R : is_write (lab y)),
  clos_refl po x y ∨
  (∃ m : actid,
     clos_refl_trans hb_weak x m ∧ is_read (lab m) ∧
     clos_refl_trans hb_weak m y ∧ po m y).

The observation condition is equivalent to the simplified one.

Proposition observation_condition_simplify :
  ∀ (T: transitive po)
    (INCL : inclusion deps po)
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom)
    (CcoT: transitive co)
    (ACYC: acyclic hb_power)
    (UNI: uniproc_condition),
  observation_condition ↔ observation_condition_simpl.

Lemma hb_from_read (T: transitive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom) x y :
  hb_power x y → is_read (lab x) →
  po x y ∧ is_access (lab y).

Lemma is_accessE a : is_access a ↔ is_read a ∨ is_write a.

Lemma hbE (T: transitive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom) x y :
  hb_power x y ↔
  sync x y ∧ is_write (lab x) ∧ is_read (lab y) ∨ hb_weak x y.

Lemma rt_hbE (T: transitive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom) x y :
  clos_refl_trans hb_power x y ↔
  ∃ z, clos_refl_trans hb_weak x z ∧
            (z = y ∨ sync z y ∧ is_write (lab z) ∧ is_read (lab y)).

Lemma t_hbE (T: transitive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom) x y :
  clos_trans hb_power x y ↔
  clos_trans hb_weak x y ∨
  ∃ z, clos_refl_trans hb_weak x z ∧ sync z y
            ∧ is_write (lab z) ∧ is_read (lab y).

Lemma acyclic_hbE
      (T: transitive po)
      (IRR: irreflexive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) :
  acyclic hb_power ↔ acyclic hb_weak.

Lemma sync_fence_weak_trans :
  ∀ (T: transitive po) a b c
         (S : sync a b)
         (F: fence_weak b c),
  sync a c ∧ is_write (lab a) ∧ is_read (lab c) ∨ fence_weak a c.

Lemma fence_weak_sync_trans :
  ∀ (T: transitive po) a b c
         (F: fence_weak a b)
         (S : sync b c),
  sync a c ∧ is_write (lab a) ∧ is_read (lab c) ∨ fence_weak a c.

Lemma fence_weak_sync_trans2 :
  ∀ (T: transitive po) a b c d
         (F: fence_weak a b)
         (PO: clos_refl po b c)
         (S : sync c d),
  sync a d ∧ is_write (lab a) ∧ is_read (lab d) ∨ fence_weak a d.

Lemma sync_trans2 (T: transitive po) a b c d :
  sync a b →
  clos_refl po b c →
  sync c d →
  sync a d.

Lemma prop_baseE (T: transitive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) x y :
  prop_base x y ↔
  prop_base_weak x y ∨ sync x y ∧ is_write (lab x) ∧ is_read (lab y).

Lemma base_weak_sync_trans (T: transitive po)
      (CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
      (INCL: inclusion deps po)
      a b c :
  prop_base_weak a b →
  sync b c →
  prop_base_weak a c
  ∨ sync a c ∧ is_write (lab a) ∧ is_read (lab c).

Lemma sync_expand (T: transitive po)
      (CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
      (INCL: inclusion deps po)
      a b :
  sync a b →
  fence_weak a b
  ∨ sync a b ∧ is_write (lab a) ∧ is_read (lab b).

Lemma prop_base_weak_hb_weak_trans a b c :
  prop_base_weak a b →
  clos_refl_trans hb_weak b c →
  prop_base_weak a c.

Lemma sync_hb_sync :
  ∀ (T: transitive po)
      (CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
      (INCL: inclusion deps po)
      a b c d
      (S: sync a b)
      (C: clos_refl_trans hb_weak b c)
      (S': sync c d),
  prop_base_weak a c ∧ sync c d ∨
  sync a b ∧ clos_refl_trans hb_weak b d ∨
  sync a d ∧ is_write (lab a) ∧ is_read (lab d).

Lemma rt_prop_baseE (T: transitive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) x y
      (P: clos_refl_trans prop_base x y) :
  clos_refl_trans prop_base_weak x y ∨
  ∃ z,
    clos_refl_trans prop_base_weak x z ∧
    ∃ w,
      sync z w ∧ clos_refl_trans hb_weak w y.

We prove that the two definitions of the propagation order are equivalent.

Lemma propE (T: transitive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) x y :
  prop x y ↔ prop_weak x y.

As a result, we can further simplify the observation condition.

Lemma observation_condition_alternative :
  ∀ (T: transitive po)
    (INCL : inclusion deps po)
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom)
    (UNI: uniproc_condition),
  observation_condition_simpl ↔ observation_condition_alt.

Lemma sync_base_weak_trans (T: transitive po)
      (CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
      (INCL: inclusion deps po)
      a b c :
  sync a b →
  prop_base_weak b c →
  is_read (lab b) →
  prop_base_weak a c ∨ sync a c ∧ is_write (lab a) ∧ is_read (lab c).

Lemma sync_rt_base_weak_trans (T: transitive po)
      (CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
      (INCL: inclusion deps po)
      a b c :
  sync a b →
  clos_refl_trans prop_base_weak b c →
  is_read (lab b) →
  clos_refl_trans prop_base_weak a c
  ∨ sync a c ∧ is_write (lab a) ∧ is_read (lab c).

Lemma rt_base_weak_sync_trans (T: transitive po)
      (CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
      (INCL: inclusion deps po)
      a b c :
  clos_refl_trans prop_base_weak a b →
  sync b c →
  is_write (lab b) →
  clos_refl_trans prop_base_weak a c
  ∨ sync a c ∧ is_write (lab a) ∧ is_read (lab c).

Notation "P +++ Q" := (union P Q) (at level 50, left associativity).

Lemma propE2 (T: transitive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) :
  prop ↔ prop_weak.

Lemma propagation_simpl1
      (T: transitive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) :
  acyclic (co +++ prop) ↔
  acyclic (co +++ restr_rel (fun x ⇒ is_write (lab x)) prop_base_weak
              +++ (seq (seq (clos_refl fre) (clos_refl rfe))
                       (seq (clos_refl_trans prop_base_weak)
                            (seq sync (clos_refl_trans hb_weak))))).

Lemma inclusion_base_weak_base :
  inclusion prop_base_weak prop_base.

Lemma prop_base_so_trans so :
  transitive (prop_base_so so).

Lemma inclusion_fence_so so : inclusion fence_weak (fence_so so).

Lemma inclusion_hb_so so : inclusion hb_weak (hb_so so).

Lemma inclusion_base_so so :
  inclusion prop_base_weak (prop_base_so so).

Lemma inclusion_fence_hb_so so : inclusion (fence_so so) (hb_so so).

Lemma inclusion_base_hb_so so :
  inclusion (prop_base_so so) (clos_trans (hb_so so)).

Hint Resolve inclusion_fence_so : inclusion.
Hint Resolve inclusion_hb_so : inclusion.
Hint Resolve inclusion_base_so : inclusion.
Hint Resolve inclusion_fence_hb_so : inclusion.
Hint Resolve inclusion_base_hb_so : inclusion.

Equivalence between the two models


Lemma so_sync_case_split :
  ∀ so (CsoF : is_total (fun a : actid ⇒ lab a = Async) so)
            (T : transitive so)
            (IRR: irreflexive so)
         x y (S: union (so_step so) sync x y)
         z w (S': union (so_step so) sync z w),
  sync x w ∧ sync z y ∨ so_step so x w ∨ so_step so z y.

Lemma rfe_base_so_trans (CrfD: ConsistentRF_dom) so a b c:
  rfe a b →
  prop_base_so so b c →
  prop_base_so so a c.

Lemma rrfe_base_so_trans (CrfD: ConsistentRF_dom) so a b c:
  clos_refl rfe a b →
  prop_base_so so b c →
  prop_base_so so a c.

Lemma helper_so_irreflexive :
  ∀ (T: transitive po)
    (IRR: irreflexive po)
    (INCL: inclusion deps po)
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom) so
    (CsoF : is_total (fun a ⇒ lab a = Async) so)
    (CsoT : transitive so)
    (CsoI : irreflexive so)
    (UNI: uniproc_condition)
    (NTA: acyclic (hb_so so))
    (OBS: ∀ x y, fre x y → prop_base_so so y x → False),
 irreflexive
     (seq (seq (clos_refl fre) (clos_refl rfe))
        (seq (clos_refl_trans prop_base_weak)
           (seq (so_step so +++ sync) (clos_refl_trans hb_weak)))).

Lemma helper_so_transitive :
  ∀ (T: transitive po)
    (IRR: irreflexive po)
    (INCL: inclusion deps po)
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom) so
    (CsoF : is_total (fun a ⇒ lab a = Async) so)
    (CsoT : transitive so)
    (CsoI : irreflexive so)
    (UNI: uniproc_condition)
    (NTA: acyclic (hb_so so))
    (OBS: ∀ x y, fre x y → prop_base_so so y x → False),
  transitive
    (seq (seq (clos_refl fre) (clos_refl rfe))
         (seq (clos_refl_trans prop_base_weak)
              (seq (union (so_step so) sync) (clos_refl_trans hb_weak)))).

Lemma propagation_expand
      (T: transitive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) :
  acyclic (co +++ prop) ↔
  acyclic (seq (seq (clos_refl fre) (clos_refl rfe))
               (seq (clos_refl_trans prop_base_weak)
                    (seq sync (clos_refl_trans hb_weak)))) ∧
  acyclic (co +++ restr_rel (fun x ⇒ is_write (lab x)) prop_base_weak
              +++ restr_rel (fun x ⇒ is_write (lab x))
                (clos_trans
                   (seq (seq (clos_refl fre) (clos_refl rfe))
                        (seq (clos_refl_trans prop_base_weak)
                             (seq sync (clos_refl_trans hb_weak)))))).

Completeness of the model with a total order on syncs with respect to the default Power model.

Lemma SyncTotal_complete
      (INCL: inclusion deps po) so
      (C: ConsistentSyncTotal so) :
  ConsistentPower.

For the soundness direction, we use the following auxiliary definition.

Definition Trel :=
  restr_rel (fun x ⇒ lab x = Async)
    (seq (seq po (clos_refl_trans hb_weak))
         (seq (clos_refl_trans (co +++ prop_weak))
              (seq (clos_refl chapo)
                   (seq (clos_refl_trans prop_base_weak) po)))).

Lemma helper_prop_alt_restr
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) :
  restr_rel (fun x : actid ⇒ ¬ is_access (lab x))
    (seq (clos_refl chapo)
         (seq (clos_refl_trans prop_base_weak)
              (seq
                 (fun x y ⇒
                    ∃ s : actid, po x s ∧ po s y ∧ lab s = Async)
                 (clos_refl_trans hb_weak))))
  ↔
  restr_rel (fun x : actid ⇒ ¬ is_access (lab x))
     (fun x y ⇒ ∃ s, po x s ∧ po s y ∧ lab s = Async).

Lemma seqA2 X (r r' r'' : relation X) x y :
  seq (seq r r') r'' x y ↔ seq r (seq r' r'') x y.

Lemma helper1 :
  ∀
    (T: transitive po)
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom) x y
    (R : clos_trans
         (seq (clos_refl chapo)
              (seq (clos_refl_trans prop_base_weak)
                   (seq
                      (fun x y : actid ⇒
                         ∃ s : actid, po x s ∧ po s y ∧ lab s = Async)
                      (clos_refl_trans hb_weak)))) x y)
    (ACC : is_access (lab y)),
  seq
    (seq (clos_refl chapo)
         (seq (clos_refl_trans prop_base_weak)
              (seq
                 (fun x y : actid ⇒
                    ∃ s, po x s ∧ po s y ∧ lab s = Async
                              ∧ is_access (lab y))
                 (clos_refl_trans hb_weak))))
    (clos_refl_trans
       (seq (clos_refl chapo)
            (seq (clos_refl_trans prop_base_weak)
                 (seq sync (clos_refl_trans hb_weak))))) x y.

Lemma helper2 :
  ∀
    (T: transitive po)
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom) x y
    (R : clos_trans
         (seq (clos_refl chapo)
              (seq (clos_refl_trans prop_base_weak)
                   (seq
                      (fun x y : actid ⇒
                         ∃ s : actid, po x s ∧ po s y ∧ lab s = Async)
                      (clos_refl_trans hb_weak)))) x y)
    (ACC : is_access (lab x))
    (ACC : is_access (lab y)),
    clos_trans
      (seq (clos_refl chapo)
           (seq (clos_refl_trans prop_base_weak)
                 (seq sync (clos_refl_trans hb_weak)))) x y.

Lemma acyclic_prop_alt
      (T: transitive po)
      (IRR: irreflexive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) :
  acyclic (co +++ prop) ↔
  acyclic (co +++ restr_rel (fun x ⇒ is_write (lab x)) prop_base_weak
              +++ seq (clos_refl chapo)
              (seq (clos_refl_trans prop_base_weak)
                   (seq (fun x y ⇒ ∃ s, po x s ∧ po s y ∧ lab s = Async)
                        (clos_refl_trans hb_weak)))).

Lemma inclusion_base_weak_hb2 :
  inclusion prop_base_weak (clos_trans hb_weak).

Lemma helper_prop_access
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) a b :
  seq (clos_refl chapo)
      (seq (clos_refl_trans prop_base_weak)
           (seq sync (clos_refl_trans hb_weak))) a b →
  is_access (lab a) ∧ is_access (lab b).

Lemma coprop_access
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) a b :
  clos_trans (co +++ prop_weak) a b →
  is_access (lab a) ∧ is_access (lab b).

From the propagation axiom, we get that Trel is acyclic.

Lemma acyclic_Trel
      (T: transitive po)
      (IRR: irreflexive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom)
      (H : acyclic (co +++ prop)) :
  acyclic Trel.

Lemma so_step_trans so
  (CsoF: is_total (fun a ⇒ lab a = Async) so)
  (CsoT: transitive so)
  (Cww: ∀ x y (SO : so_step so x y)
               (HB: clos_refl_trans hb_weak y x), False) a b
  (A: so_step so a b) c
  (B: clos_refl_trans hb_weak b c) d
  (C: so_step so c d) :
  so_step so a d.

Lemma rt_hb_soE so
  (CsoF: is_total (fun a ⇒ lab a = Async) so)
  (CsoT: transitive so)
  (Cww: ∀ x y (SO : so_step so x y)
               (HB: clos_refl_trans hb_weak y x), False) :
  clos_refl_trans (hb_so so) ↔
  seq (clos_refl_trans hb_weak)
      (seq (clos_refl (so_step so)) (clos_refl_trans hb_weak)).

Lemma t_hb_soE so
  (CsoF: is_total (fun a ⇒ lab a = Async) so)
  (CsoT: transitive so)
  (OTH: ∀ x y (SO : so_step so x y)
               (HB: clos_refl_trans hb_weak y x), False) :
  clos_trans (hb_so so) ↔
  union (clos_trans hb_weak)
    (seq (clos_refl_trans hb_weak)
         (seq (so_step so) (clos_refl_trans hb_weak))).

Lemma seq_union_l X (r1 r2 r : relation X) :
  seq (r1 +++ r2) r ↔ seq r1 r +++ seq r2 r.

Lemma seq_union_r X (r r1 r2 : relation X) :
  seq r (r1 +++ r2) ↔ seq r r1 +++ seq r r2.

Lemma seqA X (r1 r2 r3 : relation X) :
  seq (seq r1 r2) r3 ↔ seq r1 (seq r2 r3).

Lemma unionA X (r1 r2 r3 : relation X) :
  union (union r1 r2) r3 ↔ union r1 (union r2 r3).

Lemma unionC X (r1 r2 : relation X) :
  union r1 r2 ↔ union r2 r1.

Lemma base_soE so
  (CsoF: is_total (fun a ⇒ lab a = Async) so)
  (CsoT: transitive so)
  (OTH: ∀ x y (SO : so_step so x y)
               (HB: clos_refl_trans hb_weak y x), False) :
  prop_base_so so ↔
  union
    (seq (clos_refl rfe) (seq (so_step so) (clos_refl_trans hb_weak)))
    (seq prop_base_weak (seq (clos_refl (so_step so)) (clos_refl_trans hb_weak))).

Lemma base_soE2 so
  (CsoF: is_total (fun a ⇒ lab a = Async) so)
  (CsoT: transitive so)
  (OTH: ∀ x y (SO : so_step so x y)
               (HB: clos_refl_trans hb_weak y x), False) :
  prop_base_so so ↔
  union prop_base_weak
    (union (seq rfe (seq (so_step so) (clos_refl_trans hb_weak)))
      (seq (clos_refl prop_base_weak) (seq (so_step so) (clos_refl_trans hb_weak)))).

We define some further auxiliary definitions, which help us reason about paths involving sync edges.

Definition sync_ext_l x y := po x y ∧ is_access (lab x) ∧ lab y = Async.
Definition sync_ext_r x y := po x y ∧ lab x = Async ∧ is_access (lab y).
Definition sync_ext := union sync (union sync_ext_l sync_ext_r).

Definition fence_ext := union fence (union sync_ext_l sync_ext_r).

Definition hb_ext := union ppo (union fence_ext rfe).

Definition prop_base_ext :=
  (seq (clos_refl rfe) (seq fence_ext (clos_refl_trans hb_ext))).

Definition prop_ext :=
  union (restr_rel (fun x ⇒ is_write (lab x)) prop_base_weak)
        (seq (clos_refl chapo)
             (seq (clos_refl_trans prop_base_weak)
                  (seq sync_ext (clos_refl_trans hb_weak)))).

Lemma prop_extE
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) :
  prop_ext ↔
  prop_weak +++
  seq (clos_refl chapo) (seq (clos_refl_trans prop_base_weak) sync_ext_l) +++
  seq (sync_ext_r) (clos_refl_trans hb_weak).

We prove a few basic lemmas that allow us to perform equational reasoning.

Lemma seq_sync :
  seq sync_ext_l sync_ext_r ↔ sync.

Lemma seq_sync_ext_l :
  seq sync_ext_l sync_ext_l ↔ (fun _ _ ⇒ False).

Lemma seq_sync_ext_r :
  seq sync_ext_r sync_ext_r ↔ (fun _ _ ⇒ False).

Lemma seq_sync_ext_chapo
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) :
  seq sync_ext_l (clos_refl chapo) ↔ sync_ext_l.

Lemma seq_sync_ext_base_star
      (CrfD: ConsistentRF_dom) :
  seq sync_ext_l (clos_refl_trans prop_base_weak) ↔ sync_ext_l.

Lemma seq_hb_weak_star_sync_ext
      (CrfD: ConsistentRF_dom) :
  seq (clos_refl_trans hb_weak) sync_ext_r ↔ sync_ext_r.

Lemma coprop_extE
      (T: transitive po)
      (IRR: irreflexive po)
      (INCL: inclusion deps po)
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) :
  acyclic (co +++ prop_ext) ↔
  acyclic (co +++ prop_weak).

Lemma helper_restr1
      (CrfD: ConsistentRF_dom)
      (CcoD: ConsistentMO_dom) r :
  restr_rel (fun x : actid ⇒ lab x ≠ Async)
            (restr_rel (fun x ⇒ lab x = Async) r +++ co +++ prop_ext)
  ↔
  restr_rel (fun x : actid ⇒ lab x ≠ Async)
            (co +++ prop_weak).

Lemma prop_ext_sync_r :
  ∀
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom) x y (L: lab y = Async),
  prop_ext x y ↔
  seq (clos_refl chapo) (seq (clos_refl_trans prop_base_weak) sync_ext_l) x y.

Lemma prop_ext_sync_l :
  ∀
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom) x y (L: lab x = Async),
  prop_ext x y ↔
  seq (sync_ext_r) (clos_refl_trans hb_weak) x y.

Lemma prop_ext_sync_both :
  ∀
    (CrfD: ConsistentRF_dom)
    (CcoD: ConsistentMO_dom) x y (L: lab x = Async) (L' : lab y = Async),
  prop_ext x y ↔ False.

We next prove that the soundness of the alternative model.

Lemma SyncTotal_sound
      (INCL: inclusion deps po) (C: ConsistentPower) :
  ∃ so, ConsistentSyncTotal so.

Putting the two directions together, we get that the two Power models are equivalent.

Theorem SyncTotal (INCL: inclusion deps po):
  ConsistentPower ↔ ∃ so, ConsistentSyncTotal so.

End PowerModel.

This page has been generated by coqdoc