Fences and Reduction to SC


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

Lemma clos_trans_immediate1 A (r : relation A) (T: transitive r) a b :
  clos_trans (immediate r) a b r a b.
Proof.
  unfold immediate; induction 1; desf; eauto.
Qed.

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.
Proof.
  assert (D': c, r a c r c b In c dom).
    by ins; apply D in H; desf.
  clear D; revert a b D'.
  remember (length dom) as n; revert dom Heqn; induction n.
    by destruct dom; ins; vauto.
  ins; destruct (classic ( c, r a c r c b)); desf.
  2: by eapply t_step; split; ins; eauto.
  exploit D'; eauto; intro X; apply in_split in X; desf.
  rewrite app_length in *; ins; rewrite <- plus_n_Sm, <- app_length in *; desf.
  apply t_trans with c; eapply IHn with (dom := l1 ++ l2); ins; exploit (D' c0); eauto;
  rewrite !in_app_iff; ins; desf; eauto; exfalso; eauto.
Qed.

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 xis_writeL (lab x) fence_loc)
             (clos_trans (fun a brf b = Some a)).
Proof.
  ins; red in CONS; desc.
  cut ( a b (MO: mo a b)
              (Wa: is_writeL (lab a) fence_loc)
              (Wb: is_writeL (lab b) fence_loc),
         clos_trans (fun a brf b = Some a) a b).
    by red; ins; eapply CmoF in NEQ; desf; eauto.
  ins.
  eapply clos_trans_immediate2 with (dom:=acts) (r:=mo) in MO; eauto.
  2: by ins; eapply (finiteMO FIN CmoD) in R; desf.
  induction MO; eauto.

  red in H; desc.
  destruct (WF _ Wb); [|by exfalso; eauto with hb].
  apply t_step.
  specialize (CrfD y); specialize (COrf y); destruct (rf y) eqn: RF; ins.
  2: by exfalso; eauto with caccess.
  destruct (eqP a x) as [|NEQ]; desf; exfalso.
  assert (is_writeL (lab a) fence_loc).
    by specialize (CrfD _ eq_refl); desf; destruct (lab y); ins; desf;
       eauto with caccess.
  eapply CmoF in NEQ; eauto; desf; eauto using loceq_mo.
  destruct (eqP a y) as [|NEQ']; desf; eauto with hb.
  eapply CmoF in NEQ'; eauto; desf; eauto using loceq_mo with hb.

  cut (is_writeL (lab y) fence_loc); eauto using t_trans with hb.
  apply clos_trans_immediate1, CmoD in MO1; ins; desc.
  destruct (lab x); ins; desf.
Qed.

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 xis_writeL (lab x) fence_loc)
             (happens_before sb rf).
Proof.
  red; ins; eapply rf_total_on_fences in NEQ; eauto.
  by desf; [left|right]; eapply clos_trans_mon; eauto.
Qed.

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).
Proof.
  unfold ConsistentSC, ConsistentSCalt; split; ins; desf; unnw.
  { (restr_rel (fun xIn x acts)
                      (tot_ext acts (fun x y
                                       sb x y rf y = Some x
                                       ( l : nat, mofr lab rf mo l x y))));
    intuition.
    by eapply is_total_restr; red; ins; eapply tot_ext_total; eauto;
       apply FIN.
    by eapply restr_rel_trans, tot_ext_trans.
    by unfold restr_rel; red; ins; desc; eapply tot_ext_irr; eauto.
    by exploit finiteRF; eauto; ins; desc; split; eauto using tot_ext_extends.
    by red in FIN; desc; split; eauto using tot_ext_extends.

    red; unfold restr_rel; ins; desf.
    exploit CrfD; eauto; ins; desf.
    destruct (eqP a b) as [|NEQ]; desf; [by eapply tot_ext_irr in SC; eauto|].
    destruct (eqP c b); desf; [by eapply tot_ext_irr in SC'; eauto|].
    assert (is_writeL (lab b) l).
      by destruct (lab b); ins; destruct (lab a); ins; desf.
    eapply CmoF in NEQ; desf; eauto with caccess.
      eapply tot_ext_irr with (x:=b); eauto.
      eapply tot_ext_trans, tot_ext_extends; eauto.
      by right; right; eexists; right; eauto 10 with caccess.
    eapply tot_ext_irr with (x:=a); eauto.
    eapply tot_ext_trans, tot_ext_extends; eauto.
    by right; right; eexists; left; eauto with caccess.
  }
  { (fun x y l, sc x y is_writeL (lab x) l is_writeL (lab y) l);
      intuition; repeat red; ins; desf; eauto.
    by eapply CscF in NEQ; desf; eauto with caccess; apply FIN; intro X; rewrite X in ×.
    by assert (l=l0) by (destruct (lab y); ins; desf); desf; eauto.
    eapply (CscI x); revert H; generalize x at 1 3; unfold mofr;
    induction 1; desf; eauto.
    eapply CscF in H1; desf; eauto; try (by apply FIN; intro X; rewrite X in × ).
    exfalso; eapply Cwr; try exact H; eauto with caccess.
    destruct (lab y); ins; destruct (lab z); ins; desf.
  }
Qed.

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:

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.
Proof.
  unfold com_ext, ConsistentRA; ins; desf; unnw; eauto 10;
    add_locs CrfD CmoD.
    by com_ext_trans_tac' (eqP a c).
    by com_ext_trans_tac CmoF (eqP b mid).
    by com_ext_trans_tac' (eqP a c); com_ext_trans_tac CmoF (eqP b mid).
    by com_ext_trans_tac CmoF (eqP b c).
    by com_ext_trans_tac' (eqP a c); com_ext_trans_tac CmoF (eqP b c).
    by com_ext_trans_tac' (eqP a c).
    by com_ext_trans_tac CmoF (eqP mid0 mid).
    by com_ext_trans_tac CmoF (eqP mid0 mid).
    by com_ext_trans_tac CmoF (eqP a mid).
    by com_ext_trans_tac CmoF (eqP fri0 mid).
Qed.

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.
Proof.
  unfold com_ext, ConsistentRA; ins; desf; unnw; eauto 10;
  add_locs CrfD CmoD; com_ext_trans_tac CmoF (eqP b mid).
Qed.

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.
Proof.
  unfold com_ext, ConsistentRA; ins; desf; unnw; eauto 10;
  add_locs CrfD CmoD; com_ext_trans_tac CmoF (eqP a b).
Qed.

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.
Proof.
  unfold com_ext, ConsistentRA; ins; desf; unnw; add_locs CrfD CmoD; subst.
    by com_ext_trans_tac CmoF (eqP b c).
    by com_ext_trans_tac CmoF (eqP b c); com_ext_trans_tac' (eqP a d).
    by com_ext_trans_tac CmoF (eqP mid c).
    by com_ext_trans_tac CmoF (eqP mid c); com_ext_trans_tac' (eqP a d).
    by com_ext_trans_tac CmoF (eqP b fri).
    by com_ext_trans_tac' (eqP a d); com_ext_trans_tac CmoF (eqP b fri).
    by com_ext_trans_tac CmoF (eqP mid fri).
    by com_ext_trans_tac' (eqP a d); com_ext_trans_tac CmoF (eqP fri fri0).
    by com_ext_trans_tac CmoF (eqP b mid).
    by com_ext_trans_tac CmoF (eqP b c).
    by com_ext_trans_tac CmoF (eqP mid0 mid).
    by com_ext_trans_tac CmoF (eqP mid0 mid).
    by com_ext_trans_tac CmoF (eqP a mid).
    by com_ext_trans_tac CmoF (eqP fri0 mid).
    by com_ext_trans_tac CmoF (eqP fri mid0).
    by com_ext_trans_tac CmoF (eqP fri mid0).
Qed.

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.
Proof.
  unfold mofr, NW; ins; destruct P as [|[|P]]; desc; eauto with hb.
  assert (K := CONS); red in K; desc.
  destruct (classic (happens_before sb rf a b)); eauto.
  destruct (classic (happens_before sb rf b a)).
    by desf; exfalso; eauto.
  right; red; unnw; repeat split; red; unnw; desf; eauto 6;
  [ b| b| a| a]; repeat split; eauto using loceq_mo with caccess;
  try (by intro; desf; eauto).
  exploit loceq_rf; eauto; exploit loceq_mo; eauto; instantiate; ins; congruence.
  exploit loceq_mo; eauto; instantiate; ins; congruence.
  exploit loceq_rf; eauto; exploit loceq_mo; eauto; instantiate; ins; congruence.
Qed.

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).
Proof.
  unfold com_ext; ins; desf;
  repeat match goal with J: _ |- _
                         apply (loceq_mo H0) in J ||
                         apply (loceq_rf H) in J end; congruence.
Qed.

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 ysb x y rf y = Some x) b a),
    False.
Proof.
  unfold com_ext, ConsistentRA; ins; desf;
  rewrite clos_refl_transE in *; desf; eauto with hb.
Qed.

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 ysb x y rf y = Some x) b a),
    False.
Proof.
  unfold racy_com_ext; ins; desf; eauto using com_ext_loop1.
Qed.

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 ysb 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 ysb 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.
Proof.
  unfold racy_com_ext; ins; desf; unnw.
  rewrite clos_refl_transE in HB; desf; [by eauto 6 using com_ext_trans|].
  rewrite clos_refl_transE in HB'; desf; [by eauto 6 using com_ext_trans|].
  destruct (eqP (loc (lab a)) (loc (lab c))); [by eauto 6 using com_ext_same_loc|].
  destruct (eqP (loc (lab c)) (loc (lab e))); [by eauto 6 using com_ext_same_loc|].
  edestruct FENCED as [f ?]; try exact HB; eauto.
    by red in CONS; desc; intro X; rewrite <- X in *; eauto using loceq_com_ext.
  edestruct FENCED as [f0 ?]; try exact HB'; eauto.
    by red in CONS; desc; intro X; rewrite <- X in *; eauto using loceq_com_ext.
  desf; destruct (eqP f f0) as [|N]; [|eapply hb_total_on_fences in N; eauto]; desf;
      try (by destruct (lab f); ins; desf);
      try (by destruct (lab f0); ins; desf);
      eauto with hb.
  exfalso; eauto 10 using com_ext_loop1, clos_trans_in_rt, rt_trans.
Qed.

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 ysb 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 ysb x y rf y = Some x) d a),
  False.
Proof.
  ins; exploit racy_com_ext_path2; eauto; ins; desf;
    eauto using racy_com_ext_loop1, clos_trans_in_rt, rt_trans.
Qed.

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.
Proof.
  ins; assert (KK := CONS); red; red in KK; desc; unnw; intuition.
  repeat red; ins.
  assert (RT: k,
                clos_refl_trans (fun x ysb x y rf y = Some x) x k
                (k = x m k',
                 << CE : racy_com_ext lab sb rf mo k m >>
                 << RT': clos_refl_trans (fun x ysb x y rf y = Some x) m k'>>
                (k' = x m',
                 << CE' : racy_com_ext lab sb rf mo k' m' >>
                 << RT': clos_refl_trans (fun x ysb x y rf y = Some x) m' x>>)))
      by eauto using rt_refl.
  revert H RT.
  generalize x at 1 4 5 6; intros x0 C; apply clos_trans_tn1 in C.
  induction C; ins; desc; eapply racy_com_ext_step in H; eauto.
  {
    destruct H;
    [ assert (HB: happens_before sb rf x0 k) by (eapply t_rt_trans; eauto);
      clear H RT |];
    desf; eauto using racy_com_ext_loop1, racy_com_ext_loop2, rt_trans, clos_trans_in_rt.
    by exploit racy_com_ext_path2; eauto; intro; desf;
       eauto using racy_com_ext_loop1, racy_com_ext_loop2,
                   clos_trans_in_rt, rt_trans.
  }
  destruct H; [by eapply IHC; k;eauto using rt_trans, clos_trans_in_rt|].
  desf; unnw; [| |edestruct racy_com_ext_path2 with (a:=y); try edone; desf];
  eapply IHC; clear IHC C;
  try (by eexists; eauto 10 using clos_trans_in_rt);
  try (by eexists; eauto 12 using clos_trans_in_rt, rt_refl, rt_trans).
Qed.

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.
Proof.
  by ins; eapply sc_reduction1; ins; red; ins; destruct NORACE; eauto.
Qed.

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.
Proof.
  unfold ConsistentRA; ins; destruct (eqP a b) as [|N]; desf.
    by exfalso; eauto.
  exploit CmoD; eauto; ins; desc.
  eapply NOWW in N; desf; eauto with caccess.
  exfalso; eauto.
Qed.

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.
Proof.
  unfold mofr, NW; ins; desf; eauto using no_ww_races_mo_hb with hb.
  assert (K := CONS); red in K; desc.
  destruct (classic (happens_before sb rf a b)); eauto.
  destruct (classic (happens_before sb rf b a)).
    by exfalso; eauto.
  exploit loceq_rf; eauto.
  exploit loceq_mo; eauto.
  right; z; unnw; repeat split; eauto;
  [ b| a| | |]; unnw; repeat eexists; eauto with caccess; try congruence.
  {
    destruct (classic (is_writeL (lab a) l)); [|by destruct (lab a)].
    exfalso; eapply CmoF in P1; desf; eauto using no_ww_races_mo_hb with hb.
  }
  eapply PR; repeat split; unnw; ins; eauto with caccess; congruence.
Qed.

Lemma restr_rel_out lab sb rf mo B :
  restr_rel (fun x¬ B x)
     (fun a bhappens_before sb rf a b cs_racyfr lab sb rf mo B a b)
  <--> restr_rel (fun x¬ B x) (happens_before sb rf).
Proof.
  unfold restr_rel, cs_racyfr; split; red; ins; desf; eauto.
Qed.

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.
Proof.
  unfold cs_racyfr, ConsistentRA; ins; desc; clear SERV.
  red in HB; desf; eauto.
Qed.

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.
Proof.
  unfold cs_racyfr; ins; desc; unnw.
  assert (K:=CONS); red in K; desc.
  edestruct (CmoD _ _ MO) as (l & ?); desc; eauto.
  edestruct (CrfD _ _ RF) as (l' & ?); desc; eauto.
  edestruct (CmoD _ _ MO0) as (l0 & ?); desc; eauto.
  edestruct (CrfD _ _ RF0) as (l0' & ?); desc; eauto.
  assert (l' = l) by (destruct (lab mid); ins; desf); subst.
  assert (l0' = l0) by (destruct (lab mid0); ins; desf); subst.

  destruct (eqP a c) as [|N]; clarify.
    assert (l0 = l) by (destruct (lab c); ins; desc; clarify); subst.
    clear SERV SERV0; assert (N:=NEQ); eapply CmoF in N; eauto with caccess.
    desf; eapply (no_ww_races_mo_hb CONS) in N; eauto.
    exfalso; eauto with hb.
  eapply CmoF in NEQ; eauto with caccess.
  2: by destruct (lab b); ins; desf.
  destruct NEQ as [NEQ|].
  2: by exfalso; eapply Cat with (b:=c); eauto;
        destruct (lab mid); ins; destruct (lab c); ins; desc; clarify.
  eapply (no_ww_races_mo_hb CONS) in NEQ; eauto.
  exfalso; eauto with hb.
Qed.

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.
Proof.
  unfold cs_racyfr; ins; desc; unnw.
  assert (K:=CONS); red in K; desc.
  edestruct (CmoD _ _ MO) as (l & ?); desc; eauto.
  edestruct (CrfD _ _ RF) as (l' & ?); desc; eauto.
  edestruct (CmoD _ _ MO0) as (l0 & ?); desc; eauto.
  edestruct (CrfD _ _ RF0) as (l0' & ?); desc; eauto.
  assert (l' = l) by (destruct (lab mid); ins; desf); subst.
  assert (l0' = l0) by (destruct (lab mid0); ins; desf); subst.
  assert (l0 = l) by (destruct (lab b); ins; destruct (lab c); ins; desf); subst.

  destruct (eqP b d) as [|N]; clarify.
    by exfalso; eauto with hb.
  eapply CmoF in N; eauto with caccess.
  destruct N as [N|N].
    by eapply (no_ww_races_mo_hb CONS) in N; eauto with hb.
  by exfalso; eauto with hb.
Qed.

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.
Proof.
  ins; assert (KK := CONS); red; red in KK; desc; unnw; intuition.
  eapply acyclic_mon; [|intros a b; eapply protected_step; eauto].

  apply min_cycle with (dom := B)
    (rel' := happens_before sb rf).
    by eapply PR.
    by red; eauto with hb.
    by unfold restr_rel; red; ins; desc; eauto using t_step.
    ins; desf; desf; eauto using cs_racy_loop1 with hb.

  repeat split; ins; try rewrite restr_rel_out in ×.
    by clear -ACYC; eapply acyclic_mon, inclusion_restr_rel_l;
       [eapply trans_irr_acyclic|]; red; intros; eauto;
       instantiate; eauto using hb_trans.
    by desf; eauto using cs_racy_loop1.

  assert (T: clos_refl (happens_before sb rf) c2 c1).
    clear - S'; unfold restr_rel in ×.
    rewrite clos_refl_transE in S'; desf; vauto.
    by eapply clos_trans_of_transitive in S'; desf; red; ins; desc; eauto with hb.
  clear S'; desf.
    by unfold clos_refl in *; desf; eauto with hb.
    by eapply cs_racy_loop1 in R; eauto; unfold clos_refl in *; desf; eauto with hb.
    by eapply cs_racy_loop1 in R'; eauto; unfold clos_refl in *; desf; eauto with hb.
  red in S; desf.
    eapply (cs_racy_trans CONS) in R'; eauto.
    by eapply cs_racy_loop1 in R; eauto; unfold clos_refl in *; desf; eauto with hb.
  red in T; desf.
    eapply (cs_racy_trans CONS) in R; eauto.
    by eapply cs_racy_loop1 in R'; eauto; unfold clos_refl in *; desf; eauto with hb.
  destruct (eqP (loc (lab b1)) (loc (lab b2))) as [EQ|DIFF].
    eapply cs_racy_trans2 with (a:=c1) (d:=c2) in EQ; eauto.
    by eapply cs_racy_loop1 in R; eauto; unfold clos_refl in *; desf; eauto with hb.
  red in PR; desc.
  red in R; red in R'; desc; clear SERV SERV0.
  edestruct Pout with (a:=c2) (b:=c1) as [f1 K]; desc; eauto.
    apply (loceq_mo CmoD) in MO; apply (loceq_mo CmoD) in MO0;
    apply (loceq_rf CrfD) in RF; apply (loceq_rf CrfD) in RF0;
    congruence.
  desf.
    edestruct Pin with (a:=b1) (b:=b2) as [f2 L]; desc; eauto.
    destruct (eqP f1 f2) as [|N]; desf;
      [|eapply hb_total_on_fences in N; des]; eauto 4 with hb.
      by red in K; desf; eauto 4 with hb.
      by red in K; desf; eauto 4 with hb.
      by red in K0; desf; eauto 4 with hb.
      by destruct (lab f1).
    by destruct (lab f2).
  destruct (eqP f1 b1) as [|N]; desf; red in K0; desf; eauto.
  eapply PhbF in N; desf; red in K; desf; eauto with hb.
Qed.

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 xis_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).
Proof. by destruct a; ins; desf. Qed.

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.
Proof.
  ins; red in CS; desc.
  eapply protected_sc_reduction with
    (B:= fun xis_access (lab x) thread (lab x) = 0); ins.
  repeat red; ins; eapply (CsbF (loc_owner l)) in NEQ; desf;
    eauto with hb caccess.
  repeat split; unnw; ins; repeat red; ins; desc.
    by eapply (CsbF 0) in NEQ; des; eauto with hb caccess.

  assert (thread (lab a) thread (lab b)).
    by red in RACE; desc; intro X; edestruct CsbF with (a:=a) (b:=b); eauto with hb.

    red in RACE; desc; clarify.
    desf; eapply is_write_toL, CSwrite in WRI;
    [ specialize (CSwrite b); specialize (CSread b); destruct (lab b)
    | specialize (CSwrite a); specialize (CSread a); destruct (lab a) ]; ins; desf;
      try specialize (CSread _ eq_refl);
      try specialize (CSwrite _ eq_refl); desf; constructor; (split; ins; congruence).

    destruct (eqP a b) as [|NEQ]; try congruence.
    by eapply CsbF in NEQ; eauto; desf;
       [edestruct FENCED with (a := a) (b := b)|
        exfalso; red in CONS]; desc; eauto 8 with hb.

  eapply not_and_or in Da; destruct Da as [[]|Da]; eauto with caccess.
  eapply not_and_or in Db; destruct Db as [[]|Db]; eauto with caccess.

  assert (sb a b c d,
                      clos_refl (happens_before sb rf) a c
                      rf d = Some c ¬ sb c d
                      clos_refl (happens_before sb rf) d b).
    red in CONS; desc; clear - HB CsbT.
    unfold clos_refl; induction HB; desf; eauto 10 with hb.
    by destruct (classic (sb x y)); eauto 10.
  desf; [by unfold clos_refl; eapply FENCED in H; desf; eauto 10 with hb|].
  red in CONS; desc.

    unfold clos_refl; assert (NEQ: c d) by (intro; desf; eauto with hb).
    assert (K := H0);
    eapply CrfD in H0; desf; exploit CSwrite; eauto with caccess.
    exploit CSread; eauto 8 with caccess; intro M; ins; desf; try congruence.
    by eapply CsbF in NEQ; desf; eauto 6 with caccess; exfalso; eauto with hb.
    by rewrite M in *; c; repeat split; eauto with caccess;
       red in H2; desf; eauto with hb.
    by d; repeat split; eauto with caccess;
       red in H; desf; eauto with hb.
Qed.


This page has been generated by coqdoc