# Elimination of redundant memory accesses

Require Import Peano_dec ClassicalDescription List Vbase Relations.
Require Import ExtraRelations actions c11 cmon coherence reorder.
Set Implicit Arguments.

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.

Lemma release_seq_only_rmw_rf_relevant :
mt2 lab sb rf rf' mo x y,
release_seq mt2 lab sb rf mo x y
( x (RMW: is_rmw (lab x)), rf' x = rf x) →
release_seq mt2 lab sb rf' mo x 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: XProp) g rel
(T: is_total (fun yf (g y)) rel)
a b v (C: f vf (g b)) (cond : Prop) (C : f vcond),
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 aFalse)
(D: x, rel a xFalse) (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 aFalse)
(D: x, rel a xFalse) (cond : Prop),
transitive _ (lin_ext_a rel cond a b).

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

Lemma is_total_lin_ext_b :
X (f: XProp) g rel
(T: is_total (fun yf (g y)) rel)
a b v (C: f vf (g a)) (cond : Prop) (C : f vcond),
is_total (fun yf (fupd g b v y)) (lin_ext_b rel cond a b).

Lemma irreflexive_lin_ext_b :
X (rel : relation X)
(IRR: irreflexive rel)
a b (NEQ: a b)
(C: x, rel x bFalse)
(D: x, rel b xFalse) (cond : Prop),
irreflexive (lin_ext_b rel cond a b).

Lemma transitive_lin_ext_b :
(X: eqType) (rel : relation X)
(IRR: irreflexive rel)
(T: transitive _ rel) a b
(C: x, rel x bFalse)
(D: x, rel b xFalse) (cond : Prop),
transitive _ (lin_ext_b rel cond a b).

Definition lin_ext_c A (rel : relation A) (cond: Prop) (a b x y : A) :=
clos_trans _ rel x y
cond x = b clos_trans _ rel a y y b.

Lemma transitive_lin_ext_c :
X (rel : relation X) (A: acyclic rel) (cond: Prop) a b
(C: x, rel x bcondx = a rel x a),
transitive _ (lin_ext_c rel cond a b).

Lemma irreflexive_lin_ext_c :
X (rel : relation X) (A: acyclic rel) cond a b,
irreflexive (lin_ext_c rel cond a b).

Lemma acyclic_lin_ext_c :
X (rel : relation X) (A: acyclic rel) (cond: Prop) a b
(C: x, rel x bcondx = a rel x a),
acyclic (lin_ext_c rel cond a b).

Lemma lin_ext_c_extends :
X (rel : relation X) cond a b x y,
rel x ylin_ext_c rel cond a b x y.

Lemma release_seq_upd_mo :
mt2 lab sb rf mo x y a b
(RS: release_seq mt2 lab sb rf (lin_ext_a mo True a b) x y)
(Cmo: x, mo x xFalse)
(NMO: x, mo a xFalse)
(NMO: x, mo x aFalse)
(NRF: x, rf x = Some aFalse)
(NAEQ: is_na (lab a) is_na (lab b))
(SB: sb a b)
(DOM: x, sb a xx = b sb b x)
(NRMW: ¬ is_rmw (lab b))
(NEQ: y a),
if x == a then release_seq mt2 lab sb rf mo b y else release_seq mt2 lab sb rf mo x y.

Lemma release_seq_upd_ow :
lab rf mo x y
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a tid (Aa: lab a = Askip tid)
b typ l v (Ab: lab b = Astore tid typ l v) v'
(sb : relation actid) (SB: sb a b)
(DOM: x, sb a xx = b sb b x) mt2
(RS: release_seq mt2 (fun xif x == a then Astore tid typ l v' else lab x) sb
rf (lin_ext_a mo True a b) x y)
(NEQ: y a),
if x == a then release_seq mt2 lab sb rf mo b y else release_seq mt2 lab sb rf mo x y.

lab mo rf x y
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a tid (Aa: lab a = Askip tid)
b (sb : relation actid) (SB: sb a b)
(DOM: x, sb a xx = b sb b x) asw
typ l v (Ab: lab b = Astore tid typ l v) mt2 v'
(HB: happens_before mt2 (fun xif x == a then Astore tid typ l v' else lab x)
sb asw rf (lin_ext_a mo True a b) x y),
happens_before mt2 lab sb asw rf mo x y.

mt2 lab sb asw rf mo a c
(HB: happens_before mt2 lab sb asw rf mo a c) tid
(Aa: lab a = Askip tid) b
(SBR: sb a b)
(DOM: x, sb a xx = b sb b x)
(DOM': x, asw a xx = b asw b x),
c = b happens_before mt2 lab sb asw rf mo b c.

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

mt (MT: mt MTorig) mt2 acts lab dsb sb asw rf mo sc
(CONS: Semiconsistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc)
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 xx = b sb b x)
(DOM': x, asw a xx = b asw b x)
v' lab' (LAB': lab' = fupd lab a (Astore tid typ l v')),
mo' sc',
CONS': Semiconsistent mt mt2 MTSChb acts lab' sb dsb asw rf mo' sc'
OBS: c d (INc: In c acts) (INd: In d acts)
(NLc: loc (lab c) l) (NLd: loc (lab d) l),
mo c d mo' c d
RACE: race_free mt2 lab' sb asw rf mo'race_free mt2 lab sb asw rf mo .

mt mt2 acts lab dsb sb asw rf mo sc
tid typ l v a b v' lab',
Consistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc
sb a b
lab b = Astore tid typ l v
lab' = fupd lab a (Astore tid typ l v') →
mt MTorig
rf' mo' sc',
CONS': Consistent mt mt2 MTSChb acts lab' sb dsb asw rf' mo' sc'
OBS: c d (INc: In c acts) (INd: In d acts)
(NLc: loc (lab c) l) (NLd: loc (lab d) l),
mo c d mo' c d
RACE: racy mt2 lab sb asw rf moracy mt2 lab' sb asw rf' mo' .

mt2 lab sb asw rf mo b c
(HB: happens_before mt2 lab sb asw rf mo c b) tid
(A: lab b = Askip tid) a
(SBR: sb a b)
(DOM: x, sb x bx = a sb x a)
(DOM': x, asw x bx = a asw x a),
c = a happens_before mt2 lab sb asw rf mo c a.

lab sb rf mo
(Cmo: ConsistentMO lab mo)
b tid (Ab: lab b = Askip tid)
mt2 typ l v x y
(H: release_seq mt2 (fun xif x == b then Aload tid typ l v else lab x)
sb rf mo x y)
rf' (H': x (RMW: is_rmw (lab x)), rf' x = rf x),
release_seq mt2 lab sb rf' mo x y.

lab mo rf x y
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a tid typ l v (Aa: lab a = Astore tid typ l v)
b (Ab: lab b = Askip tid)
(sb: relation actid) (SB: sb a b)
(Csb: ConsistentSB lab sb) asw typ' mt2
(HB: happens_before mt2 (fun xif x == b then Aload tid typ' l v else lab x)
sb asw (fun xif x == b then Some a else rf x) mo x y),
happens_before mt2 lab sb asw rf mo x y.

mt (MT: mt MTorig) mt2 acts lab sb dsb asw rf mo sc
(CONS: Semiconsistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc)
tid typ l v
a (Aa: lab a = Astore tid typ l v)
b (Ab: lab b = Askip tid)
(SB: sb a b)
(DOM: x, sb x bx = a sb x a)
(DOM': x, asw x bx = a asw x a)
lab' typ'
(SCtyp': typ' = RATscfst mt2 = MT2sb)
(LAB': lab' = fun xif x == b then Aload tid typ' l v else lab x),
rf' sc',
CONS': Semiconsistent mt mt2 MTSChb acts lab' sb dsb asw rf' mo sc'
RACE: race_free mt2 lab' sb asw rf' morace_free mt2 lab sb asw rf mo .

mt mt2 acts lab dsb sb asw rf mo sc tid typ typ' l v a b lab',
Consistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc
sb a b
lab a = Astore tid typ l v
lab' = fupd lab b (Aload tid typ' l v) →
mt MTorig
(fst mt2 = MT2sb typ' RATsc) →
rf' sc',
CONS': Consistent mt mt2 MTSChb acts lab' sb dsb asw rf' mo sc'
RACE: racy mt2 lab sb asw rf moracy mt2 lab' sb asw rf' mo .

Ltac first_splitsok :=
first [left; repeat split; unfold same_thread; ins; [] |
right; left; repeat split; unfold same_thread; ins; [] |
do 2 right; left; repeat split; unfold same_thread; ins; [] |
do 3 right; repeat split; unfold same_thread; ins; [] ].

lab mo rf x y
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a tid typ l v (Aa: lab a = Aload tid typ l v)
b (Ab: lab b = Askip tid)
(sb : relation actid) (SB: sb a b) mt2 asw
(HB: happens_before mt2 (fun xif x == b then Aload tid typ l v else lab x)
sb asw (fun xif x == b then rf a else rf x) mo x y),
happens_before mt2 lab sb asw rf mo x y.

mt (MT: mt MTorig) mt2 acts lab sb dsb asw rf mo sc
(CONS: Semiconsistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc)
tid typ l v
a (Aa: lab a = Aload tid typ l v)
b (Ab: lab b = Askip tid)
(SBab: sb a b)
(DOM: x, sb x bx = a sb x a)
(DOM: x, asw x bx = a asw x a)
lab' (LAB': lab' = fun xif x == b then Aload tid typ l v else lab x),
rf' sc',
CONS': Semiconsistent mt mt2 MTSChb acts lab' sb dsb asw rf' mo sc'
RACE: race_free mt2 lab' sb asw rf' morace_free mt2 lab sb asw rf mo .

mt mt2 acts lab dsb sb asw rf mo sc tid typ l v a b lab',
Consistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc
sb a b