# 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 xis_writeL (lab x) fence_loc)
(clos_trans (fun a brf 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 xis_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).

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.

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 ysb 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 ysb x y rf y = Some x) b a),
False.

Next, paths of the form hb*; 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.

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.

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

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

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.