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

Lemma ModelTSO_SRA :
lab sb rf mo
(C: ModelTSO lab sb rf mo),
acyclic (sb +++ rf_external sb rf +++ mo).
Proof.
ins; red in C; desc; intros x X.
eapply cycle_decomp_u_total in X; eauto; desf; eauto.
apply clos_trans_of_transitive in X0; eauto.
rewrite clos_refl_transE in X; desf; eauto.
eapply Cww; eexists; split; eauto.
Qed.

Lemma hbWW_in_mo sb rf mo
(ChbI : irreflexive (happens_before sb rf))
(Cmohb : irreflexive (mo;; happens_before sb rf))
dom (CmoF : is_total dom mo) x (Wx: dom x) y (Wy: dom y)
(HB: happens_before sb rf x y) :
mo x y.
Proof.
destruct (eqP x y) as [|NEQ]; [by desf; exfalso; eauto|].
apply CmoF in NEQ; desf; eauto.
by exfalso; unfold seq in *; eauto.
Qed.

Equivalent TSO definitions

The two presented TSO-coherence definitions are equivalent.

Theorem ModelTSO_simplify :
lab sb (T: transitive sb) rf mo,
ModelTSO lab sb rf mo
ModelTSO_simpl lab sb rf mo.
Proof.
unfold ModelTSO, ModelTSO_simpl; split; ins; desf; unnw.
{ intuition.
eapply irreflexive_inclusion, ChbI;
red; unfold seq, clos_refl; ins; desf; eauto with hb.
eapply irreflexive_inclusion, ChbI;
red; unfold seq, clos_refl; ins; desf; eauto with hb.
eapply irreflexive_inclusion, Cww;
red; unfold seq, clos_refl; ins; desf; eauto 8 with hb.
eapply irreflexive_inclusion, Cww;
red; unfold seq, clos_refl; ins; desf; eauto 8 with hb.
eapply irreflexive_inclusion, Cwr;
red; unfold seq, clos_refl; ins; desf; eauto 8 with hb.
}

assert (L: a b (HB: happens_before sb rf a b),
(clos_refl sb ;; clos_refl mo ;;
rf_external sb rf ;; clos_refl sb) a b sb a b).
{
unfold happens_before, union, seq; ins.
apply clos_trans_tn1 in HB; induction HB; desf; eauto 10.

left; repeat (eexists; try edone).
by clear - H IHHB2 T; unfold clos_refl in *; desf; eauto.

left; eexists; split; try edone; y; repeat (eexists; try edone); vauto.
destruct (eqP z0 y) as [|NEQ]; desf; vauto.
apply CmoF in NEQ; desf; eauto.
assert (mo y z1) by (unfold clos_refl in IHHB0; desf; eauto).
clear IHHB IHHB0; exfalso; unfold clos_refl, seq in *;
desf; [eapply Cat'|eapply Cww]; eauto 8.
red in IHHB0; desf.
by apply proj1, CrfD in IHHB1; desc; eauto with caccess.
by apply CmoD in IHHB0; desc; eauto with caccess.
by apply proj1, CrfD in H; desc; eauto with caccess.
}

assert ( a (W: is_write (lab a)) b (HB: happens_before sb rf a b),
(clos_refl mo ;; rf_external sb rf ;; clos_refl sb) a b sb a b).
{
unfold happens_before, union, seq; ins.
apply clos_trans_tn1 in HB; induction HB; desf; eauto 10.

left; repeat (eexists; try edone).
by clear - H IHHB1 T; unfold clos_refl in *; desf; eauto.

left; y; repeat (eexists; try edone); vauto.
destruct (eqP a y) as [|NEQ]; desf; vauto.
apply CmoF in NEQ; desf; eauto.
assert (mo y z0) by (unfold clos_refl in IHHB; desf; eauto).
clear IHHB; exfalso; unfold clos_refl, seq in *;
desf; [eapply Cat'|eapply Cww]; eauto 8.
by apply proj1, CrfD in H; desc; eauto with caccess.

left; y; repeat (eexists; try edone); vauto.
destruct (eqP a y) as [|NEQ]; desf; vauto.
apply CmoF in NEQ; desf; eauto.
exfalso; unfold clos_refl, seq in *; eapply Cww; eauto 8.
by apply proj1, CrfD in H; desc; eauto with caccess.
}

intuition.
× intros ? X; apply L in X; unfold seq in *; ins; desf; eauto 6.
assert (M: clos_refl sb z1 z); [revert X X2|clear X X2].
by unfold clos_refl; ins; desf; eauto.
unfold clos_refl in X0; desf; eauto.
by unfold clos_refl in M; desf; eauto 7 using r_step, r_refl.
by unfold clos_refl in M; desf; eauto 7 using r_step, r_refl.

× unfold seq in *; intros x X; desc; eapply H in X0; desf; eauto 7 using r_step.
assert (mo x z0) by (unfold clos_refl in X0; desf; eauto); clear X0.
by unfold clos_refl in X2; desf; eauto 7 using r_step.
by eapply CmoD in X; desf; eauto.

× unfold seq in *; intros x X; desc; eapply H in X0; desf; eauto 7 using r_step.
unfold clos_refl in X0; desf; eauto 7;
unfold clos_refl in X2; desf; eauto 7 using r_step.
by unfold rf_external, reads_before in *; desf; eauto.
by unfold rf_external, reads_before in *; desf; eauto.
by eapply CwrE; eauto 8.
by unfold reads_before in *; desf; eauto with caccess.
Qed.

Reducing TSO to SC

Given a TSO-coherent execution, it is also SC-coherent if an additional irreflexivity condition holds.

Definition sb_minus (sb : relation actid) rf mo x y :=
immediate sb x y ¬ mo x y c (MO: mo x c) (RF: rf y = Some c), False.

Lemma sb_minusI acts
sb (sbT: transitive sb) (sbI : irreflexive sb)
(sbD: a b, sb a b In b acts)
rf mo (IRR: irreflexive mo) x y
(X: clos_trans (immediate (clos_trans (sb +++ rf_external sb rf +++ mo))) x y) :
clos_trans (sb_minus sb rf mo +++ rf_external sb rf +++ mo) x y.
Proof.
induction X; desf; eauto using clos_trans.
eapply immediate_clos_trans_elim in H; desf.
unfold union, sb_minus, immediate in *; desf; eauto using clos_trans.
destruct (classic (mo x y)); eauto using clos_trans.
destruct (classic ((mo ;; (fun x yrf y = Some x)) x y));
unfold seq, rf_external in *; desf; eauto 15 using clos_trans.
apply t_step; left; left; intuition; eauto 10 using clos_trans.
Qed.

Lemma ModelTSO_to_SC :
acts lab sb (FIN: ExecutionFinite acts lab sb) (T: transitive sb) rf mo
(C: ModelTSO lab sb rf mo),
ModelSC_bigmo_simpl lab sb rf mo
irreflexive (reads_before lab rf mo ;; mo ;;
eqv_rel (fun xis_write_only (lab x)) ;;
sb_minus sb rf mo ;; eqv_rel (fun x¬ is_write (lab x)) ;;
clos_refl sb).
Proof.
ins.
assert (ACYC := ModelTSO_SRA C).
unfold ModelTSO, ModelSC_bigmo_simpl in *; split; ins; desf; unnw;
intuition; eauto.
eapply irreflexive_inclusion, CwrI.
eapply inclusion_seq_mon; try done.
eapply inclusion_seq_mon; try done.
by clear - T; unfold inclusion, seq, sb_minus, immediate, eqv_rel, clos_refl;
ins; desf; eauto.

unfold seq; intros x (y & X & z & Y & Z).
assert (Z': clos_trans (sb +++ rf_external sb rf +++ mo) z x).
by apply t_step; vauto.
eapply clos_trans_immediate2 with (dom:=acts) in Z'; vauto; cycle 1.
{ clear - CmoD CrfD FIN.
intros ? ? M; apply t_rt_step in M; unfold union, rf_external in *; desf.
by apply FIN in M0; desf.
by eapply finiteRF in M0; desf; eauto.
by eapply finiteMO2 in M0; desf; eauto.
}
eapply sb_minusI with (acts := acts) in Z'; eauto.
2: by red; eauto using sb_in_hb.
2: by intros ? ? M; apply FIN in M; desf.

assert (K: (mo ;; clos_refl (rf_external sb rf) ;; clos_refl_trans (sb_minus sb rf mo)) y x).
clear X Z.
rewrite unionA in Z'.
eapply path_ur with (adom := fun xis_write (lab x))
(bdom := fun xTrue) in Z'; ins; eauto.
destruct Z' as [Z'|Z']; desc.
by unfold clos_refl, seq; eauto 8 using clos_trans_in_rt.
cut ((mo;; clos_refl (rf_external sb rf)) y z0).
cut (clos_refl_trans (sb_minus sb rf mo) z0 x).
by clear; unfold seq; ins; desf; eauto 10 using rt_trans.
by rewrite clos_refl_transE; desf; eauto.
clear Z'0.
apply clos_trans_tn1 in Z'.
induction Z'.
unfold seq, union, clos_refl in H0 |- *; desf; eauto.
rename z into x0.
cut (mo x0 y0); eauto.
eapply hbWW_in_mo; eauto; ins.
by apply CmoD in Y; desf.
by clear - H0; unfold sb_minus, immediate in H0;
induction H0; desc; eauto with hb.

clear Z'.
unfold seq, union in H0, IHZ' |- *; desf; eauto.
{
cut (mo z1 z0); eauto 8.
eapply hbWW_in_mo; eauto; ins.
by apply CmoD in IHZ'; desf.
apply rt_t_trans with y0; unfold union.
by unfold clos_refl in *; desf; eauto using clos_refl_trans.
by unfold sb_minus, immediate in *; eapply clos_trans_mon; eauto;
ins; desf; eauto.
}
{
unfold clos_refl in *; desf; eauto.
cut (mo z1 y0); eauto 8.
eapply hbWW_in_mo; eauto with hb; ins.
by apply CmoD in IHZ'; desf.
by apply proj1, CrfD in H0; desf; eauto with caccess.
}
{
unfold clos_refl in *; desf; eauto.
cut (mo z1 y0); eauto 8.
eapply hbWW_in_mo; eauto with hb; ins.
by apply CmoD in IHZ'; desf.
by apply CmoD in H0; desf.
}
unfold union, rf_external in R; desf;
[apply CrfD in R|apply CmoD in R]; desf; eauto with caccess.

clear Z' Y Z.
unfold clos_refl, seq in *; desf; cycle 1.
{ rewrite clos_refl_transE in *; desf.
- eapply (Cwr x); eexists z0; split;
unfold reads_before, rf_external in *; desf; eauto with hb.
repeat eexists; eauto.
by apply CrfD in K0; desf; destruct (lab x); ins; desf; eauto with caccess.
- eapply CwrE; repeat (eexists; try edone).
by clear -K1 T; unfold sb_minus, immediate in *;
induction K1; desf; eauto.
}
rewrite clos_refl_transE in *; desf; eauto.
{ eapply H; do 2 (eexists; split; try edone).
destruct (is_rmw (lab z1)) eqn: RMW.
exfalso; eapply CwrU; repeat (eexists; try edone).
by clear -K1 T; unfold sb_minus, immediate in *;
induction K1; desf; eauto.
assert (is_write (lab z1)) by (apply CmoD in K; desf).
eexists; split; [by split; try done; destruct (lab z1)|].
eapply t_step_rt in K1; desc.
eexists; split; eauto.
cut (¬ is_write (lab z0)).
eexists; split; try done.
rewrite clos_refl_transE in *; desf; eauto.
by right; clear -K0 T; unfold sb_minus, immediate in *;
induction K0; desf; eauto.
intro; unfold sb_minus, immediate in *; desc.
destruct (eqP z0 z1) as [|NEQ]; desf; eauto with hb.
by eapply CmoF in NEQ; desf; eauto with hb.
}
Qed.

Soundness and completeness of write-read reordering

Lemma rf_external_reorder lab sb rf a b
(Crf: ConsistentRF_dom lab rf)
(LOC: loc (lab a) loc (lab b)) :
rf_external (reorder sb b a) rf <--> rf_external sb rf.
Proof.
unfold rf_external, reorder; split; red; ins; intuition; desf; eauto.
apply H3; intro; desf; eapply LOC; eapply loceq_rf; eauto.
by eapply loceq_rf in H0; eauto.
Qed.

Lemma irreflexive_reorder A (r r' : relation A) a b :
irreflexive (r ;; r')
¬ r a b
irreflexive (r ;; reorder r' a b).
Proof.
unfold irreflexive, seq, reorder; ins; desf; eauto.
Qed.

Lemma irreflexive_reorder2 A (r r' : relation A) a b :
irreflexive (r ;; reorder r' a b)
¬ r b a
irreflexive (r ;; r').
Proof.
unfold irreflexive, seq, reorder; ins; desf; eauto.
eapply (H x); z; split; ins; left; split; ins.
intro; desf.
Qed.

Theorem reorderWR_sound_TSO :
lab sb rf mo a b
(C: ModelTSO_simpl lab (reorder sb a b) rf mo)
(Wa: is_write_only (lab a))
(LOC: loc (lab a) loc (lab b))
(Esb1: x, sb a x x = b sb b x)
(Esb2: x, sb x b x = a sb x a),
ModelTSO_simpl lab sb rf mo.
Proof.
ins; unfold ModelTSO_simpl in *; desf; unnw.
revert CrfI ChbI Cat' Cww Cwr Cat CwrE CwrU.
rewrite rf_external_reorder; eauto.
intros CrfI ChbI Cat' Cww Cwr Cat CwrE CwrU.
intuition.
all: rewrite <- ?seqA; try eapply irreflexive_reorder2; rewrite ?seqA; try edone;
unfold seq, immediate in *; intro M; desf; eauto.

× clear - CrfD M LOC.
unfold clos_refl in *; desf; eauto; apply proj1, CrfD in M; desc.
by destruct (lab b); ins; desf; destruct (lab a); ins; desf; eauto.

× by clear -M CmoD Rb; apply CmoD in M; desc; destruct (lab b).

× clear - CmoD CrfD M M0 Wa Rb LOC.
unfold reads_before, clos_refl, rf_external in *; desf; eauto.
by destruct (lab b); ins; desf; destruct (lab a); ins; desf.
by eapply CrfD in M0; desf; destruct (lab a).

× by apply proj1, CrfD in M0; desc; destruct (lab a).

× by unfold eqv_rel in *; desf; destruct (lab a).
Qed.

Reordering an adjacent write-read pair is complete under TSO provided there is no mo ;; rf_external from the store to the load.

Theorem reorderWR_complete_TSO :
lab sb rf mo a b
(C: ModelTSO_simpl lab sb rf mo)
(Wa: is_write_only (lab a))
(LOC: loc (lab a) loc (lab b))
(Esb1: x, sb a x x = b sb b x)
(Esb2: x, sb x b x = a sb x a)
(COND: ¬ (mo ;; rf_external sb rf) a b),
ModelTSO_simpl lab (reorder sb a b) rf mo.
Proof.
ins; unfold ModelTSO_simpl in *; desf; unnw.
rewrite rf_external_reorder; eauto.
intuition.
all: rewrite <- ?seqA; try eapply irreflexive_reorder; rewrite ?seqA; try edone;
unfold seq, immediate in *; intro M; desf; eauto.

× clear - CrfD M LOC.
unfold clos_refl in *; desf; eauto; apply proj1, CrfD in M; desc.
by destruct (lab b); ins; desf; destruct (lab a); ins; desf; eauto.

× unfold clos_refl, seq in *; desf; eauto.
by apply CmoD in M; desc; destruct (lab b).

× clear - CmoD CrfD M M0 Wa Rb LOC.
unfold reads_before, clos_refl, rf_external in *; desf; eauto.
by destruct (lab b); ins; desf; destruct (lab a); ins; desf.
by eapply CrfD in M0; desf; destruct (lab a).

× by unfold reads_before in *; desf; destruct (lab a); ins.

× by unfold eqv_rel in *; desf; destruct (lab b).
Qed.

Soundness and completeness of read-after-write elimination

Lemma rf_external_elimRaW lab (sb' sb : relation actid) rf' a b
(Crf: ConsistentRF_dom lab rf')
(Esb2: x, sb x b x = a sb x a)
(EQsb: sb' <--> restr_rel (fun xx b) sb) :
rf_external sb (fun xif x == b then Some a else rf' x) <-->
rf_external sb' rf'.
Proof.
assert (RF: rf' b = None).
specialize (Crf b); destruct (rf' b); ins.
by specialize (Crf _ eq_refl); rewrite LAB in *; desf.
rewrite EQsb.
unfold rf_external, restr_rel in *; split; red; ins; desf; desf;
rewrite ?Esb2 in *; try solve [exfalso; eauto]; split; ins; intro; desf.
destruct H0; intuition; desf.
by apply Crf in H; rewrite LAB in *; desf.
Qed.

Lemma reads_before_elimRaW lab' mo' rf' a b l v
(CrfD: ConsistentRF_dom lab' rf')
(CmoD: ConsistentMO_big_dom lab' mo')
(WRI: is_writeLV (lab' a) l v)
(LAB: lab' b = Askip) :
(fun xif x == b then Aload l v else lab' x)
(fun xif x == b then Some a else rf' x) mo' <-->
reads_before lab' rf' mo' +++ (fun x yx=b mo' a y l = loc (lab' y)).
Proof.
unfold reads_before, union; split; red; ins; desf; ins; desf; eauto 10.
by right; intuition; destruct (lab' y); ins.
by eapply CrfD in H; rewrite LAB in *; desf.
by eapply CmoD in H0; rewrite LAB in *; desf.
by eapply CmoD in H0; rewrite LAB in *; desf.
by repeat eexists; eauto; apply CmoD in H0; desf; destruct (lab' y); ins; desf.
Qed.

Eliminating a redundant load after an adjacent previous store is sound under TSO.

Lemma elimRaW_sound_TSO :
lab' sb' rf' mo'
(C: ModelTSO_simpl lab' sb' rf' mo')
a l v (Wa: is_writeLV (lab' a) l v)
b
(sb : relation actid)
(Esb1: x, sb a x x = b sb b x)
(Esb2: x, sb x b x = a sb x a)
(T: transitive sb)
(IRR: irreflexive sb)
(EQsb: sb' <--> restr_rel (fun xx b) sb) lab
(LAB: lab = fun xif x == b then Aload l v else lab' x),
ModelTSO_simpl lab sb
(fun xif x == b then Some a else rf' x) mo'.
Proof.
ins; unfold ModelTSO_simpl in *; desf; unnw; desf.
assert (NEQ: a b) by (intro; desf; rewrite SKIP in *; done).
assert (EQsb': x y, sb x y
sb' x y
clos_refl sb' x a y = b
x = b sb' a y).
assert (SBab : sb a b) by (rewrite Esb1; eauto).
unfold clos_refl, restr_rel in *; ins; rewrite !(same_relation_exp EQsb).
repeat split; ins; desf; eauto; try rewrite Esb2; eauto.
destruct (eqP y b); desf; eauto;
rewrite ?Esb2 in H; desf; eauto 6;
destruct (eqP x b); desf; try solve [edestruct IRR; eauto]; eauto 8.
by rewrite Esb1 in *; desf.

repeat apply conj; unnw; ins; desf; desf; rewrite ?P; vauto.
by red; ins; unnw; desf; desf; ins; eauto; apply CrfD in RF; desf; rewrite SKIP in ×.
by red; ins; desf; desf; eauto.
by red; ins; desf; desf; eauto; eapply CmoD in MO; try rewrite SKIP in *; desf.
by red; ins; desf; desf; eauto.

all: rewrite ?rf_external_elimRaW; eauto.

all: unfold union, seq, eqv_rel in *; red; ins; desf; try rewrite EQsb' in *; desf; eauto;
repeat first [
match goal with
| EQsb : ?sb' <--> restr_rel _ _, H: ?sb' _ _ |- _
by apply EQsb, proj2 in H; desf
| CmoD : ConsistentMO_big_dom _ ?mo, H: ?mo _ _ |- _
by apply CmoD in H; rewrite SKIP in *; ins; desf
| H: rf_external _ _ _ _ |- _
by apply proj1, CrfD in H; rewrite SKIP in *; ins; desf
end |
by unfold reads_before in *; rewrite SKIP in *; desf |
by eauto |
by eapply Cww; eauto 8 |
by eapply Cwr; eauto 8 |
by eapply CwrE; eauto 8 |
by eapply CwrU; eauto 8 |
unfold clos_refl in *; desf].
Qed.

Eliminating a redundant load after an adjacent previous store is also complete under TSO.

Lemma elimRaW_complete_TSO :
lab' sb' rf' mo'
a l v (Wa: is_writeLV (lab' a) l v)
b
(sb : relation actid)
(Esb2: x, sb x b x = a sb x a)
(EQsb: sb' <--> restr_rel (fun xx b) sb)
(RFb : rf' b = None) lab rf
(EQlab : lab = fun xif x == b then Aload l v else lab' x)
(EQrf : rf = fun xif x == b then Some a else rf' x)
(C: ModelTSO_simpl lab sb rf mo'),
ModelTSO_simpl lab' sb' rf' mo'.
Proof.
ins; unfold ModelTSO_simpl in C; desf.
assert (CrfD': ConsistentRF_dom lab' rf').
red; ins.
generalize (CrfD a0) as XX; ins; desf; desf; unnw; eauto.
by eapply XX in RF; desf; ins; desf; eauto.
assert (CmoD': ConsistentMO_big_dom lab' mo').
by red; ins; eapply CmoD in MO; desf; desf.

revert CrfI ChbI Cat' Cww Cwr Cat CwrE CwrU.
rewrite rf_external_elimRaW; eauto.
intros CrfI ChbI Cat' Cww Cwr Cat CwrE CwrU.

assert (KK: inclusion sb' sb).
rewrite EQsb; apply inclusion_restr_rel_l; reflexivity.
assert (LL: inclusion (reads_before lab' rf' mo')
(fun x y : actidx = b mo' a y l = loc (lab' y)))).
by vauto.

unfold ModelTSO_simpl; ins; unnw.
intuition; eauto.

by red; ins; eapply (COrf a0); desf; desf; rewrite SKIP in *; ins.
by red; ins; apply CmoF; desf; ins; desf; rewrite SKIP in *; ins.

all: try solve [try rewrite LL; try rewrite KK at 2; eauto].
rewrite EQsb; eapply irreflexive_inclusion, CwrU; clear - SKIP.
unfold eqv_rel, seq, union, restr_rel; red; ins; desf.
repeat (eexists; try edone); desf; ins; desf; eauto.
Qed.

Equivalent TSO definition in terms of transformations

The allowed transformations on plain executions under TSO are:

Inductive TSO_transform (pe pe' : plain_exec) : Prop :=
| TSO_transform_reorderWR ll1 l1 l2 ll2 a b
(Wa: is_write_only (pe.(pe_lab) a))
(LOC: loc (pe.(pe_lab) a) loc (pe.(pe_lab) b))
(EQinit : pe_inits pe' = pe_inits pe)
(EQlab : pe_lab pe' = pe_lab pe)
(EQ : pe.(pe_threads) = ll1 ++ (l1 ++ a :: b :: l2) :: ll2)
(EQ : pe'.(pe_threads) = ll1 ++ (l1 ++ b :: a :: l2) :: ll2)
| TSO_transform_elimRaW ll1 l1 l2 ll2 a b l v
(Wa: pe.(pe_lab) a = Astore l v)
(Rb: pe.(pe_lab) b = Aload l v)
(EQinit : pe'.(pe_inits) = pe.(pe_inits))
(EQ : pe.(pe_threads) = ll1 ++ (l1 ++ a :: b :: l2) :: ll2)
(EQ': pe'.(pe_threads) = ll1 ++ (l1 ++ a :: l2) :: ll2)
(LAB': x, x b pe'.(pe_lab) x = pe.(pe_lab) x).

These transformations preserve wellformedness.

Lemma TSO_transform_wf pe pe' :
TSO_transform pe pe'
pe_wellformed pe
pe_wellformed pe'.
Proof.
unfold pe_wellformed; destruct pe, pe', 1; ins; desf; unnw; intuition.
eauto using Permutation_nodup, Permutation_in, Permutation_reord.
eapply Permutation_in, RNG; eauto using Permutation_reord.
eapply MAIN, Permutation_in, H; eauto using Permutation_reord.
by specialize (@Permutation_reord nat nil); ins.

revert TP; rewrite !concat_app, !concat_cons, <- !app_assoc; simpl.
rewrite <- !Permutation_middle, perm_swap, nodup_cons; tauto.

assert (a0 b) by (intro; desf).
rewrite LAB' in H; try congruence;
generalize (RNG _ H); rewrite !concat_app, !concat_cons, !in_app_iff;
ins; desf; eauto 6.
rewrite LAB'.
eapply MAIN; revert H; rewrite !concat_app, !concat_cons, !in_app_iff;
ins; desf; eauto 6.
intro; desf.
generalize (nodup_append_right _ _ TP), H; clear.
rewrite !concat_app, !concat_cons, <- !app_assoc; simpl.
rewrite <- !Permutation_middle, perm_swap, nodup_cons; tauto.
Qed.

The transformations decrease the following metric.

Fixpoint metric A lab n (l : list A) :=
match l with
| nil ⇒ 0
| x :: l
n + metric lab (S n) l
else metric lab (S n) l
end.

Lemma TSO_transform_metric pe pe' :
TSO_transform pe pe'
n,
< metric pe.(pe_lab) n (concat pe.(pe_threads)).
Proof.
destruct pe, pe', 1; ins; desf.
rewrite !concat_app, !concat_cons, <- !app_assoc in *; ins.
rewrite !app_assoc; generalize (concat ll1 ++ l1) as m.
intro; revert n; induction m; ins; desf;
try by unfold is_write_only in *; desf.
specialize (IHm (S n)); omega.
rewrite !concat_app, !concat_cons, <- !app_assoc in *; ins.
rewrite !app_assoc; generalize (concat ll1 ++ l1) as m.
intro.
apply Nat.le_lt_trans with (metric pe_lab n (m ++ a :: l2 ++ concat ll2)).
revert n; generalize (m ++ a :: l2 ++ concat ll2) as k;
induction k; ins; desf; try specialize (IHk (S n)); try omega.
destruct (eqP a0 b); desf; try rewrite SKIP in *; ins.
rewrite LAB' in Heq; ins; congruence.
assert (X: l n, metric pe_lab n l metric pe_lab (S n) l).
by clear; induction l; ins; desf; specialize (IHl (S n)); omega.
revert n; induction m; ins; desf; try specialize (IHm (S n));
specialize (X (l2 ++ concat ll2) (S n)); rewrite ?Rb in *; ins; omega.
Qed.

Lemma mk_po_elim init ll1 l1 a b l2 ll2 :
NoDup (init ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2))
mk_po init (ll1 ++ (l1 ++ a :: l2) :: ll2) <-->
restr_rel (fun x : actidx b)
(mk_po init (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)).
Proof.
ins; split; unfold restr_rel; red; ins; desf.
split.
replace (l1 ++ a :: b :: l2) with ((l1 ++ a :: nil) ++ b :: l2)
by (rewrite <- app_assoc; done).
by eapply mk_po_insert; rewrite <- app_assoc.
by split; intro; desf; [eapply mk_po_in1 in H0|eapply mk_po_in2_weak in H0];
rewrite concat_app, concat_cons, <- app_assoc in *; ins;
rewrite <- !Permutation_middle, perm_swap in *; inv H.
replace (l1 ++ a :: l2) with ((l1 ++ a :: nil) ++ l2)
by (rewrite <- app_assoc; done).
eby eapply mk_po_remove; try rewrite <- app_assoc.
Qed.

We show that the transformations are sound with respect to the TSO memory model.

Lemma TSO_transform_sound :
pe pe'
(T: TSO_transform pe pe')
(WF: pe_wellformed pe)
(C: Consistent ModelTSO pe'),
Consistent ModelTSO pe.
Proof.
destruct pe as [i ll lab], pe' as [i' ll' lab'], 1; ins;
unfold Consistent, pe_wellformed in *; ins; desf.
{
assert (P: Permutation (i ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2))
(i ++ concat (ll1 ++ (l1 ++ b :: a :: l2) :: ll2))).
by clear; rewrite !concat_app, !concat_cons, <- !app_assoc; ins;
eauto using Permutation_app, perm_swap.
rewrite ModelTSO_simplify in *; eauto using Permutation_nodup, transitive_mk_po.
rewrite <- mk_po_reorder in C; eauto using Permutation_nodup.
exploit mk_po_immediate; eauto; intro X.
eapply mk_po_helper in X; eauto; desc.
2: by intro; eapply nodup_app; eauto 8 using in_concat, in_or_app, in_eq.
do 2 eexists; rewrite ModelTSO_simplify; eauto using transitive_mk_po.
eapply reorderWR_sound_TSO; eauto.
}
{
assert (NEQ: a b) by congruence.
assert (P: Permutation (i ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2))
(b :: i ++ concat (ll1 ++ (l1 ++ a :: l2) :: ll2))).
by clear; rewrite !concat_app, !concat_cons, <- !app_assoc;
simpl; rewrite <- !Permutation_middle; apply perm_swap.
rewrite ModelTSO_simplify in *;
eauto using Permutation_nodup, nodup_consD, transitive_mk_po.
exploit mk_po_immediate; eauto; intro X.
eapply mk_po_helper in X; eauto; desc.
2: by intro; eapply nodup_app; eauto 8 using in_concat, in_or_app, in_eq.
eapply elimRaW_sound_TSO with (lab:=lab) (a:=a) (b:=b) in C;
eauto using mk_po_elim, transitive_mk_po.
by do 2 eexists; eapply ModelTSO_simplify; eauto using transitive_mk_po.
by rewrite LAB', Wa.
by red; ins; eapply mk_po_irreflexive; eauto.
by exten; ins; desf; desf; rewrite LAB'.
}
Qed.

We show that in any TSO-coherent execution that is not SC-incoherent, it is possible to apply a transformation that preserves TSO-coherence.

Lemma TSO_transform_possible :
linit ll lab rf mo
(TSO: ModelTSO lab (mk_po linit ll) rf mo)
(WF: pe_wellformed (PlainExec linit ll lab))
(NSC: ¬ ModelSC_bigmo_simpl lab (mk_po linit ll) rf mo),
ll' lab' rf' mo',
TSO_transform (PlainExec linit ll lab) (PlainExec linit ll' lab')
ModelTSO_simpl lab' (mk_po linit ll') rf' mo'.
Proof.
ins.
red in WF; ins; desc.
assert (FIN: ExecutionFinite (linit ++ concat ll) lab (mk_po linit ll)).
by red; unnw; intuition; eauto using mk_po_in1, mk_po_in2_weak.
rewrite ModelTSO_to_SC in NSC; ins; eauto using transitive_mk_po.
eapply not_all_ex_not in NSC; desc.
apply imply_to_and, proj1 in NSC.
unfold seq, eqv_rel, sb_minus in *; desf.
rename z1 into a, z3 into b.
assert (INa: In a (linit ++ concat ll)).
by apply proj1, mk_po_in1 in NSC2.
rewrite in_app_iff in *; desf.
{ exfalso.
assert (Y: In n (concat ll)).
by red in NSC4, NSC2; desf; eauto using mk_po_in2.
red in TSO; desc.
assert (In z (linit ++ concat ll)).
by apply FIN; eapply CmoD in NSC0; intro M; rewrite M in *; desf.
rewrite in_app_iff in *; desf.
by eapply Cwr; eexists; split; eauto; eapply sb_in_hb; vauto.
by eapply Cww; eexists; split; eauto; eapply sb_in_hb; vauto.
}
assert (Rb: is_read_only (lab b)); [|clear NSC5].
by apply proj1, mk_po_in2, MAIN in NSC2; destruct (lab b).

assert (IMM := NSC2); eapply mk_po_immediateD in NSC2; desf.
2: by intro; eapply nodup_app; eauto.
rewrite ModelTSO_simplify in *; eauto using transitive_mk_po.

exploit mk_po_immediate; eauto; intro X.
eapply mk_po_helper in X; eauto; desc.
2: by intro; eapply nodup_app; eauto.

destruct (eqP (loc (lab a)) (loc (lab b))).
destruct (lab b) eqn: Lb; ins; desf.
generalize TSO; intro M; red in M; desc.
unfold immediate in *; desc.
assert (RFab: rf b = Some a).
{ destruct (rf b) eqn: RF.
2: by eapply COrf in RF; try rewrite Lb in ×.
f_equal; apply NNPP; intro NEQ; apply CmoF in NEQ; desf; eauto.
eapply Cwr; repeat eexists; eauto with hb caccess; try intro;
desf; try rewrite Lb in *; ins.
by destruct (lab a); ins.
eapply CrfD in RF; desc; eauto with caccess.
by destruct (lab a); ins.
}

assert (ZZZ := RFab); apply CrfD in ZZZ; desf; rewrite Lb in *; ins; desf.

{
assert (NEQ: a b) by (intro; desf; rewrite Lb in *; done).

do 5 eexists;
[eapply TSO_transform_elimRaW
with (pe' := PlainExec _ _ (fun xif x == b then Askip else lab x))
(a:=a) (b:=b) |
eapply elimRaW_complete_TSO
with (rf' := fun xif x == b then None else rf x)
(lab' := fun xif x == b then Askip else lab x)
(a:=a) (b:=b); try eexact TSO]; eauto; try reflexivity;
ins; desf; desf; eauto using mk_po_elim.

by destruct (lab a); ins; desf.
by exten; intro; desf; desf; eauto.
by exten; intro; desf; desf; eauto.
}

do 5 eexists;
[eapply TSO_transform_reorderWR; simpl; try edone|].
rewrite <- mk_po_reorder; eauto using Permutation_nodup, Permutation_reord.
eapply reorderWR_complete_TSO; eauto using Permutation_nodup.
by unfold seq, rf_external; intro; desf; eauto.
Qed.

Our main theorem: TSO is equivalent to this set of transformations over SC.

Theorem TSO_alternative :
pe (WF: pe_wellformed pe),
Consistent ModelTSO pe

pe',
clos_refl_trans TSO_transform pe pe'
Consistent ModelSC_bigmo pe'.
Proof.
split.
ins; red in H; desc; revert rf mo H WF.
induction pe using
(well_founded_ind (well_founded_ltof _
(fun pmetric p.(pe_lab) 0 (concat p.(pe_threads))))).
ins; desf; unfold ltof in *; ins.
destruct pe as [init ll lab]; ins; desf.
destruct (classic (ModelSC_bigmo_simpl lab
(mk_po init ll) rf mo)) as [Y|N].
unfold Consistent, pe_wellformed in *; simpls; desc.
by apply ModelSC_bigmo_simplify in Y;
eauto using clos_refl_trans, transitive_mk_po.
eapply TSO_transform_possible in N; desf.
exploit TSO_transform_wf; eauto; ins.
rewrite <- ModelTSO_simplify in ×.
eapply (H (PlainExec _ _ _)) in N0; ins; desf; eauto using clos_refl_trans.
by eapply TSO_transform_metric in N; eauto.
by unfold pe_wellformed in *; desc; eauto using transitive_mk_po.

intros (pe' & R & A).
assert (WF' : pe_wellformed pe').
by clear - R WF; induction R; eauto using TSO_transform_wf.
assert (C: Consistent ModelTSO pe').
{
unfold Consistent, pe_wellformed in *; ins; desf.
rewrite ModelSC_bigmo_simplify in *; eauto using transitive_mk_po.
eexists rf, mo; unfold ModelTSO, ModelSC_bigmo_simpl in *; desc; unnw; intuition.
clear -CwrI; unfold irreflexive, seq, eqv_rel in *; desf;
by ins; desf; eauto 8.
}
clear A; eapply clos_rt_rtn1 in R; induction R; eauto using TSO_transform_wf.
cut (pe_wellformed y); eauto using TSO_transform_sound.
clear - R WF; apply clos_rtn1_rt in R; induction R; eauto using TSO_transform_wf.
Qed.