Require Import Omega Classical List Relations Peano_dec Even Div2.
Require Import Vbase ExtraRelations cactions RAmodels.
Set Implicit Arguments.
Remove Hints plus_n_O.
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.
Proof. by destruct x. Qed.
Lemma is_write_to_store x : is_write (to_store x) = is_write x.
Proof. by destruct x. Qed.
Lemma is_read_to_load x : is_read (to_load x) = is_read x.
Proof. by destruct x. Qed.
Lemma is_read_to_store x : is_read (to_store x) = false.
Proof. by destruct x. Qed.
Lemma is_rmw_to_load x : is_rmw (to_load x) = false.
Proof. by destruct x. Qed.
Lemma is_rmw_to_store x : is_rmw (to_store x) = false.
Proof. by destruct x. Qed.
Lemma odd2 x: odd (double x) ↔ False.
Proof.
unfold double; split; ins; induction x; ins; inv H.
rewrite <- plus_n_Sm in *; inv H1; eauto.
Qed.
Lemma evenS x : even (S x) ↔ odd x.
Proof.
split; inversion 1; vauto.
Qed.
Lemma oddS x : odd (S x) ↔ even x.
Proof.
split; inversion 1; vauto.
Qed.
Lemma even2 x: even (double x) ↔ True.
Proof.
unfold double; split; ins; induction x; ins; vauto.
rewrite <- plus_n_Sm in *; vauto.
Qed.
Lemma div22 x : div2 (double x) = x.
Proof.
unfold double; induction x; ins.
rewrite <- plus_n_Sm; ins; congruence.
Qed.
Lemma div2S2 x : div2 (S (double x)) = x.
Proof.
unfold double; induction x; ins.
rewrite <- plus_n_Sm; ins; congruence.
Qed.
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)).
Proof.
unfold ConsistentSRArmw, ConsistentSRA in *; desf; unnw.
assert (HBE: ∀ x y, happens_before sb' rf' x y ↔
happens_before sb rf (div2 x) (div2 y) ∨
In (div2 x) acts ∧ div2 x = div2 y ∧ y = S x).
{ split; ins; desf.
rename H into P; induction P; desf; eauto with hb;
rewrite ?POE, ?RFE in *; desf;
rewrite ?div2S2 in *; desf;
try rewrite <- IHP0 in *; eauto with hb.
apply div2_even in IHP0; apply div2_even in IHP4.
rewrite ?evenS, ?oddS, ?even2, ?odd2, ?div22, ?div2S2 in *; desf;
eby edestruct not_even_and_odd.
cut (happens_before sb' rf' (S (double (div2 x))) (double (div2 y))).
intro H'; eapply finiteHB in H; eauto; desc.
destruct (even_odd_dec x) as [A|A];
try rewrite (even_double _ A); try rewrite (odd_double _ A);
destruct (even_odd_dec y) as [B|B];
try rewrite (even_double _ B); try rewrite (odd_double _ B); eauto;
eapply hb_trans; eauto;
try (by apply t_step; left; rewrite POE; right;
rewrite div22, div2S2; eauto).
eapply hb_trans; eauto;
apply t_step; left; rewrite POE; right; rewrite div22, div2S2; eauto.
induction H.
eapply t_step; rewrite POE, RFE, div22, div2S2; desf; eauto.
by rewrite odd2 in ×.
eapply hb_trans, hb_trans; eauto.
eapply finiteHB in H; desc; eauto.
apply t_step; left; rewrite POE; right; rewrite div22, div2S2; eauto.
by apply t_step; left; rewrite POE; eauto.
}
intuition.
split; unnw; ins; desf; rewrite !in_app_iff.
by left; rewrite (even_double _ e); apply in_map, FIN; intro X; rewrite X in ×.
by right; rewrite (odd_double _ o);
apply in_map with (f := (fun x : nat ⇒ S (double x))), FIN;
intro X; rewrite X in ×.
rewrite POE in *; desf.
apply FIN in H; desc; split;
[destruct (even_odd_dec a)|destruct (even_odd_dec b)];
try (by left; rewrite (even_double _ e); apply in_map);
try (by right; rewrite (odd_double _ o);
apply in_map with (f := (fun x : nat ⇒ S (double x)))).
apply div2_even in H0; rewrite (even_double _ H0);
split; [left; apply in_map
|right; apply in_map with (f := (fun x : nat ⇒ S (double x)))]; ins.
red; ins; rewrite POE in *; desf; eauto; rewrite <- H1, <- ?H3 in *; eauto;
ins; omega.
by destruct (lab (div2 x)); desf.
red; ins; rewrite RFE in *; desf; try (eby edestruct not_even_and_odd);
rewrite ?evenS, ?oddS, ?even2, ?odd2, ?div22, ?div2S2 in *; desf.
by eapply CrfD in Heq; desf; ∃ l, v; split; unfold to_load, to_store; desf.
red; ins; desf; rewrite ?is_read_to_load, ?is_read_to_store in *; ins.
rewrite RFE in *; desf; try (eby edestruct not_even_and_odd); eauto.
red; ins; desc; clarify; unnw; split; rewrite ?POE in ×.
by right; repeat split; eauto; apply FIN; intro X; rewrite X in ×.
split; intros; rewrite ?POE in ×.
by rewrite <- RF0 in *; apply div2_even in RF0; desf; eauto with hb.
split; intros; rewrite ?POE in ×.
by rewrite <- RF0 in *; apply div2_even in RF0; desf; eauto with hb.
rewrite <- RF0; apply div2_even in RF0.
destruct (lab (div2 a)); try done; desf; ins; eauto;
eby edestruct not_even_and_odd.
red; ins; rewrite HBE in *; desf; eauto; omega.
red; ins; desf; try (eby edestruct not_even_and_odd).
eapply CmoD in MO1; desf;
destruct (lab (div2 a)); ins; destruct (lab (div2 b)); ins; desf.
red; ins; desf; rewrite ?is_write_to_store, ?is_write_to_load in *; ins.
assert (NEQ' : div2 a ≠ div2 b); [|by eapply CmoF in NEQ'; desf; eauto].
rewrite (odd_double _ o), (odd_double _ o0) in NEQ; congruence.
by red; ins; desf; repeat split; eauto.
by red; ins; desf; repeat split; eauto.
red; ins; desf; repeat split; eauto.
rewrite HBE in *; desf; eauto.
eby apply div2_even in HB0; edestruct not_even_and_odd.
red; ins; desf; repeat split; eauto;
rewrite HBE, RFE in *; desf; eauto; try (eby edestruct not_even_and_odd);
try (eby apply div2_even in HB0; edestruct not_even_and_odd).
rewrite ?evenS, ?oddS, ?even2, ?odd2, ?div22, ?div2S2 in *; desf.
eapply Cwr; eauto; eapply CrfD in Heq; eapply CmoD in MO1; desf;
destruct (lab a0); ins; destruct (lab (div2 b)); ins; desf.
red; ins; desf; repeat split; eauto; rewrite <- RMW0 in *;
rewrite RFE in *; desf; eauto; try (eby edestruct not_even_and_odd);
try (eby apply div2_even in HB0; edestruct not_even_and_odd).
rewrite ?evenS, ?oddS, ?even2, ?odd2, ?div22, ?div2S2 in *; desf.
eapply Cat with (a:=a0) (c:=div2 c); eauto.
eapply CrfD in Heq; eapply CmoD in MO1; desf;
destruct (lab a0); ins; destruct (lab (div2 b)); ins; desf.
Qed.
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).
Proof.
desf; rewrite ?RMWR, ?GETL in *; desf.
by apply C in Heq; desf; destruct (lab a); ins.
by apply C in Heq0; desf; destruct (lab a0); ins; destruct (lab a); ins.
Qed.
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.
Proof.
unfold ConsistentSRArmw, ConsistentSRA in *; desf; unnw.
assert (HBE: ∀ x y (K: happens_before sb rf' x y),
happens_before sb rf x y).
{ ins; induction K; desf; eauto with hb.
rewrite RFE in *; desf; rewrite ?GETL in *; eauto with hb.
eapply Crmw in Heq0; desf; eauto with hb.
}
intuition; repeat red; unnw; ins; eauto.
split; ins; desf; apply FIN; eauto; intro X; rewrite X in *; ins.
by destruct (lab a0); ins.
rewrite RFE in *; desf; eauto;
rewrite ?GETL, ?RMWR in *; desf;
try (by exfalso; eapply Crmw in Heq1; eapply CrfD in RF;
desc; destruct (lab b));
apply CrfD in RF; desc;
∃ l,v; try apply Crmw in Heq0; try apply Crmw in Heq2;
desc; destruct (lab a0); ins; try destruct (lab a1); ins;
by destruct (lab a); ins; destruct (lab b); ins; desf.
desf; eauto; rewrite RFE in *; desf; eauto.
by eapply GETL, Crmw in Heq1; desf; eauto with caccess.
eapply CmoD in MO; split; desf; rewrite ?RMWR, ?GETL in *; desf;
exploit Crmw; eauto; ins; desf.
by destruct (lab a); ins.
by destruct (lab a0); ins; destruct (lab a); ins; desf.
by destruct (lab b); ins.
by destruct (lab a0); ins; destruct (lab b); ins; desf.
eapply CmoF; eauto; [clear - IWa | clear - IWb]; desf.
by destruct (lab a0); ins; desf.
by destruct (lab a); ins; desf.
assert (LOC': loc (lab a) = loc (lab b)); [|clear LOC].
by apply CmoD in MO; des; erewrite !loc_helper in LOC; eauto.
rewrite RFE in *; desf; eauto.
rewrite GETL in *; desf; apply Crmw in Heq0; desc.
eapply Cwr; eauto with hb.
apply HBE in HB.
apply t_rt_step in HB; desf.
destruct (eqP z a0); desf;
[|by apply POI in HB0; try apply t_rt_step; eauto].
rewrite clos_refl_transE in HB; desf.
by exfalso; apply CmoD in MO; desc; destruct (lab a0).
by exfalso; apply CrfD in HB0; desc; destruct (lab c).
assert (LOC': loc (lab a) = loc (lab b)); [|clear LOC].
by apply CmoD in MO; des; erewrite !loc_helper in LOC; eauto.
rewrite RFE in *; desf; eauto.
rewrite GETL in *; desf; eauto.
specialize (NORMW c); apply CrfD in RF; apply CmoD in MO'; desf.
by destruct (lab c); ins; desf.
Qed.
This page has been generated by coqdoc