Library mcertikos.objects.BigLogThreadConfigFunction

Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Memory.
Require Import AuxLemma.
Require Import Constant.
Require Import GlobIdent.
Require Export GlobalOracle.
Require Import Integers.
Require Import BigStepGlobalOracle.
Require Import CalRealProcModule.

Fixpoint B_GetContainerUsed_aux (tid: Z) (cid : Z) (l: BigLog) : bool :=
  match l with
    | nil ⇒ false
    | TBEVENT cpuid e :: l´ ⇒
      match e with
      | TBSHARED (BTDSPAWN _ new_id _ _ _ _) ⇒
        if zeq cid cpuid then
          if zeq tid new_id then true else B_GetContainerUsed_aux tid cid l´
        else B_GetContainerUsed_aux tid cid l´
      | _ ⇒ B_GetContainerUsed_aux tid cid l´
      end
  end.

Definition B_GetContainerUsed (tid: Z) (cid : Z) (l: BigLog) : bool :=
  
  if zeq tid (cid + 1) then true
  else if zle_le 0 tid TOTAL_CPU then false
       else B_GetContainerUsed_aux tid cid l.

Definition B_GetContainerUsed_opt (tid : option Z) (cid : Z) (l : BigLog) : bool :=
  match tid with
    | None ⇒ false
    | Some tid´ ⇒ B_GetContainerUsed tid´ cid l
  end.

Fixpoint B_GetlastPush_aux (cpuid : Z) (l: BigLog):=
  match l with
    | nil ⇒ CalRealProcModule.real_syncchpool (ZMap.init SyncChanUndef)
    | TBEVENT tid e :: l´ ⇒
      let res := B_GetlastPush_aux cpuid l´ in
      match e with
        | TBLOCK _ (BREL_LOCK _ s´) ⇒
          if zeq tid cpuid then s´ else res
        | TBSHARED (BTDSLEEP _ _ s´) ⇒
          if zeq tid cpuid then s´ else res
        | _ ⇒ res
      end
  end.

Definition B_GetlastPush (cpuid: Z) (l : BigLogType) :=
  match l with
  | BigUndef ⇒ (ZMap.init SyncChanUndef)
  | BigDef l´ ⇒ B_GetlastPush_aux cpuid l´
  end.

Fixpoint B_inLock_aux (cpuid : Z) (l : BigLog) :=
  match l with
    | nil ⇒ false
    | TBEVENT tid e :: l´ ⇒
      match e with
       | TBLOCK _ (BWAIT_LOCK _ _) ⇒
         if zeq tid cpuid then true else B_inLock_aux cpuid l´
       | TBSHARED (BTDWAKE _ _) ⇒
         if zeq tid cpuid then true else B_inLock_aux cpuid l´
       | TBSHARED (BTDWAKE_DIFF _ _ _ _) ⇒
         if zeq tid cpuid then true else B_inLock_aux cpuid l´
       | TBSHARED (BBUFFERE _ _ _) ⇒
         if zeq tid cpuid then true else B_inLock_aux cpuid l´
       | _ ⇒ if zeq tid cpuid then false else B_inLock_aux cpuid l´
      end
  end.

Definition B_inLock (cpuid: Z) (l : BigLogType) :=
  match l with
  | BigUndef ⇒ false
  | BigDef l´ ⇒ B_inLock_aux cpuid l´
  end.