Require Import Classical List Permutation Relations Peano_dec Setoid Omega.
Require Import Vbase extralib ExtraRelations cactions WMModels.
Set Implicit Arguments.
Remove Hints plus_n_O.

Lemma ConsistentMO_dom_restr_eq lab mo :
ConsistentMO_big_dom lab mo
ConsistentMO_dom lab (restr_eq_rel (fun x : actidloc (lab x)) mo).
Proof.
unfold ConsistentMO_dom, ConsistentMO_big_dom, restr_eq_rel; intuition.
exploit H; eauto; ins; desf; destruct (lab a); ins; destruct (lab b); ins; vauto.
Qed.

Lemma is_total_restr_eq X lab (mo : relation X) l :
is_total (fun ais_write (lab a)) mo
is_total (fun ais_writeL (lab a) l) (restr_eq_rel (fun xloc (lab x)) mo).
Proof.
unfold restr_eq_rel; red; ins; apply H in NEQ; eauto with caccess;
destruct (lab a); ins; destruct (lab b); ins; desf; vauto.
Qed.

## Equivalent SC definitions

We show that all the presented alternative definitions of sequential consistency are equivalent to one another.
1. The total order version is equivalent to the (po U rf U mo U rb)-acyclic version.

Theorem ModelSC_total_mo lab sb rf :
( mo, ModelSC_total lab sb rf mo)
( mo, ModelSC_mo lab sb rf mo).
Proof.
unfold ModelSC_total, ModelSC_mo; split; ins; desf; unnw.
{ (fun x y l, mo x y is_writeL (lab x) l is_writeL (lab y) l);
intuition; repeat red; ins; desf; eauto.
by eapply CscF in NEQ; desf; eauto with caccess.
by assert (l=l0) by (destruct (lab y); ins; desf); desf; eauto.
eapply (CscI x); revert H; generalize x at 1 3; unfold reads_before, union;
induction 1; desf; eauto.
eapply CscF in H1; desf; eauto with caccess.
exfalso; eapply Cwr; try exact H; eauto with caccess.
destruct (lab y); ins; destruct (lab z); ins; desf.
}
{ (tot_ext_nat (sb +++ rf_external sb rf +++ mo +++ reads_before lab rf mo));
unfold inclusion; intuition; eauto using tot_ext_nat_trans, tot_ext_nat_irr;
try solve [unfold union; eauto using tot_ext_nat_extends].
by red; ins; eapply tot_ext_nat_total; eauto.
red; ins; desf.
exploit CrfD; eauto; ins; desf.
destruct (eqP a b) as [|NEQ]; desf; [by eapply tot_ext_nat_irr in SC; eauto|].
destruct (eqP c b); desf; [by eapply tot_ext_nat_irr in SC'; eauto|].
assert (is_writeL (lab b) l).
by destruct (lab b); ins; destruct (lab a); ins; desf.
eapply CmoF in NEQ; desf; eauto with caccess.
eapply tot_ext_nat_irr with (x:=b); eauto.
eapply tot_ext_nat_trans, tot_ext_nat_extends; eauto.
by unfold union, reads_before; eauto 10 with caccess.
eapply tot_ext_nat_irr with (x:=a); eauto.
eapply tot_ext_nat_trans, tot_ext_nat_extends; eauto.
by unfold union; eauto with caccess.
}
Qed.

2. The total order version is equivalent to the paper's version.

Theorem ModelSC_total_bigmo lab sb rf :
( mo, ModelSC_total lab sb rf mo)
( mo, ModelSC_bigmo lab sb rf mo).
Proof.
split; intro X; desc.
{
(restr_rel (fun xis_write (lab x)) mo).
unfold ModelSC_bigmo, ModelSC_total, ConsistentMO_big_dom in *; desf; unnw.
assert (HBSC: inclusion (happens_before sb rf) mo).
by induction 1; unfold union in *; desf; eauto.
assert (RB: inclusion (reads_before lab rf mo) mo).
apply CscF in H1; desf; eauto with caccess.
edestruct Cwr; try exact H; eauto with caccess.
by eapply CrfD in H; desf; destruct (lab x); ins; desf;
destruct (lab z); ins; desf; destruct (lab y); ins; desf.
assert (MO: inclusion (mo;;mo) mo) by (red; unfold seq; ins; desf; eauto).
rewrite HBSC.
intuition;
eauto using restr_rel_trans, irreflexive_restr;
try solve [unfold restr_rel in *; desf].
by apply is_total_restr; red; ins; apply CscF; eauto with caccess.
all: by rewrite (inclusion_restr_rel_l (inclusion_refl _)), ?RB, ?MO.
}
{
eapply ModelSC_total_mo; eauto.
(restr_eq_rel (fun xloc (lab x)) mo).
unfold ModelSC_bigmo, ModelSC_mo in *; desf; unnw; intuition;
eauto using transitive_restr_eq, ConsistentMO_dom_restr_eq,
is_total_restr_eq;
try (by rewrite inclusion_restr_eq).
rewrite inclusion_restr_eq.
cut (acyclic (happens_before sb rf +++ mo +++ reads_before lab rf mo)).
apply inclusion_acyclic; unfold happens_before, union;
red; ins; desf; eauto 10 using t_step.
eapply min_cycle with (rel':=mo); eauto.
by unfold union; red; eauto using clos_trans.
by unfold union, irreflexive, seq in *; ins; desf; eauto.
assert (EQ: a b,
(restr_rel
(fun x¬ is_write (lab x))
(happens_before sb rf +++ mo +++ reads_before lab rf mo)) a b
happens_before sb rf a b).
by unfold restr_rel, union, reads_before; ins; desf;
exfalso; exploit CmoD; eauto; ins; desf.

repeat split.
by eapply inclusion_acyclic; eauto;
eapply trans_irr_acyclic; ins; vauto.
by unfold union, reads_before; intuition; unfold irreflexive, seq in *;
ins; desf; eauto.
ins; eapply clos_refl_trans_mon in S'; eauto.
unfold union, reads_before in R'; desf;
try (by exploit CmoD; eauto; ins; desf).
assert (happens_before sb rf b2 c1).
by eapply t_rt_trans in S'; eauto using t_step;
eapply clos_trans_of_clos_trans.
clear R' S'.
unfold union, irreflexive, seq, clos_refl in *; desf; eauto 6.
by eapply ChbI, t_trans; eauto.
by eapply Cww; repeat eexists; try eapply t_trans; eauto.
}
Qed.

3. The paper's version is equivalent to a simplified version.

Theorem ModelSC_bigmo_simplify lab sb (T: transitive sb) rf mo :
ModelSC_bigmo lab sb rf mo
ModelSC_bigmo_simpl lab sb rf mo.
Proof.
unfold ModelSC_bigmo, ModelSC_bigmo_simpl; split; ins; desf; unnw; intuition.
clear - CwrS.
by unfold irreflexive, seq, happens_before, union in *; ins; desf;
eauto 12 using clos_trans.
by unfold irreflexive, seq, happens_before, union in *; ins; desf;
eauto 8 using clos_trans.
unfold irreflexive, seq; ins; desf.
assert (M: clos_refl sb x x) by vauto.
revert M H; generalize x at 2 3.
eapply clos_trans_tn1 in H1; unfold union in ×.
induction H1;
ins; desf; unfold clos_refl, irreflexive, seq, union in *; desf; eauto 12;
try apply clos_tn1_trans in H1;
try solve [unfold rf_external, reads_before in *; desf; eauto].
destruct (eqP z0 y) as [|NEQ]; desf; ins; eauto.
eapply CmoF in NEQ; eauto.
2: by eapply CmoD in H0; desf; eauto with caccess.
2: by eapply proj1, CrfD in H; desf; eauto with caccess.
desf; unfold irreflexive, seq, clos_refl, rf_external in *; desf; eauto.
eauto 10.
Qed.

The same theorems about SC-consistency of plain executions.

Corollary ConsistentSC_total_mo pe :
Consistent ModelSC_total pe
Consistent ModelSC_mo pe.
Proof.
unfold Consistent; split; intros (rf & H); rf;
eapply ModelSC_total_mo; eauto.
Qed.

Corollary ConsistentSC_total_bigmo pe :
Consistent ModelSC_total pe
Consistent ModelSC_bigmo pe.
Proof.
unfold Consistent; split; intros (rf & H); rf;
eapply ModelSC_total_bigmo; eauto.
Qed.