Fences and Reduction to SC

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

Lemma clos_trans_immediate1 A (r : relation A) (T: transitive r) a b :
  clos_trans (immediate r) a b → r a b.

Lemma clos_trans_immediate2 A (r : relation A)
      (T: transitive r) (IRR: irreflexive r) dom
      (D: ∀ a b (R: r a b), In b dom) a b :
  r a b →
  clos_trans (immediate r) a b.

In an RA-consistent execution, fences are totally ordered by rf+.

Proposition rf_total_on_fences :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo)
         (WF: wellformed_fences lab sb),
    is_total (fun x ⇒ is_writeL (lab x) fence_loc)
             (clos_trans (fun a b ⇒ rf b = Some a)).

Corollary hb_total_on_fences :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo)
         (WF: wellformed_fences lab sb),
    is_total (fun x ⇒ is_writeL (lab x) fence_loc)
             (happens_before sb rf).

We next prove that the two axiomatisations of SC are equivalent.

Theorem ConsistentSC_alt acts lab sb rf :
(∃ mo, ConsistentSC acts lab sb rf mo ) ↔
(∃ sc, ConsistentSCalt acts lab sb rf sc ).

First reduction theorem from RA to SC

The following criterion states where fences are necessary to ensure sequential consistency.

Definition sc_fence_criterion lab sb rf :=
  ∀ a (Ra: racy lab sb rf a)
         b (Rb: racy lab sb rf b)
         (HB: happens_before sb rf a b)
         (DIFF: loc (lab a) ≠ loc (lab b)),
  ∃ f,
    happens_before sb rf a f ∧
    happens_before sb rf f b ∧
    is_rmw (lab f) ∧
    loc (lab f) = fence_loc.

Definition of the relation (mo U fr); rf?, which is used in the proof of the reduction from RA to SC.

Definition com_ext rf (mo : relation actid) a b :=
  ≪ MO : mo a b ≫ ∨
  (∃ fri, ≪ RF : rf a = Some fri ≫ ∧ ≪ MO : mo fri b ≫ ∧ ≪NEQ: a ≠ b ≫) ∨
  (∃ mid, ≪ MO : mo a mid ≫ ∧ ≪ RF: rf b = Some mid ≫) ∨
  (∃ fri mid, ≪ RF : rf a = Some fri ≫ ∧ ≪ MO : mo fri mid ≫ ∧
  ≪ RF' : rf b = Some mid ≫).

Definition racy_com_ext lab sb rf mo a b :=
    ≪ CE : com_ext rf mo a b ≫ ∧
    ≪ RACY: racy lab sb rf a ≫ ∧
    ≪ RACY': racy lab sb rf b ≫.

Ltac com_ext_trans_tac CmoF a :=
  let N := fresh in destruct a as [|N]; [|eapply CmoF in N];
  desf; eauto 10 with caccess;
  try (by exfalso; eauto using loceq_mo with hb).

Ltac com_ext_trans_tac' a :=
  destruct a; desf; eauto 9 with caccess;
  try (by exfalso; eauto using loceq_mo with hb).

Ltac add_locs CrfD CmoD :=
    repeat match goal with
      | [H: _ = Some _ |- _] ⇒ generalize (CrfD _ _ H); revert H
      | [H: _ |- _] ⇒ generalize (CmoD _ _ H); revert H
    end; ins; desf;
    repeat match goal with
      | H: is_writeL ?a ?l, H' : context[loc ?a] |- _ ⇒
        let EQ := fresh in assert (EQ: loc a = l) by (destruct a; ins; desf); rewrite EQ in *; clear EQ
      | H: is_readLV ?a ?l _, H' : context[loc ?a] |- _ ⇒
        let EQ := fresh in assert (EQ: loc a = l) by (destruct a; ins; desf); rewrite EQ in *; clear EQ
      | H: is_writeLV ?a ?l _, H' : is_readLV ?a ?l' _ |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
      | H: is_writeL ?a ?l, H' : is_readLV ?a ?l' _ |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
      | H: is_writeL ?a ?l, H' : is_writeLV ?a ?l' _ |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
    end.

We prove some basic properties of com_ext:

transitivity: com_ext; com_ext ≤ com_ext
com_ext; rf ≤ com_ext
com_ext; hb; com_ext ≤ com_ext when the two com_ext are to the same location
po U rf U mo U fr ≤ hb U com_ext

Lemma com_ext_trans :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) a b c,
    com_ext rf mo a b →
    com_ext rf mo b c →
    com_ext rf mo a c.

Lemma com_ext_rf_trans :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) a b c,
    com_ext rf mo a b →
    rf c = Some b →
    com_ext rf mo a c.

Lemma rf_com_ext_trans :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) a b c,
    rf b = Some a →
    com_ext rf mo b c →
    com_ext rf mo a c.

Lemma com_ext_same_loc :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) a b c d,
    com_ext rf mo a b →
    happens_before sb rf b c →
    loc (lab a) = loc (lab c) →
    com_ext rf mo c d →
    com_ext rf mo a d.

Lemma racy_com_ext_step :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) a b
         (P: sb a b ∨ rf b = Some a ∨ ∃ l, mofr lab rf mo l a b),
    happens_before sb rf a b ∨
    racy_com_ext lab sb rf mo a b.

Lemma loceq_com_ext lab rf mo a b :
  ConsistentRF_dom lab rf →
  ConsistentMO_dom lab mo →
  com_ext rf mo a b →
  loc (lab a) = loc (lab b).

Next, we prove the absence of cycles in hb U com_ext. First, cycles with a single com_ext edge are ruled out by RA-coherence.

Lemma com_ext_loop1 :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) a b
         (FR: com_ext rf mo a b)
         (HB: clos_refl_trans (fun x y ⇒ sb x y ∨ rf y = Some x) b a),
    False.

Lemma racy_com_ext_loop1 :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) a b
         (FR: racy_com_ext lab sb rf mo a b)
         (HB: clos_refl_trans (fun x y ⇒ sb x y ∨ rf y = Some x) b a),
    False.

Next, paths of the form com_ext; hb*; com_ext; hb*; com_ext can be shortened by using the total order on fences.

Lemma racy_com_ext_path2 :
  ∀ acts lab sb rf mo
    (CONS: ConsistentRA acts lab sb rf mo)
    (WF: wellformed_fences lab sb)
    (FENCED: sc_fence_criterion lab sb rf) a b
    (FR: racy_com_ext lab sb rf mo a b) c
    (HB: clos_refl_trans (fun x y ⇒ sb x y ∨ rf y = Some x) b c) d
    (FR': racy_com_ext lab sb rf mo c d) e
    (HB': clos_refl_trans (fun x y ⇒ sb x y ∨ rf y = Some x) d e) g
    (FR'': racy_com_ext lab sb rf mo e g),
  racy_com_ext lab sb rf mo a d ∨
  racy_com_ext lab sb rf mo c g ∨
  happens_before sb rf b e.

Consequently, there are no cycles with at two com_ext edges.

Lemma racy_com_ext_loop2 :
  ∀ acts lab sb rf mo
    (CONS: ConsistentRA acts lab sb rf mo)
    (WF: wellformed_fences lab sb)
    (FENCED: sc_fence_criterion lab sb rf) a b
    (FR: racy_com_ext lab sb rf mo a b) c
    (HB: clos_refl_trans (fun x y ⇒ sb x y ∨ rf y = Some x) b c) d
    (FR': racy_com_ext lab sb rf mo c d)
    (HB': clos_refl_trans (fun x y ⇒ sb x y ∨ rf y = Some x) d a),
  False.

As a result, we get the RA to SC reduction theorem.

Theorem sc_reduction1 :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo)
         (WF: wellformed_fences lab sb)
         (FENCED: sc_fence_criterion lab sb rf),
    ConsistentSC acts lab sb rf mo.

As a corollary, we get a per-execution DRF theorem.

Corollary per_execution_drf :
  ∀ acts lab sb rf mo
    (CONS: ConsistentRA acts lab sb rf mo)
    (WF: wellformed_fences lab sb)
    (NORACE: ¬ ∃ x, racy lab sb rf x),
  ConsistentSC acts lab sb rf mo.

Reduction theorem from RA to SC for protected programs

Definition protected_events lab sb rf (B : actid → Prop) :=
  ≪ PhbF : is_total B (happens_before sb rf) ≫ ∧
  ≪ Prace: ∀ a b (RACE: races_with lab sb rf a b), B a ∨ B b ≫ ∧
  ≪ Pin : ∀ a (Ra: racy lab sb rf a) (WRI: is_write (lab a)) (Da : B a)
                  b (Rb : racy lab sb rf b) (RD: is_read_only (lab b)) (Db : B b)
                  (HB : happens_before sb rf a b)
                  (DIFF: loc (lab a) ≠ loc (lab b)),
           ∃ f,
             happens_before sb rf a f ∧
             happens_before sb rf f b ∧
             is_rmw (lab f) ∧
             loc (lab f) = fence_loc ≫ ∧
  ≪ Pout : ∀ a (Ra: racy lab sb rf a) (WRI: is_write (lab a)) (Da : ¬ B a)
                  b (Rb : racy lab sb rf b) (RD: is_read_only (lab b)) (Db : ¬ B b)
                  (HB : happens_before sb rf a b)
                  (DIFF: loc (lab a) ≠ loc (lab b)),
           ∃ c,
             clos_refl (happens_before sb rf) a c ∧
             clos_refl (happens_before sb rf) c b ∧
             (is_rmw (lab c) ∧ loc (lab c) = fence_loc ∨ B c ) ≫.

Definition cs_racyfr lab sb rf mo B a b :=
  ∃ mid,
    ≪ RF : rf a = Some mid ≫ ∧
    ≪ MO : mo mid b ≫ ∧
    ≪ NEQ: a ≠ b ≫ ∧
    ≪ RACY: racy lab sb rf a ≫ ∧
    ≪ RACY': racy lab sb rf b ≫ ∧
    ≪ READ: is_read_only (lab a) ≫ ∧
    ≪ WRI: is_write (lab b) ≫ ∧
    ≪ SERV: B a ∨ B b ≫.

Lemma no_ww_races_mo_hb :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo)
         (NOWW: no_ww_races lab sb rf) a b
         (MO: mo a b),
    happens_before sb rf a b.

Lemma protected_step :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo)
         (NOWW: no_ww_races lab sb rf) B
         (PR: protected_events lab sb rf B) a b
         (P: sb a b ∨ rf b = Some a ∨ ∃ l, mofr lab rf mo l a b),
    happens_before sb rf a b ∨
    cs_racyfr lab sb rf mo B a b.

Lemma restr_rel_out lab sb rf mo B :
  restr_rel (fun x ⇒ ¬ B x)
     (fun a b ⇒ happens_before sb rf a b ∨ cs_racyfr lab sb rf mo B a b)
  ↔ restr_rel (fun x ⇒ ¬ B x) (happens_before sb rf).

Coherence disallows cycles with one cs_racyfr edge.

Lemma cs_racy_loop1 :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) B a b
         (FR: cs_racyfr lab sb rf mo B a b)
         (HB: clos_refl (happens_before sb rf) b a),
    False.

Lemma cs_racy_trans :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo)
         (NOWW: no_ww_races lab sb rf) B a b
         (FR: cs_racyfr lab sb rf mo B a b) c
         (FR': cs_racyfr lab sb rf mo B b c),
    sb b c.

Lemma cs_racy_trans2 :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo)
         (NOWW: no_ww_races lab sb rf) B a b
         (FR: cs_racyfr lab sb rf mo B a b) c
         (HB: happens_before sb rf b c) d
         (FR': cs_racyfr lab sb rf mo B c d)
         (SAME: loc (lab b) = loc (lab c)),
    happens_before sb rf b d.

Theorem protected_sc_reduction :
  ∀ acts lab sb rf mo
    (CONS: ConsistentRA acts lab sb rf mo)
    (WF: wellformed_fences lab sb)
    (NOWW: no_ww_races lab sb rf) B
    (PR: protected_events lab sb rf B),
  ConsistentSC acts lab sb rf mo.

Reduction theorem from RA to SC for client-server programs

Definition of client-server programs.

Definition client_server (lab : actid → act) :=
  ∃ loc_owner : nat → nat ,
    ≪ CSwrite: ∀ a l (WW: is_writeL (lab a) l),
                  thread (lab a) = loc_owner l ≫ ∧
    ≪ CSread : ∀ a l (RR: is_readL (lab a) l),
                  thread (lab a) = loc_owner l ∨
                  loc_owner l = 0 ∧ thread (lab a) ≠ 0 ∨
                  thread (lab a) = 0 ≫.

Definition plain (lab : actid → act) (sb : relation actid) :=
  ∀ tid, is_total (fun x ⇒ is_access (lab x) ∧ thread (lab x) = tid) sb.

The following criterion states where fences are necessary to ensure sequential consistency for client-server programs.

Definition cs_sc_fence_criterion lab sb rf :=
  ∀ a (RACYa: racy lab sb rf a) (Wa: is_write (lab a))
         b (RACYb: racy lab sb rf b) (Ra: is_read_only (lab b))
           (DIFF: loc (lab a) ≠ loc (lab b))
           (PO: sb a b),
  ∃ f,
    sb a f ∧ sb f b ∧
    is_rmw (lab f) ∧ loc (lab f) = fence_loc.

Lemma is_write_toL a : is_write a → is_writeL a (loc a).

Corollary client_server_sc_reduction :
  ∀ acts lab sb rf mo
    (CONS: ConsistentRA acts lab sb rf mo)
    (WF: wellformed_fences lab sb)
    (CS: client_server lab)
    (CsbF: plain lab sb)
    (FENCED: cs_sc_fence_criterion lab sb rf),
  ConsistentSC acts lab sb rf mo.

This page has been generated by coqdoc