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.

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.

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 y ⇒ rf 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 x ⇒ is_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 x ⇒ is_write (lab x))
                        (bdom := fun x ⇒ True) 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.

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))
         (Rb: is_read_only (lab b))
         (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.

Theorem reorderWR_complete_TSO :
  ∀ lab sb rf mo a b
         (C: ModelTSO_simpl lab sb rf mo)
         (Wa: is_write_only (lab a))
         (Rb: is_read_only (lab b))
         (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.

Lemma rf_external_elimRaW lab (sb' sb : relation actid) rf' a b
      (Crf: ConsistentRF_dom lab rf')
      (LAB: lab b = Askip)
      (Esb2: ∀ x, sb x b ↔ x = a ∨ sb x a)
      (EQsb: sb' <--> restr_rel (fun x ⇒ x ≠ b) sb) :
  rf_external sb (fun x ⇒ if 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) :
  reads_before
    (fun x ⇒ if x == b then Aload l v else lab' x)
    (fun x ⇒ if x == b then Some a else rf' x) mo' <-->
  reads_before lab' rf' mo' +++ (fun x y ⇒ x=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.

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)
     (SKIP: lab' b = Askip)
     (T: transitive sb)
     (IRR: irreflexive sb)
     (EQsb: sb' <--> restr_rel (fun x ⇒ x ≠ b) sb) lab
     (LAB: lab = fun x ⇒ if x == b then Aload l v else lab' x),
     ModelTSO_simpl lab sb
       (fun x ⇒ if 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: rewrite ?reads_before_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.

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 x ⇒ x ≠ b) sb)
     (SKIP: lab' b = Askip)
     (RFb : rf' b = None) lab rf
     (EQlab : lab = fun x ⇒ if x == b then Aload l v else lab' x)
     (EQrf : rf = fun x ⇒ if 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.
  rewrite reads_before_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')
                    (reads_before lab' rf' mo' +++
                     (fun x y : actid ⇒ x = 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.

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))
      (Rb: is_read_only (pe.(pe_lab) b))
      (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)
      (SKIP: pe'.(pe_lab) b = Askip)
      (LAB': ∀ x, x ≠ b → pe'.(pe_lab) x = pe.(pe_lab) x).

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.

Fixpoint metric A lab n (l : list A) :=
  match l with
    | nil ⇒ 0
    | x :: l ⇒
      if is_read_only (lab x) then
        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))
    < 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 : actid ⇒ x ≠ 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.

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.

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 x ⇒ if x == b then Askip else lab x))
          (a:=a) (b:=b) |
   eapply elimRaW_complete_TSO
   with (rf' := fun x ⇒ if x == b then None else rf x)
        (lab' := fun x ⇒ if 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.

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 p ⇒ metric 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.