Require Import List Relations Setoid Omega Permutation.
Require Import Classical ClassicalDescription.
Require Import Vbase extralib ExtraRelations.
Set Implicit Arguments.

Definition actid := nat.

Inductive act :=
  | Askip
  | Async
  | Alwsync
  | Aload (l : nat) (v : nat)
  | Astore (l : nat) (v : nat).

Definition loc a :=
  match a with
    | Aload l _
    | Astore l _ ⇒ 1
    | _ ⇒ 0
  end.

Definition is_access a :=
  match a with
    | Aload _ _ | Astore _ _ ⇒ true
    | _ ⇒ false
  end.

Definition is_read a :=
  match a with
    | Aload _ _ ⇒ true
    | _ ⇒ false
  end.

Definition is_write a :=
  match a with
    | Astore _ _ ⇒ true
    | _ ⇒ false
  end.

Definition is_fence a :=
  match a with
    | Alwsync | Async ⇒ true
    | _ ⇒ false
  end.

Lemma is_read_access a : is_read a → is_access a.

Lemma is_write_access a : is_write a → is_access a.

Hint Resolve is_read_access is_write_access : access.

Section PowerModel.

Variable acts : list actid.
Variable lab : actid → act.
Variable po : relation actid.
Variable deps : relation actid.
Variable rmw : relation actid.
Variable ppo : relation actid.
Variable rf : actid → option actid.
Variable co : relation actid.

Definition rfe x y := rf y = Some x ∧ ¬ po x y.

Definition fr x y := ∃ z, rf x = Some z ∧ co z y.

Definition fre x y := ∃ z, rf x = Some z ∧ co z y ∧ ¬ po x y.

Definition coe x y := co x y ∧ ¬ po x y.

Definition po_loc x y :=
  po x y ∧ is_access (lab x) ∧ is_access (lab y) ∧ loc (lab x) = loc (lab y).

Definition sync x y :=
  ∃ s, po x s ∧ po s y ∧ lab s = Async ∧
   is_access (lab x) ∧ is_access (lab y).

Definition lwsync x y :=
  (∃ s, po x s ∧ po s y ∧ lab s = Alwsync)
  ∧ (is_read (lab x) ∧ is_access (lab y) ∨
      is_access (lab x) ∧ is_write (lab y)).

Definition fence := sync +++ lwsync.

Definition hb_power := ppo +++ fence +++ rfe.

Definition prop_base :=
  clos_refl rfe ;; fence ;; clos_refl_trans hb_power.

Definition chapo :=
  rfe +++ fre +++ coe +++ (fre ;; rfe) +++ (coe ;; rfe).

Definition prop :=
  restr_rel (fun x ⇒ is_write (lab x)) prop_base
  +++ (clos_refl chapo ;; clos_refl prop_base ;; sync ;; clos_refl_trans hb_power).

Definition ExecutionFinite :=
  << CLOlab: ∀ a, lab a ≠ Askip → In a acts >> ∧
  << CLOsb : ∀ a b, po a b → In a acts ∧ In b acts >>.

Definition ConsistentRF_dom :=
  ∀ a b (RF: rf b = Some a),
  ∃ l v, <<WRI: lab a = Astore l v>> ∧ <<READ: lab b = Aload l v >>.

Definition CompleteRF :=
  ∀ a (RF: rf a = None)
         (READ: is_read (lab a)), False.

Definition ConsistentMO_dom :=
  ∀ a b (MO: co a b),
    is_write (lab a) ∧ is_write (lab b) ∧ loc (lab a) = loc (lab b).

Definition ConsistentRMW_dom :=
  ∀ a b (RF: rmw a b),
  << PO: po a b >> ∧
  << READ: is_read (lab a) >> ∧
  << WRITE: is_write (lab b) >> ∧
  << LOCEQ: loc (lab a) = loc (lab b) >>.

Definition ppo_lower_bound :=
  ∀ a b,
    clos_trans (deps +++ po_loc) a b →
    is_read (lab a) →
    is_write (lab b) →
    ppo a b.

Definition ppo_upper_bound :=
  ∀ a b,
    ppo a b →
    immediate po a b →
    clos_trans (deps +++ po_loc) a b.

Definition ConsistentPower :=
  << CppoL: ppo_lower_bound >> ∧

  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >> ∧
  << Crmw: ConsistentRMW_dom >> ∧
  << CcoD: ConsistentMO_dom >> ∧
  << CcoF: ∀ l, is_total (fun a ⇒ ∃ v, lab a = Astore l v) co >> ∧
  << CcoT: transitive co >> ∧
  << CcoI: irreflexive co >> ∧
  << LOC_SC : acyclic (po_loc +++ (fun x y ⇒ rf y = Some x) +++ co +++ fr) >> ∧
  << ATOM : irreflexive (rmw ;; fre ;; coe) >> ∧
  << NTA : acyclic hb_power >> ∧
  << OBS : irreflexive (fre ;; prop ;; clos_refl_trans hb_power) >> ∧
  << PROP: acyclic (co +++ prop) >>.

Lemma loceq_rf :
  ∀ (CrfD: ConsistentRF_dom) a b (H: rf b = Some a),
    loc (lab a) = loc (lab b).

Lemma loceq_co :
  ∀ (CcoD: ConsistentMO_dom) a b (H: co a b),
    loc (lab a) = loc (lab b).

Lemma loceq_fr :
  ∀ (CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
         a b (H: fr a b),
    loc (lab a) = loc (lab b).

Lemma fr_dom :
  ∀ (CrfD: ConsistentRF_dom)
         (CcoD: ConsistentMO_dom) x y
         (FR: fr x y),
  is_read (lab x) ∧ is_write (lab y) ∧ loc (lab x) = loc (lab y).

Lemma rfe_dom :
  ∀ (CrfD: ConsistentRF_dom) x y
         (RFE: rfe x y),
  is_write (lab x) ∧ is_read (lab y) ∧ loc (lab x) = loc (lab y).

Lemma fre_dom :
  ∀
         (CrfD: ConsistentRF_dom)
         (CcoD: ConsistentMO_dom) x y
         (FRE: fre x y),
  is_read (lab x) ∧ is_write (lab y) ∧ loc (lab x) = loc (lab y).

Definition nta_rel :=
  deps +++ po_loc
       +++ (fun x y ⇒ po x y ∧ (is_fence (lab x) ∨ is_fence (lab y)))
       +++ rfe.

Lemma acyclic_nta
      (CsbT: transitive po)
      (CsbI: irreflexive po)
      (Cdeps: inclusion deps po)
      (CrfD: ConsistentRF_dom)
      (NTA : acyclic hb_power)
      (PPO_lower : ppo_lower_bound) :
  acyclic nta_rel.

End PowerModel.

Definition ntb_rel i ll lab deps rf x y :=
   In x i ∧ In y (concat ll) ∨
   nta_rel lab (mk_po i ll) deps rf x y.

Lemma acyclic_ntb i ll lab deps ppo rf
      (ND: NoDup (i ++ concat ll))
      (INIT: ∀ x, is_read (lab x) → In x (concat ll))
      (Cdeps: inclusion deps (mk_po i ll))
      (CrfD: ConsistentRF_dom lab rf)
      (NTA : acyclic (hb_power lab (mk_po i ll) ppo rf))
      (PPO_lower : ppo_lower_bound lab (mk_po i ll) deps ppo) :
  acyclic (ntb_rel i ll lab deps rf).

Add Parametric Morphism : rfe with signature
  same_relation ==> eq ==> same_relation as rfe_mor.

Add Parametric Morphism : coe with signature
  same_relation ==> eq ==> same_relation as coe_mor.

Add Parametric Morphism : fre with signature
  same_relation ==> eq ==> eq ==> same_relation as fre_mor.

Add Parametric Morphism : po_loc with signature
  eq ==> same_relation ==> same_relation as po_loc_mor.

Add Parametric Morphism : sync with signature
  eq ==> same_relation ==> same_relation as sync_mor.

Add Parametric Morphism : lwsync with signature
  eq ==> same_relation ==> same_relation as lwsync_mor.

Add Parametric Morphism : hb_power with signature
  eq ==> same_relation ==> eq ==> eq ==> same_relation as hb_power_mor.

Add Parametric Morphism : prop_base with signature
  eq ==> same_relation ==> eq ==> eq ==> same_relation as prop_base_mor.

Add Parametric Morphism : prop with signature
  eq ==> same_relation ==> eq ==> eq ==> eq ==> same_relation as prop_mor.

Add Parametric Morphism : ppo_lower_bound with signature
  eq ==> same_relation ==> eq ==> eq ==> iff as ppo_lower_mor.

Add Parametric Morphism : ConsistentRMW_dom with signature
  eq ==> same_relation ==> eq ==> iff as ConsistentRMW_dom_mor.

Add Parametric Morphism : ConsistentPower with signature
  eq ==> same_relation ==> eq ==> eq ==> eq ==> eq ==> eq ==> iff as ConsistentPower_mor.

Add Parametric Morphism : nta_rel with signature
  eq ==> same_relation ==> eq ==> eq ==> same_relation as nta_rel_mor.

Lemma po_loc_reorder lab po a b
   (LOC: loc (lab a) ≠ loc (lab b)) :
  po_loc lab (reorder po a b) <--> po_loc lab po.

Lemma rfe_reorder lab po rf a b
      (Crf: ConsistentRF_dom lab rf)
      (LOC: loc (lab a) ≠ loc (lab b)) :
  rfe (reorder po b a) rf <--> rfe po rf.

Lemma fre_reorder lab po rf co a b
      (Crf: ConsistentRF_dom lab rf)
      (Cco: ConsistentMO_dom lab co)
      (LOC: loc (lab a) ≠ loc (lab b)) :
  fre (reorder po b a) rf co <--> fre po rf co.

Lemma coe_reorder lab po co a b
      (Cco: ConsistentMO_dom lab co)
      (LOC: loc (lab a) ≠ loc (lab b)) :
  coe (reorder po b a) co <--> coe po co.

Lemma sync_reorder lab (po : relation actid) a b
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b)) :
  sync lab (reorder po a b) <--> sync lab po.

Lemma lwsync_reorder lab (po : relation actid) a b
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b)) :
  lwsync lab (reorder po a b) <--> lwsync lab po.

Lemma hbp_reorder lab po ppo rf a b
      (Crf: ConsistentRF_dom lab rf)
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
      (LOC: loc (lab a) ≠ loc (lab b)) :
  hb_power lab (reorder po a b) ppo rf <--> hb_power lab po ppo rf.

Lemma base_reorder lab po ppo rf a b
      (Crf: ConsistentRF_dom lab rf)
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
      (LOC: loc (lab a) ≠ loc (lab b)) :
  prop_base lab (reorder po a b) ppo rf <--> prop_base lab po ppo rf.

Lemma prop_reorder lab po ppo rf co a b
      (Crf: ConsistentRF_dom lab rf)
      (Cmo: ConsistentMO_dom lab co)
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
      (LOC: loc (lab a) ≠ loc (lab b)) :
  prop lab (reorder po a b) ppo rf co <--> prop lab po ppo rf co.

Lemma nta_rel_reorder lab po ppo rf a b
      (Crf: ConsistentRF_dom lab rf)
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
      (LOC: loc (lab a) ≠ loc (lab b)) :
  nta_rel lab (reorder po a b) ppo rf <--> nta_rel lab po ppo rf.

Lemma ntb_rel_reorder i ll1 l1 a b l2 ll2 lab ppo rf
      (WF: NoDup (i ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)))
      (Crf: ConsistentRF_dom lab rf)
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
      (LOC: loc (lab a) ≠ loc (lab b)) :
  ntb_rel i (ll1 ++ (l1 ++ a :: b :: l2) :: ll2) lab ppo rf <-->
  ntb_rel i (ll1 ++ (l1 ++ b :: a :: l2) :: ll2) lab ppo rf.

Lemma ConsistentRMW_dom_reorder lab po rmw x y
      (LOC: loc (lab x) ≠ loc (lab y)) :
  ConsistentRMW_dom lab (reorder po x y) rmw ↔
  ConsistentRMW_dom lab po rmw.

Lemma ppo_lower_bound_reorder lab po deps ppo a b
      (LOC: loc (lab a) ≠ loc (lab b)) :
  ppo_lower_bound lab (reorder po a b) deps ppo ↔
  ppo_lower_bound lab po deps ppo.

Lemma ConsistentPower_reorder :
  ∀ lab po deps rmw ppo rf co a b
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
      (LOC: loc (lab a) ≠ loc (lab b)),
    ConsistentPower lab po deps rmw ppo rf co ↔
    ConsistentPower lab (reorder po a b) deps rmw ppo rf co.

Definition Power_reorder lab init deps (ll ll' : list (list actid)) :=
 ∃ ll1 l1 a b l2 ll2,
     << NFa: ¬ is_fence (lab a) >> ∧
     << NFb: ¬ is_fence (lab b) >> ∧
     << LOC: loc (lab a) ≠ loc (lab b) >> ∧
     << Nab: ¬ deps a b >> ∧
     << WF: NoDup (init ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)) >> ∧
     << EQ : ll = ll1 ++ (l1 ++ a :: b :: l2) :: ll2 >> ∧
     << EQ': ll' = ll1 ++ (l1 ++ b :: a :: l2) :: ll2 >>.

Fixpoint metric (ord: relation actid) (ll : list actid) :=
  match ll with
    | nil ⇒ 0
    | a :: ll ⇒
      length (filter (fun x ⇒ if excluded_middle_informative (ord x a)
                               then true else false) ll) +
      metric ord ll
  end.

Add Parametric Morphism : metric with signature
  same_relation ==> eq ==> eq as metric_mor.

Lemma reorder_metric (ord : relation actid)
      (T: transitive ord) (IRR: irreflexive ord) ll1 l1 a b (ORD: ord b a) l2 ll2 :
  metric ord (concat (ll1 ++ (l1 ++ b :: a :: l2) :: ll2)) <
  metric ord (concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)).

Theorem Power_alternative :
  ∀ lab init ll (ND: NoDup (init ++ concat ll)) deps
         (WF: inclusion deps (mk_po init ll))
         (INIT: ∀ x, is_read (lab x) → In x (concat ll))
         (MAIN: ∀ x, In x (concat ll) → is_access (lab x))
         rmw ppo rf co,
    ConsistentPower lab (mk_po init ll) deps rmw ppo rf co
    ↔
    ∃ ll',
      clos_refl_trans (Power_reorder lab init deps) ll ll' ∧
      ConsistentPower lab (mk_po init ll') deps rmw ppo rf co ∧
      acyclic (mk_po init ll' +++ (fun x y ⇒ rf y = Some x)).