Library mcertikos.mcslock.MCSMCurIDCSource
Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import GlobalOracle.
Local Open Scope positive_scope.
// macros only for MCS_LOCK
#define BUSY 1
#define FREE 0
#define INVALID_MCS_NODE TOTAL_CPU
#define TRUE 1
#define FALSE 0
// num of CPUs and procs
#define TOTAL_CPU 8
// macros for num of chans and num of cvs
#define READ_Q_START 0
#define MSG_Q_START (READ_Q_START + TOTAL_CPU) // 7
#define SLEEP_Q_START (MSG_Q_START + TOTAL_CPU) // 16
#define num_cv 255
#define TDQ_SIZE (SLEEP_Q_START + num_proc * num_cv + 1) // 16 + num_proc * 255 + 1
#define num_chan TDQ_SIZE // num_proc
// macros for lock index
#define ID_AT 0
#define ID_TCB 1
#define ID_SC 2
#define ID_range 3
#define ID_AT_range 1
#define ID_TCB_range num_chan
#define ID_SC_range num_cv // 255
#define lock_TCB_range (ID_AT_range + ID_TCB_range)
#define lock_range (ID_AT_range + ID_TCB_range + ID_SC_range)
#define lock_AT_start 0
#define lock_TCB_start ID_AT_range // 1
#define lock_SC_start lock_TCB_range
#define WRONG 123456789
// defined in MBoot layer
extern void mcs_init_node_log(unsigned int lock_index);
extern void mcs_GET_NEXT_log(unsigned int lock_index, unsigned int cpuid);
extern void mcs_SET_NEXT_log(unsigned int lock_index, unsigned int cpuid, unsigned int prev_id);
extern void mcs_GET_BUSY_log(unsigned int lock_index, unsigned int cpuid);
extern void mcs_SET_BUSY_log(unsigned int lock_index, unsigned int cpuid);
// Data Type
typedef struct _mcs_node{
unsigned int next;
unsigned int busy;
}mcs_node;
typedef struct _mcs_lock{
unsigned int tail;
mcs_node node_pool[TOTAL_CPU];
}mcs_lock;
mcs_lock MCS_LOCK_LOC[lock_range];
// mcs_init_node
void
mcs_init_node(unsigned int lock_index)
{
mcs_init_node_log(lock_index);
MCS_LOCK_LOC[lock_index].tail = INVALID_MCS_NODE;
(MCS_LOCK_LOC[lock_index].node_pool[0]).busy = FREE;
(MCS_LOCK_LOC[lock_index].node_pool[0]).next = INVALID_MCS_NODE;
(MCS_LOCK_LOC[lock_index].node_pool[1]).busy = FREE;
(MCS_LOCK_LOC[lock_index].node_pool[1]).next = INVALID_MCS_NODE;
(MCS_LOCK_LOC[lock_index].node_pool[2]).busy = FREE;
(MCS_LOCK_LOC[lock_index].node_pool[2]).next = INVALID_MCS_NODE;
(MCS_LOCK_LOC[lock_index].node_pool[3]).busy = FREE;
(MCS_LOCK_LOC[lock_index].node_pool[3]).next = INVALID_MCS_NODE;
(MCS_LOCK_LOC[lock_index].node_pool[4]).busy = FREE;
(MCS_LOCK_LOC[lock_index].node_pool[4]).next = INVALID_MCS_NODE;
(MCS_LOCK_LOC[lock_index].node_pool[5]).busy = FREE;
(MCS_LOCK_LOC[lock_index].node_pool[5]).next = INVALID_MCS_NODE;
(MCS_LOCK_LOC[lock_index].node_pool[6]).busy = FREE;
(MCS_LOCK_LOC[lock_index].node_pool[6]).next = INVALID_MCS_NODE;
(MCS_LOCK_LOC[lock_index].node_pool[7]).busy = FREE;
(MCS_LOCK_LOC[lock_index].node_pool[7]).next = INVALID_MCS_NODE;
}
// mcs_GET_NEXT
unsigned int
mcs_GET_NEXT(unsigned int lock_index, unsigned int cpuid)
{
mcs_GET_NEXT_log(lock_index, cpuid);
return (MCS_LOCK_LOC[lock_index].node_pool[cpuid]).next;
}
// mcs_SET_NEXT
void
mcs_SET_NEXT(unsigned int lock_index, unsigned int cpuid, unsigned int prev_id)
{
mcs_SET_NEXT_log(lock_index, cpuid, prev_id);
(MCS_LOCK_LOC[lock_index].node_pool[prev_id]).next = cpuid;
}
// mcs_GET_BUSY
unsigned int
mcs_GET_BUSY(unsigned int lock_index, unsigned int cpuid)
{
mcs_GET_BUSY_log(lock_index, cpuid);
return (MCS_LOCK_LOC[lock_index].node_pool[cpuid]).busy;
}
// mcs_SET_BUSY
void
mcs_SET_BUSY(unsigned int lock_index, unsigned int cpuid)
{
mcs_SET_BUSY_log(lock_index, cpuid);
unsigned int next = (MCS_LOCK_LOC[lock_index].node_pool[cpuid]).next;
(MCS_LOCK_LOC[lock_index].node_pool[next]).busy = FALSE;
}
// ATOMIC ONE - assembly one
// - The behaviour of mcs_SWAP_TAIL
// unsigned int
// mcs_SWAP_TAIL(unsigned int bound, unsigned int lock_index, unsigned int cpuid)
// {
// unsigned int res;
// (MCS_LOCK_LOC[lock_index].node_pool[cpuid]).busy = BUSY;
// (MCS_LOCK_LOC[lock_index].node_pool[cpuid]).next = INVALID_MCS_NODE;
//
// res = MCS_LOCK_LOC[lock_index].tail;
// MC_LOCK_LOC[lock_index].tail = cpuid;
// return res;
// }
// ATOMIC ONE - assembly one
// - The behaviour of mcs_CAS_TAIL
// unsigned int
// mcs_CAS_TAIL(unsigned int lock_index, unsigned int cpuid)
// {
// if (MCS_LOCK_LOC[lock_index].tail != cpuid){
// // just update the log by adding one CAS event
// // It's ok because we already updated the oracle using CAS_log_pre, and
// // mcs_CAS is an atomic operation
// return FALSE;
// } else {
// MCS_LOCK_LOC[lock_index].tail = INVALID_MCS_NODE;
// return TRUE;
// }
// }
Definition _cpuid : positive := 10.
Definition _lock_index : positive := 11.
Definition _prev_id : positive := 13.
Definition f_mcs_init_node_body :=
(Ssequence
(Scall None
(Evar mcs_init_node_log (Tfunction (Tcons tuint Tnil) tvoid cc_default))
((Etempvar _lock_index tuint) :: nil))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint) (tptr t_struct_mcs_lock))
t_struct_mcs_lock) _tail tuint) (Econst_int (Int.repr TOTAL_CPU) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint) (tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool
(tarray t_struct_mcs_node TOTAL_CPU)) (Econst_int (Int.repr 0) tint)
(tptr t_struct_mcs_node)) t_struct_mcs_node) _busy tuint)
(Econst_int (Int.repr 0) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint) (tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool
(tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 0) tint) (tptr t_struct_mcs_node))
t_struct_mcs_node) _next tuint)
(Econst_int (Int.repr TOTAL_CPU) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock)) t_struct_mcs_lock)
_node_pool (tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 1) tint) (tptr t_struct_mcs_node))
t_struct_mcs_node) _busy tint)
(Econst_int (Int.repr 0) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock)) t_struct_mcs_lock)
_node_pool (tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 1) tint) (tptr t_struct_mcs_node))
t_struct_mcs_node) _next tuint)
(Econst_int (Int.repr TOTAL_CPU) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock)) t_struct_mcs_lock)
_node_pool (tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 2) tint)
(tptr t_struct_mcs_node)) t_struct_mcs_node) _busy
tuint) (Econst_int (Int.repr 0) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock)) t_struct_mcs_lock)
_node_pool (tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 2) tint)
(tptr t_struct_mcs_node)) t_struct_mcs_node) _next
tuint) (Econst_int (Int.repr TOTAL_CPU) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool
(tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 3) tint)
(tptr t_struct_mcs_node)) t_struct_mcs_node)
_busy tuint) (Econst_int (Int.repr 0) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool
(tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 3) tint)
(tptr t_struct_mcs_node)) t_struct_mcs_node)
_next tuint) (Econst_int (Int.repr TOTAL_CPU) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool
(tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 4) tint)
(tptr t_struct_mcs_node)) t_struct_mcs_node)
_busy tuint) (Econst_int (Int.repr 0) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool
(tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 4) tint)
(tptr t_struct_mcs_node))
t_struct_mcs_node) _next tuint)
(Econst_int (Int.repr TOTAL_CPU) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool
(tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 5) tint)
(tptr t_struct_mcs_node))
t_struct_mcs_node) _busy tuint)
(Econst_int (Int.repr 0) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC
(tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool
(tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 5) tint)
(tptr t_struct_mcs_node))
t_struct_mcs_node) _next tuint)
(Econst_int (Int.repr TOTAL_CPU) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC
(tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool
(tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 6) tint)
(tptr t_struct_mcs_node))
t_struct_mcs_node) _busy tuint)
(Econst_int (Int.repr 0) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC
(tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool
(tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 6) tint)
(tptr t_struct_mcs_node))
t_struct_mcs_node) _next tuint)
(Econst_int (Int.repr TOTAL_CPU) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC
(tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool
(tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 7) tint)
(tptr t_struct_mcs_node))
t_struct_mcs_node) _busy tuint)
(Econst_int (Int.repr 0) tint))
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC
(tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool
(tarray t_struct_mcs_node TOTAL_CPU))
(Econst_int (Int.repr 7) tint)
(tptr t_struct_mcs_node))
t_struct_mcs_node) _next tuint)
(Econst_int (Int.repr TOTAL_CPU) tint))))))))))))))))))).
Definition f_mcs_init_node :=
{|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_lock_index, tuint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := f_mcs_init_node_body
|}.
Definition f_mcs_GET_NEXT_body :=
(Ssequence
(Scall None
(Evar mcs_GET_NEXT_log (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid cc_default))
((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint):: nil))
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock)) t_struct_mcs_lock)
_node_pool (tarray t_struct_mcs_node TOTAL_CPU))
(Etempvar _cpuid tuint) (tptr t_struct_mcs_node))
t_struct_mcs_node) _next tuint)))).
Definition f_mcs_GET_NEXT := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := ((_lock_index, tuint) :: (_cpuid, tuint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := f_mcs_GET_NEXT_body
|}.
Definition f_mcs_SET_NEXT_body :=
(Ssequence
(Scall None
(Evar mcs_SET_NEXT_log (Tfunction (Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tvoid cc_default))
((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint):: (Etempvar _prev_id tuint) :: nil))
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint) (tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool (tarray t_struct_mcs_node TOTAL_CPU))
(Etempvar _prev_id tuint) (tptr t_struct_mcs_node))
t_struct_mcs_node) _next tuint) (Etempvar _cpuid tuint))).
Definition f_mcs_SET_NEXT :=
{|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_lock_index, tuint) :: (_cpuid, tuint) ::
(_prev_id, tuint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := f_mcs_SET_NEXT_body
|}.
Definition f_mcs_GET_BUSY_body :=
(Ssequence
(Scall None
(Evar mcs_GET_BUSY_log (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid cc_default))
((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint)
(tptr t_struct_mcs_lock)) t_struct_mcs_lock)
_node_pool (tarray t_struct_mcs_node TOTAL_CPU))
(Etempvar _cpuid tuint) (tptr t_struct_mcs_node))
t_struct_mcs_node) _busy tuint)))).
Definition f_mcs_GET_BUSY :=
{|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := ((_lock_index, tuint) :: (_cpuid, tuint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := f_mcs_GET_BUSY_body
|}.
Definition f_mcs_SET_BUSY_body :=
(Ssequence
(Scall None
(Evar mcs_SET_BUSY_log (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid cc_default))
((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))
(Ssequence
(Sset _next
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint) (tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool (tarray t_struct_mcs_node TOTAL_CPU))
(Etempvar _cpuid tuint) (tptr t_struct_mcs_node))
t_struct_mcs_node) _next tuint))
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar MCS_LOCK_LOC (tarray t_struct_mcs_lock lock_range))
(Etempvar _lock_index tuint) (tptr t_struct_mcs_lock))
t_struct_mcs_lock) _node_pool (tarray t_struct_mcs_node num_proc))
(Etempvar _next tuint) (tptr t_struct_mcs_node))
t_struct_mcs_node) _busy tuint) (Econst_int (Int.repr 0) tint)))).
Definition f_mcs_SET_BUSY :=
{|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_lock_index, tuint) :: (_cpuid, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_next, tuint) :: nil);
fn_body := f_mcs_SET_BUSY_body
|}.