Correspondence between SRA and SRArmw


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 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)).
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 : natS (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 : natS (double x)))).
  apply div2_even in H0; rewrite (even_double _ H0);
  split; [left; apply in_map
         |right; apply in_map with (f := (fun x : natS (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 rto_rmw (lab r) (lab a)
           | Nonelab 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 rrf r
                               | Nonerf x
                             end) :
  ConsistentSRA acts (fun xif rmw_read x then Askip 0
                               else match getr x with
                                      | Some rto_rmw (lab r) (lab x)
                                      | Nonelab 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