# 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 :
forall mt2 lab sb rf mo a b (HB: release_seq mt2 lab sb rf mo a b)
(sb' : relation actid) (MON: forall x y (SB: sb x y), sb' x y),
release_seq mt2 lab sb' rf mo a b.
Proof.
unfold release_seq, release_seq_elem, NW; ins; desf; desf; eauto;
try by
right; repeat split;
ins; desf; eauto 8 using clos_trans_mon; exploit HB1; eauto; ins; desf;
eauto 8 using clos_trans_mon.

induction HB; destruct mt2 as [[]?]; desf; ins; desf; ins;
eauto using release_seq_alt.
red in RSthr; ins; eapply clos_trans_mon in RSthr; try eassumption; vauto.
Qed.

Lemma happens_before_mon_sb :
forall mt2 lab sb asw rf mo a b (HB: happens_before mt2 lab sb asw rf mo a b)
(sb' : relation actid) (MON: forall x y (SB: sb x y), sb' x y),
happens_before mt2 lab sb' asw rf mo a b.
Proof.
unfold happens_before; ins; induction HB as [? ? []|]; vauto;
constructor 1; eauto;
unfold synchronizes_with, NW in *; desf;
eauto 21 using clos_trans_mon, release_seq_mon_sb.
Qed.

Lemma release_seq_mon_rf :
forall mt2 lab sb rf mo a b (HB: release_seq mt2 lab sb rf mo a b)
rf' (M: forall c d (RF: rf c = Some d), rf' c = Some d),
release_seq mt2 lab sb rf' mo a b.
Proof.
unfold release_seq, release_seq_elem, NW; ins; desf; desf; eauto.
induction HB; desf; destruct mt2; ins; desf;
eauto using release_seq_alt.
Qed.

Lemma happens_before_mon_rf :
forall rf rf' (M: forall 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.
Proof.
unfold happens_before; ins; induction HB as [? ? []|]; vauto;
constructor 1; eauto;
unfold synchronizes_with, NW in *; desf;
eauto 20 using release_seq_mon_rf.
Qed.

## 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
(exists 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 : actid -> option actid) :=
length (filter (fun x => match rf x with Some _ => true | None => false end) acts).

Lemma restrict_measure_rf :
forall mt2 lab sb asw rf mo acts,
restrict_measure acts (restrict_rf_once mt2 lab sb asw rf mo)
<= restrict_measure acts rf.
Proof.
unfold restrict_measure, restrict_rf_once; induction acts; ins; desf; ins; omega.
Qed.

Lemma restrict_measure_rf_dec :
forall mt2 lab sb asw rf mo acts
(INA: forall a b, rf a = Some b -> In 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.
Proof.
ins; assert (H: exists x y, In x acts /\ rf x = Some y /\
restrict_rf_once mt2 lab sb asw rf mo x = None).
{ apply NNPP; intro; destruct NEQ; extensionality z; apply NNPP; intro.
destruct H; exists z; specialize (INA z); unfold restrict_rf_once in *; desf.
by destruct (rf z); ins; eauto.
}
desf; clear INA NEQ; induction acts; ins; desf.
clear IHacts; pose proof (restrict_measure_rf mt2 lab sb asw rf mo acts).
unfold restrict_measure in *; ins; desf; ins; omega.
specialize (IHacts H).
unfold restrict_measure, restrict_rf_once in *; ins; desf; ins; omega.
Qed.

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 n => restrict_rf_once mt2 lab sb asw
(restrict_rf_n n mt2 lab sb asw rf mo) mo
end.

Lemma restrict_rf_nC :
forall 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.
Proof.
by induction n; ins; rewrite IHn.
Qed.

Lemma restrict_rf_n_fix_helper :
forall mt2 lab sb asw mo acts n rf
(INA: forall a b, rf a = Some b -> In 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.
Proof.
induction n; ins; try (right; omega).
rewrite restrict_rf_nC.
exploit (IHn (restrict_rf_once mt2 lab sb asw rf mo)); ins; desf; eauto.
by unfold restrict_rf_once in H; desf; eauto.
apply NNPP; intro X; apply not_or_and in X; desf.
destruct X; rewrite <- restrict_rf_nC at 2; do 2 f_equal; apply NNPP; intro X.
eapply restrict_measure_rf_dec with (acts := acts) in X; ins.
destruct X0; omega.
Qed.

Lemma restrict_rf_n_fix_helper2 :
forall mt2 lab sb asw mo acts n rf
(INA: forall a b, rf a = Some b -> In 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.
Proof.
ins; eapply restrict_rf_n_fix_helper in INA; des; [by apply INA|].
cut (restrict_measure acts rf <= length acts); [omega|].
clear; unfold restrict_measure; induction acts; ins; desf; ins; omega.
Qed.

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 :
forall 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.
Proof.
induction n; ins.
unfold restrict_rf_once; desf; ins; desf; eauto.
destruct n0; repeat eexists; eauto.
eapply happens_before_mon_rf, H; unfold restrict_rf_once; ins; desf.
Qed.

Lemma restrict_rf_unfold :
forall 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
(exists 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.
Proof.
ins; unfold restrict_rf at 1.
rewrite <- (restrict_rf_n_fix_helper2) with (acts:=acts); ins.
unfold restrict_rf; unfold restrict_rf_once at 1; ins; desf; desf.
eapply restrict_rf_n_unchanged with (n := S _); eauto.
eapply finiteRF in H; desf; eauto.
Qed.

Lemma restrict_rf_mon :
forall 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.
Proof.
unfold restrict_rf; intros until 0; induction (S _); ins.
unfold restrict_rf_once in *; desf; ins; desf; eauto.
Qed.

Happens-before is unaffected by restrict_rf.

Lemma happens_before_restrict_rf :
forall 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.
Proof.
eauto using happens_before_mon_rf, restrict_rf_mon.
Qed.

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 :
forall 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.
Proof.
unfold Consistent, Semiconsistent; ins; desf; unfold NW; intuition.
by repeat red; intros; eapply IRR; ins; desf;
eauto using happens_before_restrict_rf.

red in ACYC; red; desf; unfold rfna in *; try (by exfalso; eauto);
by repeat red; intros; desf; ins; eapply clos_trans_mon, ACYC in H; ins; desf;
eauto using happens_before_restrict_rf; rewrite restrict_rf_unfold in *; desf; eauto.
by repeat red; ins; eapply CmoH; eauto using happens_before_restrict_rf.
by red in Csc; desf; red; intuition; repeat red; ins; eapply Chbsc;
eauto using happens_before_restrict_rf.
by red; ins; rewrite restrict_rf_unfold in * |-; desf; edestruct Cscr; vauto; desf;
eauto using happens_before_restrict_rf.
by intro a; rewrite restrict_rf_unfold at 1; ins; desf;
eauto 8 using happens_before_restrict_rf.
by red; ins; rewrite restrict_rf_unfold in * |-; unfold NW; desf; desf;
eauto 8 using happens_before_restrict_rf.
by red; ins; rewrite restrict_rf_unfold in *; ins; desf; eapply Crf in RF; desf; unfold NW;
eauto 8 using happens_before_restrict_rf.
by red; ins; rewrite restrict_rf_unfold in *; ins; desf; eapply CrfH in RF; desf; unfold NW;
eauto 8 using happens_before_restrict_rf.
by red; ins; rewrite restrict_rf_unfold in *; desf; eapply Crr;
eauto using happens_before_restrict_rf.
by red; ins; rewrite restrict_rf_unfold in *; desf; eapply Cwr;
eauto using happens_before_restrict_rf.
by red; ins; rewrite restrict_rf_unfold in *; desf; eapply Crw;
eauto using happens_before_restrict_rf.
by red; ins; rewrite restrict_rf_unfold in *; desf; eapply Crmw;
eauto using happens_before_restrict_rf.
Qed.

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.
Proof.
ins; unfold racy in *; desc; unnw; repeat (eexists; try edone);
eauto using happens_before_restrict_rf.
Qed.

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.
Proof.
rewrite !race_free_iff_not_racy; eauto using racy_restrict_rf.
Qed.

## Label monotonicity

Definition RATord x y :=
match x, y with
| RATna, RATna => true
| RATna, _ => false
| _, RATna => false
| RATrlx, _ => true
| _, RATrlx => false
| RATacq, _ => true
| _, RATacq => false
| RATsc, RATsc => true
end.

Definition WATord x y :=
match x, y with
| WATna, WATna => true
| WATna, _ => false
| _, WATna => false
| WATrlx, _ => true
| _, WATrlx => false
| WATrel, _ => true
| _, WATrel => false
| WATsc, WATsc => true
end.

Definition UATord x y :=
match x, y with
| UATrlx, _ => true
| _, UATrlx => false
| UATacq, UATrel => false
| UATacq, _ => true
| UATrel, UATacq => false
| UATrel, _ => true
| UATrel_acq, UATrel_acq => true
| UATrel_acq, UATsc => true
| UATsc, UATsc => true
| _, _ => false
end.

Definition FATord x y :=
match x, y with
| FATacq, FATrel => false
| FATacq, _ => true
| FATrel, FATacq => false
| FATrel, _ => true
| FATrel_acq, FATrel_acq => true
| FATrel_acq, FATsc => true
| FATsc, FATsc => true
| _, _ => false
end.

Definition act_ord x y :=
match x, y with
| Askip tid, Afence tid' typ => tid = tid'
| Aalloc tid l n, Aalloc tid' l' n' =>
tid = tid' /\ l = l' /\ n = n'
| Aload tid typ l v, Aload tid' typ' l' v' =>
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.
Proof. destruct x; ins; desf; ins; destruct typ; ins. Qed.

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.
Proof. tac. Qed.

Proof. tac. Qed.

Lemma act_ord_na : is_na x -> is_na y.
Proof. tac. Qed.

Lemma act_ord_na_rev : is_na y -> is_na x.
Proof. tac. Qed.

Lemma act_ord_sc : is_sc x -> is_sc y.
Proof. tac. Qed.

Lemma act_ord_rmw : is_rmw x -> is_rmw y.
Proof. tac. Qed.

Lemma act_ord_rmw_rev : is_rmw y -> is_rmw x.
Proof. tac. Qed.

Lemma act_ord_writeLV_rev l v : is_writeLV y l v -> is_writeLV x l v.
Proof. tac. Qed.

Proof. tac. Qed.

Lemma act_ord_write : is_write x -> is_write y.
Proof. tac. Qed.

Lemma act_ord_writeL l : is_writeL x l -> is_writeL y l.
Proof. tac. Qed.

Lemma act_ord_writeL_rev l : is_writeL y l -> is_writeL x l.
Proof. tac. Qed.

Lemma act_ord_writeLV l v : is_writeLV x l v -> is_writeLV y l v.
Proof. tac. Qed.

Lemma act_ord_access : is_access x -> is_access y.
Proof. tac. Qed.

Proof. tac. Qed.

Proof. tac. Qed.

Lemma act_ord_release_write : is_release_write x -> is_release_write y.
Proof. tac. Qed.

Lemma act_ord_release_fence : is_release_fence x -> is_release_fence y.
Proof. tac. Qed.

Proof. tac. Qed.

Lemma act_ord_acquire_fence : is_acquire_fence x -> is_acquire_fence y.
Proof. tac. Qed.

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 :
forall lab lab' (LO: forall a, act_ord (lab' a) (lab a))
(sb sb' : relation actid) (SBO: forall a b, sb' a b -> sb a b)
rf rf' (RFO: forall 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.
Proof.
ins.
eapply release_seq_mon_sb; eauto; clear SBO.
eapply release_seq_mon_rf; eauto; clear RFO.
unfold release_seq, release_seq_elem in *; ins.
destruct (snd mt2); unfold same_thread in *.

rewrite <- (act_ord_thread _ _ (LO a)), <- (act_ord_thread _ _ (LO b)); unfold NW;
desf; vauto; right; intuition; eauto using clos_trans_mon with act_ord_lemmas;
try by exploit RSO; eauto;
try rewrite <- (act_ord_thread _ _ (LO c));
intuition eauto using clos_trans_mon with act_ord_lemmas.

destruct mt2 as [[] ?]; induction RS; ins;
try rewrite !(fun x => act_ord_thread _ _ (LO x)) in *;
eauto using release_seq_alt with act_ord_lemmas.
Qed.

The happens-before relation is monotone.

Lemma happens_before_mon :
forall lab lab' (LO: forall a, act_ord (lab' a) (lab a))
(sb sb' : relation actid) (SBO: forall a b, sb' a b -> sb 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.
Proof.
ins; eapply (clos_trans_mon _ HB).
intuition; right; left; unfold synchronizes_with, NW, diff_thread in *; des;
try rewrite (act_ord_thread _ _ (LO a0)) in *;
try rewrite (act_ord_thread _ _ (LO b0)) in *;
[left|right;left|do 2 right;left|do 3 right]; repeat eexists;
eauto using clos_trans_mon, release_seq_mon with act_ord_lemmas.
Qed.

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 :
forall 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: forall a, act_ord (lab' a) (lab a))
(sb' : relation actid) (SBO: forall a b, sb' a b -> sb a b)
(CSb': ConsistentSB lab' sb') (DSBO: inclusion _ dsb (clos_trans _ sb')),
exists sc',
Semiconsistent mt mt2 mtsc acts lab' sb' dsb asw rf mo sc'.
Proof.
ins; exists (fun a b => sc a b /\ is_sc (lab' a) /\ is_sc (lab' b)).
unfold Semiconsistent in *; desf; unfold NW; intuition.
{ split; unfold NW; ins; desf; apply FIN; eauto.
by specialize (LO a); intro X; rewrite X in *; destruct (lab' a); ins; desf. }
by repeat red; intros; eapply IRR; ins; desf;
eauto using happens_before_mon.
red in ACYC; red; desf; unfold rfna in *; try (by exfalso; eauto);
by repeat red; intros; desf; ins; eapply clos_trans_mon, ACYC in H; ins; desf;
eauto using happens_before_mon with act_ord_lemmas.
{ red; red in Cdsb; repeat split; ins; desf.
by apply Cdsb0 in DSB; specialize (LO a); destruct (lab a), (lab' a); ins.
by apply Cdsb1 in DSB; specialize (LO b); destruct (lab b), (lab' b); ins. }
{ red in Cmo; desf; red; unfold NW; intuition.
by apply CmoD in MO; desf; eauto using act_ord_writeL_rev.
by red; ins; eapply CmoF; eauto with act_ord_lemmas. }
by repeat red; ins; eapply CmoH; eauto using happens_before_mon, act_ord_writeL.
{ red in Csc; desf; red; unfold NW; intuition; red; ins; desf; eauto.
by eapply CscF in NEQ; desf; eauto using act_ord_sc.
by split; try done; apply Chbsc; eauto using act_ord_sc, happens_before_mon.
by split; try done; apply Cmosc; eauto using act_ord_sc, happens_before_mon. }
{ destruct mtsc; ins; try (by exfalso; eauto).
red; ins; exploit Cscr; eauto using act_ord_sc; ins; desf.
case_eq (is_sc (lab' a)) as isSCa; [left|right; split; ins].
unfold sc_restr in *; red in x0; desc; split; repeat split; eauto with act_ord_lemmas.
by generalize (LO a), x2; clear; destruct (lab' a); ins; destruct (lab a); ins.
by generalize (act_ord_loc _ _ (LO a)), (act_ord_loc _ _ (LO b)); congruence.
ins; desf; exploit (x1 c); repeat split; eauto with act_ord_lemmas.
by generalize (act_ord_loc _ _ (LO a)), (act_ord_loc _ _ (LO c)); congruence.
by generalize (act_ord_loc _ _ (LO b)), (act_ord_loc _ _ (LO c)); congruence.

unfold sc_restr in SC0; desf.
destruct x0 as [A B]; red in A; desc; apply (B x); red; intuition; try rewrite A1;
eauto with act_ord_lemmas;
try by generalize (act_ord_loc _ _ (LO b)), (act_ord_loc _ _ (LO x)); congruence.
by red in Csc; desc; apply CscD in A; desc; eauto using act_ord_sc, happens_before_mon.

right; split; ins; eauto using act_ord_sc.
unfold sc_restr in *; desc; eapply (x1 x); repeat split;
eauto using happens_before_mon with act_ord_lemmas.
by generalize (act_ord_loc _ _ (LO b)), (act_ord_loc _ _ (LO x)); congruence.
}
by red; ins; eauto 10 using happens_before_mon, act_ord_writeLV_rev, act_ord_readLV_rev
with act_ord_lemmas.
by red; unfold NW; ins; eapply Crf in RF; desf;
eauto 10 using happens_before_mon, act_ord_writeLV_rev, act_ord_readLV_rev
with act_ord_lemmas.
by red; unfold NW; ins; eapply CrfH in RF; desf;
eauto 10 using happens_before_mon, act_ord_writeLV_rev, act_ord_readLV_rev
with act_ord_lemmas.
by red; ins; eapply Crr; eauto using happens_before_mon;
generalize (act_ord_loc _ _ (LO a)), (act_ord_loc _ _ (LO b)); congruence.
by red; ins; eapply Cwr; eauto using happens_before_mon;
generalize (act_ord_loc _ _ (LO a)), (act_ord_loc _ _ (LO b)); congruence.
by red; ins; eapply Crw; eauto using happens_before_mon;
generalize (act_ord_loc _ _ (LO a)), (act_ord_loc _ _ (LO b)); congruence.
by red; ins; eapply Crmw; eauto using happens_before_mon with act_ord_lemmas.
by red; ins; eapply Ca; generalize (LO a), (LO b);
rewrite ALLOCa, ALLOCb; ins; desf; desf.
Qed.

Corollary Consistent_mon :
forall 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: forall a, act_ord (lab' a) (lab a))
(sb' : relation actid) (SBO: forall a b, sb' a b -> sb a b)
(CSb': ConsistentSB lab' sb') (DSBO: inclusion _ dsb (clos_trans _ sb')),
exists rf' sc',
Consistent mt mt2 mtsc acts lab' sb' dsb asw rf' mo sc'.
Proof.
ins; red in CONS; desc.
edestruct Semiconsistent_mon with (sb' := sb'); eauto.
by unfold Semiconsistent, NW; intuition eauto.
eauto using Consistent_restrict_rf.
Qed.