# "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 : c, rel b crel a c
LA_ca : c, rel c bc arel c a
LA_cb : c, rel c arel c b
LA_bc : c, rel a cc brel 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 : c, rel b crel a c
LA_cb : c, rel c arel 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 : c, rel b cclos_trans _ rel a c
LA_cb : c, rel c aclos_trans _ rel c b .

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

Lemma adjacent_weaken rel a b :

Lemma adjacentW_weaken rel a b :

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
| |- x, _eexists
| |- _ _split
end.

lab rf
(Crf: ConsistentRF lab rf)
a b (RF: rf a = Some b),

Lemma Crf_Write:
lab rf
(Crf: ConsistentRF lab rf)
a b (RF: rf a = Some b),
is_write (lab b).

Lemma Cmo_Write1:
lab mo
(Cmo: ConsistentMO lab mo)
a b (MO: mo a b),
is_write (lab a).

Lemma Cmo_Write2:
lab mo
(Cmo: ConsistentMO lab mo)
a b (MO: mo a b),
is_write (lab b).

Lemma RS_Write1:
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).

Lemma sync_release:
mt2 lab sb rf mo flag a b,
synchronizes_with mt2 lab sb rf mo flag a b
is_release (lab a).

Lemma sync_acquire:
mt2 lab sb rf mo flag a b,
synchronizes_with mt2 lab sb rf mo flag a b
is_acquire (lab b).

Hint Immediate sync_release sync_acquire : sync.

Lemma rf_eq_loc:
lab rf (Crf: ConsistentRF lab rf)
a b (RF: rf b = Some a),
loc (lab a) = loc (lab b).

Lemma rf_has_loc1:
lab rf (Crf: ConsistentRF lab rf)
a b (RF: rf b = Some a),
has_loc (lab a).

Lemma rf_has_loc2:
lab rf (Crf: ConsistentRF lab rf)
a b (RF: rf b = Some a),
has_loc (lab b).

Lemma rf_same_loc:
lab rf (Crf: ConsistentRF lab rf)
a b (RF: rf b = Some a),
same_loc (lab a) (lab b).

Lemma mo_eq_loc:
lab mo (Cmo: ConsistentMO lab mo)
a b (MO: mo a b),
loc (lab a) = loc (lab b).

Lemma mo_has_loc1:
lab mo (Cmo: ConsistentMO lab mo)
a b (MO: mo a b),
has_loc (lab a).

Lemma mo_has_loc2:
lab mo (Cmo: ConsistentMO lab mo)
a b (MO: mo a b),
has_loc (lab b).

Lemma mo_same_loc:
lab mo (Cmo: ConsistentMO lab mo)
a b (MO: mo a b),
same_loc (lab a) (lab b).

Hint Immediate
rf_has_loc1 rf_has_loc2 rf_same_loc
mo_has_loc1 mo_has_loc2 mo_same_loc : loc.

Lemma reordering_ct:
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.

Lemma reordering_rse:
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.

Lemma reordering_st :
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 = ay = bFalse),
same_thread mt2 lab sb x y.

Lemma reordering_rs:
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.

Lemma reordering_sw:
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.

Lemma reordering_hb_intermediate:
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).

Lemma reordering_hb_cycle:
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.

Lemma reordering_hb_right:
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.

Lemma reordering_hb_left:
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.

Final reordering_hb lemma

Lemma reordering_hb:
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).

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.

Lemma path_decomp_three_steps:
X (eq_X_dec: (x y: X), {x=y} + {xy})
rel x y
(XY: clos_trans X rel x y),
rel x y
( z, rel x z rel z y)
( z t, z y t x rel x z clos_trans X rel z t rel t y).

Lemma reordering_acyclic_hb:
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).

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

We develop separate lemmas for the acyclity axioms.
• MTorig

Lemma acyclicity_orig:
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.

• MThbUrfnaAcyclic and MThbUrfAcyclic

Lemma decomp_path_sbUrf_UNION:
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 ysb x y rf y = Some x P x y) x y
clos_refl_trans _ (fun x ysb x y rf y = Some x P x y) x a
clos_refl_trans _ (fun x ysb x y rf y = Some x P x y) b y.

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

Lemma acyclicity_relUrf:
mt acts lab rel rf P
(ACYC: acyclic (fun x yrel 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).

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

Lemma acyclicity_hbUrf:
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 yhappens_before mt2 lab (sb UNION1 (a,b)) asw rf mo x y rf y = Some x)
is_read (lab a) is_write (lab b).

Lemma acyclicity_hbUrfna:
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 yhappens_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).

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

Theorem Semiconsistent_reordering :
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 moracy mt2 lab (sb UNION1 (a,b)) asw rf mo .

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

Theorem Consistent_reordering :
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)
rf',
CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a,b)) dsb asw rf' mo sc
RACE: racy mt2 lab sb asw rf moracy mt2 lab (sb UNION1 (a,b)) asw rf mo .

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

Corollary Consistent_reordering_paper :
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