Library mcertikos.mcslock.MCSStateDataType

This file provide some data types that will be used in the layer definitions and refinement proofs

Require Import Coqlib.
Require Import Constant.
Require Import Maps.
Require Import Values.
Require Import Integers.
Require Import AST.
Require Import AsmX.
Require Export AuxFunctions.

*Data types for abstract data

Section MCSSTATEFORINTROLEVELS.

  Definition NULL := TOTAL_CPU.

  Definition MCSNodePool : Type := ZMap.t (bool × Z).

  Definition MCSNodePoolInit := ZMap.init (false , NULL ).

Agent Container

  Inductive MCSStruct : Type :=
    mkMCSStruct {
        last : Z;
        nodepool : MCSNodePool
      }.

  Definition MCSLockPool : Type := ZMap.t MCSStruct.

  Definition mcs_lock_pool_init := ZMap.init (mkMCSStruct NULL MCSNodePoolInit).

End MCSSTATEFORINTROLEVELS.