Library CompOptCert.Event

Require Import List.
Require Import PeanoNat.
Require Import Orders.
Require Import MSetList.

Require Import sflib.

Require Import DataStructure.
Require Import Basic.
Require Import Loc.

Set Implicit Arguments.

Require Import Integers.
Module Const := Int.

Lemma const_neq_sym:
  ∀ (x y:Const.t),
    x ≠ y ↔ y ≠ x.
Proof.
  intros.
  split.
  - intro. intro. rewrite H0 in H. contradiction.
  - intro. intro. rewrite H0 in H. contradiction.
Qed.

Lemma loc_neq_sym:
  ∀ (x y:Loc.t),
    x ≠ y ↔ y ≠ x.
Proof.
  intros.
  split.
  - intro. intro. rewrite H0 in H. contradiction.
  - intro. intro. rewrite H0 in H. contradiction.
Qed.

Module Ordering.
  Inductive t :=
  | plain
  | relaxed
  | strong_relaxed
  | acqrel
  | seqcst
  .

  Inductive atomicity :=
  | atomic
  | nonatomic
  .

  Definition mem_ord_match (ord: t) (o: atomicity): Prop :=
    match o with
    | nonatomic ⇒ ord = plain
    | atomic ⇒ (ord = acqrel) ∨ (ord = relaxed) ∨ (ord = strong_relaxed)
    end
  .

  Definition LocOrdMap := Loc.t → atomicity.

  Definition le (lhs rhs:t): bool :=
    match lhs, rhs with
    | plain, _ ⇒ true
    | _, plain ⇒ false

    | relaxed, _ ⇒ true
    | _, relaxed ⇒ false

    | strong_relaxed, _ ⇒ true
    | _, strong_relaxed ⇒ false

    | acqrel, _ ⇒ true
    | _, acqrel ⇒ false

    | seqcst, seqcst ⇒ true
    end.
  Global Opaque le.

  Global Program Instance le_PreOrder: PreOrder le.
  Next Obligation.
    ii. destruct x; auto.
  Qed.
  Next Obligation.
    ii. destruct x, y, z; auto.
  Qed.
  Hint Resolve le_PreOrder_obligation_2.

  Definition join (lhs rhs:t): t :=
    match lhs, rhs with
    | plain, _ ⇒ rhs
    | _, plain ⇒ lhs

    | relaxed, _ ⇒ rhs
    | _, relaxed ⇒ lhs

    | strong_relaxed, _ ⇒ rhs
    | _, strong_relaxed ⇒ lhs

    | acqrel, _ ⇒ rhs
    | _, acqrel ⇒ lhs

    | seqcst, _ ⇒ rhs
    end.

  Lemma join_comm lhs rhs: join lhs rhs = join rhs lhs.
  Proof. destruct lhs, rhs; ss. Qed.

  Lemma join_assoc a b c: join (join a b) c = join a (join b c).
  Proof. destruct a, b, c; ss. Qed.

  Lemma join_l lhs rhs:
    le lhs (join lhs rhs).
  Proof. destruct lhs, rhs; ss. Qed.

  Lemma join_r lhs rhs:
    le rhs (join lhs rhs).
  Proof. destruct lhs, rhs; ss. Qed.

  Lemma join_spec lhs rhs o
        (LHS: le lhs o)
        (RHS: le rhs o):
    le (join lhs rhs) o.
  Proof. destruct lhs, rhs; ss. Qed.

  Lemma join_cases lhs rhs:
    join lhs rhs = lhs ∨ join lhs rhs = rhs.
  Proof. destruct lhs, rhs; auto. Qed.
End Ordering.

Module Event.
  Structure t := mk {
    output: Const.t;
    
  }.
End Event.

Module VisibleEvent.
  Inductive t :=
  | out (e: Event.t)
  | abort
  | done.
End VisibleEvent.

Module AuxEvent.
  Inductive t :=
  | na
  | prc
  | atm
  | out (e: Event.t)
  | sw
  | tterm
  .
End AuxEvent.

Module MachineEvent.
  Inductive t :=
  | silent
  | switch
  | syscall (e: Event.t)
  .
End MachineEvent.

Module ProgramEvent.
  Inductive t :=
  | silent
  | read (loc:Loc.t) (val:Const.t) (ord:Ordering.t)
  | write (loc:Loc.t) (val:Const.t) (ord:Ordering.t)
  | update (loc:Loc.t) (valr valw:Const.t) (ordr ordw:Ordering.t)
  | fence (ordr ordw:Ordering.t)
  | syscall (e:Event.t)
  .

  Definition is_reading (e:t): option (Loc.t × Const.t × Ordering.t) :=
    match e with
    | read loc val ord ⇒ Some (loc, val, ord)
    | update loc valr _ ordr _ ⇒ Some (loc, valr, ordr)
    | _ ⇒ None
    end.

  Definition is_writing (e:t): option (Loc.t × Const.t × Ordering.t) :=
    match e with
    | write loc val ord ⇒ Some (loc, val, ord)
    | update loc _ valw _ ordw ⇒ Some (loc, valw, ordw)
    | _ ⇒ None
    end.

  Definition is_updating (e:t): option (Loc.t × Const.t × Ordering.t) :=
    match e with
    | update loc valr _ ordr _ ⇒ Some (loc, valr, ordr)
    | _ ⇒ None
    end.

End ProgramEvent.