# The Power memory model

In this section, we define the Power memory model of Alglave et al. We show that it is equivalent to reorderings over a stronger model requiring the relation (po U rf) to be acyclic.

Require Import List Relations Setoid Omega Permutation.
Require Import Classical ClassicalDescription.
Require Import Vbase extralib ExtraRelations.
Set Implicit Arguments.

Definition actid := nat.

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

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

Definition is_access a :=
match a with
| Aload _ _ | Astore _ _true
| _false
end.

match a with
| _false
end.

Definition is_write a :=
match a with
| Astore _ _true
| _false
end.

Definition is_fence a :=
match a with
| Alwsync | Asynctrue
| _false
end.

Lemma is_write_access a : is_write a is_access a.

Hint Resolve is_read_access is_write_access : access.

## Power memory model definition

Section PowerModel.

Variable acts : list actid.
Variable lab : actid act.
Variable po : relation actid.
Variable deps : relation actid.
Variable rmw : relation actid.
Variable ppo : relation actid.
Variable rf : actid option actid.
Variable co : relation actid.

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 x y :=
po x y is_access (lab x) is_access (lab y) loc (lab x) = loc (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 := sync +++ lwsync.

Definition hb_power := ppo +++ fence +++ rfe.

Definition prop_base :=
clos_refl rfe ;; fence ;; clos_refl_trans hb_power.

Definition chapo :=
rfe +++ fre +++ coe +++ (fre ;; rfe) +++ (coe ;; rfe).

Definition prop :=
restr_rel (fun xis_write (lab x)) prop_base
+++ (clos_refl chapo ;; clos_refl prop_base ;; 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)

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 >>
<< WRITE: is_write (lab b) >>
<< LOCEQ: loc (lab a) = loc (lab b) >>.

The constraints on the preserved program order (PPO)

Definition ppo_lower_bound :=
a b,
clos_trans (deps +++ po_loc) a b
is_write (lab b)
ppo a b.

Definition ppo_upper_bound :=
a b,
ppo a b
immediate po a b
clos_trans (deps +++ po_loc) a b.

The Power model

Definition ConsistentPower :=
<< CppoL: ppo_lower_bound >>

<< 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 : acyclic (po_loc +++ (fun x yrf y = Some x) +++ co +++ fr) >>
<< ATOM : irreflexive (rmw ;; fre ;; coe) >>
<< NTA : acyclic hb_power >>
<< OBS : irreflexive (fre ;; prop ;; clos_refl_trans hb_power) >>
<< PROP: acyclic (co +++ prop) >>.

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

## A stronger acyclicity condition

Definition nta_rel :=
deps +++ po_loc
+++ (fun x ypo x y (is_fence (lab x) is_fence (lab y)))
+++ rfe.

Lemma acyclic_nta
(CsbT: transitive po)
(CsbI: irreflexive po)
(Cdeps: inclusion deps po)
(CrfD: ConsistentRF_dom)
(NTA : acyclic hb_power)
(PPO_lower : ppo_lower_bound) :
acyclic nta_rel.

End PowerModel.

Definition ntb_rel i ll lab deps rf x y :=
In x i In y (concat ll)
nta_rel lab (mk_po i ll) deps rf x y.

Lemma acyclic_ntb i ll lab deps ppo rf
(ND: NoDup (i ++ concat ll))
(INIT: x, is_read (lab x) In x (concat ll))
(Cdeps: inclusion deps (mk_po i ll))
(CrfD: ConsistentRF_dom lab rf)
(NTA : acyclic (hb_power lab (mk_po i ll) ppo rf))
(PPO_lower : ppo_lower_bound lab (mk_po i ll) deps ppo) :
acyclic (ntb_rel i ll lab deps rf).

Add Parametric Morphism : rfe with signature
same_relation ==> eq ==> same_relation as rfe_mor.

Add Parametric Morphism : coe with signature
same_relation ==> eq ==> same_relation as coe_mor.

Add Parametric Morphism : fre with signature
same_relation ==> eq ==> eq ==> same_relation as fre_mor.

Add Parametric Morphism : po_loc with signature
eq ==> same_relation ==> same_relation as po_loc_mor.

Add Parametric Morphism : sync with signature
eq ==> same_relation ==> same_relation as sync_mor.

Add Parametric Morphism : lwsync with signature
eq ==> same_relation ==> same_relation as lwsync_mor.

Add Parametric Morphism : hb_power with signature
eq ==> same_relation ==> eq ==> eq ==> same_relation as hb_power_mor.

Add Parametric Morphism : prop_base with signature
eq ==> same_relation ==> eq ==> eq ==> same_relation as prop_base_mor.

Add Parametric Morphism : prop with signature
eq ==> same_relation ==> eq ==> eq ==> eq ==> same_relation as prop_mor.

Add Parametric Morphism : ppo_lower_bound with signature
eq ==> same_relation ==> eq ==> eq ==> iff as ppo_lower_mor.

Add Parametric Morphism : ConsistentRMW_dom with signature
eq ==> same_relation ==> eq ==> iff as ConsistentRMW_dom_mor.

Add Parametric Morphism : ConsistentPower with signature
eq ==> same_relation ==> eq ==> eq ==> eq ==> eq ==> eq ==> iff as ConsistentPower_mor.

Add Parametric Morphism : nta_rel with signature
eq ==> same_relation ==> eq ==> eq ==> same_relation as nta_rel_mor.

## Soundness and completeness of reorderings

Lemma po_loc_reorder lab po a b
(LOC: loc (lab a) loc (lab b)) :
po_loc lab (reorder po a b) <--> po_loc lab po.

Lemma rfe_reorder lab po rf a b
(Crf: ConsistentRF_dom lab rf)
(LOC: loc (lab a) loc (lab b)) :
rfe (reorder po b a) rf <--> rfe po rf.

Lemma fre_reorder lab po rf co a b
(Crf: ConsistentRF_dom lab rf)
(Cco: ConsistentMO_dom lab co)
(LOC: loc (lab a) loc (lab b)) :
fre (reorder po b a) rf co <--> fre po rf co.

Lemma coe_reorder lab po co a b
(Cco: ConsistentMO_dom lab co)
(LOC: loc (lab a) loc (lab b)) :
coe (reorder po b a) co <--> coe po co.

Lemma sync_reorder lab (po : relation actid) a b
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b)) :
sync lab (reorder po a b) <--> sync lab po.

Lemma lwsync_reorder lab (po : relation actid) a b
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b)) :
lwsync lab (reorder po a b) <--> lwsync lab po.

Lemma hbp_reorder lab po ppo rf a b
(Crf: ConsistentRF_dom lab rf)
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
(LOC: loc (lab a) loc (lab b)) :
hb_power lab (reorder po a b) ppo rf <--> hb_power lab po ppo rf.

Lemma base_reorder lab po ppo rf a b
(Crf: ConsistentRF_dom lab rf)
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
(LOC: loc (lab a) loc (lab b)) :
prop_base lab (reorder po a b) ppo rf <--> prop_base lab po ppo rf.

Lemma prop_reorder lab po ppo rf co a b
(Crf: ConsistentRF_dom lab rf)
(Cmo: ConsistentMO_dom lab co)
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
(LOC: loc (lab a) loc (lab b)) :
prop lab (reorder po a b) ppo rf co <--> prop lab po ppo rf co.

Lemma nta_rel_reorder lab po ppo rf a b
(Crf: ConsistentRF_dom lab rf)
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
(LOC: loc (lab a) loc (lab b)) :
nta_rel lab (reorder po a b) ppo rf <--> nta_rel lab po ppo rf.

Lemma ntb_rel_reorder i ll1 l1 a b l2 ll2 lab ppo rf
(WF: NoDup (i ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)))
(Crf: ConsistentRF_dom lab rf)
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
(LOC: loc (lab a) loc (lab b)) :
ntb_rel i (ll1 ++ (l1 ++ a :: b :: l2) :: ll2) lab ppo rf <-->
ntb_rel i (ll1 ++ (l1 ++ b :: a :: l2) :: ll2) lab ppo rf.

Lemma ConsistentRMW_dom_reorder lab po rmw x y
(LOC: loc (lab x) loc (lab y)) :
ConsistentRMW_dom lab (reorder po x y) rmw
ConsistentRMW_dom lab po rmw.

Lemma ppo_lower_bound_reorder lab po deps ppo a b
(LOC: loc (lab a) loc (lab b)) :
ppo_lower_bound lab (reorder po a b) deps ppo
ppo_lower_bound lab po deps ppo.

Lemma ConsistentPower_reorder :
lab po deps rmw ppo rf co a b
(NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
(LOC: loc (lab a) loc (lab b)),
ConsistentPower lab po deps rmw ppo rf co
ConsistentPower lab (reorder po a b) deps rmw ppo rf co.

## Reduction of the Power memory model

Definition Power_reorder lab init deps (ll ll' : list (list actid)) :=
ll1 l1 a b l2 ll2,
<< NFa: ¬ is_fence (lab a) >>
<< NFb: ¬ is_fence (lab b) >>
<< LOC: loc (lab a) loc (lab b) >>
<< Nab: ¬ deps a b >>
<< WF: NoDup (init ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)) >>
<< EQ : ll = ll1 ++ (l1 ++ a :: b :: l2) :: ll2 >>
<< EQ': ll' = ll1 ++ (l1 ++ b :: a :: l2) :: ll2 >>.

Fixpoint metric (ord: relation actid) (ll : list actid) :=
match ll with
| nil ⇒ 0
| a :: ll
length (filter (fun xif excluded_middle_informative (ord x a)
then true else false) ll) +
metric ord ll
end.

Add Parametric Morphism : metric with signature
same_relation ==> eq ==> eq as metric_mor.

Lemma reorder_metric (ord : relation actid)
(T: transitive ord) (IRR: irreflexive ord) ll1 l1 a b (ORD: ord b a) l2 ll2 :
metric ord (concat (ll1 ++ (l1 ++ b :: a :: l2) :: ll2)) <
metric ord (concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)).

Power-coherence is equivalent to performing reorderings over the stronger Power model that additionally requires (po U rf) to be acyclic.

Theorem Power_alternative :
lab init ll (ND: NoDup (init ++ concat ll)) deps
(WF: inclusion deps (mk_po init ll))
(INIT: x, is_read (lab x) In x (concat ll))
(MAIN: x, In x (concat ll) is_access (lab x))
rmw ppo rf co,
ConsistentPower lab (mk_po init ll) deps rmw ppo rf co

ll',
clos_refl_trans (Power_reorder lab init deps) ll ll'
ConsistentPower lab (mk_po init ll') deps rmw ppo rf co
acyclic (mk_po init ll' +++ (fun x yrf y = Some x)).