# Correspondence between SRA and SRArmw

Require Import Omega Classical List Relations Peano_dec Even Div2.
Require Import Vbase ExtraRelations cactions RAmodels.
Set Implicit Arguments.

We relate SRA-coherence with an alternative definition that does not have update events, but rather splits them into two po-adjacent events: an atomic read event followed by an atomic write event.

match a with
| Armw tid kind l v v'Aload tid RATacq l v
| Astore tid _ _ _Askip tid
| _a
end.

Definition to_store a :=
match a with
| Armw tid kind l v v'Astore tid WATrel l v'
| _a
end.

Lemma is_write_to_store x : is_write (to_store x) = is_write x.

Lemma is_rmw_to_store x : is_rmw (to_store x) = false.

Lemma odd2 x: odd (double x) False.

Lemma evenS x : even (S x) odd x.

Lemma oddS x : odd (S x) even x.

Lemma even2 x: even (double x) True.

Lemma div22 x : div2 (double x) = x.

Lemma div2S2 x : div2 (S (double x)) = x.

We first prove that given an SRA-coherent execution, splitting its update events into pairs of atomic read and write events yields an SRArmw-coherent execution.

Theorem ConsistentSRA_rmw acts lab sb rf mo
(CONS: ConsistentSRA acts lab sb rf mo) acts'
(AEQ: acts' = map (fun xdouble x) acts
++ map (fun xS (double x)) acts)
sb' (POE: x y, sb' x y sb (div2 x) (div2 y)
In (div2 x) acts div2 x = div2 y y = S x)
rf' (RFE: x, rf' x =
if even_odd_dec x then
match rf (div2 x) with
| Some ySome (S (double y))
| NoneNone
end
else None) :
ConsistentSRArmw acts' (fun xif even_odd_dec x then to_load (lab (div2 x))
else to_store (lab (div2 x)))
sb' rf'
(fun x yis_rmw (lab (div2 x)) div2 x = div2 y y = S x)
(fun x yodd x odd y mo (div2 x) (div2 y)).

We now prove the other direction. Given an SRArmw-coherent execution, merging the matching atomic read and write events into a single update events yields an SRA-coherent execution.

Definition to_rmw a a' :=
match a, a' with
| Aload _ _ _ v, Astore tid kind l v'
Armw tid UATrel_acq l v v'
end.

Lemma loc_helper
lab sb rmw (C: ConsistentRMW_dom lab sb rmw)
getr (GETL: x y, getr y = Some x rmw x y)
a (W : is_write (lab a)) :
else
match getr a with
| Some rto_rmw (lab r) (lab a)
| Nonelab a
end) = loc (lab a).

Theorem ConsistentSRA_rmw2 acts lab sb rf mo rmw
(CONS: ConsistentSRArmw acts lab sb rf rmw mo)
(NORMW: a, is_rmw (lab a) = false)
getr (GETL: x y, getr y = Some x rmw x y)

rf' (RFE: x, rf' x =