Library mcertikos.conlib.conmclib.Concurrent_Linking_Def

Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Events.
Require Import Globalenvs.
Require Import Conventions.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import Smallstep.
Require Import CommonTactic.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Concurrent_Linking_Lib.


Section HARDWARESETTING.

  Class HardWaredSetting :=
    {
      private_state: Type;
      shared_piece: Type;
      

      
      atomic_event: Type;
      atomic_event_ident: atomic_event → ident;
      
      shared_piece_dec (d1 d2: shared_piece) : {d1 = d2} + {d1 ≠ d2};
      atomic_event_dec (d1 d2: atomic_event) : {d1 = d2} + {d1 ≠ d2};

      core_set: ZSet;
      
      sched_id: Z;
      sched_valid: core_set sched_id = false
    }.

  Context `{hardware: HardWaredSetting}.

  Context `{pmap: PartialMap}.


  Inductive command :=
  | PRIVATE
  | ATOMIC (id: Z) (e: ident)
  | ACQ_SHARED (id: Z)
  | REL_SHARED (id: Z).

  Inductive event :=
  | EYIELD (from: Z)
  | EBACK (to: Z)
  | EACQ (from id: Z)
  | EREL (from id: Z) (d: shared_piece)
  | EATOMIC (from id: Z) (e: atomic_event).

  Definition event_source (e: event) :=
    match e with
      | EYIELD i ⇒ i
      | EBACK _ ⇒ sched_id
      | EACQ i _ ⇒ i
      | EREL i _ _ ⇒ i
      | EATOMIC i _ _ ⇒ i
    end.

  Definition event_des (e: event) :=
    match e with
      | EYIELD i ⇒ sched_id
      | EBACK i ⇒ i
      | EACQ i _ ⇒ i
      | EREL i _ _ ⇒ i
      | EATOMIC i _ _ ⇒ i
    end.

  Inductive EvTy :=
  | YIELDTY
  | EBACKTY
  | EACQTY
  | ERELTY
  | EATOMICTY.

  Definition GetEvTy (ev: event) :=
    match ev with
    | EYIELD _ ⇒ YIELDTY
    | EBACK _ ⇒ EBACKTY
    | EACQ _ _ ⇒ EACQTY
    | EREL _ _ _ ⇒ ERELTY
    | EATOMIC _ _ _ ⇒ EATOMICTY
    end.

  Definition Log := list event.

  Definition lastEvTy (l :Log) : option EvTy :=
    match l with
    | nil ⇒ None
    | e::l´ ⇒ Some (GetEvTy e)
    end.


  Definition get_curid_from_log (start_core : Z) (l : Log) : Z :=
    match l with
    | nil ⇒ start_core
    | e::l´ ⇒ event_des e
    end.

  Fixpoint log_get_atomic (l: Log) (eid: Z) :=
    match l with
      | nil ⇒ nil
      | e :: l´ ⇒
        match e with
          | EATOMIC _ eid´ _ ⇒
            if zeq eid eid´ then
              e :: (log_get_atomic l´ eid)
            else
              log_get_atomic l´ eid
          | EACQ _ eid´ ⇒
            if zeq eid eid´ then
              e :: (log_get_atomic l´ eid)
            else
              log_get_atomic l´ eid
          | EREL _ eid´ _ ⇒
            if zeq eid eid´ then
              e :: (log_get_atomic l´ eid)
            else
              log_get_atomic l´ eid
          | _ ⇒ log_get_atomic l´ eid
        end
    end.

End HARDWARESETTING.


Section ORACLE_DEF.

  Class OracleProp {ret log : Type} {log_len: log → Z} `{zset_op: ZSet_operation}
        `{hdset: HardWaredSetting}:=
    {
      Oracle : Type;
      oget: ZSet → log → Oracle → option ret;
      append_o: Oracle → Oracle → Oracle;
      uoracle: Z → log → ret → Oracle;
      empty_o: Oracle;
      
      log_dec (l1 l2: log) : {l1 = l2} + {l1 ≠ l2};

      log_len_diff_neq:
        ∀ (l1 l2: log) (Hneq: log_len l1 ≠ log_len l2), l1 ≠ l2;

      domain (o: Oracle) (D: ZSet) :=
        ∀ l (Hr: D (log_len l) = false), ∀ A, oget A l o = None;

      domain_disjoint (o1 o2: Oracle) :=
        ∃ A B, domain o1 A ∧ domain o2 B ∧ disjoint_set A B;

      oracle_eq:
        ∀ o1 o2
               (Heq: ∀ A l, oget A l o1 = oget A l o2),
          o1 = o2;

      append_o_left:
        ∀ A o1 o2 l e
               (Hdis: domain_disjoint o1 o2),
          oget A l o1 = Some e →
          oget A l (append_o o1 o2) = Some e;

      append_o_right:
        ∀ A o1 o2 l
               (Hdis: domain_disjoint o1 o2),
          oget A l o1 = None →
          oget A l (append_o o1 o2) = oget A l o2;
      
      append_o_or:
        ∀ A l o1 o2 e
               (Hdis: domain_disjoint o1 o2),
          oget A l (append_o o1 o2) = Some e →
          oget A l o1 = Some e
          ∨ (oget A l o1 = None
              ∧ oget A l o2 = Some e);

      append_o_associativity:
        ∀ o1 o2 o3
               (Hdis: domain_disjoint o1 o2),
          append_o o1 (append_o o2 o3) = append_o (append_o o1 o2) o3;

      uoracle_eq:
        ∀ l curid e A,
          A curid = true →
          oget A l (uoracle curid l e) = Some e;

      uoracle_neq:
        ∀ l l´ curid e A,
          l´ ≠ l ∨ A curid = false →
          oget A l´ (uoracle curid l e) = None;

      empty_o_empty:
        ∀ A l,
          oget A l empty_o = None;

      append_o_empty:
        ∀ o,
          append_o o empty_o = o;

      oget_subset:
        ∀ A1 A2 o l e,
          oget A1 l o = Some e →
          subset A1 A2 →
          oget A2 l o = Some e
    }.

  Require Import AuxStateDataType.

  Section WITHORACLE.

    Definition RZSet (s e: Z): ZSet :=
      fun i ⇒ if zle_lt s i e then true else false.

    Context `{op: OracleProp}.

    Require Import Coq.Logic.FunctionalExtensionality.

    Lemma event_dec_aux:
      ∀ (e1 e2: event),
        {e1 = e2} + {e1 ≠ e2}.
    Proof.
      intros.
      destruct e1; destruct e2; try decide equality;
      try eapply zeq; try eapply shared_piece_dec; try eapply atomic_event_dec.
    Qed.

    Lemma Log_dec_aux:
      ∀ (l1 l2: Log),
        {l1 = l2} + {l1 ≠ l2}.
    Proof.
      induction l1; intros.
      - destruct l2.
        + left. trivial.
        + right. congruence.
      - destruct l2.
        + right. congruence.
        + destruct (event_dec_aux a e); subst.
          × destruct (IHl1 l2); subst.
            {
              left; trivial.
            }
            {
              right. intros HF. elim n.
              inv HF. trivial.
            }
          × right. intros HF. elim n.
            inv HF. trivial.
    Qed.

    Remark Log_dec (l1 l2: Log) : {l1 = l2} + {l1 ≠ l2}.
    Proof.
      eapply Log_dec_aux; eauto.
    Qed.

    Lemma uoracle_some_imply:
      ∀ l l´ curid e e´ A,
        oget A l (uoracle curid l´ e) = Some e´ →
        A curid = true ∧ l´ = l ∧ e´ = e.
    Proof.
      intros. destruct (A curid) eqn: Hcurid.
      - destruct (log_dec l´ l); subst.
        + rewrite uoracle_eq in H; trivial.
          inv H; eauto.
        + rewrite uoracle_neq in H; try congruence.
          left; auto.
      - rewrite uoracle_neq in H; try congruence.
        right; trivial.
    Qed.

    Definition list_Len {A: Type} (l: list A) :=
      Z.of_nat (length l).

    Lemma subset_false:
      ∀ A B,
        subset A B →
        ∀ i, B i = false → A i = false.
    Proof.
      intros. destruct (A i) eqn: HA; trivial.
      eapply H in HA. congruence.
    Qed.

    Lemma domain_weak:
      ∀ o A B,
        domain o A →
        subset A B →
        domain o B.
    Proof.
      intros. unfold domain in ×.
      intros. eapply H. eapply subset_false; eauto.
    Qed.

    Lemma subset_RZSet:
      ∀ s1 s2 e1 e2,
        s1 ≥ s2 → e1 ≤ e2 →
        subset (RZSet s1 e1) (RZSet s2 e2).
    Proof.
      unfold RZSet, subset. intros.
      destruct (zle_lt s1 i e1); inv HA.
      rewrite zle_lt_true; trivial. omega.
    Qed.

    Lemma domain_empty:
      ∀ A, domain empty_o A.
    Proof.
      intros. intros l. intros.
      eapply empty_o_empty.
    Qed.

    Lemma disjoint_RZSet:
      ∀ s1 s2 e1 e2,
        e1 ≤ s2 →
        disjoint_set (RZSet s1 e1) (RZSet s2 e2).
    Proof.
      unfold disjoint_set, RZSet. intros.
      destruct (zle_lt s1 i e1); destruct (zle_lt s2 i e2); eauto.
      omega.
    Qed.

    Lemma domain_disjoint_RZSet:
      ∀ o1 o2 s1 s2 e1 e2,
        e1 ≤ s2 →
        domain o1 (RZSet s1 e1) →
        domain o2 (RZSet s2 e2) →
        domain_disjoint o1 o2.
    Proof.
      intros. unfold domain_disjoint.
      refine_split´; eauto.
      eapply disjoint_RZSet; eauto.
    Qed.

    Lemma disjoint_set_commutativity:
      ∀ o1 o2,
        disjoint_set o1 o2 →
        disjoint_set o2 o1.
    Proof.
      unfold disjoint_set; intros.
      specialize (H i). destruct H as (HA1 & HA2).
      eauto.
    Qed.

    Lemma domain_disjoint_commutativity:
      ∀ o1 o2,
        domain_disjoint o1 o2 →
        domain_disjoint o2 o1.
    Proof.
      unfold domain_disjoint; intros.
      destruct H as (A & B & Hd1 & Hd2 & Hdis).
      ∃ B, A.
      refine_split´; trivial.
      eapply disjoint_set_commutativity; eauto.
    Qed.

    Lemma append_o_commutativity_disjoint:
      ∀ o1 o2 (Hdis: domain_disjoint o1 o2),
        append_o o1 o2 = append_o o2 o1.
    Proof.
      intros. pose proof Hdis as Hdis´. destruct Hdis as (A & B & Hdom1 & Hdom2 & Hdis).
      eapply oracle_eq. intros.
      specialize (Hdom1 l).
      specialize (Hdom2 l).
      specialize (Hdis (log_len l)).
      destruct (A (log_len l)).
      - destruct Hdis as (Hdis & _).
        specialize (Hdis eq_refl). specialize (Hdom2 Hdis).
        destruct (oget A0 l o1) eqn: Hget1.
        + erewrite append_o_left; eauto.
          rewrite append_o_right; eauto.
          apply domain_disjoint_commutativity; trivial.
        + erewrite append_o_right; eauto.
          erewrite append_o_right; eauto. congruence.
          apply domain_disjoint_commutativity; trivial.
      - specialize (Hdom1 eq_refl).
        rewrite append_o_right; eauto.
        destruct (oget A0 l o2) eqn: Hget2.
        + erewrite append_o_left; eauto.
          apply domain_disjoint_commutativity; trivial.
        + erewrite append_o_right; eauto.
          apply domain_disjoint_commutativity; trivial.
    Qed.

    Lemma append_o_swap:
      ∀ o1 o2 (Hdis: domain_disjoint o1 o2) o3,
        append_o o1 (append_o o2 o3) = append_o (append_o o2 o1) o3.
    Proof.
      intros. erewrite append_o_associativity; trivial.
      exploit (append_o_commutativity_disjoint o1 o2); trivial.
      intros Ha. unfold Log. rewrite Ha. trivial.
    Qed.

    Definition ZSet_empty: ZSet :=
      fun i ⇒ false.

    Lemma domain_disjoint_empty:
      ∀ o A (Hd: domain o A),
        domain_disjoint o empty_o.
    Proof.
      unfold domain_disjoint. intros.
      ∃ A, ZSet_empty.
      refine_split´; eauto.
      - eapply domain_empty.
      - unfold disjoint_set. intros.
        split; trivial. intros. inv H.
    Qed.

    Lemma domain_trans´:
      ∀ o1 o2 A B (Hdis: domain_disjoint o1 o2),
        domain o1 A →
        domain o2 B →
        domain (append_o o1 o2) (union_set A B).
    Proof.
      unfold domain; intros.
      eapply union_false´ in Hr.
      destruct Hr as (HA & HB).
      specialize (H _ HA A0).
      specialize (H0 _ HB A0).
      rewrite append_o_right; eauto.
    Qed.

    Lemma domain_invert_left:
      ∀ o1 o2 C,
        domain_disjoint o1 o2 →
        domain (append_o o1 o2) C →
        domain o1 C.
    Proof.
      unfold domain; intros.
      specialize (H0 _ Hr A).
      destruct (oget A l o1) eqn: HA; trivial.
      erewrite append_o_left in H0; eauto.
    Qed.

    Lemma domain_invert_right:
      ∀ o1 o2 C,
        domain_disjoint o1 o2 →
        domain (append_o o1 o2) C →
        domain o2 C.
    Proof.
      intros. erewrite append_o_commutativity_disjoint in H0; eauto.
      eapply domain_invert_left; eauto.
      eapply domain_disjoint_commutativity. trivial.
    Qed.

    Lemma domain_join:
      ∀ o A B,
        domain o A →
        domain o B →
        domain o (join_set A B).
    Proof.
      unfold domain; intros.
      eapply join_set_not_in in Hr.
      destruct Hr; eauto.
    Qed.

    Lemma disjoint_join:
      ∀ A B,
        disjoint_set A B →
        ∀ A´, disjoint_set (join_set A A´) B.
    Proof.
      unfold disjoint_set; intros.
      split; intros.
      - eapply join_set_imply in H0. eapply H; eapply H0.
      - eapply join_set_not_in_rely. left. eapply H; trivial.
    Qed.

    Lemma disjoint_union:
      ∀ A B C,
        disjoint_set A B →
        disjoint_set A C →
        disjoint_set A (union_set B C).
    Proof.
      unfold disjoint_set in ×. intros.
      specialize (H i).
      specialize (H0 i).
      destruct H as (HA1 & HB1).
      destruct H0 as (HA2 & HB2).
      split; intros.
      - eapply union_false; eauto.
      - destruct (A i); trivial.
        erewrite union_false in H; eauto.
    Qed.

    Lemma domain_disjoint_append_union:
      ∀ o1 o2 o3,
        domain_disjoint o1 o2 →
        domain_disjoint o1 o3 →
        domain_disjoint o2 o3 →
        domain_disjoint o1 (append_o o2 o3).
    Proof.
      intros. rename H1 into Hdd.
      unfold domain_disjoint.
      unfold domain_disjoint in H0, H; intros.
      destruct H as (A & B & HDA & HDB & Hdis).
      destruct H0 as (A´ & C & HDA´ & HDC & Hdis´).
      specialize (domain_join _ _ _ HDA HDA´). clear HDA HDA´. intros HDA.
      specialize (domain_trans´ _ _ _ _ Hdd HDB HDC). clear HDB HDC. intros Ha.
      refine_split´; eauto. clear HDA Ha.
      eapply disjoint_union.
      - eapply disjoint_join; eauto.
      - rewrite join_set_commutativity.
        eapply disjoint_join; eauto.
    Qed.

    Lemma domain_disjoint_append:
      ∀ o1 o2 o3,
        domain_disjoint o1 o2 →
        domain_disjoint (append_o o1 o2) o3 →
        domain_disjoint o1 o3 ∧ domain_disjoint o2 o3.
    Proof.
      intros. unfold domain_disjoint.
      unfold domain_disjoint in H0.
      destruct H0 as (C & D & HDC & HDD & Hdis´).
      specialize (domain_invert_left _ _ _ H HDC); eauto.
      erewrite append_o_commutativity_disjoint in HDC; eauto.
      apply domain_disjoint_commutativity in H.
      specialize (domain_invert_left _ _ _ H HDC); eauto. clear HDC.
      intros HDB HDA.
      split.
      - ∃ C, D. refine_split´; trivial.
      - ∃ C, D. refine_split´; trivial.
    Qed.

    Lemma RZSet_union:
      ∀ s z e,
        s ≤ z → z ≤ e →
        RZSet s e = union_set (RZSet s z) (RZSet z e).
    Proof.
      unfold RZSet. intros.
      eapply functional_extensionality_dep; intros.
      destruct (zle_lt s x e).
      - destruct (zlt x z).
        + rewrite union_left; trivial.
          rewrite zle_lt_true; trivial. omega.
        + rewrite union_right; trivial.
          rewrite zle_lt_true; trivial. omega.
      - rewrite union_false; trivial.
        + destruct (zle_lt s x z); trivial. omega.
        + destruct (zle_lt z x e); trivial. omega.
    Qed.

    Lemma domain_trans:
      ∀ o1 o2 s z e (Hdis: domain_disjoint o1 o2),
        s ≤ z → z ≤ e →
        domain o1 (RZSet s z) →
        domain o2 (RZSet z e) →
        domain (append_o o1 o2) (RZSet s e).
    Proof.
      intros. erewrite RZSet_union; eauto.
      eapply domain_trans´; eauto.
    Qed.

  End WITHORACLE.

  Section WITHORACLE_LOG.

    Context `{op: OracleProp (log := Log) (log_len := list_Len)}.

    Lemma domain_uoracle:
      ∀ l cid z,
        domain (uoracle cid l z) (RZSet (list_Len l) (list_Len l + 1)).
    Proof.
      intros. intros l0. intros.
      eapply uoracle_neq. destruct (Log_dec l l0); subst.
      - unfold RZSet in Hr. subdestruct. omega.
      - left; eauto.
    Qed.

    Lemma domain_uoracle_append1:
      ∀ l l´ cid z e1 e2,
        domain (uoracle cid (e1 :: l) z) (RZSet (list_Len l) (list_Len (l´ ++ e2 :: e1 :: l))).
    Proof.
      intros. eapply domain_weak.
      eapply domain_uoracle.
      unfold list_Len. simpl.
      eapply subset_RZSet. xomega.
      erewrite app_length. simpl. xomega.
    Qed.

  End WITHORACLE_LOG.

  Section WITHORACLE2.

    Context `{op: OracleProp (ret:= event) (log := Log) (log_len := list_Len)}.


    Definition valid_log_check (start_core : Z) (l : Log) :=
      match l with
      | nil ⇒ True
      | e::l´ ⇒
        match e with
        | EBACK j ⇒ lastEvTy l´ = Some YIELDTY ∧ core_set j = true
        | EYIELD from ⇒ lastEvTy l´ ≠ Some YIELDTY ∧ from = get_curid_from_log start_core l´ ∧ core_set from = true
        | _ ⇒ match l´ with
              | EBACK j´::_ ⇒ j´ = event_source e ∧ core_set j´ = true
              | _ ⇒ False
              end
        end
      end.

    Inductive valid_log : Z → Log → Prop :=
    | valid_log_nil :
        ∀ tid, core_set tid = true → valid_log_check tid nil → valid_log tid nil
    | valid_log_cons:
        ∀ tid e l, core_set tid = true → valid_log tid l → valid_log_check tid (e::l) → valid_log tid (e::l).

    Definition valid_oracle (start_core : Z) (A: ZSet) (o: Oracle) :=
      ∀ l e,
        valid_log start_core l →
        oget A l o = Some e →
        
        A (event_source e) = false ∧
        valid_log start_core (e::l).


  End WITHORACLE2.

End ORACLE_DEF.


Section HARDSEMCLASS.

  Class HardSemantics `{hdset :HardWaredSetting} :=
    {
      PC : private_state → command → Prop;
      private_step: Z → private_state → private_state → Prop;
      get_shared: private_state → shared_piece → private_state → Prop;
      set_shared: private_state → option shared_piece → private_state → Prop;
      atomic_step: Z → Z → private_state → Log → private_state → atomic_event → Prop;
      

      
      PC_determ ps c1 c2:
        PC ps c1 →
        PC ps c2 →
        c1 = c2;
      private_step_determ n ps ps1 ps2:
        private_step n ps ps1 →
        private_step n ps ps2 →
        ps1 = ps2;
      get_shared_determ ps sp1 ps1 sp2 ps2:
        get_shared ps sp1 ps1 →
        get_shared ps sp2 ps2 →
        sp1 = sp2 ∧ ps1 = ps2;
      set_shared_determ ps sp ps1 ps2:
        set_shared ps sp ps1 →
        set_shared ps sp ps2 →
        ps1 = ps2;
      atomic_step_determ_ps curid id ps l ps1 ev1 ps2 ev2:
        atomic_step curid id ps l ps1 ev1 →
        atomic_step curid id ps l ps2 ev2 →
        ps1 = ps2;
      atomic_step_determ_ev curid id ps l1 l2 ps1 ps2 ev1 ev2:
        atomic_step curid id ps l1 ps1 ev1 →
        atomic_step curid id ps l2 ps2 ev2 →
        ev1 = ev2;
      

      atomic_step_valid:
        ∀ i ps ps´ l l´ e eid
               (Hstep: atomic_step i eid ps l ps´ e)
               (Hlog: log_get_atomic l eid = log_get_atomic l´ eid),
          atomic_step i eid ps l´ ps´ e
    }.

End HARDSEMCLASS.

Section HARDSEMSTEP.

  Context `{hdsem: HardSemantics}.
  Context `{pmap: PartialMap}.

  Inductive Owner :=
  | OFREE (s: option shared_piece)
  | OWN (i: Z).

  Inductive hstate: Type :=
  | HState: Z → (pMap private_state core_set) → Log → hstate.

  Inductive local_view :=
  | LView: private_state → Log → local_view.

  Function CalOwner (l: Log) (id: Z):=
    match l with
      | nil ⇒ OFREE None
      | e :: l´ ⇒
        let o:= CalOwner l´ id in
        match e with
          | EACQ from id´ ⇒
            if zeq id id´ then
              match o with
                | OFREE _ ⇒ OWN from
                | _ ⇒ o
              end
            else o
          | EREL from id´ d ⇒
            if zeq id id´ then
              match o with
                | OWN i ⇒
                  if zeq i from then
                    OFREE (Some d)
                  else o
                | _ ⇒ o
              end
            else o
          | _ ⇒ o
        end
    end.

  Inductive hardware_local_step : Z → local_view → local_view → Prop :=
  | hardware_local_exec_step_acq:
      ∀ curid ps ps´ d l id
             (HPC: PC ps (ACQ_SHARED id))
             (Howner: CalOwner l id = OFREE d)
             (Hupdate_s: set_shared ps d ps´),
        hardware_local_step curid (LView ps l) (LView ps´ (EACQ curid id :: nil))

  | hardware_local_exec_step_rel:
      ∀ curid ps ps´ d l id
             (HPC: PC ps (REL_SHARED id))
             (Howner: CalOwner l id = OWN curid)
             (Hupdate_s: get_shared ps d ps´),
        hardware_local_step curid (LView ps l)
                            (LView ps´ (EREL curid id d :: nil))

  | hardware_local_exec_step_private:
      ∀ curid ps ps´ l
             (HPC: PC ps PRIVATE)
             (Hprivate: private_step curid ps ps´),
        hardware_local_step curid (LView ps l)
                            (LView ps´ nil)

  | hardware_local_exec_step_atomic:
      ∀ curid ps ps´ l e id
             (HPC: PC ps (ATOMIC id (atomic_event_ident e)))
             (Hatomic: atomic_step curid id ps l ps´ e),
        hardware_local_step curid (LView ps l)
                            (LView ps´ (EATOMIC curid id e :: nil))
  .

  Lemma hardware_local_exec_step_determ curid lv lv1´ lv2´:
    hardware_local_step curid lv lv1´ →
    hardware_local_step curid lv lv2´ →
    lv1´ = lv2´.
  Proof.
    intros.
    inversion H.
    - inversion H0; subst; inv H5.
      + exploit (PC_determ ps (ACQ_SHARED id) (ACQ_SHARED id0)); eauto; intros; inv H1.
        rewrite Howner0 in Howner; inv Howner.
        exploit (set_shared_determ ps d ps´ ps´0) ; eauto; intros; subst; auto.
      + exploit (PC_determ ps (ACQ_SHARED id) (REL_SHARED id0)); eauto; intros; inv H1.
      + exploit (PC_determ ps (ACQ_SHARED id) PRIVATE); eauto; intros; inv H1.
      + exploit (PC_determ ps (ACQ_SHARED id) (ATOMIC id0 (atomic_event_ident e))); eauto; intros; inv H1.
    - inversion H0; subst; inv H5.
      + exploit (PC_determ ps (REL_SHARED id) (ACQ_SHARED id0)); eauto; intros; inv H1.
      + exploit (PC_determ ps (REL_SHARED id) (REL_SHARED id0)); eauto; intros; inv H1.
        exploit (get_shared_determ ps d ps´ d0 ps´0) ; eauto; intros.
        destruct H1; subst; auto.
      + exploit (PC_determ ps (REL_SHARED id) PRIVATE); eauto; intros; inv H1.
      + exploit (PC_determ ps (REL_SHARED id) (ATOMIC id0 (atomic_event_ident e))); eauto; intros; inv H1.
    - inversion H0; subst; inv H5.
      + exploit (PC_determ ps PRIVATE (ACQ_SHARED id)); eauto; intros; inv H1.
      + exploit (PC_determ ps PRIVATE (REL_SHARED id)); eauto; intros; inv H1.
      + exploit (private_step_determ curid ps ps´ ps´0); eauto; intros; inv H1; auto.
      + exploit (PC_determ ps PRIVATE (ATOMIC id (atomic_event_ident e))); eauto; intros; inv H1.
    - inversion H0; subst; inv H5.
      + exploit (PC_determ ps (ATOMIC id (atomic_event_ident e)) (ACQ_SHARED id0)); eauto; intros; inv H1.
      + exploit (PC_determ ps (ATOMIC id (atomic_event_ident e)) (REL_SHARED id0)); eauto; intros; inv H1.
      + exploit (PC_determ ps (ATOMIC id (atomic_event_ident e)) PRIVATE); eauto; intros; inv H1.
      + exploit (PC_determ ps (ATOMIC id (atomic_event_ident e))
                           (ATOMIC id0 (atomic_event_ident e0))); eauto; intros; inv H1.
        exploit (atomic_step_determ_ps curid id0 ps l ps´ e ps´0 e0); eauto.
        exploit (atomic_step_determ_ev curid id0 ps l l ps´ ps´0 e e0); eauto; intros; subst; auto.
  Qed.

  Inductive hardware_step (start: Z) : hstate → trace → hstate → Prop :=
  | hardware_exec_step_progress:
      ∀ curid curid´ lsp lsp´ ps l l´ l0 ps´
             (Hl0: l0 = EBACK curid´ :: EYIELD curid :: l)
             (Hget_local´ : pget curid´ lsp = Some ps)
             (Hget_local : core_set curid = true)
             (Hlocal: hardware_local_step curid´ (LView ps l0) (LView ps´ l´))
             (Hset_local: lsp´ = pset curid´ ps´ lsp),
        hardware_step start (HState curid lsp l) E0 (HState curid´ lsp´ (l´ ++ l0))
  .

End HARDSEMSTEP.

Section YIELD_BACK.

  Class Fairness :=
    {
      time_bound: nat
    }.

  Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
  Context `{hdsem: HardSemantics (hdset := hdset)}.
  Context `{pmap: PartialMap}.

  Definition back_id_option (e: event) :=
    match e with
      | EBACK curid0 ⇒ Some curid0
      | _ ⇒ None
    end.

  Fixpoint AbsYieldBack (n: nat) (curid: Z) (l res: Log) (oracle: Oracle) :=
    match n with
      | O ⇒ None
      | S n´ ⇒
        match oget (s_set curid) (res ++ l) oracle with
          | Some e ⇒
            let res´ := e :: res in
            let r := AbsYieldBack n´ curid l res´ oracle in
            match back_id_option e with
              | Some curid´ ⇒
                if zeq curid curid´ then Some res´
                else r
              | _ ⇒ r
            end
          | _ ⇒ None
        end
    end.

  Definition log_event_source (e: event) :=
    match e with
      | EACQ i _ ⇒ Some i
      | EREL i _ _ ⇒ Some i
      | EATOMIC i _ _ ⇒ Some i
      | _ ⇒ None
    end.

  Lemma YieldBack_valid_last_event´:
    ∀ n n´ tid l ini_l o l_res,
      (n ≤ n´)%nat →
      valid_log tid (ini_l ++ l) →
      valid_oracle tid (s_set tid) o →
      AbsYieldBack n tid l ini_l o = Some l_res →
      ∃ ev l_res´, l_res = ev::l_res´ ∧ ev = EBACK tid ∧ core_set tid = true.
  Proof.
    induction n; intros; subst.
    - simpl in H2; inv H2.
    - simpl in H2.
      assert (core_set tid = true).
      { inv H0; auto. }
      subdestruct.
      + subst.
        unfold back_id_option in Hdestruct0;
        destruct e; inv Hdestruct0.
        inv H2.
        unfold valid_oracle in H1.
        eapply H1 in H0; eauto.
      + assert ((n ≤ n´)%nat).
        { omega. }
        apply IHn with (n´ := n´) in H2; auto.
        unfold valid_oracle in H1.
        eapply H1; eauto.
      + assert ((n ≤ n´)%nat).
        { omega. }
        apply IHn with (n´ := n´) in H2; auto.
        unfold valid_oracle in H1.
        eapply H1; eauto.
  Qed.

  Lemma YieldBack_valid_last_event:
    ∀ n tid l ini_l o l_res,
      valid_log tid (ini_l ++ l) →
      valid_oracle tid (s_set tid) o →
      AbsYieldBack n tid l ini_l o = Some l_res →
      ∃ ev l_res´, l_res = ev::l_res´ ∧ ev = EBACK tid ∧ core_set tid = true.
  Proof.
    intros; eapply YieldBack_valid_last_event´; eauto.
  Qed.

  Lemma YieldBack_satisfies_valid_log´:
    ∀ n n´ tid l l_init o l_res,
      (n ≤ n´)%nat →
      valid_log tid (l_init ++ l) →
      valid_oracle tid (s_set tid) o →
      AbsYieldBack n tid l l_init o = Some l_res →
      valid_log tid (l_res ++ l).
  Proof.
    induction n; intros; subst.
    - simpl in H2; inv H2; auto.
    - simpl in H2.
      assert (core_set tid = true).
      { inv H0; auto. }
      subdestruct.
      + subst; inv H2.
        simpl; unfold back_id_option in Hdestruct0;
          destruct e; inv Hdestruct0.
        unfold valid_oracle in H1.
        eapply H1 in H0; eauto.
        destruct H0.
        simpl in H2.
        auto.
      + assert ((n ≤ n´)%nat).
        { omega. }
        apply IHn with (n´ := n´) in H2; auto.
        unfold valid_oracle in H1.
        generalize (H1 (l_init++l) e H0 Hdestruct); intros.
        destruct H5; eauto.
      + assert ((n ≤ n´)%nat).
        { omega. }
        apply IHn with (n´ := n´) in H2; auto.
        unfold valid_oracle in H1.
        generalize (H1 (l_init++l) e H0 Hdestruct); intros.
        destruct H5; eauto.
  Qed.

  Lemma YieldBack_satisfies_valid_log:
    ∀ n tid l l_init o l_res,
      valid_log tid (l_init ++ l) →
      valid_oracle tid (s_set tid) o →
      AbsYieldBack n tid l l_init o = Some l_res →
      valid_log tid (l_res ++ l).
  Proof.
    intros; eapply YieldBack_satisfies_valid_log´; eauto.
  Qed.

  Definition valid_oracle_members (tid : Z) (l : Log) :=
    ∀ ev, In ev l → event_source ev ≠ tid.

  Lemma valid_log_last_valid_log:
    ∀ tid l ev l´,
      valid_log tid l →
      l = ev::l´ →
      valid_log tid l´.
  Proof.
    intros; subst.
    inv H; auto.
  Qed.

  Lemma valid_log_prefix_valid_log:
    ∀ tid l1 l l2,
      valid_log tid l →
      l = l1 ++ l2 →
      valid_log tid l2.
  Proof.
    induction l1; simpl in *; subst.
    - intros; simpl.
      rewrite <- H0; auto.
    - intros.
      destruct l; try inv H0.
      remember (l1 ++ l2) as l´.
      assert (valid_log tid l´).
      eapply valid_log_last_valid_log; eauto.
      eapply IHl1 in H0; eauto.
  Qed.

  Lemma YieldBack_prefix´:
    ∀ n n´ tid l init_l o res,
      (n ≤ n´)%nat →
      AbsYieldBack n tid l init_l o = Some res →
      ∃ l´, res = l´ ++ init_l.
  Proof.
    induction n; intros; subst.
    - inv H0.
    - assert ((n ≤ n´)%nat) by omega.
      simpl in H0.
      subdestruct.
      + inv H0.
        ∃ (e::nil); simpl; auto.
      + eapply IHn with (n´ := n´) in H0; auto.
        destruct H0.
        ∃ (x++e::nil).
        rewrite H0.
        rewrite app_assoc_reverse.
        simpl; auto.
      + eapply IHn with (n´ := n´) in H0; auto.
        destruct H0.
        ∃ (x++e::nil).
        rewrite H0.
        rewrite app_assoc_reverse.
        simpl; auto.
  Qed.

  Lemma YieldBack_prefix:
    ∀ n tid l init_l o res,
      AbsYieldBack n tid l init_l o = Some res →
      ∃ l´, res = l´ ++ init_l.
  Proof.
    intros.
    eapply YieldBack_prefix´; eauto.
  Qed.

  Lemma YieldBack_satisfies_valid_oracle_members:
    ∀ n tid l l_init o l_res,
      valid_log tid (l_init ++ l) →
      valid_oracle tid (s_set tid) o →
      AbsYieldBack n tid l l_init o = Some l_res →
      valid_oracle_members tid l_init →
      valid_oracle_members tid l_res.
  Proof.
    induction n.
    - intros.
      simpl in H1.
      inv H1.
    - intros.
      exploit YieldBack_satisfies_valid_log; eauto; intros.
      simpl in H1.
      subdestruct; inv H1.
      + unfold back_id_option in Hdestruct0.
        unfold valid_oracle in H0.
        eapply H0 in H; eauto; clear H0.
        destruct H.
        apply s_set_not_in_imply in H.
        unfold valid_oracle_members in ×.
        intros.
        simpl in H1.
        destruct H1; subst; auto.
      + assert (valid_oracle_members tid (e::l_init)).
        { unfold valid_oracle in H0.
          eapply H0 in Hdestruct; eauto.
          destruct Hdestruct.
          apply s_set_not_in_imply in H1.
          unfold valid_oracle_members in ×.
          intros.
          simpl in H6; destruct H6; subst; auto. }
        eapply IHn in H5; eauto.
        simpl.
        unfold back_id_option in Hdestruct0; simpl.
        destruct e; try (inv Hdestruct0; fail).
        inv Hdestruct0.
        assert (∃ l´, l_res = l´ ++ EBACK z :: l_init).
        { eapply YieldBack_prefix; eauto. }
        destruct H4.
        rewrite H4 in H3.
        rewrite app_assoc_reverse in H3.
        remember ((EBACK z :: l_init) ++ l) as l´.
        remember (x ++ l´) as l2.
        eapply valid_log_prefix_valid_log in Heql2; eauto.
        subst; auto.
      + assert (valid_oracle_members tid (e::l_init)).
        { unfold valid_oracle in H0.
          eapply H0 in Hdestruct; eauto.
          destruct Hdestruct.
          apply s_set_not_in_imply in H1.
          unfold valid_oracle_members in ×.
          intros.
          simpl in H6; destruct H6; subst; auto. }
        eapply IHn in H5; eauto.
        simpl.
        unfold back_id_option in Hdestruct0; simpl.
        destruct e; try (inv Hdestruct0; fail).
        × inv Hdestruct0.
          assert (∃ l´, l_res = l´ ++ EYIELD from :: l_init).
          { eapply YieldBack_prefix; eauto. }
          destruct H4.
          rewrite H4 in H3.
          rewrite app_assoc_reverse in H3.
          remember ((EYIELD from :: l_init) ++ l) as l´.
          remember (x ++ l´) as l2.
          eapply valid_log_prefix_valid_log in Heql2; eauto.
          subst; auto.
        × inv Hdestruct0.
          assert (∃ l´, l_res = l´ ++ EACQ from id :: l_init).
          { eapply YieldBack_prefix; eauto. }
          destruct H4.
          rewrite H4 in H3.
          rewrite app_assoc_reverse in H3.
          remember ((EACQ from id :: l_init) ++ l) as l´.
          remember (x ++ l´) as l2.
          eapply valid_log_prefix_valid_log in Heql2; eauto.
          subst; auto.
        × inv Hdestruct0.
          assert (∃ l´, l_res = l´ ++ EREL from id d :: l_init).
          { eapply YieldBack_prefix; eauto. }
          destruct H4.
          rewrite H4 in H3.
          rewrite app_assoc_reverse in H3.
          remember ((EREL from id d :: l_init) ++ l) as l´.
          remember (x ++ l´) as l2.
          eapply valid_log_prefix_valid_log in Heql2; eauto.
          subst; auto.
        × inv Hdestruct0.
          assert (∃ l´, l_res = l´ ++ EATOMIC from id e :: l_init).
          { eapply YieldBack_prefix; eauto. }
          destruct H4.
          rewrite H4 in H3.
          rewrite app_assoc_reverse in H3.
          remember ((EATOMIC from id e :: l_init) ++ l) as l´.
          remember (x ++ l´) as l2.
          eapply valid_log_prefix_valid_log in Heql2; eauto.
          subst; auto.
  Qed.

  Definition valid_cache_log_members (tid : Z) (l : Log) :=
    ∀ ev, In ev l → event_source ev ≠ tid ∨ GetEvTy ev = YIELDTY.

End YIELD_BACK.


Section ORACLESTEP.

  Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
  Context `{hdsem: HardSemantics (hdset := hdset)}.
  Context `{pmap: PartialMap}.

  Inductive local_state: Type :=
  | LState: private_state → bool → local_state.

  Inductive state: Type :=
  | State: Z → (pMap local_state core_set) → Log → state.

  Inductive oracle_step (oracle: Oracle): state → trace → state → Prop :=
  | oracle_exec_step_progress:
      ∀ curid lsp lsp´ ps l l´ ps´
             (Hget_local : pget curid lsp = Some (LState ps false))
             (Hlocal: hardware_local_step curid (LView ps l) (LView ps´ l´))
             (Hset_local: lsp´ = pset curid (LState ps´ true) lsp),
        oracle_step oracle (State curid lsp l) E0 (State curid lsp´ (l´ ++ l))
                      
  | oracle_exec_step_yield_pos:
      ∀ curid curid´ lsp lsp´ ps l l´ l0
             (Hl0: l0 = EYIELD curid :: l)
             (Hl1: l´ = EBACK curid´ :: l0)
             (Hget_local : pget curid lsp = Some (LState ps true))
             (Hset_local: lsp´ = pset curid (LState ps false) lsp)
             (Horacle: oget core_set l0 oracle = Some (EBACK curid´)),
        oracle_step oracle (State curid lsp l) E0 (State curid´ lsp´ l´).

  Lemma oracle_step_determ oracle s t1 s1 t2 s2:
    oracle_step oracle s t1 s1 →
    oracle_step oracle s t2 s2 →
    t1 = E0 ∧ t2 = E0 ∧ s1 = s2.
  Proof.
    intros.
    inv H.
    - inv H0; subst.
      + refine_split; eauto.
        rewrite Hget_local in Hget_local0; inv Hget_local0.
        eapply (hardware_local_exec_step_determ curid) in Hlocal0; eauto.
        inv Hlocal0; auto.
      + rewrite Hget_local in Hget_local0.
        inv Hget_local0.
    - inv H0; subst.
      + rewrite Hget_local in Hget_local0.
        inv Hget_local0.
      + refine_split; eauto.
        rewrite Horacle in Horacle0.
        inv Horacle0.
        rewrite Hget_local in Hget_local0.
        inv Hget_local0; auto.
  Qed.

  Definition state_log_len (s: state) :=
    match s with
      | State _ _ l ⇒ list_Len l
    end.

  Definition get_lv_val (pv : local_state) :=
    match pv with
    | (LState lv b) ⇒ lv
    end.

  Definition get_b_val (pv : local_state) : bool :=
    match pv with
    | (LState _ b) ⇒ b
    end.

End ORACLESTEP.


Section ENV.

  Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
  Context `{hdsem: HardSemantics (hdset := hdset)}.
  Context `{pmap: PartialMap}.

  Inductive estate {A: ZSet}: Type :=
  | EState: Z → (pMap local_state A) → Log → estate.

  Definition back_id (curid: Z) (e: event) :=
    match e with
      | EBACK curid0 ⇒ curid0
      | EYIELD _ ⇒ sched_id
      | _ ⇒ curid
    end.

  Definition measure (l : Log) : nat :=
    match lastEvTy l with
    | Some YIELDTY ⇒ O
    | _ ⇒ S O
    end.

  Definition state_measure (A : ZSet) (est : estate (A := A)) :=
    match est with
    | EState _ _ l ⇒ measure l
    end.

  Definition est_curid (A : ZSet) (st : estate (A:= A)) : Z :=
    match st with
    | EState curid _ _ ⇒ curid
    end.

  Definition get_b_val_op (A : ZSet) (curid : Z) (lsp : pMap local_state A) :=
    match pget curid lsp with
    | Some lv ⇒ Some (get_b_val lv)
    | None ⇒ None
    end.

  Definition est_get_b_val_op (A : ZSet) (curid : Z) (est: (estate (A := A))) :=
    match est with
    | (EState _ lsp _) ⇒ get_b_val_op A curid lsp
    end.

  Definition est_ps (A : ZSet) (est: (estate (A := A))) :=
    match est with
    | (EState curid lsp _) ⇒ pget curid lsp
    end.

  Definition est_lsp (A : ZSet) (est: (estate (A := A))) :=
    match est with
    | (EState curid lsp _) ⇒ lsp
    end.

  Definition est_ps_bool (A : ZSet) (est: (estate (A := A))) :=
    match est with
    | (EState curid lsp _) ⇒ match pget curid lsp with
                             | Some pv ⇒ Some (get_b_val pv)
                             | _ ⇒ None
                             end
    end.

  Definition est_ps_lv (A : ZSet) (est: (estate (A := A))) :=
    match est with
    | (EState curid lsp _) ⇒ match pget curid lsp with
                             | Some pv ⇒ Some (get_lv_val pv)
                             | _ ⇒ None
                             end
    end.


  Definition est_log (A : ZSet) (est: (estate (A := A))) :=
    match est with
    | (EState _ _ l) ⇒ l
    end.


  Function is_env_local_event (e: event) :=
    match e with
    | EACQ _ _ ⇒ True
    | EREL _ _ _ ⇒ True
    | EATOMIC _ _ _ ⇒ True
    | _ ⇒ False
    end.

  Inductive env_step {A: ZSet} (oracle: Oracle): (estate (A:= A)) → trace → (estate (A:= A)) → Prop :=
  | env_exec_step_progress:
      ∀ curid lsp lsp´ ps l l´ ps´
             (Hget_local : pget curid lsp = Some (LState ps false))
             (Hlocal: hardware_local_step curid (LView ps l) (LView ps´ l´))
             (Hset_local: lsp´ = pset curid (LState ps´ true) lsp),
        env_step oracle (EState curid lsp l) E0 (EState curid lsp´ (l´ ++ l))
                      
  | env_exec_step_yield_pos:
      ∀ curid curid´ lsp lsp´ ps l l´ l0
             (Hl0: l0 = EYIELD curid :: l)
             (Hl1: l´ = EBACK curid´ :: l0)
             (Hget_local : pget curid lsp = Some (LState ps true))
             (Hset_local: lsp´ = pset curid (LState ps false) lsp)
             (Horacle: oget A l0 oracle = Some (EBACK curid´)),
        env_step oracle (EState curid lsp l) E0 (EState curid´ lsp´ l´)

  | env_exec_step_skip:
      ∀ curid curid´ lsp l l´ e
             (Hl´: l´ = e :: l)
             (Hget_local : pget curid lsp = None)
             (Horacle: oget A l oracle = Some e)
             (Hcurid´: curid´ = back_id curid e),
        env_step oracle (EState curid lsp l) E0 (EState curid´ lsp l´).

  Section determ.

    Variable cores: ZSet.

    Lemma env_step_determ oracle s t1 s1 t2 s2:
      env_step (A := cores) oracle s t1 s1 →
      env_step (A := cores) oracle s t2 s2 →
      t1 = E0 ∧ t2 = E0 ∧ s1 = s2.
    Proof.
      intros.
      inv H.
      - inv H0; subst.
        + refine_split; eauto.
          rewrite Hget_local in Hget_local0; inv Hget_local0.
          eapply (hardware_local_exec_step_determ curid) in Hlocal0; eauto.
          inv Hlocal0; auto.
        + rewrite Hget_local in Hget_local0.
          inv Hget_local0.
        + rewrite Hget_local in Hget_local0.
          inv Hget_local0.
      - inv H0; subst.
        + rewrite Hget_local in Hget_local0.
          inv Hget_local0.
        + refine_split; eauto.
          rewrite Horacle in Horacle0.
          inv Horacle0.
          rewrite Hget_local in Hget_local0.
          inv Hget_local0.
          auto.
        + rewrite Hget_local in Hget_local0.
          inv Hget_local0.
      - inv H0.
        + rewrite Hget_local in Hget_local0.
          inv Hget_local0.
        + rewrite Hget_local in Hget_local0.
          inv Hget_local0.
        + rewrite Horacle in Horacle0.
          inv Horacle0.
          refine_split; eauto.
    Qed.

  End determ.


  Section STAR_E0.

    Lemma env_step_E0:
      ∀ {A: ZSet} o s1 t s2,
        env_step (A:= A) o s1 t s2 →
        t = E0.
    Proof.
      intros. inv H; trivial.
    Qed.

    Lemma star_env_step_E0:
      ∀ {A: ZSet} o s1 t s2,
        star (env_step (A:= A)) o s1 t s2 →
        t = E0.
    Proof.
      intro. induction 1.
      - trivial.
      - eapply env_step_E0 in H. subst. trivial.
    Qed.

  End STAR_E0.

  Lemma hardware_local_step_event:
    ∀ curid ps ps´ l l´,
      hardware_local_step curid (LView ps l) (LView ps´ l´) →
      l´ = nil ∨ (∃ e, is_env_local_event e ∧ l´ = e :: nil).
  Proof.
    intros. inv H; eauto.
    - right. refine_split´; eauto. simpl; trivial.
    - right. refine_split´; eauto. simpl; trivial.
      - right. refine_split´; eauto. simpl; trivial.
  Qed.

  Lemma one_step_event:
    ∀ {A: ZSet} o curid curid´ rsm rsm´ l l´ t,
      env_step (A:= A) o (EState curid rsm l) t (EState curid´ rsm´ l´) →
      l´ = l ∨ (∃ l0, l´ = l0 ++ l).
  Proof.
    intros. inv H.
    - eapply hardware_local_step_event in Hlocal; eauto.
    - right.
      ∃ (EBACK curid´ :: EYIELD curid ::nil). trivial.
    - right.
      ∃ (e ::nil). trivial.
  Qed.

End ENV.


Section SINGLE.

  Context `{op: OracleProp (ret:= event) (log := Log) (log_len := list_Len)}.
  Context `{hdsem: HardSemantics (hdset:= hdset)}.
  Context `{pmap: PartialMap}.

  Inductive single_state: Type :=
  | SState: Z → local_state → Log → single_state.

  Inductive single_step (curid: Z) (oracle: Oracle): single_state → trace → single_state → Prop :=
  | single_exec_step_progress:
      ∀ ps l l´ ps´
             (Hlocal: hardware_local_step curid (LView ps l) (LView ps´ l´)),
       single_step curid oracle (SState curid (LState ps false) l) E0
                   (SState curid (LState ps´ true) (l´ ++ l))
                      
  | single_exec_step_yield_pos:
      ∀ curid´ ps l l´ l0
             (Hl0: l0 = EYIELD curid :: l)
             (Hl1: l´ = EBACK curid´ :: l0)
             (Horacle: oget (s_set curid) l0 oracle = Some (EBACK curid´)),
        single_step curid oracle (SState curid (LState ps true) l) E0
                    (SState curid´ (LState ps false) l´)

  | single_exec_step_skip:
      ∀ curid´ curid0 l l´ e ls
             (Hl´: l´ = e :: l)
             (Hget_local : curid´ ≠ curid)
             (Horacle: oget (s_set curid) l oracle = Some e)
             (Hcurid´: curid0 = back_id curid´ e),
        single_step curid oracle (SState curid´ ls l) E0 (SState curid0 ls l´).

  Lemma single_step_determ curid oracle s t1 s1 t2 s2:
    single_step curid oracle s t1 s1 →
    single_step curid oracle s t2 s2 →
    t1 = E0 ∧ t2 = E0 ∧ s1 = s2.
  Proof.
    intros.
    inv H.
    - inv H0; subst.
      + refine_split; eauto.
        eapply (hardware_local_exec_step_determ curid (LView ps l) (LView ps´ l´) (LView ps´0 l´0)
                                                 Hlocal) in Hlocal0.
        inv Hlocal0.
        auto.
      + elim Hget_local; auto.
    - inv H0; subst.
      + rewrite Horacle in Horacle0.
        inv Horacle0.
        refine_split; eauto.
      + elim Hget_local; eauto.
    - inv H0; subst.
      + elim Hget_local; eauto.
      + elim Hget_local; eauto.
      + rewrite Horacle in Horacle0.
        inv Horacle0.
        refine_split; eauto.
  Qed.

End SINGLE.

Section SINGLE_BIG.

  Context `{op: OracleProp(ret:= event) (log:= Log) (log_len := list_Len)}.
  Context `{hdsem: HardSemantics (hdset:= hdset)}.
  Context `{pmap: PartialMap}.
  Context `{fair: Fairness}.

  Inductive single_big_step (curid: Z) (oracle: Oracle): single_state → trace → single_state → Prop :=
  | single_exec_step_progress_big:
      ∀ ps l l´ ps´
             (Hlocal: hardware_local_step curid (LView ps l) (LView ps´ l´)),
       single_big_step curid oracle (SState curid (LState ps false) l) E0
                       (SState curid (LState ps´ true) (l´ ++ l))
                      
  | single_exec_step_yield_pos_big:
      ∀ ps l l´ l0
             (Hl0: l0 = EYIELD curid :: l)
             (Hl1: AbsYieldBack time_bound curid l0 nil oracle = Some l´),
        single_big_step curid oracle (SState curid (LState ps true) l) E0
                        (SState curid (LState ps false) (l´ ++ l0)).

  Lemma big_step_determ curid oracle s t1 s1 t2 s2:
    single_big_step curid oracle s t1 s1 →
    single_big_step curid oracle s t2 s2 →
    t1 = E0 ∧ t2 = E0 ∧ s1 = s2.
  Proof.
    intros.
    inv H.
    - inv H0; subst.
      + refine_split; eauto.
        eapply (hardware_local_exec_step_determ curid (LView ps l) (LView ps´ l´) (LView ps´0 l´0)
                                                 Hlocal) in Hlocal0.
        inv Hlocal0.
        reflexivity.
    - inv H0; subst.
      rewrite Hl1 in Hl2; inv Hl2.
      refine_split; eauto.
  Qed.

End SINGLE_BIG.

Section SINGLE_BIG2.

  Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
  Context `{hdsem: HardSemantics (hdset:= hdset)}.
  Context `{pmap: PartialMap}.
  Context `{fair: Fairness}.

  Inductive rstate: Type :=
  | RState: private_state → Log → rstate.

  Inductive single_big2_step (curid: Z) (oracle: Oracle): rstate → trace → rstate → Prop :=
  | single_exec_step_progress_big2:
      ∀ ps l l0 l1 l´ ps´
             (Hl0: l0 = EYIELD curid :: l)
             (Hl1: AbsYieldBack time_bound curid l0 nil oracle = Some l1)
             (Hlocal: hardware_local_step curid (LView ps (l1 ++ l0)) (LView ps´ l´)),
       single_big2_step curid oracle (RState ps l) E0
                       (RState ps´ (l´ ++ l1 ++ l0)).

  Lemma big2_step_determ curid oracle s t1 s1 t2 s2:
    single_big2_step curid oracle s t1 s1 →
    single_big2_step curid oracle s t2 s2 →
    t1 = E0 ∧ t2 = E0 ∧ s1 = s2.
  Proof.
    intros.
    inv H.
    inv H0.
    rewrite Hl1 in Hl2; inv Hl2.
    eapply (hardware_local_exec_step_determ curid (LView ps (l3 ++ EYIELD curid :: l))
                                            (LView ps´ l´) (LView ps´0 l´0)
                                            Hlocal) in Hlocal0.
    inv Hlocal0.
    auto.
  Qed.

End SINGLE_BIG2.

Section SINGLE_SPLIT.

  Context `{op: OracleProp (ret:= event) (log:= Log) (log_len := list_Len)}.
  Context `{hdsem: HardSemantics (hdset:= hdset)}.
  Context `{pmap: PartialMap}.
  Context `{fair: Fairness}.

  Inductive single_local_view :=
  | SView: private_state → single_local_view.

  Inductive single_local_step : Z → single_local_view → single_local_view → Prop :=

  | single_local_exec_step_private:
      ∀ curid ps ps´
             (HPC: PC ps PRIVATE)
             (Hprivate: private_step curid ps ps´),
        single_local_step curid (SView ps)
                       (SView ps´).

  Lemma single_local_step_determ curid lv lv1´ lv2´:
    single_local_step curid lv lv1´ →
    single_local_step curid lv lv2´ →
    lv1´ = lv2´.
  Proof.
    destruct 1;
      inversion 1.
    f_equal.
    eapply private_step_determ; eauto.
  Qed.

  Inductive single_log_step : Z → local_view → local_view → Prop :=
  | single_local_exec_step_acq:
      ∀ curid ps ps´ d l id
             (HPC: PC ps (ACQ_SHARED id))
             (Howner: CalOwner l id = OFREE d)
             (Hupdate_s: set_shared ps d ps´),
        single_log_step curid (LView ps l)
                       (LView ps´ (EACQ curid id :: nil))

  | single_local_exec_step_rel:
      ∀ curid ps ps´ d l id
             (HPC: PC ps (REL_SHARED id))
             (Howner: CalOwner l id = OWN curid)
             (Hupdate_s: get_shared ps d ps´),
        single_log_step curid (LView ps l)
                       (LView ps´ (EREL curid id d :: nil))

  | single_local_exec_step_atomic:
      ∀ curid ps ps´ l e id
             (HPC: PC ps (ATOMIC id (atomic_event_ident e)))
             (Hatomic: atomic_step curid id ps l ps´ e),
        single_log_step curid (LView ps l)
                       (LView ps´ (EATOMIC curid id e :: nil))
  .

  Lemma single_log_step_determ curid lv lv1´ lv2´:
    single_log_step curid lv lv1´ →
    single_log_step curid lv lv2´ →
    lv1´ = lv2´.
  Proof.
    intros.
    inversion H.
    - inversion H0; subst; inv H5.
      + exploit (PC_determ ps (ACQ_SHARED id) (ACQ_SHARED id0)); eauto; intros; inv H1.
        rewrite Howner0 in Howner; inv Howner.
        exploit (set_shared_determ ps d ps´ ps´0) ; eauto; intros; subst; auto.
      + exploit (PC_determ ps (ACQ_SHARED id) (REL_SHARED id0)); eauto; intros; inv H1.
      + exploit (PC_determ ps (ACQ_SHARED id) (ATOMIC id0 (atomic_event_ident e))); eauto; intros; inv H1.
    - inversion H0; subst; inv H5.
      + exploit (PC_determ ps (REL_SHARED id) (ACQ_SHARED id0)); eauto; intros; inv H1.
      + exploit (PC_determ ps (REL_SHARED id) (REL_SHARED id0)); eauto; intros; inv H1.
        exploit (get_shared_determ ps d ps´ d0 ps´0) ; eauto.
        intros; destruct H1; subst; auto.
      + exploit (PC_determ ps (REL_SHARED id) (ATOMIC id0 (atomic_event_ident e))); eauto; intros; inv H1.
    - inversion H0; subst; inv H5.
      + exploit (PC_determ ps (ATOMIC id (atomic_event_ident e)) (ACQ_SHARED id0)); eauto; intros; inv H1.
      + exploit (PC_determ ps (ATOMIC id (atomic_event_ident e)) (REL_SHARED id0)); eauto; intros; inv H1.
      + exploit (PC_determ ps (ATOMIC id (atomic_event_ident e))
                           (ATOMIC id0 (atomic_event_ident e0))); eauto; intros; inv H1.
        exploit (atomic_step_determ_ps curid id0 ps l ps´ e ps´0 e0); eauto.
        exploit (atomic_step_determ_ev curid id0 ps l l ps´ ps´0 e e0); eauto.
        intros; subst; auto.
  Qed.

  Inductive srstate: Type :=
  | SRState (ps: private_state) (l: Log) (al: Log).

  Inductive single_split_step (curid: Z) (oracle: Oracle): srstate → trace → srstate → Prop :=
  | single_exec_step_progress_split_local:
      ∀ ps l l0 l1 al al0 ps´
             (Hal0: al0 = EYIELD curid :: al)
             (Hl0: l0 = al0 ++ l)
             (Hl1: AbsYieldBack time_bound curid l0 nil oracle = Some l1)
             (Hlocal: single_local_step curid (SView ps) (SView ps´)),
        single_split_step curid oracle (SRState ps l al) E0
                          (SRState ps´ l (l1 ++ al0))

  | single_exec_step_progress_split_log:
      ∀ ps l l0 l1 l´ al ps´
             (Hl0: l0 = EYIELD curid :: al ++ l)
             (Hl1: AbsYieldBack time_bound curid l0 nil oracle = Some l1)
             (Hlocal: single_log_step curid (LView ps (l1 ++ l0)) (LView ps´ l´)),
       single_split_step curid oracle (SRState ps l al) E0
                         (SRState ps´ (l´ ++ l1 ++ l0) nil).

  Lemma single_split_determ curid oracle s t1 s1 t2 s2:
    single_split_step curid oracle s t1 s1 →
    single_split_step curid oracle s t2 s2 →
    t1 = E0 ∧ t2 = E0 ∧ s1 = s2.
  Proof.
    intros.
    inv H.
    - inv H0; subst.
      + refine_split; eauto.
        rewrite Hl1 in Hl2; inv Hl2.
        eapply (single_local_step_determ curid (SView ps) (SView ps´) (SView ps´0)) in Hlocal0; eauto.
        inv Hlocal0.
        auto.
      + simpl in ×.
        rewrite Hl1 in Hl2; inv Hl2.
        inv Hlocal0; inv Hlocal.
        × exploit (PC_determ ps (ACQ_SHARED id) PRIVATE); eauto; intros; inv H.
        × exploit (PC_determ ps (REL_SHARED id) PRIVATE); eauto; intros; inv H.
        × exploit (PC_determ ps (ATOMIC id (atomic_event_ident e)) PRIVATE); eauto; intros; inv H.
    - inv H0.
      + inv Hlocal0; inv Hlocal.
        × exploit (PC_determ ps (ACQ_SHARED id) PRIVATE); eauto; intros; inv H.
        × exploit (PC_determ ps (REL_SHARED id) PRIVATE); eauto; intros; inv H.
        × exploit (PC_determ ps (ATOMIC id (atomic_event_ident e)) PRIVATE); eauto; intros; inv H.
      + rewrite Hl1 in Hl2; inv Hl2.
        eapply (single_log_step_determ curid (LView ps (l3 ++ EYIELD curid :: al ++ l))
                                       (LView ps´0 l´0) (LView ps´ l´)) in Hlocal; eauto.
        inv Hlocal.
        auto.
  Qed.

End SINGLE_SPLIT.

Section SINGLE_REORDER.

  Context `{op: OracleProp (ret:= Log) (log:= Log) (log_len := list_Len)}.
  Context `{hdsem: HardSemantics (hdset:= hdset)}.
  Context `{pmap: PartialMap}.
  Context `{fair: Fairness}.

  Inductive single_reorder_step (curid: Z) (oracle: Oracle): rstate → trace → rstate → Prop :=
  | single_exec_step_progress_reorder_local:
      ∀ ps l ps´
             (Hlocal: single_local_step curid (SView ps) (SView ps´)),
        single_reorder_step curid oracle (RState ps l) E0
                          (RState ps´ l)

  | single_exec_step_progress_reorder_log:
      ∀ ps l l0 l´ ps´
             (Hl0: oget (s_set curid) l oracle = Some l0)
             (Hlocal: single_log_step curid (LView ps (l0 ++ l)) (LView ps´ l´)),
        single_reorder_step curid oracle (RState ps l) E0
                         (RState ps´ (l´ ++ l0 ++ l)).

  Lemma single_reorder_determ curid oracle s t1 s1 t2 s2:
    single_reorder_step curid oracle s t1 s1 →
    single_reorder_step curid oracle s t2 s2 →
    t1 = E0 ∧ t2 = E0 ∧ s1 = s2.
  Proof.
    intros.
    inv H.
    - inv H0; subst.
      + refine_split; eauto.
        eapply (single_local_step_determ curid (SView ps) (SView ps´) (SView ps´0)) in Hlocal0; eauto.
        inv Hlocal0.
        auto.
      + inv Hlocal0; inv Hlocal.
        × exploit (PC_determ ps (ACQ_SHARED id) PRIVATE); eauto; intros; inv H.
        × exploit (PC_determ ps (REL_SHARED id) PRIVATE); eauto; intros; inv H.
        × exploit (PC_determ ps (ATOMIC id (atomic_event_ident e)) PRIVATE); eauto; intros; inv H.
    - inv H0.
      + inv Hlocal0; inv Hlocal.
        × exploit (PC_determ ps (ACQ_SHARED id) PRIVATE); eauto; intros; inv H.
        × exploit (PC_determ ps (REL_SHARED id) PRIVATE); eauto; intros; inv H.
        × exploit (PC_determ ps (ATOMIC id (atomic_event_ident e)) PRIVATE); eauto; intros; inv H.
      + rewrite Hl0 in Hl1.
        inv Hl1.
        eapply (single_log_step_determ curid (LView ps (l2 ++ l))
                                       (LView ps´0 l´0) (LView ps´ l´)) in Hlocal; eauto.
        inv Hlocal.
        auto.
  Qed.

  Fixpoint reduce_log (l: Log) :=
    match l with
      | nil ⇒ nil
      | e :: l´ ⇒
        match log_event_source e with
          | None ⇒ (reduce_log l´)
          | _ ⇒ e :: (reduce_log l´)
        end
    end.

  Lemma match_log_CalOwner:
    ∀ l id,
      CalOwner l id = CalOwner (reduce_log l) id.
  Proof.
    induction l; simpl; intros; trivial.
    destruct a; simpl; try congruence.
    + rewrite IHl. trivial.
    + rewrite IHl. trivial.
  Qed.

  Lemma match_log_get_atomic:
    ∀ l id,
      log_get_atomic l id = log_get_atomic (reduce_log l) id.
  Proof.
    induction l; simpl; intros; trivial.
    destruct a; simpl; try congruence;
    (destruct (zeq id id0); simpl; try congruence).
  Qed.

  Lemma single_log_log_imply1:
    ∀ tid l l´ ps ps´
           (Hlocal : single_log_step tid (LView ps l) (LView ps´ l´)),
      single_log_step tid (LView ps (reduce_log l)) (LView ps´ l´).
  Proof.
    intros. inv Hlocal; econstructor; eauto.
    - erewrite <- match_log_CalOwner; eauto.
    - erewrite <- match_log_CalOwner; eauto.
    - eapply atomic_step_valid; eauto.
      eapply match_log_get_atomic; eauto.
  Qed.

  Lemma single_log_log_imply2:
    ∀ tid l l´ ps ps´
      (Hlocal: single_log_step tid (LView ps (reduce_log l)) (LView ps´ l´)),
      single_log_step tid (LView ps l) (LView ps´ l´).
  Proof.
    intros. inv Hlocal.
    - erewrite <- match_log_CalOwner in Howner; eauto.
      econstructor; eauto.
    - erewrite <- match_log_CalOwner in Howner; eauto.
      econstructor; eauto.
    - assert (log_get_atomic l id = log_get_atomic (reduce_log l) id).
      { eapply match_log_get_atomic; eauto. }
      econstructor; eauto.
      symmetry in H.
      eapply atomic_step_valid in H; eauto.
  Qed.

  Lemma single_log_log_imply3:
    ∀ tid l l´ ps ps´
      (Hlocal : single_log_step tid (LView ps l) (LView ps´ l´)),
      l´ = reduce_log l´.
  Proof.
    intros; subst.
    inversion Hlocal; simpl; auto.
  Qed.

  Lemma reduce_log_reduce_log_eq:
    ∀ l,
      reduce_log l = reduce_log (reduce_log l).
  Proof.
    induction l; simpl; auto.
    destruct a; simpl in *; try (f_equal; auto; fail); auto.
  Qed.

  Lemma reduce_log_split:
    ∀ l1 l2,
      reduce_log (l1 ++ l2) = reduce_log (l1) ++ reduce_log (l2).
  Proof.
    induction l1; simpl; trivial; intros.
    destruct (log_event_source a); eauto.
    rewrite <- app_comm_cons.
    rewrite IHl1. trivial.
  Qed.

End SINGLE_REORDER.

Section SINGLE_SEPERATE.

  Context `{hdset: HardWaredSetting}.

  Inductive separate_event :=
  | SEACQ (from: Z)
  | SEREL (from: Z) (d: shared_piece)
  | SEATOMIC (from: Z) (e: atomic_event).

  Definition separate_log_type := list separate_event.

  Definition separate_log := ZMap.t separate_log_type.

  Context `{op: OracleProp (ret:= separate_log_type)
                           (log:= Z × separate_log_type × ident) (hdset := hdset)}.
  Context `{hdsem: HardSemantics (hdset := hdset)}.
  Context `{pmap: PartialMap}.
  Context `{fair: Fairness}.

  Inductive sp_state: Type :=
  | SPState: private_state → separate_log → sp_state.

  Inductive separate_log_step : Z → Z → local_view → private_state → separate_event → Prop :=
  | separate_local_exec_step_acq:
      ∀ curid ps ps´ d l id
             (HPC: PC ps (ACQ_SHARED id))
             (Howner: CalOwner l id = OFREE d)
             (Hupdate_s: set_shared ps d ps´),
        separate_log_step curid id (LView ps l)
                          ps´ (SEACQ curid)

  | separate_local_exec_step_rel:
      ∀ curid ps ps´ d l id
             (HPC: PC ps (REL_SHARED id))
             (Howner: CalOwner l id = OWN curid)
             (Hupdate_s: get_shared ps d ps´),
        separate_log_step curid id (LView ps l)
                          ps´ (SEREL curid d)

  | separate_local_exec_step_atomic:
      ∀ curid ps ps´ l e id
             (HPC: PC ps (ATOMIC id (atomic_event_ident e)))
             (Hatomic: atomic_step curid id ps l ps´ e),
        separate_log_step curid id (LView ps l)
                          ps´ (SEATOMIC curid e)
  .

  Function separate_event_2_event (e: separate_event) (id: Z) :=
    match e with
    | SEACQ from ⇒ EACQ from id
    | SEREL from d ⇒ EREL from id d
    | SEATOMIC from e ⇒ EATOMIC from id e
    end.

  Function separate_log_type_2_log (l: separate_log_type) (id: Z) :=
    match l with
    | nil ⇒ nil
    | e1 :: l1 ⇒
      (separate_event_2_event e1 id) :: (separate_log_type_2_log l1 id)
    end.

  Function separate_event_2_ident (e: separate_event):=
    match e with
    | SEACQ _ ⇒ acquire_shared
    | SEREL _ _ ⇒ release_shared
    | SEATOMIC _ e ⇒ atomic_event_ident e
    end.

  Inductive single_separate_step (curid: Z) (oracle: Oracle):
    sp_state → trace → sp_state → Prop :=
  | single_exec_step_progress_separate_local:
      ∀ ps l ps´
             (Hlocal: single_local_step curid (SView ps) (SView ps´)),
        single_separate_step curid oracle (SPState ps l) E0
                             (SPState ps´ l)

  | single_exec_step_progress_separate_log:
      ∀ ps gl gl´ l l0 sl e ps´ id
             (Hl: l = ZMap.get id gl)