# Monotonicity

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

## Basic monotonicity properties

Monotonicity with respect to program order.

Lemma release_seq_mon_sb :
mt2 lab sb rf mo a b (HB: release_seq mt2 lab sb rf mo a b)
(sb' : relation actid) (MON: x y (SB: sb x y), sb' x y),
release_seq mt2 lab sb' rf mo a b.

Lemma happens_before_mon_sb :
mt2 lab sb asw rf mo a b (HB: happens_before mt2 lab sb asw rf mo a b)
(sb' : relation actid) (MON: x y (SB: sb x y), sb' x y),
happens_before mt2 lab sb' asw rf mo a b.

Lemma release_seq_mon_rf :
mt2 lab sb rf mo a b (HB: release_seq mt2 lab sb rf mo a b)
rf' (M: c d (RF: rf c = Some d), rf' c = Some d),
release_seq mt2 lab sb rf' mo a b.

Lemma happens_before_mon_rf :
rf rf' (M: c d (RF: rf c = Some d), rf' c = Some d)
mt2 lab sb asw mo a b (HB : happens_before mt2 lab sb asw rf mo a b),
happens_before mt2 lab sb asw rf' mo a b.

## Domain restriction for reads-from map

In this subsection, we show that every semiconsistent execution can be turned into a consistent one by removing some rf edges (Theorem ConsistentRFrestrict).

Definition restrict_rf_once mt2 lab sb asw rf mo a :=
if excluded_middle_informative
( b l, happens_before mt2 lab sb asw rf mo b a
is_writeL (lab b) l is_readL (lab a) l)
then rf a else None.

We define a measure that is decreased by each restrict_rf_once step.

Definition restrict_measure acts (rf : actidoption actid) :=
length (filter (fun xmatch rf x with Some _true | Nonefalse end) acts).

Lemma restrict_measure_rf :
mt2 lab sb asw rf mo acts,
restrict_measure acts (restrict_rf_once mt2 lab sb asw rf mo)
restrict_measure acts rf.

Lemma restrict_measure_rf_dec :
mt2 lab sb asw rf mo acts
(INA: a b, rf a = Some bIn a acts)
(NEQ: restrict_rf_once mt2 lab sb asw rf mo rf),
restrict_measure acts (restrict_rf_once mt2 lab sb asw rf mo)
< restrict_measure acts rf.

Perform restrict_rf_once n number of times.

Fixpoint restrict_rf_n n mt2 lab sb asw rf mo :=
match n with
| 0 ⇒ rf
| S nrestrict_rf_once mt2 lab sb asw
(restrict_rf_n n mt2 lab sb asw rf mo) mo
end.

Lemma restrict_rf_nC :
mt2 lab sb asw mo n rf,
restrict_rf_once mt2 lab sb asw (restrict_rf_n n mt2 lab sb asw rf mo) mo =
restrict_rf_n n mt2 lab sb asw (restrict_rf_once mt2 lab sb asw rf mo) mo.

Lemma restrict_rf_n_fix_helper :
mt2 lab sb asw mo acts n rf
(INA: a b, rf a = Some bIn a acts),
restrict_rf_n (S n) mt2 lab sb asw rf mo = restrict_rf_n n mt2 lab sb asw rf mo
restrict_measure acts (restrict_rf_n n mt2 lab sb asw rf mo) + n
restrict_measure acts rf.

Lemma restrict_rf_n_fix_helper2 :
mt2 lab sb asw mo acts n rf
(INA: a b, rf a = Some bIn a acts)
(GT: length acts < n),
restrict_rf_n (S n) mt2 lab sb asw rf mo
= restrict_rf_n n mt2 lab sb asw rf mo.

Given that restrict_rf_once always decrements the measure, we know that restrict_rf_n will reach a fixed point. We define restrict_rf to be that fixed point.

Definition restrict_rf mt2 (acts : list actid) lab sb asw rf mo :=
restrict_rf_n (S (length acts)) mt2 lab sb asw rf mo.

We prove various properties of the fixed point.

Lemma restrict_rf_n_unchanged :
mt2 lab sb asw n rf mo a b l,
happens_before mt2 lab sb asw (restrict_rf_n n mt2 lab sb asw rf mo) mo b a
is_writeL (lab b) l
restrict_rf_n n mt2 lab sb asw rf mo a = rf a.

Lemma restrict_rf_unfold :
mt2 acts rf lab sb asw mo
(FIN: ExecutionFinite acts lab sb asw)
(Crf: ConsistentRF lab rf) a,
restrict_rf mt2 acts lab sb asw rf mo a =
if excluded_middle_informative
( b l, happens_before mt2 lab sb asw (restrict_rf mt2 acts lab sb asw rf mo) mo b a
is_writeL (lab b) l is_readL (lab a) l)
then rf a else None.

Lemma restrict_rf_mon :
mt2 acts lab sb asw rf mo a b,
restrict_rf mt2 acts lab sb asw rf mo a = Some b
rf a = Some b.

Happens-before is unaffected by restrict_rf.

Lemma happens_before_restrict_rf :
mt2 acts lab sb asw rf mo a b,
happens_before mt2 lab sb asw (restrict_rf mt2 acts lab sb asw rf mo) mo a b
happens_before mt2 lab sb asw rf mo a b.

Finally, we show our main theorem, that for every semiconsistent execution there exists a consistent execution that differs only in the rf component.

Theorem Consistent_restrict_rf :
mt (MT: mt MTorig) mt2 mtsc acts lab sb dsb asw rf mo sc,
Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc
Consistent mt mt2 mtsc acts lab sb dsb asw (restrict_rf mt2 acts lab sb asw rf mo) mo sc.

Theorem racy_restrict_rf mt2 acts lab sb asw rf mo :
racy mt2 lab sb asw rf mo
racy mt2 lab sb asw (restrict_rf mt2 acts lab sb asw rf mo) mo.

Corollary race_free_restrict_rf mt2 acts lab sb asw rf mo :
race_free mt2 lab sb asw (restrict_rf mt2 acts lab sb asw rf mo) mo
race_free mt2 lab sb asw rf mo.

## Label monotonicity

Definition RATord x y :=
match x, y with
| RATna, RATnatrue
| RATna, _false
| _, RATnafalse
| RATrlx, _true
| _, RATrlxfalse
| RATacq, _true
| _, RATacqfalse
| RATsc, RATsctrue
end.

Definition WATord x y :=
match x, y with
| WATna, WATnatrue
| WATna, _false
| _, WATnafalse
| WATrlx, _true
| _, WATrlxfalse
| WATrel, _true
| _, WATrelfalse
| WATsc, WATsctrue
end.

Definition UATord x y :=
match x, y with
| UATrlx, _true
| _, UATrlxfalse
| UATacq, UATrelfalse
| UATacq, _true
| UATrel, UATacqfalse
| UATrel, _true
| UATrel_acq, UATrel_acqtrue
| UATrel_acq, UATsctrue
| UATsc, UATsctrue
| _, _false
end.

Definition FATord x y :=
match x, y with
| FATacq, FATrelfalse
| FATacq, _true
| FATrel, FATacqfalse
| FATrel, _true
| FATrel_acq, FATrel_acqtrue
| FATrel_acq, FATsctrue
| FATsc, FATsctrue
| _, _false
end.

Definition act_ord x y :=
match x, y with
| Askip tid, Afence tid' typtid = tid'
| Aalloc tid l n, Aalloc tid' l' n'
tid = tid' l = l' n = n'
tid = tid' RATord typ typ' l = l' v = v'
| Astore tid typ l v, Astore tid' typ' l' v'
tid = tid' WATord typ typ' l = l' v = v'
| Armw tid typ l v w, Armw tid' typ' l' v' w'
tid = tid' UATord typ typ' l = l' v = v' w = w'
| Afence tid typ, Afence tid' typ'
tid = tid' FATord typ typ'
| _, _False
end.

Lemma act_ord_refl x : act_ord x x.

Section act_ord_lemmas.

Variables x y : act.
Hypothesis (AO : act_ord x y).

Ltac tac :=
generalize AO; unfold act_ord; desf; ins; desf;
match goal with
| typ : write_access_type |- _solve [destruct typ; ins; desf]
| typ : read_access_type |- _solve [destruct typ; ins; desf]
| typ : rmw_access_type |- _solve [destruct typ; ins; desf]
| typ : fence_access_type |- _solve [destruct typ; ins; desf]
end.

Lemma act_ord_loc : loc x = loc y.

Lemma act_ord_na : is_na xis_na y.

Lemma act_ord_na_rev : is_na yis_na x.

Lemma act_ord_sc : is_sc xis_sc y.

Lemma act_ord_rmw : is_rmw xis_rmw y.

Lemma act_ord_rmw_rev : is_rmw yis_rmw x.

Lemma act_ord_writeLV_rev l v : is_writeLV y l vis_writeLV x l v.

Lemma act_ord_write : is_write xis_write y.

Lemma act_ord_writeL l : is_writeL x lis_writeL y l.

Lemma act_ord_writeL_rev l : is_writeL y lis_writeL x l.

Lemma act_ord_writeLV l v : is_writeLV x l vis_writeLV y l v.

Lemma act_ord_access : is_access xis_access y.

Lemma act_ord_release_write : is_release_write xis_release_write y.

Lemma act_ord_release_fence : is_release_fence xis_release_fence y.

Lemma act_ord_acquire_fence : is_acquire_fence xis_acquire_fence y.

End act_ord_lemmas.

Hint Resolve act_ord_na act_ord_na_rev act_ord_sc
act_ord_rmw act_ord_write act_ord_writeL act_ord_writeLV
act_ord_release_write act_ord_release_fence

Release sequences are monotone.

Lemma release_seq_mon :
lab lab' (LO: a, act_ord (lab' a) (lab a))
(sb sb' : relation actid) (SBO: a b, sb' a bsb a b)
rf rf' (RFO: c d (RF: rf' c = Some d), rf c = Some d)
mt2 mo a b
(RS: release_seq mt2 lab' sb' rf' mo a b),
release_seq mt2 lab sb rf mo a b.

The happens-before relation is monotone.

Lemma happens_before_mon :
lab lab' (LO: a, act_ord (lab' a) (lab a))
(sb sb' : relation actid) (SBO: a b, sb' a bsb a b)
mt2 asw rf mo a b (HB: happens_before mt2 lab' sb' asw rf mo a b),
happens_before mt2 lab sb asw rf mo a b.

Next comes the main theorem of this section. For any sufficiently corrected model, removing synchronisation from consistent executions preserves their consistency. We first prove this theorem for all axioms except ConsistentRF_dom_some; then using Theorem ConsistentRFrestrict, we extend it to all the axioms.

Theorem Semiconsistent_mon :
mt (MT: mt MTorig) mt2 mtsc (MTSC: mtsc MTSCorig) acts lab sb dsb asw rf mo sc
(CONS: Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
lab' (LO: a, act_ord (lab' a) (lab a))
(sb' : relation actid) (SBO: a b, sb' a bsb a b)
(CSb': ConsistentSB lab' sb') (DSBO: inclusion _ dsb (clos_trans _ sb')),
sc',
Semiconsistent mt mt2 mtsc acts lab' sb' dsb asw rf mo sc'.

Corollary Consistent_mon :
mt (MT: mt MTorig) mt2 mtsc (MTSC: mtsc MTSCorig)
acts lab sb dsb asw rf mo sc
(CONS: Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
lab' (LO: a, act_ord (lab' a) (lab a))
(sb' : relation actid) (SBO: a b, sb' a bsb a b)
(CSb': ConsistentSB lab' sb') (DSBO: inclusion _ dsb (clos_trans _ sb')),
rf' sc',
Consistent mt mt2 mtsc acts lab' sb' dsb asw rf' mo sc'.