AbsMachineLocks

Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import CLemmas.
Require Import CommonTactic.

Require Import RData.
Require Import Constants.
Require Import HypsecCommLib.

Local Open Scope Z_scope.

Section Bounds.
  Definition lock_bound := 10 % Z.
  Lemma lock_bound_lt_max: 0 <= lock_bound <= Int.max_unsigned.
  Proof. unfold lock_bound. pose proof max_unsigned_val. omega. Qed.

  Definition fairness := 20 % nat.
  Lemma positive_fairness: (0 < fairness)%nat.
  Proof. unfold fairness. omega. Qed.

End Bounds.

Global Opaque lock_bound fairness.

Section CalLockOpsCode.

  Local Notation wrap z := (Int.unsigned (Int.repr z)) (only parsing).

  (* returns (ticket_value * now_value * waiting_list), but with wraparounds *)
  Fixpoint CalTicketLockWraparound (l: MultiLog): option (Z * Z * list nat) :=
    let wrapSome tnq :=
      match tnq with (t, n, q) => Some (wrap t, wrap n, q) end
    in

    match l with
    | nil => Some (0, 0, nil)
    | TEVENT _ e :: l' =>
      match CalTicketLockWraparound l', e with
      | None,              _                      => None
      | Some prv,          TSHARED _
      | Some prv,          TTICKET GET_NOW
      | Some prv,          TTICKET HOLD_LOCK      => wrapSome prv
      | Some (t', n', q'), TTICKET (INC_TICKET p) => let t := t' + 1 in
                                                     let q := q' ++ (p::nil) in
                                                     wrapSome (t, n', q)
      | Some (t', n', q'), TTICKET INC_NOW        => let n := n' + 1 in
                                                     match q' with
                                                     | nil as q | _ :: q =>
                                                       wrapSome (t', n, q)
                                                     end
      | _,                _                      => None
      end
    end.

  (* b  := wait bound
   * c  := current CPU
   * t  := c's ticket number
   * l  := log
   * to := oracle
   *
   * advance l to when now == t, i.e. when c can obtain the lock,
   * with wait bound b, and with integer wraparound
   *)
  Fixpoint CalTicketWaitWraparound (b: nat) (c t: Z)
                                   (l: MultiLog) (to: MultiOracle):
                                   option (list MultiOracleEvent) :=
    match b with
    | O    => None
    | S b' => let l' := TEVENT c (TTICKET GET_NOW) :: (to c l) ++ l in
              match CalTicketLockWraparound l' with
              | Some (_, n, _) => if zeq t n
                                   then Some l'
                                   else CalTicketWaitWraparound b' c t l' to
              | _               => None
              end
    end.

End CalLockOpsCode.

Section CalLockOps.

  (* returns (ticket_value * now_value * waiting_list) *)
  Fixpoint CalTicketLock (l: MultiLog): option (Z * Z * list nat) :=
    match l with
    | nil => Some (0, 0, nil)
    | TEVENT _ e :: l' =>
      match CalTicketLock l', e with
      | None,              _                      => None
      | Some prv,          TSHARED _
      | Some prv,          TTICKET GET_NOW
      | Some prv,          TTICKET HOLD_LOCK      => Some prv
      | Some (t', n', q'), TTICKET (INC_TICKET p) => let t := t' + 1 in
                                                     let q := q' ++ (p::nil) in
                                                     Some (t, n', q)
      | Some (t', n', q'), TTICKET INC_NOW        => let n := n' + 1 in
                                                     match q' with
                                                     | nil as q | _ :: q =>
                                                       Some (t', n, q)
                                                     end
      | _,                _                      => None
      end
    end.

  (* b  := wait bound
   * c  := current CPU
   * t  := c's ticket number
   * l  := log
   * to := oracle
   *
   * advance l to when now == t, i.e. when c can obtain the lock,
   * with wait bound b, but without integer wraparound
   *)
  Fixpoint CalTicketWait (b: nat) (c t: Z)
                         (l: MultiLog) (to: MultiOracle):
                         option (list MultiOracleEvent) :=
    match b with
      | O    => None
      | S b' => let l' := TEVENT c (TTICKET GET_NOW) :: (to c l) ++ l in
                match CalTicketLock l' with
                  | Some (_, n, _) => if zeq t n
                                       then Some l'
                                       else CalTicketWait b' c t l' to
                  | _               => None
                end
    end.
End CalLockOps.

Section CalLockOpsQ.

  Inductive qhead_status := LEMPTY | LGET | LHOLD.
  Definition enq {X: Type} (l: list X) (x: X) := l ++ (x::nil).

  (* returns (n * self_c * other_c * qst * q * tq)
   * where n    := now
   *       sctr := how long do I have left
   *       octr := how long do others have left
   *       qst  := queue status
   *       q    := queue of CPUs waiting
   *       tq   := queue of the hold time each CPU has requested
   *)
  Fixpoint Q_CalTicketLock (l: MultiLog):
      option (Z * nat * nat * qhead_status * list Z * list nat) :=
    match l with
    | nil => Some (0, O, fairness, LEMPTY, nil, nil)
    | TEVENT c e :: l' =>
      match Q_CalTicketLock l', e with
      | Some (n, sctr, octr, _, nil, nil), TTICKET (INC_TICKET p) =>
          (* when the queues are empty, we can only INC_TICKET *)
          Some (n, sctr, octr, LEMPTY, c::nil, p::nil)

      | Some (n, sctr, octr, qst, (_::_) as q, (_::_) as tq), TTICKET (INC_TICKET p) =>
          if in_dec zeq c q      (* were we previously in the queue? *)
          then None              (* because we should not have been *)
          else match octr with   (* decrement others' counters *)
               | O       => None (* timed out *)
               | S octr' => Some (n, sctr, octr', qst, q ++ c::nil, tq ++ p::nil)
               end

      | Some (n, sctr, octr, qst, c'::q', p'::tq'), TTICKET GET_NOW =>
          if zeq c c'                 (* was c at the head of the queue? *)
          then match qst with         (* yes; check queue state *)
               | LGET | LHOLD => None (* must be LEMPTY ~> LGET *)
               | LEMPTY       => Some (n, p', fairness, LGET, c'::q', p'::tq')
               end
          else match octr with        (* no; how long do we have to wait? *)
               | O => None            (* timed out *)
               | S octr' => Some (n, sctr, octr', qst, c'::q', p'::tq')
               end

      | Some (n, sctr, octr, qst, c'::q', (_::_) as tq), TTICKET HOLD_LOCK =>
          if zeq c c'                   (* was c at the head of the queue? *)
          then match qst with           (* yes; check queue state *)
               | LEMPTY | LHOLD => None (* must be LGET ~> LHOLD *)
               | LGET           => Some (n, sctr, fairness, LHOLD, c'::q', tq)
               end
          else None                     (* no; only queue head can obtain lock *)

      | Some (n, sctr, octr, qst, c'::q', _::tq'), TTICKET INC_NOW =>
          if zeq c c'                  (* was c at the head of the queue? *)
          then match qst with          (* yes; check queue state *)
               | LEMPTY | LGET => None (* must be LHOLD ~> LEMPTY *)
               | LHOLD         => Some (n + 1, O, fairness, LEMPTY, q', tq')
               end
          else None                    (* no; only head can release lock *)

      | Some (n, sctr, octr, qst, c'::q', (_::_) as tq), TSHARED _ =>
          if zeq c c'                   (* was c at the head of the queue? *)
          then match qst, sctr with     (* yes; decrement self ctr *)
               | LHOLD, S sctr' => Some (n, sctr', fairness, LHOLD, c'::q', tq)
               | _,     _       => None (* lock must be in held state *)
               end
          else None                     (* no; only head can perform mem ops *)

      | _, _ => None
      end
    end.

  (* b  := wait bound
   * c  := current CPU
   * l  := log
   * to := oracle
   *
   * advance l to when c is at the head of the wait queue,
   * i.e. when c can obtain the lock, with wait bound b
   *)
  Fixpoint Q_CalTicketWait (b: nat) (c: Z) (l: MultiLog) (to: MultiOracle):
                           option (list MultiOracleEvent) :=
    let l' := TEVENT c (TTICKET GET_NOW) :: to c l ++ l in
    match b, Q_CalTicketLock l' with
    | S b', Some (_, _, _, _, c'::q', _) => if zeq c c'
                                            then Some l'
                                            else Q_CalTicketWait b' c l' to
    | _,    _                            => None
    end.

  (* Q_CalTicketLock without now *)
  Fixpoint Q_CalLock (l: MultiLog):
      option (nat * nat * qhead_status * list Z * list nat) :=
    match l with
    | nil => Some (O, fairness, LEMPTY, nil, nil)
    | TEVENT c e :: l' =>
      match Q_CalLock l', e with
      | Some (sctr, octr, _, nil, nil), TTICKET (INC_TICKET p) =>
          (* when the queues are empty, we can only INC_TICKET *)
          Some (sctr, octr, LEMPTY, c::nil, p::nil)

      | Some (sctr, octr, qst, (_::_) as q, (_::_) as tq), TTICKET (INC_TICKET p) =>
          if in_dec zeq c q      (* were we previously in the queue? *)
          then None              (* because we should not have been *)
          else match octr with   (* decrement others' counters *)
               | O       => None (* timed out *)
               | S octr' => Some (sctr, octr', qst, q ++ c::nil, tq ++ p::nil)
               end

      | Some (sctr, octr, qst, c'::q', p'::tq'), TTICKET GET_NOW =>
          if zeq c c'                 (* was c at the head of the queue? *)
          then match qst with         (* yes; check queue state *)
               | LGET | LHOLD => None (* must be LEMPTY ~> LGET *)
               | LEMPTY       => Some (p', fairness, LGET, c'::q', p'::tq')
               end
          else match octr with        (* no; how long do we have to wait? *)
               | O => None            (* timed out *)
               | S octr' => Some (sctr, octr', qst, c'::q', p'::tq')
               end

      | Some (sctr, octr, qst, c'::q', (_::_) as tq), TTICKET HOLD_LOCK =>
          if zeq c c'                   (* was c at the head of the queue? *)
          then match qst with           (* yes; check queue state *)
               | LEMPTY | LHOLD => None (* must be LGET ~> LHOLD *)
               | LGET           => Some (sctr, fairness, LHOLD, c'::q', tq)
               end
          else None                     (* no; only queue head can obtain lock *)

      | Some (sctr, octr, qst, c'::q', _::tq'), TTICKET INC_NOW =>
          if zeq c c'                  (* was c at the head of the queue? *)
          then match qst with          (* yes; check queue state *)
               | LEMPTY | LGET => None (* must be LHOLD ~> LEMPTY *)
               | LHOLD         => Some (O, fairness, LEMPTY, q', tq')
               end
          else None                    (* no; only head can release lock *)

      | Some (sctr, octr, qst, c'::q', (_::_) as tq), TSHARED _ =>
          if zeq c c'                   (* was c at the head of the queue? *)
          then match qst, sctr with     (* yes; decrement self ctr *)
               | LHOLD, S sctr' => Some (sctr', fairness, LHOLD, c'::q', tq)
               | _,     _       => None (* lock must be in held state *)
               end
          else None                     (* no; only head can perform mem ops *)

      | _, _ => None
      end
    end.

  (* b  := wait bound
   * c  := current CPU
   * l  := log
   * to := oracle
   *
   * advance l to when c is at the head of the wait queue,
   * i.e. when c can obtain the lock, with wait bound b
   *)
  Fixpoint Q_CalWait (n: nat) (c: Z)
                     (l: MultiLog) (to: MultiOracle):
                     option (list MultiOracleEvent) :=
    let l' := TEVENT c (TTICKET GET_NOW) :: to c l ++ l in
    match n, Q_CalLock l' with
    | S n', Some (_, _, _, c'::q', _) => if zeq c c'
                                            then Some l'
                                            else Q_CalWait n' c l' to
    | _,    _                            => None
    end.

End CalLockOpsQ.

Section CalLockOpsH.

  Fixpoint H_CalLock (l: MultiLog): option (nat * qhead_status * option Z) :=
    match l with
    | nil => Some (O, LEMPTY, None)
    | TEVENT i e :: l' =>
      match H_CalLock l', e with
      | Some (self_c, LHOLD, Some i'), TTICKET REL_LOCK =>
          if negb (zeq i i') then None else
          Some (O, LEMPTY, None)

      | Some (self_c, LHOLD, Some i'), TSHARED _ =>
          if negb (zeq i i') then None else
          match self_c with
          | O         => None
          | S self_c' => Some (self_c', LHOLD, Some i')
          end

      | Some (_, LEMPTY, None), TTICKET (WAIT_LOCK n) =>
          Some (n, LHOLD, Some i)

      | _, _ => None
      end
    end.
End CalLockOpsH.

Section GetLog.

  (* Get latest shared memory event *)
  Fixpoint GetSharedMemEvent (l: MultiLog): option SharedMemEvent :=
    match l with
    | nil => None
    | TEVENT _ (TSHARED e) :: l' => Some e
    | _ :: l' => GetSharedMemEvent l'
    end.

End GetLog.

Section WaitTime.

  Fixpoint CalSumWait (l: list nat) :=
    match l with
    | nil     => O
    | a :: l' => (4 + a + CalSumWait l') % nat
    end.

  Definition rm_head {A: Type} (l: list A) :=
    match l with
      | nil => nil
      | _ :: l' => l'
    end.

  Definition CalStatus (h: qhead_status) :=
    match h with
      | LEMPTY => O
      | LHOLD => 1%nat
      | LGET => 2%nat
    end.

  Definition decrease_number (self_c other_c: nat) (h: qhead_status) (tq: list nat) :=
    match h with
      | LEMPTY => (other_c + (CalSumWait tq) * fairness) % nat
      | _ => (other_c + (self_c + CalSumWait (rm_head tq) + CalStatus h)  * fairness)%nat
    end.

  (* given waiting list l, calculate how long one has to left to wait *)
  Definition CalWaitTime (l: list nat) :=
    S (fairness + (CalSumWait l) * fairness).

End WaitTime.

Section Invariants.

  Section QLOCK_POOL_LENGTH_INV.

    Definition qlock_length (l: MultiLog):=
      forall self_c other_c b q tq
             (Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq)),
        (forall i, In i q -> 0 <= i < TOTAL_CPU).

    Definition qlock_pool_length (l: MultiLogPool):=
      forall lk q (Hdef: ZMap.get lk l = Some q),
        qlock_length q.

    Lemma qlock_pool_length_gss:
      forall l l' z (Hq: qlock_pool_length l) (Hlen: qlock_length l'),
        qlock_pool_length (ZMap.set z (Some l') l).
    Proof.
      intros. unfold qlock_pool_length in *; intros.
      destruct (zeq lk z); subst.
      - rewrite ZMap.gss in *. inv Hdef. trivial.
      - rewrite ZMap.gso in *; eauto.
    Qed.

    Lemma qlock_length_cons:
      forall i e l (Hrange: 0 <= i < TOTAL_CPU) (Hl: qlock_length l),
        qlock_length (TEVENT i e :: l).
    Proof.
      unfold qlock_length; intros.
      simpl in Hcal.
      subdestruct; inv Hcal; eauto.
      - inv H; trivial. inv H0.
      - eapply Hl; eauto. right; trivial.
      - rewrite app_comm_cons in H.
        eapply in_app_or in H.
        inv H; eauto. inv H0; trivial. inv H.
      - eapply Hl; eauto. right; trivial.
      - rewrite app_comm_cons in H.
        eapply in_app_or in H.
        inv H; eauto. inv H0; trivial. inv H.
    Qed.

    Lemma qlock_length_append:
      forall l' l (Hlen1: qlock_length l)
                  (Hto: forall i0 e, In (TEVENT i0 e) l' -> 0 <= i0 < TOTAL_CPU),
        qlock_length (l' ++ l).
    Proof.
      induction l'; simpl; intros; trivial.
      destruct a.
      eapply qlock_length_cons; eauto.
    Qed.

    Lemma Q_CalWait_length:
      forall n l l' i to
             (Hrange: 0 <= i < TOTAL_CPU)
             (Hlen: qlock_length l)
             (Hto: forall q i0 e, In (TEVENT i0 e) (to i q) -> 0 <= i0 < TOTAL_CPU)
             (Hwait: Q_CalWait n i l to = Some l'),
        qlock_length l'.
    Proof.
      Local Transparent Q_CalWait.
      induction n; simpl; intros; try congruence.
      subdestruct; subst.
      - inv Hwait.
        eapply qlock_length_cons; eauto.
        eapply qlock_length_append; eauto.
      - eapply IHn; try eapply Hwait; eauto.
        eapply qlock_length_cons; eauto.
        eapply qlock_length_append; eauto.
    Qed.

  End QLOCK_POOL_LENGTH_INV.

  Section CORRECT_QLOCK_POOL_STATUS_INV.

    Definition correct_qlock_status (l: MultiLog) (k: LockStatus) (cpu: Z):=
      forall self_c other_c b q tq
             (Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq)),
        (k = LockFalse -> ~ In cpu q) /\
          (forall lb, k = LockOwn lb ->
            exists q', q = cpu :: q' /\ b = LHOLD /\ ~ In cpu q').

    Definition correct_qlock_pool_status (l: MultiLogPool) (k: ZMap.t LockStatus) (cpu: Z):=
      forall lk q (Hdef: ZMap.get lk l = Some q),
        correct_qlock_status q (ZMap.get lk k) cpu.

    Lemma correct_qlock_pool_status_gss':
      forall l k c l' z
             (HP: correct_qlock_pool_status l k c)
             (Hc: correct_qlock_status l' (ZMap.get z k) c),
        correct_qlock_pool_status (ZMap.set z (Some l') l) k c.
    Proof.
      Local Transparent Q_CalLock.
      intros. unfold correct_qlock_pool_status in *; intros.
      destruct (zeq lk z); subst.
      - rewrite ZMap.gss in *. inv Hdef. trivial.
      - rewrite ZMap.gso in *; eauto.
    Qed.

    Inductive MatchLock: LockStatus -> LockStatus -> Prop :=
    | MLFALSE: MatchLock LockFalse LockFalse
    | MLOWN: forall a b, MatchLock (LockOwn a) (LockOwn b).

    Lemma correct_qlock_status_Match:
      forall l k k' c
             (Hc: correct_qlock_status l k c)
             (Hl: MatchLock k' k),
        correct_qlock_status l k' c.
    Proof.
      intros. unfold correct_qlock_status in *; intros.
      exploit Hc; eauto.
      intros (HF & HO).
      split; intros; subst; eauto.
      - inv Hl. eapply HF; eauto.
      - inv Hl. eapply HO; eauto.
    Qed.

    Lemma correct_qlock_pool_status_gss:
      forall l k c l' k' z
             (HP: correct_qlock_pool_status l k c)
             (Hc: correct_qlock_status l' k' c),
        correct_qlock_pool_status (ZMap.set z (Some l') l) (ZMap.set z k' k) c.
    Proof.
      intros.
      unfold correct_qlock_pool_status in *; intros.
      destruct (zeq lk z); subst.
      - rewrite ZMap.gss in *. inv Hdef.
        trivial.
      - rewrite ZMap.gso in *; eauto.
    Qed.

    Lemma correct_qlock_pool_status_gss_match:
      forall l k c l' k' z
             (HP: correct_qlock_pool_status l k c)
             (Hc: correct_qlock_status l' (ZMap.get z k) c)
             (Hl: MatchLock k' (ZMap.get z k)),
        correct_qlock_pool_status (ZMap.set z (Some l') l) (ZMap.set z k' k) c.
    Proof.
      intros. eapply correct_qlock_pool_status_gss; eauto.
      eapply correct_qlock_status_Match; eauto.
    Qed.


    Lemma Q_CalLock_unique:
      forall l self_c other_c b q tq
             (Hcal: Q_CalLock l = Some (self_c, other_c, b, q, tq)),
        forall i, In i q -> count_occ zeq q i = 1%nat.
    Proof.
      induction l; simpl; intros.
      { inv Hcal. inv H. }
      subdestruct
      ; inv Hcal
      ; try (exploit IHl; now eauto)
      ; try (match goal with H: ~In ?z (?z::?q) |- _ => contradiction H end;
            left; reflexivity
        )
      .
      - simpl in H. destruct H as [HF|HF]; inv HF.
        simpl. rewrite zeq_true. trivial.
      - specialize (IHl _ _ _ _ _ refl_equal).
        exploit (IHl i).
        { right; trivial. }
        simpl. destruct (zeq i z); subst.
        + rewrite zeq_true. intros.
          eapply (count_occ_In zeq) in H.
          omega.
        + rewrite zeq_false; auto.
      - specialize (IHl _ _ _ _ _ refl_equal).
        destruct (zeq i cpuid); subst.
        + rewrite app_comm_cons.
          rewrite count_occ_append.
          replace (count_occ zeq (z :: l3) cpuid) with O.
          { simpl. f_equal. rewrite zeq_true. trivial. }
          destruct (count_occ zeq (z :: l3) cpuid) eqn: Hpos; trivial.
          assert (Hpos': (count_occ zeq (z :: l3) cpuid > O)%nat) by omega.
          eapply count_occ_In in Hpos'.
          destruct Hpos'.
          * subst; congruence.
          * match goal with H: ~In cpuid (_::l3) |- _ => contradiction H end.
            right. assumption.

        + rewrite app_comm_cons.
          rewrite count_occ_append.
          rewrite IHl.
          { simpl. rewrite zeq_false; auto. }
          {
            rewrite app_comm_cons in H.
            apply in_app_or in H.
            destruct H as [HF| HF]; trivial.
            destruct HF as [HF'|HF']; inv HF'. congruence.
          }
    Qed.

    Lemma correct_status_HOLD_LOCK:
      forall l c b,
        correct_qlock_status (TEVENT c (TTICKET HOLD_LOCK) :: l) (LockOwn b) c.
    Proof.
      unfold correct_qlock_status.
      simpl; intros.
      subdestruct; inv Hcal.
      split; intros. inv H. inv H.
      refine_split'; trivial.
      intro HF.
      assert (Hin: In z (z :: l3)).
      { left; trivial. }
      eapply Q_CalLock_unique in Hdestruct; eauto.
      simpl in Hdestruct. rewrite zeq_true in Hdestruct.
      inv Hdestruct. eapply (count_occ_In zeq) in HF. omega.
    Qed.

    Lemma correct_status_INC_NOW:
      forall l c lb
             (Hc: correct_qlock_status l (LockOwn lb) c),
        correct_qlock_status (TEVENT c (TTICKET INC_NOW) :: l) LockFalse c.
    Proof.
      unfold correct_qlock_status.
      simpl; intros.
      subdestruct; inv Hcal.
      exploit Hc; eauto.
      intros (_ & HL). specialize (HL _ refl_equal).
      destruct HL as (q' & Heq & _ & Hnot). inv Heq.
      split; intros; trivial. inv H.
    Qed.

  End CORRECT_QLOCK_POOL_STATUS_INV.

  Section VALID_QLOCK_POOL_INV.

    Definition valid_qlock (l: MultiLog) :=
      exists self_c other_c b q tq,
        Q_CalLock l = Some (self_c, other_c, b, q, tq).

    Definition valid_qlock_pool (l: MultiLogPool):=
      forall r q (Hdef: ZMap.get r l = Some q),
        valid_qlock q.

    Lemma valid_qlock_pool_init:
      valid_qlock_pool (ZMap.init None).
    Proof.
      unfold valid_qlock_pool; intros.
      rewrite ZMap.gi in Hdef. inv Hdef.
    Qed.

    Lemma valid_qlock_pool_gss:
      forall t l p
             (Hvalid: valid_qlock_pool t)
             (Hlock: valid_qlock l),
        valid_qlock_pool (ZMap.set p (Some l) t).
    Proof.
      unfold valid_qlock_pool; intros.
      destruct (zeq p r); subst.
      - rewrite ZMap.gss in Hdef. inv Hdef. trivial.
      - rewrite ZMap.gso in Hdef; eauto.
    Qed.

    Lemma valid_qlock_pool_gss':
      forall t l p x
             (Hvalid: valid_qlock_pool t)
             (Hlock: Q_CalLock l = Some x),
        valid_qlock_pool (ZMap.set p (Some l) t).
    Proof.
      intros. eapply valid_qlock_pool_gss; eauto.
      unfold valid_qlock.
      destruct x. repeat destruct p0. eauto 20.
    Qed.

  End VALID_QLOCK_POOL_INV.

  Section VALID_MULTI_ORACLE_POOL_INV.

    Definition valid_multi_oracle_domain (o: MultiOracle) :=
      forall i i0 e l (Hin: In (TEVENT i0 e) (o i l)),
      i0 <> i /\ 0 <= i0 < TOTAL_CPU.

    Definition valid_multi_oracle_queue (o: MultiOracle):=
      forall i l
             (Hin': forall i1 e1, In (TEVENT i1 e1) l -> 0 <= i1 < TOTAL_CPU)
             (Hin: valid_qlock l)
             (Hlast: match l with TEVENT c0 e0 :: l' => c0 = i | _ => True end),
      exists self_c other_c b q tq,
        Q_CalLock ((o i l) ++ l) = Some (self_c, other_c, b, q, tq) /\
        other_c <> O.

    Definition valid_multi_oracle_pool (o: MultiOraclePool):=
      forall r,
        valid_multi_oracle_domain (ZMap.get r o) /\
        valid_multi_oracle_queue (ZMap.get r o).

    Lemma Q_CalWait_valid_last:
      forall n l l' i to
             (Hvalid: forall i1 e1,
                        In (TEVENT i1 e1) l -> 0 <= i1 < TOTAL_CPU)
             (Hto: valid_multi_oracle_domain to)
             (Hwait: Q_CalWait n i l to = Some l')
             (Hi: 0 <= i < TOTAL_CPU),
      (forall i1 e1,
         In (TEVENT i1 e1) l' -> 0 <= i1 < TOTAL_CPU).
    Proof.
      induction n; simpl; intros; try congruence.
      subdestruct; subst.
      - inv Hwait.
        inv H.
        + inv H0. eauto.
        + eapply in_app_or in H0. inv H0.
          * eapply Hto. eauto.
          * eapply Hvalid. eauto.
      - eapply IHn; try eapply Hwait; eauto.
        intros. inv H0.
        + inv H1. eauto.
        + eapply in_app_or in H1. inv H1.
          * eapply Hto. eauto.
          * eapply Hvalid. eauto.
    Qed.

  End VALID_MULTI_ORACLE_POOL_INV.

  Section VALID_LAST_POOL_INV.

    Definition valid_last (c: Z) (q: MultiLog) :=
      (forall i1 e1, In (TEVENT i1 e1) q -> 0 <= i1 < TOTAL_CPU) /\
      (match q with nil => True | TEVENT c0 _ :: _ => c0 = c end).

    Definition valid_last_pool (c: Z) (l: MultiLogPool) :=
      forall lk q (Hdef: ZMap.get lk l = Some q),
      valid_last c q.

    Lemma valid_last_pool_gss:
      forall c l l' z (HP: valid_last_pool c l) (Hc: valid_last c l'),
      valid_last_pool c (ZMap.set z (Some l') l).
    Proof.
      intros. unfold valid_last_pool in *; intros.
      destruct (zeq lk z); subst.
      - rewrite ZMap.gss in *. inv Hdef. trivial.
      - rewrite ZMap.gso in *; eauto.
    Qed.

    Lemma valid_last_event:
      forall c l e (Hc: 0 <= c < TOTAL_CPU)
             (Hvalid: valid_last c l),
        valid_last c (TEVENT c e :: l).
    Proof.
      unfold valid_last. intros. destruct Hvalid as (Hvalid1 & Hvalid2).
      split; trivial. intros. inv H.
      - inv H0. eauto.
      - eauto.
    Qed.

  End VALID_LAST_POOL_INV.

End Invariants.