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 x ⇒ is_writeL (lab x) fence_loc)
(clos_trans (fun a b ⇒ rf 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 b ⇒ rf 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 x ⇒ is_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 x ⇒ In 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
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 y ⇒ sb 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 y ⇒ sb 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 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.
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 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.
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 y ⇒ sb 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 y ⇒ sb 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 y ⇒ sb 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.
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 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).
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.
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).
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 x ⇒ is_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