# "Roach motel" reorderings

Require Import Peano_dec List Vbase Relations ExtraRelations.
Require Import actions c11 cmon.
Set Implicit Arguments.

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 : forall c, rel b c -> rel a c >> /\
<< LA_ca : forall c, rel c b -> c <> a -> rel c a >> /\
<< LA_cb : forall c, rel c a -> rel c b >> /\
<< LA_bc : forall c, rel a c -> c <> b -> rel b c >>.

A weaker notion of adjacency, that drops conditions (ii) and (iv) from the previous definition.

Definition adjacentW (rel: relation actid) (a b: actid) :=
<< LA_ac : forall c, rel b c -> rel a c >> /\
<< LA_cb : forall c, rel c a -> rel c b >>.

An even weaker notion that uses clos_trans _ rel instead of rel in the conclusion.

Definition adjacentWW (rel: relation actid) (a b: actid) :=
<< LA_ac : forall c, rel b c -> clos_trans _ rel a c >> /\
<< LA_cb : forall c, rel c a -> clos_trans _ rel c b >>.

Ltac unfolds :=
repeat match goal with |- context [?x] => unfold x end.

Lemma adjacent_weaken rel a b :
Proof. unfolds; intuition. Qed.

Lemma adjacentW_weaken rel a b :
Proof. unfolds; intuition. Qed.

Definition has_loc a :=
match a with
| Aalloc _ _ _
| Aload _ _ _ _
| Astore _ _ _ _
| Armw _ _ _ _ _ => true
| _ => false
end.

Notation same_loc a b :=
(<< SL_A : has_loc a >> /\
<< SL_B : has_loc b >> /\
<< SL_Eq: loc a = loc b >>).

Two distinct actions a and b are reorderable if
• they belong to the same thread,
• they do not access the same location,
• a is not an acquire access or fence,
• b is not a release access or fence,
• if the model type mt is MThbUrfnaAcyclic or MThbUrfAcyclic, and a is a read, then b is not a write,
• if a is a release fence, then b is not an atomic write,
• if b is an acquire fence, then a is not an atomic read, and
• a and b are not both SC actions.

Definition admissible_reordering mt acts lab (a b: actid) :=
<< AR_Neq: a <> b >> /\
<< AR_In_a: In a acts >> /\
<< AR_In_b: In b acts >> /\
<< AR_SL: ~ same_loc (lab a) (lab b) >> /\
<< AR_Not_Acq_Wr: ~ is_acquire (lab a) >> /\
<< AR_Not_Rel_Ra: ~ is_release (lab b) >> /\
<< AR_Arfna_RW: mt = MThbUrfnaAcyclic ->
is_write (lab b) ->
False >> /\
<< AR_Arf_RW: mt = MThbUrfAcyclic ->
is_write (lab b) ->
False >> /\
<< AR_Not_Fence_Rel_Write: is_fence (lab a) ->
is_release (lab a) ->
is_write (lab b) ->
~ is_na (lab b) ->
False >> /\
~ is_na (lab a) ->
is_fence (lab b) ->
is_acquire (lab b) ->
False >> /\
<< AR_Not_Both_Sc: ~ (is_sc (lab a) /\ is_sc (lab b)) >>.

The tactic xplit deals with all existential quantifiers and conjunctions in the goal.

Ltac xplit :=
repeat match goal with
| |- exists x, _ => eexists
| |- _ /\ _ => split
end.

forall lab rf
(Crf: ConsistentRF lab rf)
a b (RF: rf a = Some b),
Proof.
by ins; eapply Crf in RF; desf; eauto with access.
Qed.

Lemma Crf_Write:
forall lab rf
(Crf: ConsistentRF lab rf)
a b (RF: rf a = Some b),
is_write (lab b).
Proof.
by ins; eapply Crf in RF; desf; eauto with access.
Qed.

Lemma Cmo_Write1:
forall lab mo
(Cmo: ConsistentMO lab mo)
a b (MO: mo a b),
is_write (lab a).
Proof.
unfold ConsistentMO; ins; des; eapply CmoD in MO.
desf; eauto with access.
Qed.

Lemma Cmo_Write2:
forall lab mo
(Cmo: ConsistentMO lab mo)
a b (MO: mo a b),
is_write (lab b).
Proof.
unfold ConsistentMO; ins; des; eapply CmoD in MO.
desf; eauto with access.
Qed.

Lemma RS_Write1:
forall mt2 lab sb rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a b
(RS: release_seq mt2 lab sb rf mo a b)
(Wc: is_write (lab b)),
is_write (lab a).
Proof.
unfold release_seq; ins; desf.
desf; eauto using Cmo_Write1.
induction RS; desf; eauto using Cmo_Write1, Crf_Write.
Qed.

Lemma sync_release:
forall mt2 lab sb rf mo flag a b,
synchronizes_with mt2 lab sb rf mo flag a b ->
is_release (lab a).
Proof.
intros.
unfold synchronizes_with in *.
des; eauto with access.
Qed.

Lemma sync_acquire:
forall mt2 lab sb rf mo flag a b,
synchronizes_with mt2 lab sb rf mo flag a b ->
is_acquire (lab b).
Proof.
intros.
unfold synchronizes_with in *.
des; eauto with access .
Qed.

Hint Immediate sync_release sync_acquire : sync.

Lemma rf_eq_loc:
forall lab rf (Crf: ConsistentRF lab rf)
a b (RF: rf b = Some a),
loc (lab a) = loc (lab b).
Proof.
ins; eapply Crf in RF; desf.
by destruct (lab a); destruct (lab b); inversion READ; inversion WRITE; subst; auto.
Qed.

Lemma rf_has_loc1:
forall lab rf (Crf: ConsistentRF lab rf)
a b (RF: rf b = Some a),
has_loc (lab a).
Proof.
ins; eapply Crf in RF; desf.
by destruct (lab a); inversion WRITE; auto.
Qed.

Lemma rf_has_loc2:
forall lab rf (Crf: ConsistentRF lab rf)
a b (RF: rf b = Some a),
has_loc (lab b).
Proof.
ins; eapply Crf in RF; desf.
by destruct (lab b); inversion READ; auto.
Qed.

Lemma rf_same_loc:
forall lab rf (Crf: ConsistentRF lab rf)
a b (RF: rf b = Some a),
same_loc (lab a) (lab b).
Proof.
ins; xplit; eauto using rf_eq_loc, rf_has_loc1, rf_has_loc2.
Qed.

Lemma mo_eq_loc:
forall lab mo (Cmo: ConsistentMO lab mo)
a b (MO: mo a b),
loc (lab a) = loc (lab b).
Proof.
unfold ConsistentMO; ins; desf; eapply CmoD in MO; desf.
by destruct (lab a); destruct (lab b); inversion MO; inversion MO0; subst; auto.
Qed.

Lemma mo_has_loc1:
forall lab mo (Cmo: ConsistentMO lab mo)
a b (MO: mo a b),
has_loc (lab a).
Proof.
unfold ConsistentMO; ins; desf; eapply CmoD in MO; desf.
by destruct (lab a); inversion MO; subst; auto.
Qed.

Lemma mo_has_loc2:
forall lab mo (Cmo: ConsistentMO lab mo)
a b (MO: mo a b),
has_loc (lab b).
Proof.
unfold ConsistentMO; ins; desf; eapply CmoD in MO; desf.
by destruct (lab b); inversion MO0; subst; auto.
Qed.

Lemma mo_same_loc:
forall lab mo (Cmo: ConsistentMO lab mo)
a b (MO: mo a b),
same_loc (lab a) (lab b).
Proof.
ins; xplit; eauto using mo_eq_loc, mo_has_loc1, mo_has_loc2.
Qed.

Hint Immediate
rf_has_loc1 rf_has_loc2 rf_same_loc
mo_has_loc1 mo_has_loc2 mo_same_loc : loc.

Lemma reordering_ct:
forall rel a b (LA: adjacentWW rel a b)
x y (Ct: clos_trans _ (rel UNION1 (a,b)) x y),
clos_trans _ rel x y \/ a=x /\ b=y.
Proof.
ins; induction Ct; desf; dupdes LA; eauto using clos_trans.
by eapply t_step_rt in IHCt2; desf; eauto using t_rt_trans.
by eapply t_rt_step in IHCt1; desf; eauto using rt_t_trans.
Qed.

Lemma reordering_rse:
forall lab sb
a b (LA: adjacentWW sb a b) mt2
x y (RSE: release_seq_elem mt2 lab (sb UNION1 (a,b)) x y),
release_seq_elem mt2 lab sb x y \/ a=x /\ b=y.
Proof.
unfold release_seq_elem, same_thread; ins; desf; intuition.
eapply reordering_ct in RSE; desf; eauto.
Qed.

Lemma reordering_st :
forall lab sb
a b (LA: adjacentWW sb a b) mt2
x y (RS: same_thread mt2 lab (sb UNION1 (a,b)) x y)
(NEQ : x = a -> y = b -> False),
same_thread mt2 lab sb x y.
Proof.
by eapply reordering_ct in RS; desf; intuition.
Qed.

Lemma reordering_rs:
forall mt acts lab sb rf mo
(Cmo: ConsistentMO lab mo)
a b (AR: admissible_reordering mt acts lab a b)
(LA: adjacentWW sb a b) mt2
x y (RS: release_seq mt2 lab (sb UNION1 (a,b)) rf mo x y),
release_seq mt2 lab sb rf mo x y.
Proof.
unfold release_seq; ins; desf; desf; unnw; eauto.
right; desf; intuition.
eapply reordering_rse in RSE; eauto.
desf; intuition.
dupdes Cmo; eapply CmoD in RSMO; desf.
dupdes AR; exfalso; eapply AR_SL.
by xplit; destruct (lab x); destruct (lab y); inversion RSMO; inversion RSMO0; eauto.
unnw; ins.
eapply RSO in MA; eauto.
eapply reordering_rse in MA; eauto; desf.
dupdes Cmo; eapply CmoD in RSMO; eapply CmoD in MB; desf.
destruct (lab y); inversion RSMO0; inversion MB0; subst; subst.
dupdes AR; exfalso; eapply AR_SL.
by xplit; destruct (lab x); destruct (lab c); inversion RSMO; inversion MB; eauto.
dupdes AR; exfalso; eapply AR_SL.
by xplit; destruct (lab x); destruct (lab c); inversion RSMO; inversion MB; eauto.

induction RS; vauto.
eapply RS_thr; eauto; eapply reordering_st; eauto; ins; desf.
dupdes Cmo; eapply CmoD in RSmo.
dupdes AR; exfalso; eapply AR_SL.
by destruct (lab a); destruct (lab b); ins; desf.
Qed.

Lemma reordering_sw:
forall mt acts lab sb rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a b (AR: admissible_reordering mt acts lab a b)
(LA: adjacentWW sb a b) mt2
x y (SW: synchronizes_with mt2 lab (sb UNION1 (a,b)) rf mo true x y),
synchronizes_with mt2 lab sb rf mo true x y.
Proof.
unfold synchronizes_with; ins;
destruct SW as [ H | SW ]; [ left | right ].
desf; xplit; eauto using reordering_rs.
destruct SW as [ H | SW ]; [ left | right ].
des; unnw; intuition; eauto.
xplit; eauto using reordering_rs.
eapply reordering_ct in LA; eauto.
intuition. subst.
dupdes AR; exfalso.
destruct SW as [ H | SW ]; [ left | right ].
des; unnw; intuition; eauto.
xplit; eauto using reordering_rs.
generalize LA; eapply reordering_ct in LA; eauto; intro.
intuition. subst.
dupdes AR; exfalso.
eapply AR_Not_Fence_Rel_Write;
by eauto using Crf_Write, RS_Write1, reordering_rs with access.
des; unnw; intuition; dupdes AR; des; clarify.
eapply reordering_ct in SBW; eauto.
eapply reordering_ct in SBR; eauto.
des; clarify.
xplit; eauto using reordering_rs.
by destruct AR_Not_Fence_Rel_Write; eauto using Crf_Write, RS_Write1, reordering_rs with access.
by destruct AR_Not_Fence_Rel_Write; eauto using Crf_Write, RS_Write1, reordering_rs with access.
Qed.

Lemma reordering_hb_intermediate:
forall mt acts lab sb rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a b (AR: admissible_reordering mt acts lab a b)
(LA: adjacentWW sb a b) mt2 asw
x y (HB: happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo x y),
happens_before mt2 lab sb asw rf mo x y
\/ (x = a \/ happens_before mt2 lab sb asw rf mo x a)
/\
(y = b \/ happens_before mt2 lab sb asw rf mo b y).
Proof.
ins; induction HB; desf; eauto 6 using reordering_sw, sw_in_hb with hb.
Qed.

Lemma reordering_hb_cycle:
forall mt acts lab sb rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a b (AR: admissible_reordering mt acts lab a b)
(LA: adjacentWW sb a b) mt2 asw
x (HB: happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo x x),
happens_before mt2 lab sb asw rf mo x x \/
happens_before mt2 lab sb asw rf mo b a.
Proof.
ins.
eapply reordering_hb_intermediate in HB; eauto.
destruct HB as [ ? | HB ].
by eauto.
desf; subst; eauto using hb_trans.
dupdes AR; intuition.
Qed.

Lemma reordering_hb_right:
forall mt mt2 acts lab sb asw rf mo
a b (AR: admissible_reordering mt acts lab a b)
x (HB: happens_before mt2 lab sb asw rf mo x a),
happens_before mt2 lab sb asw rf mo x b.
Proof.
ins; induction HB; eauto using hb_trans; desf.
by dupdes LASB; eauto using t_sb_in_hb, clos_trans.
by dupdes AR; exfalso; eauto with sync.
by dupdes LAASW; eauto using t_asw_in_hb, clos_trans.
Qed.

Lemma reordering_hb_left:
forall mt mt2 acts lab sb asw rf mo
a b (AR: admissible_reordering mt acts lab a b)
y (HB: happens_before mt2 lab sb asw rf mo b y),
happens_before mt2 lab sb asw rf mo a y.
Proof.
ins; induction HB; eauto using hb_trans; desf.
by dupdes LASB; eauto using t_sb_in_hb, clos_trans.
by dupdes AR; exfalso; eauto with sync.
by dupdes LAASW; eauto using t_asw_in_hb, clos_trans.
Qed.

Final reordering_hb lemma

Lemma reordering_hb:
forall mt mt2 acts lab sb asw rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a b (AR: admissible_reordering mt acts lab a b)
x y (HB: happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo x y),
happens_before mt2 lab sb asw rf mo x y \/ (x=a /\ y=b).
Proof.
ins; induction HB; desf; eauto using hb_trans, sb_in_hb, asw_in_hb.
by left; eapply sw_in_hb, reordering_sw; eauto.
by left; eapply reordering_hb_left; eauto.
by left; eapply reordering_hb_right; eauto.
Qed.

forall mt mt2 acts lab sb asw rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a b (AR: admissible_reordering mt acts lab a b)
adjacentW (happens_before mt2 lab sb asw rf mo) a b.
Proof.
ins; unfold adjacentW; repeat split; try red; ins.
eapply reordering_hb_left; eauto.
eapply reordering_hb_right; eauto.
Qed.

Lemma path_decomp_three_steps:
forall X (eq_X_dec: forall (x y: X), {x=y} + {x<>y})
rel x y
(XY: clos_trans X rel x y),
rel x y \/
(exists z, rel x z /\ rel z y) \/
(exists z t, z <> y /\ t <> x /\ rel x z /\ clos_trans X rel z t /\ rel t y).
Proof.
ins.
eapply clos_trans_t1n in XY.
destruct XY.
by eauto.
destruct (eq_X_dec y z); subst.
by eauto.
eapply clos_t1n_trans in XY.
eapply clos_trans_tn1 in XY.
destruct XY.
by eauto.
destruct (eq_X_dec y0 x); subst.
by eauto.
eapply clos_tn1_trans in XY.
by eauto 9.
Qed.

Lemma reordering_acyclic_hb:
forall mt mt2 acts lab sb asw rf mo
(IRR: irreflexive (happens_before mt2 lab sb asw rf mo))
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a b (AR: admissible_reordering mt acts lab a b)
irreflexive (happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo).
Proof.
ins; intros x HB.
eapply reordering_hb_cycle in HB; eauto.
des; eauto.
eapply path_decomp_three_steps in HB; eauto using eq_nat_dec.
dupdes AR; dupdes LASB; dupdes LAASW.
by des; eauto 7 with sync hb.
Qed.

forall mt mt2 acts lab sb asw rf mo
(IRR: irreflexive (happens_before mt2 lab sb asw rf mo))
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo)
a b (AR: admissible_reordering mt acts lab a b)
happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo
<--> happens_before mt2 lab sb asw rf mo UNION1 (a,b).
Proof.
split; unfold inclusion; ins.
eapply reordering_hb in H; eauto. by intuition.
intuition; eauto using happens_before_mon_sb.
Qed.

We develop separate lemmas for the acyclity axioms.
• MTorig

Lemma acyclicity_orig:
forall mt2 mtsc acts lab sb dsb asw rf mo sc
(CONS: Semiconsistent MTorig mt2 mtsc acts lab sb dsb asw rf mo sc)
a b,
ConsistentRF_na mt2 lab (sb UNION1 (a,b)) asw rf mo.
Proof.
ins; dupdes CONS; unfold ConsistentRF_na; ins.
by eauto using happens_before_mon_sb.
Qed.

• MThbUrfnaAcyclic and MThbUrfAcyclic

Lemma decomp_path_sbUrf_UNION:
forall sb rf P a b x y
(PATH: clos_trans actid (fun x y => (sb UNION1 (a,b)) x y \/ rf y = Some x /\ P x y) x y),
clos_trans _ (fun x y => sb x y \/ rf y = Some x /\ P x y) x y
\/ clos_refl_trans _ (fun x y => sb x y \/ rf y = Some x /\ P x y) x a
/\ clos_refl_trans _ (fun x y => sb x y \/ rf y = Some x /\ P x y) b y.
Proof.
ins. induction PATH.
by desf; intuition.
desf; intuition.
by eauto using t_trans.
by eauto using clos_trans_in_rt, rt_t_trans.
by eauto using clos_trans_in_rt, t_rt_trans.
Qed.

We prove the acyclicity result parametrically with respect to any restriction of the reads from relation.

Lemma acyclicity_relUrf:
forall mt acts lab rel rf P
(ACYC: acyclic (fun x y => rel x y \/ rf y = Some x /\ P x y))
(Crf: ConsistentRF lab rf)
a b (AR: admissible_reordering mt acts lab a b)
(ABNRW: ~ (is_read (lab a) /\ is_write (lab b))),
acyclic (fun x y => (rel UNION1 (a,b)) x y \/ rf y = Some x /\ P x y).
Proof.
ins; intros x HB.
eapply decomp_path_sbUrf_UNION in HB; desf; eauto.
dupdes LA; dupdes Crf; dupdes AR.

rewrite clos_refl_transE in HB; desf.

rewrite clos_refl_transE in *; desf.
eapply t_step_rt in HB0; des.
by eapply ACYC, t_rt_trans; [eapply clos_trans_mon; [eapply t_step, LA_ac|]|]; eauto.

rewrite clos_refl_transE in *; desf.
by eapply Crf0 in HB0; desf; destruct (lab a); destruct (lab b); ins; desf; eauto.

eapply t_rt_step in HB1; desf.
by eapply ACYC, t_rt_trans; [eapply clos_trans_mon; [eapply t_step, LA_cb|]|];
eauto using clos_refl_trans.

eapply Crf0 in HB0; eapply Crf0 in HB3; desf.
by destruct (lab a); destruct (lab b); ins; desf; eauto.

assert (M := HB).
eapply t_rt_step in M; desf.
apply LA in M0.
by eapply ACYC, t_rt_trans, HB0; eauto using rt_t_trans, t_step.
clear M.

rewrite clos_refl_transE in *; desf.
eapply t_step_rt in HB; des.
by eapply ACYC, t_rt_trans; [eapply clos_trans_mon; [eapply t_step, LA_ac|]|]; eauto.

rewrite clos_refl_transE in *; desf.
by eapply Crf in HB; desf; destruct (lab a); destruct (lab z);

eapply t_rt_step in HB0; desf.
by eapply ACYC, t_rt_trans; [eapply clos_trans_mon; [eapply t_step, LA_cb|]|];
eauto using clos_refl_trans.

eapply Crf0 in HB; eapply Crf0 in M0; desf.
by destruct (lab a); destruct (lab x); inversion WRITE0; inversion READ; eauto.

eapply t_step_rt in HB0; desf.
apply LA_ac in HB0.
by eapply ACYC, t_rt_trans, HB1; eauto using t_trans, t_step.

eapply Crf in M0; eapply Crf0 in HB0; desf.
by apply ABNRW; destruct (lab a); destruct (lab b); ins; desf.
Qed.

The two acyclity lemmas are deduced by instantiation of the parametric lemma.

Lemma acyclicity_hbUrf:
forall mt2 mtsc acts lab sb dsb asw rf mo sc
(CONS: Semiconsistent MThbUrfAcyclic mt2 mtsc acts lab sb dsb asw rf mo sc)
a b (AR: admissible_reordering MThbUrfAcyclic acts lab a b)
acyclic (fun x y => happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo x y \/ rf y = Some x)
\/ is_read (lab a) /\ is_write (lab b).
Proof.
ins; assert ((is_read (lab a) /\ is_write (lab b)) \/ ~ (is_read (lab a) /\ is_write (lab b))).
by destruct (lab a); destruct (lab b); simpl; intuition.
desf; eauto.
dupdes CONS.
left; intros x hxx.
eapply acyclicity_relUrf with
(P := fun x y => True)
(rel := happens_before mt2 lab sb asw rf mo); eauto using hb_adjacentW.
intros t htt; eapply ACYC.
by eapply clos_trans_monotonic; [ | eapply htt]; red; intuition.
eapply clos_trans_monotonic; [ | eauto ].
red; ins; desf; eauto.
Qed.

Lemma acyclicity_hbUrfna:
forall mt2 mtsc acts lab sb dsb asw rf mo sc
(CONS: Semiconsistent MThbUrfnaAcyclic mt2 mtsc acts lab sb dsb asw rf mo sc)
a b (AR: admissible_reordering MThbUrfnaAcyclic acts lab a b)
acyclic (fun x y => happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo x y \/ rfna lab rf x y)
\/ is_read (lab a) /\ is_write (lab b).
Proof.
ins; assert ((is_read (lab a) /\ is_write (lab b)) \/ ~ (is_read (lab a) /\ is_write (lab b))).
by destruct (lab a); destruct (lab b); simpl; intuition.
desf; eauto.
dupdes CONS.
left; intros x hxx.
eapply acyclicity_relUrf with (P := fun x y => is_na (lab x) \/ is_na (lab y)); eauto using hb_adjacentW.
eapply clos_trans_monotonic; [ | eauto ].
red; ins; desf; eauto.
Qed.

We prove the main theorem of this section, that the admissible reorderings preserve semiconsistent executions and data races.

Theorem Semiconsistent_reordering :
forall mt mt2 mtsc acts lab sb dsb asw rf mo sc
(CONS: Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
a b (AR: admissible_reordering mt acts lab a b)
<< CONS': Semiconsistent mt mt2 mtsc acts lab (sb UNION1 (a,b)) dsb asw rf mo sc >> /\
<< RACE: racy mt2 lab sb asw rf mo -> racy mt2 lab (sb UNION1 (a,b)) asw rf mo >>.
Proof.
ins; dupdes CONS.

assert (case_hb: forall x y,
happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo x y ->
happens_before mt2 lab sb asw rf mo x y \/ x=a /\ y=b).
by eauto using reordering_hb.

unfold Semiconsistent; desf; unfold NW; intuition.

desf; intuition.
by red; ins; desf; eauto.

by eapply reordering_acyclic_hb; eauto.

destruct mt.
by eapply acyclicity_orig; eauto.
by eauto.
exploit acyclicity_hbUrfna; eauto.
by ins; desf; dupdes AR; exfalso; eauto.
exploit acyclicity_hbUrf; eauto.
by ins; desf; dupdes AR; exfalso; eauto.
by eauto.

by dupdes AR; dupdes Csb; red; ins; desf; subst; eauto.

by dupdes Cdsb; repeat split; try red; ins; eauto using clos_trans_mon.

unfold ConsistentMOhb in *; desf; intuition; red; ins.
eapply CmoH; eauto.
destruct (case_hb _ _ REL).
by eauto. desf.
by exfalso; dupdes AR; eapply AR_SL; desf;
destruct (lab a); destruct (lab b); inversion IWa; inversion IWb;
subst; eauto.

unfold ConsistentSC in *; desf; intuition; red; ins.
unfold restr_subset; ins.
eapply Chbsc; eauto.
destruct (case_hb _ _ REL).
by eauto. desf.
by exfalso; dupdes AR; eapply AR_Not_Both_Sc; eauto.

unfold SCrestriction; ins.
generalize RF, SC.
eapply Cscr in RF. eapply RF in SC. clear RF. ins. desf.
by intuition.
right; intuition.
eapply SC1; eauto.
destruct (case_hb _ _ HB).
by eauto. desf.
unfold sc_restr in *. desf.
eapply Crf in RF. desf.

exfalso; dupdes AR; eapply AR_SL; xplit.
destruct (lab a); inversion WRITE; eauto.
by unfold sc_restr_cond, sc_restr, immediate in SC2; desf; desc; destruct (lab b); ins.

by unnw; red in SC2; unfold immediate, sc_restr in SC2; desf; desf;
destruct (lab a); destruct (lab b0); ins; desf.

unfold ConsistentRF_dom_none in *; desf; intuition; ins.
eapply CrfN; eauto.
destruct (case_hb _ _ HB).
by eauto. desf.
by exfalso; dupdes AR; eapply AR_SL; desf;
destruct (lab a); destruct (lab b); inversion READ; inversion WRI;
subst; eauto.

unfold ConsistentRFhb in *; desf; intuition; ins.
exploit Crf; eauto. ins; desf.
eapply CrfH; eauto.
destruct (case_hb _ _ HB).
by eauto. desf.
by exfalso; dupdes AR; eapply AR_SL; desf;
destruct (lab a); destruct (lab b); inversion READ; inversion WRITE;
subst; eauto.

unfold CoherentRR in *; desf; intuition; ins.
eapply Crr; [ | exact RFa | exact RFb | exact MO ].
destruct (case_hb _ _ HB).
by eauto. desf.
exfalso; dupdes AR; eapply AR_SL; desf; xplit; eauto with loc.
erewrite <- rf_eq_loc by eauto.
erewrite <- mo_eq_loc by eauto.
by eauto using rf_eq_loc.

unfold CoherentWR in *; desf; intuition; ins.
eapply Cwr; eauto.
destruct (case_hb _ _ HB).
by eauto. desf.
exfalso; dupdes AR; eapply AR_SL; desf; xplit; red; eauto with loc.
erewrite <- mo_eq_loc by eauto.
by eauto using rf_eq_loc.

unfold CoherentRW in *; desf; intuition; ins.
eapply Crw; eauto.
destruct (case_hb _ _ HB).
by eauto. desf.
exfalso; dupdes AR; eapply AR_SL; desf; xplit; red; eauto with loc.
erewrite <- rf_eq_loc by eauto.
symmetry; by eauto using mo_eq_loc.

unfold racy in *; desc; unnw; repeat (eexists; try edone);
clear WRI NA; intro HB; eapply case_hb in HB; desf;
by dupdes AR; eapply AR_SL; destruct (lab a); ins; destruct (lab b); ins.
Qed.

Using restrict_rf, we can lift this theorem to preserve consistent executions.

Theorem Consistent_reordering :
forall mt (MT: mt <> MTorig) mt2 mtsc acts lab sb dsb asw rf mo sc
(CONS: Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
a b (AR: admissible_reordering mt acts lab a b)
exists rf',
<< CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a,b)) dsb asw rf' mo sc >> /\
<< RACE: racy mt2 lab sb asw rf mo -> racy mt2 lab (sb UNION1 (a,b)) asw rf mo >>.
Proof.
ins; exploit Semiconsistent_reordering; eauto using Consistent_weaken.
intro; desf; unnw.
eexists,; eauto using Consistent_restrict_rf, race_free_restrict_rf.
Qed.

Note that the theorem above requires a weaker adjacency condition. The theorem shown in the paper is a simple corollary.

Corollary Consistent_reordering_paper :
forall mt mt2 mtsc acts lab sb dsb asw rf mo sc a b,
Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc ->
admissible_reordering mt acts lab a b ->