Validity of program transformations


Require Import Classical List Relations.
Require Import Vbase ExtraRelations cactions RAmodels.
Set Implicit Arguments.

Monotonicity

We prove that removing sb edges preserves consistency. That is, adding sb edges is a sound transformation.

Lemma hb_mon sb' sb rf :
  inclusion sb' sb →
  inclusion (happens_before sb' rf) (happens_before sb rf).
Proof.
  red; ins; eapply clos_trans_mon; vauto.
  ins; desf; eauto.
Qed.

Theorem ConsistentRA_mon :
  ∀ acts lab sb rf mo
    (CONS: ConsistentRA acts lab sb rf mo)
    sb' (Isb: inclusion sb' sb) (T: transitive sb'),
  ConsistentRA acts lab sb' rf mo.
Proof.
  unfold ConsistentRA; ins; desf; unnw; intuition;
  try red; unnw; ins; try (by exploit hb_mon; eauto).
  split; ins; apply FIN; ins; auto.
Qed.

Theorem ConsistentSRA_mon :
  ∀ acts lab sb rf mo
    (CONS: ConsistentSRA acts lab sb rf mo)
    sb' (Isb: inclusion sb' sb) (T: transitive sb'),
  ConsistentSRA acts lab sb' rf mo.
Proof.
  unfold ConsistentSRA; ins; desf; unnw; intuition;
  try red; unnw; ins; try (by exploit hb_mon; eauto).
  split; ins; apply FIN; ins; auto.
Qed.

Reorderings

We show that adding a program order edge between two adjacent reorderable events preserves consistency. That is, removing the edge is a sound transformation. Combining this with monotonicity, we get that reversing the edge is also sound.
We say that two actions a and b are adjacent according to a relation rel if
  • every action directly reachable from b is directly reachable from a;
  • every action directly reachable from a, except for b, is also directly reachable by b ;
  • every action that reaches a directly can also reach b directly; and
  • every action that reaches b directly, except for a, can also reach a directly.
Note that adjacent actions are not necessarily related by rel.

Definition adjacent (rel: relation actid) (a b: actid) :=
  << LA_ac : ∀ c, rel b c → rel a c >> ∧
  << LA_ca : ∀ c, rel c b → c ≠ a → rel c a >> ∧
  << LA_cb : ∀ c, rel c a → rel c b >> ∧
  << LA_bc : ∀ c, rel a c → c ≠ b → rel b c >>.

A location is local iff all of its accesses are ordered by program order.

Definition is_local_location lab sb l :=
  is_total (fun x : actid ⇒ is_access (lab x) ∧ loc (lab x) = l) sb.

Two events a and b are reorderable if they access different locations, and one of the following holds:
  • either a or b access a local location; or
  • a is a (release) write and b is an (acquire) read.

Definition can_reorder_relacq lab (a b : actid) :=
  << WRI : is_write_only (lab a) >> ∧
  << RD : is_read_only (lab b) >> ∧
  << DIFF: loc (lab a) ≠ loc (lab b) >>.

Definition can_reorder_local lab sb (a b : actid) :=
  << DIFF: loc (lab a) ≠ loc (lab b) >> ∧
  << LOC: is_local_location lab sb (loc (lab a))
          ∨ is_local_location lab sb (loc (lab b)) >>.

Definition can_reorder lab sb (a b : actid) :=
  can_reorder_local lab sb a b ∨
  can_reorder_relacq lab a b.

We start the proof of reordering soundness with some basic helper lemmas.

Lemma hb_ct sb rf x y :
  happens_before (clos_trans sb) rf x y ↔ happens_before sb rf x y.
Proof.
  split; red; ins; [|eapply hb_mon; eauto; vauto].
  do 2 (induction H; desf; vauto).
Qed.

Lemma hb_u1_expand sb rf :
  ∀ a b x y,
    happens_before (sb UNION1 (a,b)) rf x y ↔
    happens_before sb rf x y
    ∨ (x = a ∨ happens_before sb rf x a) ∧
       (y = b ∨ happens_before sb rf b y).
Proof.
  split; ins; desf; eauto using hb_mon with hb.
    by induction H; desf; eauto 6 with hb.
  by eapply hb_mon, H; vauto.
  by eapply hb_trans; eauto with hb; eapply hb_mon, H; vauto.
  by eapply hb_trans; eauto with hb; eapply hb_mon, H0; vauto.
  by eapply hb_trans, hb_trans; eauto with hb;
     eapply hb_mon; try eassumption; vauto.
Qed.

Lemma hb_u1_cycle sb rf (ACYC: irreflexive (happens_before sb rf)) :
  ∀ a b (NEQ: a ≠ b) x,
    happens_before (sb UNION1 (a,b)) rf x x →
    happens_before sb rf b a.
Proof.
  ins; assert (K:=H); eapply hb_u1_expand in H; desf; eauto with hb.
  exfalso; eauto with hb.
Qed.

Lemma hb_u1_right:
  ∀ lab sb rf
    (ACYC: irreflexive (happens_before sb rf))
    (Crf: ConsistentRF_dom lab rf) a b
    (CR: can_reorder_relacq lab a b ∨ is_local_location lab sb (loc (lab a)))
    (ADJ: adjacent sb a b)
    x (HB: happens_before sb rf x a),
    happens_before sb rf x b.
Proof.
  unfold adjacent, can_reorder_relacq; ins; desf;
  induction HB; desf; eauto with hb;
  exploit Crf; eauto; intro; desc.
    by destruct (lab y).
  destruct (eqP x y) as [|N]; [|apply CR in N];
    desf; eauto 6 using eq_sym, loceq_rf with caccess hb;
    try solve [exfalso; eauto with hb].
Qed.

Lemma hb_u1_left:
  ∀ lab sb rf
    (ACYC: irreflexive (happens_before sb rf))
    (Crf: ConsistentRF_dom lab rf) a b
    (CR: can_reorder_relacq lab a b ∨ is_local_location lab sb (loc (lab b)))
    (ADJ: adjacent sb a b)
    x (HB: happens_before sb rf b x),
    happens_before sb rf a x.
Proof.
  unfold adjacent, can_reorder_relacq; ins; desf;
  induction HB; desf; eauto with hb;
  exploit Crf; eauto; intro; desc.
    by destruct (lab x).
  destruct (eqP x y) as [|N]; [|apply CR in N];
    desf; eauto using loceq_rf with caccess hb;
    try solve [exfalso; eauto with hb].
Qed.

Lemma hb_u1 lab sb rf :
  ∀ (ACYC: irreflexive (happens_before sb rf))
         (Crf: ConsistentRF_dom lab rf) a b x y
    (CR: can_reorder_relacq lab a b)
    (ADJ: adjacent sb a b),
    happens_before (sb UNION1 (a,b)) rf x y ↔
    happens_before sb rf x y
    ∨ (x = a ∧ y = b).
Proof.
  ins; rewrite hb_u1_expand; split; ins; desf;
  eauto using hb_u1_left, hb_u1_right, hb_trans.
Qed.

Lemma mo_local :
  ∀ lab sb rf mo (CmoD: ConsistentMO_dom lab mo)
         (CmoI: irreflexive mo)
         (Cww: CoherentWW sb rf mo) a b
    (LOC : is_local_location lab sb (loc (lab a)) ∨
           is_local_location lab sb (loc (lab b)))
    (MO : mo a b),
  sb a b.
Proof.
  ins; destruct (eqP a b) as [|N].
    by exfalso; desf; eauto.
  assert (K := loceq_mo CmoD _ _ MO).
  specialize (CmoD _ _ MO); desc.
  desf; eapply LOC in N; desf; eauto with caccess;
  exfalso; eauto with hb.
Qed.

Lemma fr_local :
  ∀ lab sb rf mo
         (CrfD: ConsistentRF_dom lab rf)
         (CmoD: ConsistentMO_dom lab mo)
         (CmoI: irreflexive mo)
         (Cww: CoherentWW sb rf mo)
         (Cwr: CoherentWRplain sb rf mo) a b
    (LOC : is_local_location lab sb (loc (lab a)) ∨
           is_local_location lab sb (loc (lab b))) c
    (RF : rf a = Some c) (MO : mo c b) (NEQ: a ≠ b),
  sb a b.
Proof.
  ins; assert (K' := loceq_rf CrfD _ RF).
  assert (K := loceq_mo CmoD _ _ MO); rewrite K in K'.
  specialize (CrfD _ _ RF); desc.
  specialize (CmoD _ _ MO); desc.
  desf; eapply LOC in NEQ; desf; eauto with caccess;
  edestruct Cwr; eauto with hb.
Qed.

Lemma hb_u1_expand2 X (sb rf : relation X) :
  ∀ a b x y,
    clos_trans (fun x y ⇒ (sb UNION1 (a,b)) x y ∨ rf x y) x y ↔
 clos_trans (fun x y ⇒ sb x y ∨ rf x y) x y
  ∨ (x = a ∨ clos_trans (fun x y ⇒ sb x y ∨ rf x y) x a) ∧
       (y = b ∨ clos_trans (fun x y ⇒ sb x y ∨ rf x y) b y).
Proof.
  split; ins; desf; eauto using clos_trans.
    by induction H; desf; eauto 6 using clos_trans.
  by eapply clos_trans_mon; vauto; instantiate; ins; desf; vauto.
  by eapply t_trans; eauto using t_step;
     eapply clos_trans_mon; vauto; instantiate; ins; desf; vauto.
  by eapply t_trans; eauto using t_step;
     eapply clos_trans_mon; vauto; instantiate; ins; desf; vauto.
  by eapply t_trans, t_trans; eauto using t_step;
     eapply clos_trans_mon; vauto; instantiate; ins; desf; vauto.
Qed.

Reordering a write with a subsequently adjacent read is sound under SRA.

Theorem ConsistentSRA_reorder_relacq :
  ∀ acts lab sb rf mo
    (CONS: ConsistentSRA acts lab sb rf mo)
    a (INa: In a acts) b (INb: In b acts) (NEQ: a ≠ b)
    (CR: can_reorder_relacq lab a b)
    (NSB: ¬ sb b a)
    (ADJ: adjacent sb a b),
  ConsistentSRA acts lab (clos_trans (sb UNION1 (a,b))) rf mo.
Proof.
  unfold ConsistentSRA; ins; desc; unnw; intuition; vauto;
    try (red; ins; rewrite hb_ct, hb_u1 in *; desf; eauto).
  {
    split; unnw; ins; [by apply FIN|].
    by induction H; desf; eauto; apply FIN.
  }

  by eapply CmoD in MO; desf; red in CR; desf; destruct (lab b); ins.

  by eapply CrfD in RF; eapply CmoD in MO; desf; red in CR; desf;
     destruct (lab b); ins; destruct (lab a0); ins; desf.
Qed.

Reordering two adjacent accesses of different locations, such that one of them is a local access, is sound under RA.

Theorem ConsistentRA_reorder_local :
  ∀ acts lab sb rf mo
    (CONS: ConsistentRA acts lab sb rf mo)
    a (INa: In a acts) b (INb: In b acts) (NEQ: a ≠ b)
    (CR: can_reorder_local lab sb a b)
    (NSB: ¬ sb b a)
    (ADJ: adjacent sb a b),
  ConsistentRA acts lab (clos_trans (sb UNION1 (a,b))) rf mo.
Proof.
  unfold ConsistentRA; ins; desc.
  assert (NHB: ¬ happens_before sb rf b a).
    by red in CR; desf; eauto using hb_u1_left, hb_u1_right.

  unnw; split; [|repeat split; vauto].
  {
    split; unnw; ins; [by apply FIN|].
    by induction H; desf; eauto; apply FIN.
  }

  by red; ins; rewrite hb_ct in H; eapply hb_u1_cycle in H.

  {
    red; ins; rewrite hb_ct in HB; eapply hb_u1_expand in HB; ins.
    desf; eauto.
      red in CR; desc; unnw; eapply mo_local with (lab:=lab) (mo:=mo) in MO;
      try edone; tauto.

      red in CR; desf; [by eapply hb_u1_right in HB; try exact ADJ; eauto|].
      by eapply mo_local with (sb:=sb) (lab:=lab) (mo:=mo) in MO; eauto with hb.

      red in CR; desf; [|by eapply hb_u1_left in HB0; try exact ADJ; eauto].
      by eapply mo_local with (sb:=sb) (lab:=lab) (mo:=mo) in MO; eauto with hb.

      red in CR; desf; [eapply hb_u1_right in HB|eapply hb_u1_left in HB0];
      try exact ADJ; eauto with hb.
  }

  {
    red; ins; rewrite hb_ct in HB; eapply hb_u1_expand in HB; ins.
    desf; eauto.
      red in CR; desc; unnw.
      eapply fr_local with (sb:=sb) (lab:=lab) (mo:=mo) in MO;
      try edone; try tauto; congruence.

      red in CR; desf; [by eapply hb_u1_right in HB; try exact ADJ; eauto|].
      by eapply fr_local with (sb:=sb) (lab:=lab) (mo:=mo) in MO; eauto with hb;
         intro; desf.

      red in CR; desf; [|by eapply hb_u1_left in HB0; try exact ADJ; eauto].
      eapply fr_local with (a:=c) (sb:=sb) (lab:=lab) (mo:=mo) in MO; eauto with hb.
      by intro; desf.

      red in CR; desf; [eapply hb_u1_right in HB|eapply hb_u1_left in HB0];
      try exact ADJ; eauto with hb.
  }
Qed.

Reordering two adjacent accesses of different locations, such that one of them is a local access, is also sound under SRA.

Theorem ConsistentSRA_reorder_local :
  ∀ acts lab sb rf mo
    (CONS: ConsistentSRA acts lab sb rf mo)
    a (INa: In a acts) b (INb: In b acts) (NEQ: a ≠ b)
    (CR: can_reorder_local lab sb a b)
    (NSB: ¬ sb b a)
    (ADJ: adjacent sb a b),
  ∃ mo,
    ConsistentSRA acts lab (clos_trans (sb UNION1 (a,b))) rf mo.
Proof.
  ins; rewrite ConsistentSRA_alt; eexists; split.
    by eapply ConsistentRA_reorder_local; eauto using ConsistentSRA_RA.
  ins; intros x J; eapply ConsistentSRA_ac with (x:=x); eauto.
  rewrite clos_trans_of_clos_trans1 in J.
  assert (K: clos_trans
     (fun x0 y : actid ⇒
      sb x0 y ∨ rf y = Some x0 ∨ mo x0 y ∧ loc (lab x0) = loc (lab y)) b a).
    rewrite hb_u1_expand2 in J; desf; eauto using t_trans.
    by edestruct ConsistentSRA_ac; eauto.
  exfalso; clear x J.
  red in CR; red in ADJ; desf.
    eapply t_rt_step in K; desc; assert (sb z a);
    [|eapply ConsistentSRA_ac, t_rt_trans, K; eauto using t_step].
  red in CONS; desf.
    exploit loceq_rf; eauto; exploit CrfD; eauto; ins; desc.
    destruct (eqP a z) as [|N]; [|apply LOC in N]; desf; eauto with caccess;
    exfalso; eauto with hb.

    exploit CmoD; eauto; ins; desc.
    destruct (eqP a z) as [|N]; [|apply LOC in N]; desf; eauto with caccess;
    exfalso; eauto with hb.

    eapply t_step_rt in K; desc; assert (sb b z);
    [|eapply ConsistentSRA_ac, t_rt_trans, K0; eauto using t_step].
  red in CONS; desf.
    exploit loceq_rf; eauto; exploit CrfD; eauto; ins; desc.
    destruct (eqP z b) as [|N]; [|apply LOC in N]; desf; eauto with caccess;
    exfalso; eauto with hb.

    exploit CmoD; eauto; ins; desc.
    destruct (eqP z b) as [|N]; [|apply LOC in N]; desf; eauto with caccess;
    exfalso; eauto with hb.
Qed.

As a corollary, all the specified reorderable accesses may be soundly be reordered under SRA.

Corollary ConsistentSRA_reorder :
  ∀ acts lab sb rf mo
    (CONS: ConsistentSRA acts lab sb rf mo)
    a (INa: In a acts) b (INb: In b acts) (NEQ: a ≠ b)
    (CR: can_reorder lab sb a b)
    (NSB: ¬ sb b a)
    (ADJ: adjacent sb a b),
  ∃ mo,
    ConsistentSRA acts lab (clos_trans (sb UNION1 (a,b))) rf mo.
Proof.
  unfold can_reorder; ins; desf;
  eauto using ConsistentSRA_reorder_local, ConsistentSRA_reorder_relacq.
Qed.

Combining the previous theorem with monotonicity, we get the reordering proposition shown in the paper (that talks about reversing an edge).

Definition diff1 X (r: relation X) a b :=
  fun x y ⇒ r x y ∧ ¬ (x = b ∧ y = a).

Proposition ConsistentSRA_reorder_paper :
  ∀ acts lab sb rf mo
    (CONS: ConsistentSRA acts lab sb rf mo) a b
    (CR: can_reorder_local lab sb a b)
    (SB: sb a b)
    (ADJ: adjacent sb a b),
  ∃ mo,
    ConsistentSRA acts lab (clos_trans (diff1 sb a b UNION1 (a,b))) rf mo.
Proof.
  ins; assert (K:=CONS); red in K; desc.
  assert (N: a ≠ b).
    by intro; desf; eauto with hb.

  ins; apply ConsistentSRA_mon with (sb' := diff1 sb a b) in CONS.
  eapply ConsistentSRA_reorder with (a:=a) (b:=b) in CONS; eauto;
    try (by apply FIN in SB; desf).

  by unfold can_reorder, can_reorder_local, is_local_location in *; desf; unnw; eauto;
     left; split; ins; [left|right]; unfold diff1; red; intros; eapply LOC in NEQ; eauto;
     (desf; [left|right]; split; try red; ins; desf; eauto with hb).

  by unfold diff1; tauto.

  by red in ADJ; desc; unfold diff1;
     repeat split; unnw; desc; eauto; intro; desf; eauto with hb.

  by unfold diff1; red; ins; desc; eauto.

  unfold diff1, ConsistentSRA in *; red; ins; desc; split; eauto; intro; desf.
  by eapply ADJ in H0; eauto with hb.
Qed.

Redundant adjacent access eliminations

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.

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: X → Prop) g rel
    (T: is_total (fun y ⇒ f (g y)) rel)
    a b v (C: f v → f (g b)) (cond : Prop) (C : f v → cond),
  is_total (fun y ⇒ f (fupd g a v y)) (lin_ext_a rel cond a b).
Proof.
  ins; unfold lin_ext_a, fupd; repeat red; ins; desf; desf.
  destruct (eqP a0 b) as [|M]; desf; eauto 8; eapply T in M; tauto.
  destruct (eqP b0 b) as [|M]; desf; eauto 8; eapply T in M; tauto.
  eapply T in NEQ; tauto.
Qed.

Lemma irreflexive_lin_ext_a :
  ∀ X (rel : relation X)
    (IRR: irreflexive rel)
    a b (NEQ: a ≠ b)
    (C: ∀ x, rel x a → False)
    (D: ∀ x, rel a x → False) (cond : Prop),
  irreflexive (lin_ext_a rel cond a b).
Proof.
  unfold lin_ext_a; red; ins; desf; eauto.
Qed.

Lemma transitive_lin_ext_a :
  ∀ (X: eqType) (rel : relation X)
    (IRR: irreflexive rel)
    (T: transitive rel) a b
    (C: ∀ x, rel x a → False)
    (D: ∀ x, rel a x → False) (cond : Prop),
  transitive (lin_ext_a rel cond a b).
Proof.
  unfold lin_ext_a; red; ins; desf; eauto 10;
  exfalso; eauto.
Qed.

Ltac kill_incons :=
  match goal with
    | Crf : ConsistentRF_dom ?lab ?rf ,
      Cmo : ConsistentMO_dom ?lab ?mo |- _ ⇒
        try by repeat match goal with
                  | H : rf _ = _ |- _ ⇒ apply Crf in H; desc
                  | H : mo _ _ |- _ ⇒ apply Cmo in H; desc end;
               do 2 try match goal with
                 | H : lab _ = _ |- _ ⇒ rewrite H in ×
               end; ins; desf; eauto
    | Crf : ConsistentRF_dom ?lab ?rf ,
      Cmo : ConsistentMO_big_dom ?lab ?mo |- _ ⇒
        try by repeat match goal with
                  | H : rf _ = _ |- _ ⇒ apply Crf in H; desc
                  | H : mo _ _ |- _ ⇒ apply Cmo in H; desc end;
               do 2 try match goal with
                 | H : lab _ = _ |- _ ⇒ rewrite H in ×
               end; ins; desf; eauto
  end.

Adjacent overwritten write elimination


Lemma OW_adj_hb_a :
  ∀ lab sb rf (CrfD : ConsistentRF_dom lab rf) a c
         (HB: happens_before sb rf a c) tid
         (Aa: lab a = Askip tid) b
         (SBR: sb a b)
         (DOM: ∀ x, sb a x → x = b ∨ sb b x),
    b = c ∨ happens_before sb rf b c.
Proof.
  unfold happens_before; intros; apply t_step_rt in HB; desf.
  2: by apply CrfD in HB; rewrite Aa in HB; ins; desf.
  apply clos_refl_transE.
  apply DOM in HB; desf; eauto 6 using rt_trans, rt_step.
Qed.

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

Theorem OW_adjacent :
  ∀ acts lab sb rf mo
    (CONS: ConsistentSRA acts lab sb rf mo)
    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 x → x = b ∨ sb b x)
    v' lab' (LAB': lab' = fupd lab a (Astore tid typ l v')),
  ∃ mo', ConsistentSRA acts lab' sb rf mo'.
Proof.
  ins; unfold ConsistentSRA in *; desc; unnw.
  assert (INa: In a acts) by (eapply FIN in SBR; desf).

  ∃ (lin_ext_a mo True a b).
  subst; repeat apply conj; unfold NW; ins.
   by unfold fupd in *; desf; desf; apply FIN.
   by apply FIN.

   by red; unfold fupd; ins; unnw; desf; desf; kill_incons.

   by red; ins; unfold fupd in *; desf; desf; eauto.

   by red; unfold fupd, lin_ext_a in *; ins; desf; desf; kill_incons.

   by red; ins; eapply (is_total_lin_ext_a is_write lab); try eassumption;
      try rewrite Ab.

   by apply transitive_lin_ext_a; ins; kill_incons.
   by apply irreflexive_lin_ext_a; ins; kill_incons; congruence.

   unfold lin_ext_a; red; ins; desf; eauto with hb.
   by eapply OW_adj_hb_a with (sb:=sb) in HB; eauto; desf; eauto.

   unfold lin_ext_a, fupd; red; ins; desf; desf; kill_incons; eauto with hb.
   ins; desf; eapply OW_adj_hb_a with (sb:=sb) in HB; eauto; desf; kill_incons.
   by eapply Cwr in RF; eauto; instantiate; rewrite Ab in *; ins; auto.

   unfold lin_ext_a, fupd; red; ins; desf; desf; kill_incons; eauto with hb.
   by eapply (Cat _ _ MO1); eauto; rewrite Ab; ins.
Qed.

Adjacent read after write elimination


Lemma RAx_adj_hb_b :
  ∀ lab sb rf (CrfD : ConsistentRF_dom lab rf) b c
         (HB: happens_before sb rf c b) tid
         (A: lab b = Askip tid) a
         (SBR: sb a b)
         (DOM: ∀ x, sb x b → x = a ∨ sb x a),
    c = a ∨ happens_before sb rf c a.
Proof.
  unfold happens_before; intros; apply t_rt_step in HB; desf.
  2: by apply CrfD in HB0; rewrite A in HB0; ins; desf.
  apply clos_refl_transE.
  apply DOM in HB0; desf; eauto 6 using rt_trans, rt_step.
Qed.

Lemma RAW_adj_hb :
  ∀ (sb: relation actid) rf a b (SB: sb a b) x y
    (HB: happens_before sb (fun x ⇒ if x == b then Some a else rf x) x y),
    happens_before sb rf x y.
Proof.
  ins; induction HB as [??[]|]; desf; desf; eauto with hb.
Qed.

Theorem RAW_adjacent :
  ∀ acts lab sb rf mo
    (CONS: ConsistentSRA acts lab sb rf mo)
    tid typ l v
    a (Aa: lab a = Astore tid typ l v)
    b (Ab: lab b = Askip tid)
    (SBR: sb a b)
    (DOM: ∀ x, sb x b → x = a ∨ sb x a)
    lab' typ' (LAB': lab' = fun x ⇒ if x == b then Aload tid typ' l v else lab x),
  ∃ rf', ConsistentSRA acts lab' sb rf' mo.
Proof.
  intros; red in CONS; desc.
  assert (INb: In b acts) by (eapply FIN in SBR; desf).

  ∃ (fun x ⇒ if x == b then Some a else rf x); split; unnw.
    by split; unnw; ins; desf; desf; apply FIN.
  repeat apply conj; try red; ins; desf; desf; unnw; eauto;
    kill_incons; eauto using RAW_adj_hb.
    by rewrite Aa; ins; eauto 6.
  eapply RAW_adj_hb in HB; eauto.
  by eapply RAx_adj_hb_b with (sb:=sb) in HB; eauto; desf; eauto.
Qed.

Adjacent read after read elimination


Lemma RAR_adj_hb :
  ∀ (sb : relation actid) rf a b (SB: sb a b) x y
    (HB: happens_before sb (fun x ⇒ if x == b then rf a else rf x) x y),
    happens_before sb rf x y.
Proof.
  ins; induction HB; desf; desf; eauto with hb.
Qed.

Theorem RAR_adjacent :
  ∀ acts lab sb rf mo
    (CONS: ConsistentSRA acts lab sb rf mo)
    tid typ l v
    a (Aa: lab a = Aload tid typ l v)
    b (Ab: lab b = Askip tid)
    (SBR: sb a b)
    (DOM: ∀ x, sb x b → x = a ∨ sb x a)
    lab' (LAB': lab' = fun x ⇒ if x == b then Aload tid typ l v else lab x),
  ∃ rf', ConsistentSRA acts lab' sb rf' mo.
Proof.
  intros; red in CONS; desc.
  assert (INb: In b acts) by (eapply FIN in SBR; desf).

  ∃ (fun x ⇒ if x == b then rf a else rf x); split; unnw.
    by split; unnw; ins; desf; desf; apply FIN.
  repeat apply conj; try red; ins; desf; desf; unnw; eauto;
    kill_incons; eauto using RAR_adj_hb.
    by apply (COrf a); rewrite ?Aa.
  eapply RAR_adj_hb in HB; eauto.
  eapply RAx_adj_hb_b with (sb:=sb) in HB; eauto; desf; eauto; kill_incons.
Qed.

This page has been generated by coqdoc