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

Lemma ModelTSO_SRA :
  ∀ lab sb rf mo
         (C: ModelTSO lab sb rf mo),
  acyclic (sb +++ rf_external sb rf +++ mo).

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.

Theorem ModelTSO_simplify :
  ∀ lab sb (T: transitive sb) rf mo,
    ModelTSO lab sb rf mo ↔
    ModelTSO_simpl lab sb rf mo.

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.

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).

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.

Lemma irreflexive_reorder A (r r' : relation A) a b :
  irreflexive (r ;; r') →
  ¬ r a b →
  irreflexive (r ;; reorder r' a b).

Lemma irreflexive_reorder2 A (r r' : relation A) a b :
  irreflexive (r ;; reorder r' a b) →
  ¬ r b a →
  irreflexive (r ;; r').

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.

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.

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'.

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)).

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'.

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'.

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'.

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)).

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)).

Lemma TSO_transform_sound :
  ∀ pe pe'
         (T: TSO_transform pe pe')
         (WF: pe_wellformed pe)
         (C: Consistent ModelTSO pe'),
    Consistent ModelTSO pe.

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'.

Theorem TSO_alternative :
  ∀ pe (WF: pe_wellformed pe),
    Consistent ModelTSO pe
    ↔
    ∃ pe',
      clos_refl_trans TSO_transform pe pe' ∧
      Consistent ModelSC_bigmo pe'.