Library mcertikos.objects.cpulocaldef.QMCSLockOpGenDef

Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import LoadStoreSem1.
Require Import XOmega.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.

Require Import AbstractDataType.
Require Import GlobalOracle.

Require Import CalMCSLock.
Require Import ZSet.

Section QS_MCSLOCK_DEF.

  Context `{waittime: WaitTime}.

  Section MCSLockStateMapping.

    Inductive Q_MCSLockThreadState :=
      MCS_BEFORE_SET_NEXT | MCS_WAITING_BUSY | MCS_INSIDE.

    Inductive QThread :=
      QT : ∀ (s :Q_MCSLockThreadState) (tid : Z) (bound : nat), QThread.

    Definition qthread_tid (qt : QThread) : Z :=
      match qt with
        |QT _ tid _ ⇒ tid
      end.

    Definition qthread_bound (qt : QThread) : nat :=
      match qt with
        | QT _ _ bound ⇒ bound
      end.

    Definition Q_MCSLockState := list QThread.

    Fixpoint tail_id (q : Q_MCSLockState) : Z :=
      match q with
        | nil ⇒ NULL
        | t :: nil ⇒ qthread_tid t
        | t::ts ⇒ tail_id ts
      end.


    Inductive Q_CalMCSLock : MultiLog → Q_MCSLockState → Prop :=
      | Q_CalMCSLock_nil : Q_CalMCSLock nil nil
      | Q_CalMCSLock_SWAP_nil :
          ∀ bound i l, i≠NULL → Q_CalMCSLock l nil →
                            Q_CalMCSLock ((TEVENT i (TTICKET (SWAP_TAIL bound true)))::l)
                                         ((QT MCS_INSIDE i bound) :: nil)
      | Q_CalMCSLock_SWAP_not_nil :
          ∀ bound i l q,
            Q_CalMCSLock l q →
            q ≠ nil →
            i ≠ NULL →
            ¬ In i (map qthread_tid q) →
            Q_CalMCSLock ((TEVENT i (TTICKET (SWAP_TAIL bound false)))::l) ((q ++ (QT MCS_BEFORE_SET_NEXT i bound) :: nil))
      | Q_CalMCSLock_GET_NEXT :
          ∀ i l q, Q_CalMCSLock l q →
                        Q_CalMCSLock ((TEVENT i (TTICKET GET_NEXT))::l) q
      | Q_CalMCSLock_SET_NEXT :
          ∀ i bi j bj l q, Q_CalMCSLock l q →
                                ∀ pre s post,
                                  q = pre ++ (QT s j bj) :: (QT MCS_BEFORE_SET_NEXT i bi) :: post →
                                  Q_CalMCSLock ((TEVENT i (TTICKET (SET_NEXT j)))::l)
                                               (pre ++ (QT s j bj) :: (QT MCS_WAITING_BUSY i bi) :: post)
      | Q_CalMCSLock_GET_BUSY_true :
          ∀ s i j bj l q, Q_CalMCSLock l ((QT s j bj)::q) →
                               i ≠ j →
                               Q_CalMCSLock ((TEVENT i (TTICKET (GET_BUSY true)))::l) ((QT s j bj)::q)
      | Q_CalMCSLock_GET_BUSY_false :
          ∀ i bi l q, Q_CalMCSLock l ((QT MCS_WAITING_BUSY i bi)::q) →
                           Q_CalMCSLock ((TEVENT i (TTICKET (GET_BUSY false)))::l) ((QT MCS_INSIDE i bi)::q)
      | Q_CalMCSLock_SET_BUSY :
          ∀ i bi j bj l q, Q_CalMCSLock l ((QT MCS_INSIDE i bi)::(QT MCS_WAITING_BUSY j bj)::q) →
                                Q_CalMCSLock ((TEVENT i (TTICKET SET_BUSY))::l) ((QT MCS_WAITING_BUSY j bj)::q)
      | Q_CalMCSLock_CAS_TAIL_false :
          ∀ i l q, Q_CalMCSLock l q →
                        Q_CalMCSLock ((TEVENT i (TTICKET (CAS_TAIL false)))::l) q
      | Q_CalMCSLock_CAS_TAIL_true :
          ∀ i bi l, Q_CalMCSLock l ((QT MCS_INSIDE i bi)::nil) →
                         Q_CalMCSLock ((TEVENT i (TTICKET (CAS_TAIL true)))::l) nil
      | Q_CalMCSLock_SHARED_MEM :
          ∀ i l st q, Q_CalMCSLock l q →
                          Q_CalMCSLock ((TEVENT i (TSHARED st))::l) q.

    Fixpoint slowset_of_QMCSLockState (q : Q_MCSLockState) :=
      match q with
        | nil ⇒ ZSet.empty
        | (QT MCS_BEFORE_SET_NEXT i _)::q ⇒ ZSet.add i (slowset_of_QMCSLockState q)
        | _:: q ⇒ slowset_of_QMCSLockState q
      end.

    Definition head_status_of_QMCSLockState (q : Q_MCSLockState) :=
      match q with
        | (QT MCS_INSIDE _ _)::_ ⇒ LHOLD
        | _ ⇒ LEMPTY
      end.

    Inductive QState_of_QMCSLockState (q : Q_MCSLockState) : option (nat × nat × head_status × list Z × ZSet.t × list nat)
                                                             → Prop :=
    | QSTATE_OF_QMCSLOCKSTATE : ∀ self_c rel_c b qs slow tq,
        b = head_status_of_QMCSLockState q →
        qs = map qthread_tid q →
        slow = slowset_of_QMCSLockState q →
        tq = map qthread_bound q →
        QState_of_QMCSLockState q (Some (self_c, rel_c, b, qs, slow, tq)).

  End MCSLockStateMapping.

  Section RELATE_QS_MCS_LOG_DEF.

    Inductive relate_qs_mcs_log (ll : MultiLog) : Prop :=
      | RELATE_QS_MCS_LOG : ∀ q,
          Q_CalMCSLock ll q →
          QState_of_QMCSLockState q (QS_CalLock ll) →
          relate_qs_mcs_log ll.

    Inductive relate_qs_mcs_log_type: MultiLogType → Prop :=
      | RELATE_QS_MCS_LOG_TYPE_UNDEF:
          relate_qs_mcs_log_type MultiUndef
      | RELATE_QS_MCS_LOG_TYPE_DEF:
          ∀ l
                 (Hrelate_qs_mcs_log: relate_qs_mcs_log l),
            relate_qs_mcs_log_type (MultiDef l).

    Inductive relate_qs_mcs_log_pool: MultiLogPool → Prop :=
      | RELATE_QS_MCS_LOG_POOL:
          ∀ l
                 (Hrelate_qs_mcs_log_type:
                    ∀ index ofs z
                           (Hrange: index2Z index ofs = Some z),
                      relate_qs_mcs_log_type (ZMap.get z l)),
            relate_qs_mcs_log_pool l.

    Inductive relate_mcs_qs_oracle: MultiOracle → Prop :=
      | RELATE_MCS_QS_ORACLE:
          ∀ o
                 (Hrelate_mcs_qs_oracle_res:
                    ∀ i l
                           (Hrelate_qs_mcs_log: relate_qs_mcs_log l),
                      relate_qs_mcs_log (o i l ++ l)),
            
            relate_mcs_qs_oracle o.

    Inductive relate_mcs_qs_oracle_pool: MultiOraclePool → Prop :=
      | RELATE_MCS_QS_ORACLE_POOL:
          ∀ pool
                 (Hrelate_qs_mcs_oracle:
                    ∀ index ofs z
                           (Hrange: index2Z index ofs = Some z),
                      relate_mcs_qs_oracle (ZMap.get z pool)),
            relate_mcs_qs_oracle_pool pool.

  End RELATE_QS_MCS_LOG_DEF.

End QS_MCSLOCK_DEF.