Require Import List Vbase Vlistbase Relations.
Set Implicit Arguments.

Definition immediate X (rel : relation X) (a b: X) :=
  rel a b ∧ (∀ c (R1: rel a c) (R2: rel c b), False).

Definition irreflexive X (rel : relation X) := ∀ x, rel x x → False.

Definition acyclic X (rel : relation X) := irreflexive (clos_trans X rel).

Definition is_total X (cond: X → Prop) (rel: relation X) :=
  ∀ a (IWa: cond a)
         b (IWb: cond b) (NEQ: a ≠ b),
    rel a b ∨ rel b a.

Definition restr_subset X (cond: X → Prop) (rel rel': relation X) :=
  ∀ a (IWa: cond a)
         b (IWb: cond b) (REL: rel a b),
    rel' a b.

Inductive model_type := Model_standard_c11 | Model_hb_rf_acyclic.

Definition with_mt A mt (x y: A) :=
  match mt with
    | Model_standard_c11 ⇒ x
    | Model_hb_rf_acyclic ⇒ y
  end.

Definition actid := nat.

Inductive access_type :=
  | ATsc
  | ATar
  | ATacq
  | ATrel
  | ATrlx
  | ATna.

Definition release_typ typ := typ = ATrel ∨ typ = ATar ∨ typ = ATsc.

Definition acquire_typ typ := typ = ATacq ∨ typ = ATar ∨ typ = ATsc.

Definition acquire_release_typ typ := typ = ATar ∨ typ = ATsc.

Inductive act :=
  | Askip
  | Aalloc (l : nat)
  | Aload (typ : access_type) (l : nat) (v : nat)
  | Astore (typ : access_type) (l : nat) (v : nat)
  | Armw (typ : access_type) (l : nat) (v v': nat)
  | Afence (typ: access_type).

Definition loc a :=
  match a with
    | Askip ⇒ 0
    | Aalloc l
    | Aload _ l _
    | Astore _ l _
    | Armw _ l _ _ ⇒ l
    | Afence _ ⇒ 0
  end.

Definition is_alloc a :=
  match a with
    | Aalloc _ ⇒ true
    | _ ⇒ false
  end.

Definition is_rmw a :=
  match a with
    | Askip | Aalloc _ | Aload _ _ _ | Astore _ _ _ | Afence _ ⇒ false
    | Armw _ _ _ _ ⇒ true
  end.

Definition is_read a :=
  match a with
    | Askip | Aalloc _ | Astore _ _ _ | Afence _ ⇒ false
    | Aload _ _ _ | Armw _ _ _ _ ⇒ true
  end.

Definition is_write a :=
  match a with
    | Askip | Aalloc _ | Aload _ _ _ | Afence _ ⇒ false
    | Astore _ _ _ | Armw _ _ _ _ ⇒ true
  end.

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

Definition is_writeL a l :=
  match a with
    | Astore _ l' _
    | Armw _ l' _ _ ⇒ l' = l
    | _ ⇒ False
  end.

Definition is_writeLV a l v :=
  match a with
    | Astore _ l' v'
    | Armw _ l' _ v' ⇒ l' = l ∧ v' = v
    | _ ⇒ False
  end.

Definition is_readLV a l v :=
  match a with
    | Aload _ l' v'
    | Armw _ l' v' _ ⇒ l' = l ∧ v' = v
    | _ ⇒ False
  end.

Definition is_na a :=
  match a with
    | Aload ATna _ _
    | Astore ATna _ _
    | Armw ATna _ _ _ ⇒ true
    | _ ⇒ false
  end.

Definition is_at a :=
  match a with
    | Aload ATna _ _
    | Astore ATna _ _
    | Armw ATna _ _ _ ⇒ false
    | _ ⇒ true
  end.

Definition is_sc a :=
  match a with
    | Aload ATsc _ _
    | Astore ATsc _ _
    | Armw ATsc _ _ _
    | Afence ATsc ⇒ true
    | _ ⇒ false
  end.

Definition is_release_write a :=
  match a with
    | Astore ATsc _ _
    | Astore ATar _ _
    | Astore ATrel _ _
    | Armw ATsc _ _ _
    | Armw ATar _ _ _
    | Armw ATrel _ _ _ ⇒ true
    | _ ⇒ false
  end.

Definition is_acquire_read a :=
  match a with
    | Aload ATsc _ _
    | Aload ATar _ _
    | Aload ATacq _ _
    | Armw ATsc _ _ _
    | Armw ATar _ _ _
    | Armw ATacq _ _ _ ⇒ true
    | _ ⇒ false
  end.

Definition is_rlx_write a :=
  match a with
    | Astore ATacq _ _ ⇒ true
    | Astore ATrlx _ _ ⇒ true
    | Armw ATacq _ _ _ ⇒ true
    | Armw ATrlx _ _ _ ⇒ true
    | _ ⇒ false
  end.

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

Definition is_release_fence a :=
  match a with
    | Afence ATrel ⇒ true
    | Afence ATar ⇒ true
    | Afence ATsc ⇒ true
    | _ ⇒ false
  end.

Definition is_acquire_fence a :=
  match a with
    | Afence ATacq ⇒ true
    | Afence ATar ⇒ true
    | Afence ATsc ⇒ true
    | _ ⇒ false
  end.

Section Consistency.

Variable acts : list actid.

Variable lab : actid → act.

Variable sb : actid → actid → Prop.

Variable rf : actid → option actid.

Variable mo : actid → actid → Prop.

Variable sc : actid → actid → Prop.

Definition sameThread (a b : actid) :=
  ∀ c (BAc: clos_refl_trans _ sb a c) (BBc: clos_refl_trans _ sb c b),
    (∃! pre, sb pre c) ∧ (∃! post, sb c post).

Inductive release_seq (a b : actid) : Prop :=
| RS_refl (EQ: a = b)
| RS_thr (RSthr: sb a b)
         (RSmo: mo a b)
| RS_rmw c (RS: release_seq a c)
        (RSrf: rf b = Some c)
        (RSrmw: is_rmw (lab b)).

Definition synchronizes_with (a b : actid) :=
     ( is_release_write (lab a) ∧ is_acquire_read (lab b) ∧
       ∃ c, release_seq a c ∧ rf b = Some c)
  ∨ ( is_release_write (lab a) ∧ is_acquire_fence (lab b) ∧
       ∃ c a', clos_refl_trans _ sb c b ∧ release_seq a a' ∧ rf c = Some a' )
  ∨ ( is_release_fence (lab a) ∧ is_acquire_read (lab b) ∧
       ∃ c c', clos_refl_trans _ sb a c ∧ release_seq c c' ∧ rf b = some c' )
  ∨ ( is_release_fence (lab a) ∧ is_acquire_fence (lab b) ∧
       ∃ c c' d, clos_refl_trans _ sb a c ∧ clos_refl_trans _ sb d b ∧
                      release_seq c c' ∧ rf d = Some c' ).

Definition imm_happens_before a b :=
  sb a b ∨ synchronizes_with a b.

Definition happens_before :=
  clos_trans _ imm_happens_before.

Definition visible l a b :=
  happens_before a b ∧
  (∀ c (HB1: happens_before a c) (HB2: happens_before c b),
    ¬ is_writeL (lab c) l).

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

Definition ConsistentMO :=
  (∀ a b (MO: mo a b), ∃ l, is_writeL (lab a) l ∧ is_writeL (lab b) l)
  ∧ transitive _ mo
  ∧ (∀ l, is_total (fun a ⇒ is_writeL (lab a) l) mo)
  ∧ (∀ l, restr_subset (fun a ⇒ is_writeL (lab a) l) happens_before mo).

Definition ConsistentSC :=
  transitive _ sc
  ∧ is_total (fun x ⇒ is_sc (lab x)) sc
  ∧ restr_subset (fun x ⇒ is_sc (lab x)) happens_before sc
  ∧ restr_subset (fun x ⇒ is_sc (lab x)) mo sc.

Definition ConsistentRF_basic :=
  ∀ a,
    match rf a with
      | None ⇒
        ∀ b (HB: happens_before b a)
               l v (READ: is_readLV (lab a) l v)
               (WRI: is_writeL (lab b) l), False
      | Some b ⇒
          ∃ l v, is_readLV (lab a) l v ∧ is_writeLV (lab b) l v
    end.

Definition ConsistentRF_no_future :=
  ∀ a b (RF: rf b = Some a) (HB: happens_before b a), False.

Definition ConsistentRF_na :=
  ∀ a b (RF: rf a = Some b) (NA: is_na (lab a) ∨ is_na (lab b)),
    visible (loc (lab a)) b a.

Definition SCrestriction :=
  ∀ a b (RF: rf b = Some a) (SC: is_sc (lab b)),
    immediate sc a b ∨
    ¬ is_sc (lab a) ∧ (∀ x (SC: immediate sc x b) (HB: happens_before a x), False).

Definition CoherentRR :=
  ∀ a b (HB: happens_before a b) (LOC: loc (lab a) = loc (lab b))
         c (RFa: rf a = Some c) d (RFb: rf b = Some d) (MO: mo d c),
    False.

Definition CoherentWR :=
  ∀ a b (HB: happens_before a b) (LOC: loc (lab a) = loc (lab b))
         c (RF: rf b = Some c) (MO: mo c a),
    False.

Definition CoherentRW :=
  ∀ a b (HB: happens_before a b) (LOC: loc (lab a) = loc (lab b))
         c (RF: rf a = Some c) (MO: mo b c),
    False.

Definition AtomicRMW :=
  ∀ a (RMW: is_rmw (lab a)) b (RF: rf a = Some b),
    immediate mo b a.

Definition ConsistentAlloc :=
  ∀ l a (ALLOCa: lab a = Aalloc l) b (ALLOCb: lab b = Aalloc l),
    a = b.

Definition IrreflexiveHB :=
  irreflexive happens_before.

Definition AcyclicMedium :=
  acyclic (fun a b ⇒ happens_before a b ∨
                      rf b = Some a ∧ (is_na (lab b) ∨ is_na (lab a))).

Definition AcyclicStrong :=
  acyclic (fun a b ⇒ happens_before a b ∨ rf b = Some a).

Definition Consistent mt :=
  << FIN : ExecutionFinite >> ∧
  << IRR : IrreflexiveHB >> ∧
  << Cmo : ConsistentMO >> ∧
  << Csc : ConsistentSC >> ∧
  << Crf : ConsistentRF_basic >> ∧
  << Crf': with_mt mt ConsistentRF_no_future AcyclicStrong >> ∧
  << Cna : ConsistentRF_na >> ∧
  << Csc': SCrestriction >> ∧
  << Crr : CoherentRR >> ∧
  << Cwr : CoherentWR >> ∧
  << Crw : CoherentRW >> ∧
  << Crmw: AtomicRMW >> ∧
  << Ca : ConsistentAlloc >>.

Definition weakConsistent mt :=
  << FIN : ExecutionFinite >> ∧
  << IRR : IrreflexiveHB >> ∧
  << ACYC: with_mt mt AcyclicMedium AcyclicStrong >> ∧
  << Cmo : ConsistentMO >> ∧
  << Csc : ConsistentSC >> ∧
  << Crf : ConsistentRF_basic >> ∧
  << Crf': with_mt mt ConsistentRF_no_future True >> ∧
  << Csc': SCrestriction >> ∧
  << Crr : CoherentRR >> ∧
  << Cwr : CoherentWR >> ∧
  << Crw : CoherentRW >> ∧
  << Crmw: AtomicRMW >> ∧
  << Ca : ConsistentAlloc >>.

Lemma ConsistentWeaken :
  Consistent Model_hb_rf_acyclic → Consistent Model_standard_c11.
Proof.
  ins; red; red in H; des; intuition.
  unfold with_mt in *; simpl.
  by intros a b ? ?; eapply (Crf' a), (t_trans _ _ _ b); vauto.
Qed.

Lemma ConsistentWeaken2 mt :
  Consistent mt → weakConsistent mt.
Proof.
  ins; red; red in H; des; intuition; destruct mt; ins.
  intros x H; apply (IRR x); revert H; generalize x at 1 3.
  induction 1; desf; vauto; edestruct Cna; eauto using clos_trans.
Qed.

Lemma finiteRF :
  ∀ (FIN: ExecutionFinite)
         (Crf: ConsistentRF_basic) a b,
    rf a = Some b → In a acts ∧ In b acts.
Proof.
  unfold ExecutionFinite; ins; desf.
  specialize (Crf a); desf; desf.
  generalize (CLOlab a); destruct (lab a); ins;
  generalize (CLOlab b); destruct (lab b); ins; intuition congruence.
Qed.

Definition mem_safe :=
  ∀ a (IN: In a acts) (Aa: is_access (lab a)),
  ∃ b, lab b = Aalloc (loc (lab a)) ∧ happens_before b a.

Definition initialized_reads :=
  ∀ a (IN: In a acts) l v (Aa: is_readLV (lab a) l v), rf a ≠ None.

Definition race_free :=
  ∀ a (INa: In a acts) (Aa: is_access (lab a))
         b (INb: In b acts) (Ab: is_access (lab b))
         (LOC: loc (lab a) = loc (lab b)) (NEQ: a ≠ b)
         (WRI: is_write (lab a) ∨ is_write (lab b))
         (NA: is_na (lab a) ∨ is_na (lab b)),
    happens_before a b ∨ happens_before b a.

End Consistency.