# Validity of program transformations

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

## Monotonicity

We prove that removing sb edges preserves consistency. That is, adding sb edges is a sound transformation.

Lemma hb_mon sb' sb rf :
inclusion sb' sb
inclusion (happens_before sb' rf) (happens_before sb rf).

Theorem ConsistentRA_mon :
acts lab sb rf mo
(CONS: ConsistentRA acts lab sb rf mo)
sb' (Isb: inclusion sb' sb) (T: transitive sb'),
ConsistentRA acts lab sb' rf mo.

Theorem ConsistentSRA_mon :
acts lab sb rf mo
(CONS: ConsistentSRA acts lab sb rf mo)
sb' (Isb: inclusion sb' sb) (T: transitive sb'),
ConsistentSRA acts lab sb' rf mo.

## Reorderings

We show that adding a program order edge between two adjacent reorderable events preserves consistency. That is, removing the edge is a sound transformation. Combining this with monotonicity, we get that reversing the edge is also sound.
We say that two actions a and b are adjacent according to a relation rel if
• every action directly reachable from b is directly reachable from a;
• every action directly reachable from a, except for b, is also directly reachable by b ;
• every action that reaches a directly can also reach b directly; and
• every action that reaches b directly, except for a, can also reach a directly.
Note that adjacent actions are not necessarily related by rel.

Definition adjacent (rel: relation actid) (a b: actid) :=
LA_ac : c, rel b c rel a c
LA_ca : c, rel c b c a rel c a
LA_cb : c, rel c a rel c b
LA_bc : c, rel a c c b rel b c .

A location is local iff all of its accesses are ordered by program order.

Definition is_local_location lab sb l :=
is_total (fun x : actidis_access (lab x) loc (lab x) = l) sb.

Two events a and b are reorderable if they access different locations, and one of the following holds:
• either a or b access a local location; or
• a is a (release) write and b is an (acquire) read.

Definition can_reorder_relacq lab (a b : actid) :=
WRI : is_write_only (lab a)
DIFF: loc (lab a) loc (lab b) .

Definition can_reorder_local lab sb (a b : actid) :=
DIFF: loc (lab a) loc (lab b)
LOC: is_local_location lab sb (loc (lab a))
is_local_location lab sb (loc (lab b)) .

Definition can_reorder lab sb (a b : actid) :=
can_reorder_local lab sb a b
can_reorder_relacq lab a b.

We start the proof of reordering soundness with some basic helper lemmas.

Lemma hb_ct sb rf x y :
happens_before (clos_trans sb) rf x y happens_before sb rf x y.

Lemma hb_u1_expand sb rf :
a b x y,
happens_before (sb UNION1 (a,b)) rf x y
happens_before sb rf x y
(x = a happens_before sb rf x a)
(y = b happens_before sb rf b y).

Lemma hb_u1_cycle sb rf (ACYC: irreflexive (happens_before sb rf)) :
a b (NEQ: a b) x,
happens_before (sb UNION1 (a,b)) rf x x
happens_before sb rf b a.

Lemma hb_u1_right:
lab sb rf
(ACYC: irreflexive (happens_before sb rf))
(Crf: ConsistentRF_dom lab rf) a b
(CR: can_reorder_relacq lab a b is_local_location lab sb (loc (lab a)))
x (HB: happens_before sb rf x a),
happens_before sb rf x b.

Lemma hb_u1_left:
lab sb rf
(ACYC: irreflexive (happens_before sb rf))
(Crf: ConsistentRF_dom lab rf) a b
(CR: can_reorder_relacq lab a b is_local_location lab sb (loc (lab b)))
x (HB: happens_before sb rf b x),
happens_before sb rf a x.

Lemma hb_u1 lab sb rf :
(ACYC: irreflexive (happens_before sb rf))
(Crf: ConsistentRF_dom lab rf) a b x y
(CR: can_reorder_relacq lab a b)
happens_before (sb UNION1 (a,b)) rf x y
happens_before sb rf x y
(x = a y = b).

Lemma mo_local :
lab sb rf mo (CmoD: ConsistentMO_dom lab mo)
(CmoI: irreflexive mo)
(Cww: CoherentWW sb rf mo) a b
(LOC : is_local_location lab sb (loc (lab a))
is_local_location lab sb (loc (lab b)))
(MO : mo a b),
sb a b.

Lemma fr_local :
lab sb rf mo
(CrfD: ConsistentRF_dom lab rf)
(CmoD: ConsistentMO_dom lab mo)
(CmoI: irreflexive mo)
(Cww: CoherentWW sb rf mo)
(Cwr: CoherentWRplain sb rf mo) a b
(LOC : is_local_location lab sb (loc (lab a))
is_local_location lab sb (loc (lab b))) c
(RF : rf a = Some c) (MO : mo c b) (NEQ: a b),
sb a b.

Lemma hb_u1_expand2 X (sb rf : relation X) :
a b x y,
clos_trans (fun x y ⇒ (sb UNION1 (a,b)) x y rf x y) x y
clos_trans (fun x ysb x y rf x y) x y
(x = a clos_trans (fun x ysb x y rf x y) x a)
(y = b clos_trans (fun x ysb x y rf x y) b y).

Reordering a write with a subsequently adjacent read is sound under SRA.

Theorem ConsistentSRA_reorder_relacq :
acts lab sb rf mo
(CONS: ConsistentSRA acts lab sb rf mo)
a (INa: In a acts) b (INb: In b acts) (NEQ: a b)
(CR: can_reorder_relacq lab a b)
(NSB: ¬ sb b a)
ConsistentSRA acts lab (clos_trans (sb UNION1 (a,b))) rf mo.

Reordering two adjacent accesses of different locations, such that one of them is a local access, is sound under RA.

Theorem ConsistentRA_reorder_local :
acts lab sb rf mo
(CONS: ConsistentRA acts lab sb rf mo)
a (INa: In a acts) b (INb: In b acts) (NEQ: a b)
(CR: can_reorder_local lab sb a b)
(NSB: ¬ sb b a)
ConsistentRA acts lab (clos_trans (sb UNION1 (a,b))) rf mo.

Reordering two adjacent accesses of different locations, such that one of them is a local access, is also sound under SRA.

Theorem ConsistentSRA_reorder_local :
acts lab sb rf mo
(CONS: ConsistentSRA acts lab sb rf mo)
a (INa: In a acts) b (INb: In b acts) (NEQ: a b)
(CR: can_reorder_local lab sb a b)
(NSB: ¬ sb b a)
mo,
ConsistentSRA acts lab (clos_trans (sb UNION1 (a,b))) rf mo.

As a corollary, all the specified reorderable accesses may be soundly be reordered under SRA.

Corollary ConsistentSRA_reorder :
acts lab sb rf mo
(CONS: ConsistentSRA acts lab sb rf mo)
a (INa: In a acts) b (INb: In b acts) (NEQ: a b)
(CR: can_reorder lab sb a b)
(NSB: ¬ sb b a)
mo,
ConsistentSRA acts lab (clos_trans (sb UNION1 (a,b))) rf mo.

Combining the previous theorem with monotonicity, we get the reordering proposition shown in the paper (that talks about reversing an edge).

Definition diff1 X (r: relation X) a b :=
fun x yr x y ¬ (x = b y = a).

Proposition ConsistentSRA_reorder_paper :
acts lab sb rf mo
(CONS: ConsistentSRA acts lab sb rf mo) a b
(CR: can_reorder_local lab sb a b)
(SB: sb a b)
mo,
ConsistentSRA acts lab (clos_trans (diff1 sb a b UNION1 (a,b))) rf mo.

Function update for functions of type actid B. This is defined on actid B functions instead of arbitrary A B functions to work around a limitation of Coq's unification

Definition fupd B f (x : actid) (v : B) (y : actid) :=
if y == x then v else f y.

Helper lemmas for extending a strict total order

Definition lin_ext_a A (rel : relation A) (cond : Prop) (a b x y : A) :=
rel x y
cond x = a y = b
cond x = a rel b y
cond y = a rel x b.

Lemma is_total_lin_ext_a :
X (f: X Prop) g rel
(T: is_total (fun yf (g y)) rel)
a b v (C: f v f (g b)) (cond : Prop) (C : f v cond),
is_total (fun yf (fupd g a v y)) (lin_ext_a rel cond a b).

Lemma irreflexive_lin_ext_a :
X (rel : relation X)
(IRR: irreflexive rel)
a b (NEQ: a b)
(C: x, rel x a False)
(D: x, rel a x False) (cond : Prop),
irreflexive (lin_ext_a rel cond a b).

Lemma transitive_lin_ext_a :
(X: eqType) (rel : relation X)
(IRR: irreflexive rel)
(T: transitive rel) a b
(C: x, rel x a False)
(D: x, rel a x False) (cond : Prop),
transitive (lin_ext_a rel cond a b).

Ltac kill_incons :=
match goal with
| Crf : ConsistentRF_dom ?lab ?rf ,
Cmo : ConsistentMO_dom ?lab ?mo |- _
try by repeat match goal with
| H : rf _ = _ |- _apply Crf in H; desc
| H : mo _ _ |- _apply Cmo in H; desc end;
do 2 try match goal with
| H : lab _ = _ |- _rewrite H in ×
end; ins; desf; eauto
| Crf : ConsistentRF_dom ?lab ?rf ,
Cmo : ConsistentMO_big_dom ?lab ?mo |- _
try by repeat match goal with
| H : rf _ = _ |- _apply Crf in H; desc
| H : mo _ _ |- _apply Cmo in H; desc end;
do 2 try match goal with
| H : lab _ = _ |- _rewrite H in ×
end; ins; desf; eauto
end.

lab sb rf (CrfD : ConsistentRF_dom lab rf) a c
(HB: happens_before sb rf a c) tid
(Aa: lab a = Askip tid) b
(SBR: sb a b)
(DOM: x, sb a x x = b sb b x),
b = c happens_before sb rf b c.

Given two adjacent writes to the same location and with the same access type, we can eliminate the first one.

acts lab sb rf mo
(CONS: ConsistentSRA acts lab sb rf mo)
a tid (Aa: lab a = Askip tid)
b typ l v (Ab: lab b = Astore tid typ l v)
(SBR: sb a b)
(DOM: x, sb a x x = b sb b x)
v' lab' (LAB': lab' = fupd lab a (Astore tid typ l v')),
mo', ConsistentSRA acts lab' sb rf mo'.

lab sb rf (CrfD : ConsistentRF_dom lab rf) b c
(HB: happens_before sb rf c b) tid
(A: lab b = Askip tid) a
(SBR: sb a b)
(DOM: x, sb x b x = a sb x a),
c = a happens_before sb rf c a.

(sb: relation actid) rf a b (SB: sb a b) x y
(HB: happens_before sb (fun xif x == b then Some a else rf x) x y),
happens_before sb rf x y.

acts lab sb rf mo
(CONS: ConsistentSRA acts lab sb rf mo)
tid typ l v
a (Aa: lab a = Astore tid typ l v)
b (Ab: lab b = Askip tid)
(SBR: sb a b)
(DOM: x, sb x b x = a sb x a)
lab' typ' (LAB': lab' = fun xif x == b then Aload tid typ' l v else lab x),
rf', ConsistentSRA acts lab' sb rf' mo.

(sb : relation actid) rf a b (SB: sb a b) x y
(HB: happens_before sb (fun xif x == b then rf a else rf x) x y),
happens_before sb rf x y.