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).

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.

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.

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.

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).

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.

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.

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.

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).

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.

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.

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).

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.

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.

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.

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.

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.

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).

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).

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).

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.

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'.

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.

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.

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.

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.

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.

This page has been generated by coqdoc