Library mcertikos.mcslock.MMCSLockIntroCSource

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) // 8
#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 + 1024 * 255 + 1
#define num_chan TDQ_SIZE

// 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) // 1 + num_proc
#define lock_range (ID_AT_range + ID_TCB_range + ID_SC_range) // 1 + num_proc + 255
#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);

// defined in MMCSLockIntro layer
extern void mcs_init_node(unsigned int lock_index);
extern void mcs_log(unsigned int lock_index, unsigned int cpuid);
extern unsigned int mcs_GET_NEXT(unsigned int lock_index, unsigned int cpuid);
extern void mcs_SET_NEXT(unsigned int lock_index, unsigned int cpuid, unsigned int prev_id);
extern unsigned int mcs_GET_BUSY(unsigned int lock_index, unsigned int cpuid);
extern void mcs_SET_BUSY(unsigned int lock_index, unsigned int cpuid);
extern unsigned int mcs_SWAP_TAIL(unsigned int bound, unsigned int lock_index, unsigned int cpuid);
extern unsigned int mcs_CAS_TAIL(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[num_proc];
}mcs_lock;

mcs_lock MCS_LOCK_LOC[lock_range];

unsigned int mcs_get_next(unsigned int lock_index, unsigned int cpuid){
    mcs_log(lock_index, cpuid);
    return mcs_GET_NEXT(lock_index, cpuid);
}

void mcs_set_next(unsigned int lock_index, unsigned int cpuid, unsigned int prev_id){
    mcs_log(lock_index, cpuid);
    mcs_SET_NEXT(lock_index, cpuid, prev_id);
}

unsigned int mcs_get_busy(unsigned int lock_index, unsigned int cpuid){
    mcs_log(lock_index, cpuid);
    return mcs_GET_BUSY(lock_index, cpuid);
}

void mcs_set_busy(unsigned int lock_index, unsigned int cpuid){
    mcs_log(lock_index, cpuid);
    mcs_SET_BUSY(lock_index, cpuid);
}

unsigned int mcs_swap_tail(unsinged int bound unsigned int lock_index, unsigned int cpuid){
    mcs_log(lock_index, cpuid);
    return mcs_SWAP_TAIL(bound, lock_index, cpuid);
}

unsigned int mcs_cas_tail(unsigned int lock_index, unsigned int cpuid){
    mcs_log(lock_index, cpuid);
    return mcs_CAS_TAIL(lock_index, cpuid);
}

unsigned int mcs_lock_get_index(unsigned int lock_id, unsigned int offset){

    if (lock_id == ID_AT){
        if (0 <= offset && offset < ID_AT_range){
            return ID_AT;
        } else {
            return WRONG;
        }
    } else if (lock_id == ID_TCB) {
        if (0 <= offset && offset < ID_TCB_range){
            return lock_TCB_start + offset;
        } else {
            return WRONG;
        }
    } else if (lock_id == ID_SC) {
        if (0 <= offset && offset < ID_SC_range){
            return lock_SC_start + offset;
        } else {
            return WRONG;
        }
    } else {
        return WRONG;
    }
}

Definition _mbi_adr : positive := 10.
Definition _i : positive := 11.
Definition _lock_id : positive := 12.
Definition _offset : positive := 13.
Definition _lock_index : positive := 14.
Definition _cpuid : positive := 15.
Definition _prev_id : positive := 16.
Definition _res : positive := 17.
Definition _bound : positive := 18.


Definition f_mcs_lock_init_while_condition :=
  (Ebinop Olt (Etempvar _i tuint) (Econst_int (Int.repr lock_range) tint) tint).

Definition f_mcs_lock_init_while_body :=
  (Ssequence
     (Scall None
            (Evar mcs_init_node (Tfunction (Tcons tuint Tnil) tvoid
                                           cc_default)) ((Etempvar _i tuint) :: nil))
     (Sset _i
           (Ebinop Oadd (Etempvar _i tuint) (Econst_int (Int.repr 1) tint)
                   tuint))).

Definition f_mcs_lock_init_body :=
  (Ssequence
     (Scall None
            (Evar boot_loader (Tfunction (Tcons tuint Tnil) tvoid cc_default))
            ((Etempvar _mbi_adr tuint) :: nil))
     (Ssequence
        (Sset _i (Econst_int (Int.repr 0) tint))
        (Swhile
           f_mcs_lock_init_while_condition
           f_mcs_lock_init_while_body))).

Definition f_mcs_lock_init :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_mbi_adr, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((_i, tuint) :: nil);
    fn_body := f_mcs_lock_init_body
  |}.

Definition f_mcs_get_next_body :=
  (Ssequence
     (Scall None
            (Evar mcs_log (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                     cc_default))
            ((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))
     (Ssequence
        (Scall (Some _res)
               (Evar mcs_GET_NEXT (Tfunction (Tcons tuint (Tcons tuint Tnil)) tuint
                                             cc_default))
               ((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))
        (Sreturn (Some (Etempvar _res 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 := ((_res, tuint) :: nil);
  fn_body := f_mcs_get_next_body
|}.

Definition f_mcs_set_next_body :=
  (Ssequence
     (Scall None
            (Evar mcs_log (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                     cc_default))
            ((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))
     (Scall None
            (Evar mcs_SET_NEXT (Tfunction
                                  (Tcons tuint (Tcons tuint (Tcons tuint Tnil)))
                                  tvoid cc_default))
            ((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) ::
                                          (Etempvar _prev_id tuint) :: nil))).

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_log (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                     cc_default))
            ((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))
     (Ssequence
        (Scall (Some _res)
               (Evar mcs_GET_BUSY (Tfunction (Tcons tuint (Tcons tuint Tnil)) tuint
                                             cc_default))
               ((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))
        (Sreturn (Some (Etempvar _res 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 := ((_res, tuint) :: nil);
    fn_body := f_mcs_get_busy_body
  |}.

Definition f_mcs_set_busy_body :=
  (Ssequence
     (Scall None
            (Evar mcs_log (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                     cc_default))
            ((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))
     (Scall None
            (Evar mcs_SET_BUSY (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                          cc_default))
            ((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))).

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 := nil;
    fn_body := f_mcs_set_busy_body
  |}.

Definition f_mcs_swap_tail_body :=
  (Ssequence
     (Scall None
            (Evar mcs_log (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                     cc_default))
            ((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))
     (Ssequence
        (Scall (Some _res)
               (Evar mcs_SWAP_TAIL (Tfunction (Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tuint
                                              cc_default))
               ((Etempvar _bound tuint) :: (Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))
        (Sreturn (Some (Etempvar _res tuint))))).

Definition f_mcs_swap_tail :=
  {|
    fn_return := tuint;
    fn_callconv := cc_default;
    fn_params := ((_bound, tuint) :: (_lock_index, tuint) :: (_cpuid, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((_res, tuint) :: nil);
    fn_body := f_mcs_swap_tail_body
  |}.

Definition f_mcs_cas_tail_body :=
  (Ssequence
     (Scall None
            (Evar mcs_log (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                     cc_default))
            ((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))
     (Ssequence
        (Scall (Some _res)
               (Evar mcs_CAS_TAIL (Tfunction (Tcons tuint (Tcons tuint Tnil)) tuint
                                             cc_default))
               ((Etempvar _lock_index tuint) :: (Etempvar _cpuid tuint) :: nil))
        (Sreturn (Some (Etempvar _res tuint))))).

Definition f_mcs_cas_tail :=
  {|
    fn_return := tuint;
    fn_callconv := cc_default;
    fn_params := ((_lock_index, tuint) :: (_cpuid, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((_res, tuint) :: nil);
    fn_body := f_mcs_cas_tail_body
  |}.

Definition f_mcs_lock_get_index_body :=
(Sifthenelse (Ebinop Oeq (Etempvar _lock_id tuint)
               (Econst_int (Int.repr 0) tint) tint)
  (Ssequence
    (Sifthenelse (Ebinop Ole (Econst_int (Int.repr 0) tint)
                   (Etempvar _offset tuint) tint)
      (Ssequence
        (Sset 69%positive
          (Ecast
            (Ebinop Olt (Etempvar _offset tuint)
              (Econst_int (Int.repr 1) tint) tint) tbool))
        (Sset 69%positive (Ecast (Etempvar 69%positive tbool) tint)))
      (Sset 69%positive (Econst_int (Int.repr 0) tint)))
    (Sifthenelse (Etempvar 69%positive tint)
      (Sreturn (Some (Econst_int (Int.repr 0) tint)))
      (Sreturn (Some (Econst_int (Int.repr 123456789) tint)))))
  (Sifthenelse (Ebinop Oeq (Etempvar _lock_id tuint)
                 (Econst_int (Int.repr 1) tint) tint)
    (Ssequence
      (Sifthenelse (Ebinop Ole (Econst_int (Int.repr 0) tint)
                     (Etempvar _offset tuint) tint)
        (Ssequence
          (Sset 70%positive
            (Ecast
              (Ebinop Olt (Etempvar _offset tuint)
                (Ebinop Oadd
                  (Ebinop Oadd
                    (Ebinop Oadd (Econst_int (Int.repr READ_Q_START) tint)
                      (Econst_int (Int.repr TOTAL_CPU) tint) tint)
                    (Econst_int (Int.repr TOTAL_CPU) tint) tint)
                  (Econst_int (Int.repr num_proc) tint) tint) tint) tbool))
          (Sset 70%positive (Ecast (Etempvar 70%positive tbool) tint)))
        (Sset 70%positive (Econst_int (Int.repr 0) tint)))
      (Sifthenelse (Etempvar 70%positive tint)
        (Sreturn (Some (Ebinop Oadd (Econst_int (Int.repr 1) tint)
                         (Etempvar _offset tuint) tuint)))
        (Sreturn (Some (Econst_int (Int.repr 123456789) tint)))))
    (Sifthenelse (Ebinop Oeq (Etempvar _lock_id tuint)
                   (Econst_int (Int.repr 2) tint) tint)
      (Ssequence
        (Sifthenelse (Ebinop Ole (Econst_int (Int.repr 0) tint)
                       (Etempvar _offset tuint) tint)
          (Ssequence
            (Sset 71%positive
              (Ecast
                (Ebinop Olt (Etempvar _offset tuint)
                  (Ebinop Oadd
                    (Ebinop Oadd
                      (Ebinop Oadd (Econst_int (Int.repr READ_Q_START) tint)
                        (Econst_int (Int.repr TOTAL_CPU) tint) tint)
                      (Econst_int (Int.repr TOTAL_CPU) tint) tint)
                    (Econst_int (Int.repr num_proc) tint) tint) tint) tbool))
            (Sset 71%positive (Ecast (Etempvar 71%positive tbool) tint)))
          (Sset 71%positive (Econst_int (Int.repr 0) tint)))
        (Sifthenelse (Etempvar 71%positive tint)
          (Sreturn (Some (Ebinop Oadd
                           (Ebinop Oadd (Econst_int (Int.repr 1) tint)
                             (Ebinop Oadd
                               (Ebinop Oadd
                                 (Ebinop Oadd (Econst_int (Int.repr READ_Q_START) tint)
                                   (Econst_int (Int.repr TOTAL_CPU) tint) tint)
                                 (Econst_int (Int.repr TOTAL_CPU) tint) tint)
                               (Econst_int (Int.repr num_proc) tint) tint) tint)
                           (Etempvar _offset tuint) tuint)))
          (Sreturn (Some (Econst_int (Int.repr 123456789) tint)))))
      (Sreturn (Some (Econst_int (Int.repr 123456789) tint)))))).

Definition f_mcs_lock_get_index :=
  {|
    fn_return := tuint;
    fn_callconv := cc_default;
    fn_params := ((_lock_id, tuint) :: (_offset, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((71%positive, tint) :: (70%positive, tint) :: (69%positive, tint) :: nil);
    fn_body := f_mcs_lock_get_index_body
  |}.