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.
Definition to_load a :=
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'
| Aload tid _ _ _ ⇒ Askip tid
| _ ⇒ a
end.
Lemma is_write_to_load x : is_write (to_load x) = false.
Lemma is_write_to_store x : is_write (to_store x) = is_write x.
Lemma is_read_to_load x : is_read (to_load x) = is_read x.
Lemma is_read_to_store x : is_read (to_store x) = false.
Lemma is_rmw_to_load x : is_rmw (to_load x) = false.
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 x ⇒ double x) acts
++ map (fun x ⇒ S (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 y ⇒ Some (S (double y))
| None ⇒ None
end
else None) :
ConsistentSRArmw acts' (fun x ⇒ if even_odd_dec x then to_load (lab (div2 x))
else to_store (lab (div2 x)))
sb' rf'
(fun x y ⇒ is_rmw (lab (div2 x)) ∧ div2 x = div2 y ∧ y = S x)
(fun x y ⇒ odd 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'
| _, _ ⇒ Askip 0
end.
Lemma loc_helper
lab sb rmw (C: ConsistentRMW_dom lab sb rmw)
rmw_read (RMWR: ∀ x, rmw_read x = true ↔ ∃ rmw_w, rmw x rmw_w)
getr (GETL: ∀ x y, getr y = Some x ↔ rmw x y)
a (W : is_write (lab a)) :
loc (if rmw_read a
then Askip 0
else
match getr a with
| Some r ⇒ to_rmw (lab r) (lab a)
| None ⇒ lab 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)
rmw_read (RMWR: ∀ x, rmw_read x = true ↔ ∃ rmw_w, rmw x rmw_w)
getr (GETL: ∀ x y, getr y = Some x ↔ rmw x y)
rf' (RFE: ∀ x, rf' x =
if rmw_read x then None
else match getr x with
| Some r ⇒ rf r
| None ⇒ rf x
end) :
ConsistentSRA acts (fun x ⇒ if rmw_read x then Askip 0
else match getr x with
| Some r ⇒ to_rmw (lab r) (lab x)
| None ⇒ lab x
end)
sb rf' mo.
This page has been generated by coqdoc