/***********************/
/* General Definitions */
/***********************/

/* privilege level */
#define KERNEL true
#define USER false

/* scheduling priority */
#define KERNEL_PRIORITY 0
#define USER_PRIORITY 1
#define IDLE_PRIORITY 2

/* Receiving from any thread */
#define ANY (MAX_THREAD+1)

/* empty message queue cell flag */
#define EMPTY_CELL (MAX_THREAD+1)

/* message queue size */
// Topsy/Configuration.h
#define MAXNBMSGINQUEUE 3


/* Model parameters */
/*------------------*/

/* maximal number of threads */
#define MAX_THREAD 6

/* quantum of time allocated to threads */
#define TIME_QUANTUM 1

/* maximal number of thread descriptors */
#define MEMBLOCK_N MAX_THREAD


/****************************************/
/* Global variables for instrumentation */
/****************************************/

// keep track of which threads are user
bool _user_thread[MEMBLOCK_N];

// keep track of the reply channel
chan _reply_chan[MEMBLOCK_N];

inline _user_thread_init(i){
  i=0;  
  do  
    :: (i < MEMBLOCK_N) -> _user_thread[i] = false; i++;
    :: (i >= MEMBLOCK_N) -> break 
  od; 
};

/* startup is over */
bool _syst_run;

/* last created spin process */
byte _spin_process;

/* maximal number of spin processes */
//#define SPIN_PROC_N 11

/* _killed[x]=true if the Spin process of pid 'x' have requested to be killed */
bool _killed[SPIN_PROC_N];

inline _killed_init(i){
  i=0;  
  do  
    :: (i < SPIN_PROC_N) -> _killed[i] = false; i++;
    :: (i >= SPIN_PROC_N) -> break 
  od; 
};

/* thread id of currently running thread */
byte sched_running;

/********************************/
/* Macros for binary semaphores */
/********************************/

#define lock_init(x)\
x ! true;

#define lock_take(x)\
x ? _;

#define lock_release(x)\
x ! true;

#define lock\
[1] of {bool}

/*********************/
/* Memory allocation */
/*********************/

// A macro that create a "dedicated" version of the allocation library
// Memory/MMHeapMemory.c
#define HL(type,size,data,used,hmlock,hmInit,hmAlloc,hmFree)\
type data[size]; \
bool used[size]; \
chan hmlock = lock; \
inline hmInit(i){  \
                   i=0;  \
                   do  \
                     :: (i < size) -> used[i] = false; i++;  \
                     :: (i >= size) -> break  \
                   od;  \
                   lock_init(hmlock);  \
};  \
inline hmAlloc(return){  \
                         lock_take(hmlock);  \
                         return=0;  \
                         do  \
                           :: ((return < size) && (!used[return])) -> \
                              used[return] = true; break;  \
                           :: (return < size) && (used[return]) -> \
                              return++;  \
                           :: (return >= size) -> return = -1; break; \
                         od;  \
                         lock_release(hmlock);  \
};  \
inline hmFree(return){  \
                        lock_take(hmlock); \
                        if  \
                          :: return < size -> used[return] = false; \
                          :: return >= size -> return = -1; \
                        fi; \
                        lock_release(hmlock); \
}; \


/********************/
/* Bootloader model */
/********************/

// segment model, first cell is kernel memory and the second is the user memory
bool segment[2];

// Create_segment in LowCore/CoreLoad/creatgdt.inc
inline bootloader(){
  segment[0] = KERNEL;
  segment[1] = USER;
};

bool CPU_MODE;
byte _curr_ctxt; // spin pid of the currently running process
byte int_handler_ctxt; // spin pid (the int_handler is modeled as a Spin proctype)
byte ut_init_ctxt; // spin pid of the first user thread 


// mutation of memory 
inline mutation(address,value){

  if
    :: (CPU_MODE == KERNEL) -> address=value;
    :: (CPU_MODE == USER) -> setint(SEGFAULT_INT);
  fi;
  
};

// mutation of memory 
inline lookup(address,value){

  if
    :: (CPU_MODE == KERNEL) -> value=address;
    :: (CPU_MODE == USER) -> setint(SEGFAULT_INT);
  fi;
  
};


/* channel for passing interruption type */

mtype = {TIMER_INT, SOFT_INT, SEGFAULT_INT}

chan interrupt = [1] of {mtype};

// raise interrupt
// TODO modifier le nom
inline setint(i){
  atomic{
    CPU_MODE = KERNEL;
    interrupt ! i;        
    _curr_ctxt = int_handler_ctxt;
  }
}

/*******/
/* IPC */
/*******/

/* data structure for system calls */

mtype = {UNKNOWN_SYSCALL}
mtype = {TM_START, TM_STARTOK, TM_STARTFAILED, TM_EXIT};
mtype = {IO_OPEN, IO_OPENOK, IO_OPENFAILED};
mtype = {IO_CLOSE, IO_CLOSEOK, IO_CLOSEFAILED};
mtype = {IO_READ, IO_READOK, IO_READFAILED};
mtype = {IO_WRITE, IO_WRITEOK, IO_WRITEFAILED};

typedef service_msg{
  mtype service;
  byte arg
};

/* channel for passing IPC parameter */

mtype = {MSG_SND, MSG_RECV, MSG_SENDFAILED, MSG_SENDOK,MSG_RECVFAILED,MSG_RECVOK};

chan syst_call = [1] of {mtype /* syst call type */, byte /* from/to */, service_msg /* data */, chan /* for reply */};


/* IPC */


/* send a message */
inline sndmsg(to, smsg, reply){
  atomic{
    syst_call ! MSG_SND, to, smsg, reply;
    setint(SOFT_INT);
  };
  atomic{
    if
      :: reply ? MSG_SENDOK, _, smsg -> skip
      :: reply ? MSG_SENDFAILED, _, smsg -> skip
    fi;
  };
};

/* receive a message */
inline recvmsg(from, smsg, reply){
  atomic{
    syst_call ! MSG_RECV, from, smsg, reply;
    setint(SOFT_INT);
  };
  atomic{
    if
      :: reply ? MSG_RECVOK, from, smsg -> skip
      :: reply ? MSG_RECVFAILED, from, smsg -> skip
    fi;
  };
};

/* system calls are message exchange between kernel thread and client thread */
// Topsy/Syscall.c
inline genericSyscall(fromto, smsg, reply){
  sndmsg(fromto, smsg, reply);
  recvmsg(fromto, smsg, reply);
};

/***************************/
/* Thread descriptor model */
/***************************/

/* message queue */

mtype = {WAITING,NOT_WAITING};

typedef MessageQueue{  
  service_msg message[MAXNBMSGINQUEUE]; /* message queue */
  byte from[MAXNBMSGINQUEUE]; /* sender */
  byte threadIdPending; /* expected message sender */
  mtype msgPendingStatus; /* indicates if a message is pending */
  chan msgPendingPtr /* reference on pending message */  
};

/* Scheduling information */


mtype = {RUNNING, READY, BLOCKED};

typedef SchedulerInfo{
  mtype status; /* RUNNING, READY, BLOCKED */
  byte prio;    /* Priority of the thread */
};


/* Thread descriptor */

// Threads/tm-include.h
typedef Thread_desc {  
  byte contextPtr; /* spin pid of the thread */
  bool privilege; /* true = KERNEL, false = USER */
  SchedulerInfo schedInfo;  /* Scheduler specific data */
  MessageQueue msgQueue; /* Message queue */  
};


// global variables for thread id 
byte curr_id;
byte tmThread_id;
byte mmThread_id;
byte ioThread_id;
byte ut_init_id;


/****************/
/* Memory model */
/****************/

HL(Thread_desc,MEMBLOCK_N,mem,used,hmlock,hmInit,hmAlloc,hmFree)

/*****************/
/* A timer model */
/*****************/

typedef timer_state{
  byte counter;
  byte max;  
};

timer_state time;

inline timer_init(){
  time.counter = 0;
  time.max = TIME_QUANTUM;  
}

proctype timer() provided (time.counter <= time.max){
  do
    :: (time.counter < time.max) -> time.counter ++;
    :: (time.counter == time.max) ->
       atomic{
         if
           :: (CPU_MODE == KERNEL) -> skip;
           :: else -> setint(TIMER_INT);
         fi;
         time.counter++;
       };
    :: else -> skip;
  od;
}

/****************************/
/* Model of Topsy functions */
/****************************/

/* message queue related */

inline initMsgQueue(queuePtr, i){
  i=0;
  do
    :: (i < MAXNBMSGINQUEUE) -> queuePtr.from[i] = EMPTY_CELL; i++;
    :: (i >= MAXNBMSGINQUEUE) -> break
  od;
  queuePtr.msgPendingStatus = NOT_WAITING;
}


#define TM_OK 0
#define TM_MSGQUEUEOVERFLOW 1

/* add a message in queue, if possible i == TM_OK, and i == TM_MSGQUEUEOVERFLOW otherwise */
inline addMessageInQueue(queuePtr, fromth, smsg, i){
  i=0;
  do
    :: (i < MAXNBMSGINQUEUE) && (queuePtr.from[i] == EMPTY_CELL) ->
       
       queuePtr.message[i].service = smsg.service;
       queuePtr.message[i].arg = smsg.arg;
       queuePtr.from[i] = fromth;
       i = TM_OK;
       
       break
    :: (i < MAXNBMSGINQUEUE) && (!(queuePtr.from[i] == EMPTY_CELL)) ->
       i++;
    :: (i >= MAXNBMSGINQUEUE) ->
       i = TM_MSGQUEUEOVERFLOW;
       break
  od;  
}

#define TM_NOSUCHMESSAGE 1

inline getMessageFromQueue(queuePtr, fromth, smsg, i){
  i = 0;
  do
    :: (i < MAXNBMSGINQUEUE) && (queuePtr.from[i] == EMPTY_CELL) ->
       i++
    :: (i < MAXNBMSGINQUEUE) && !(queuePtr.from[i] == EMPTY_CELL) ->
       if
         :: (fromth == ANY) || (fromth == queuePtr.from[i]) ->
            smsg.service = queuePtr.message[i].service;
            smsg.arg = queuePtr.message[i].arg;
            fromth = queuePtr.from[i];
            queuePtr.from[i] = EMPTY_CELL;
            break
         :: else -> i++
       fi;
    :: (i >= MAXNBMSGINQUEUE) ->
       i = TM_NOSUCHMESSAGE;
       break
  od;  
}


// Scheduler (Threads/TMScheduler.c)
// (random algorithm)
inline schedule(i){
  
  if
    :: (used[sched_running] == true) && (mem[sched_running].schedInfo.status == RUNNING) -> mem[sched_running].schedInfo.status = READY;
    :: else -> skip;
  fi;
  
  i = 0;
  sched_running = ANY;
  
  do
    :: (i < MAX_THREAD) ->
       if
         :: (used[i] == true && mem[i].schedInfo.status == READY) ->
            if
              :: (sched_running < MAX_THREAD) ->
                 if
                   :: (mem[sched_running].schedInfo.prio > mem[i].schedInfo.prio) ->
                      sched_running = i; i++;
                   :: else -> i++;
                 fi;
              :: else -> sched_running = i; i++;
            fi;
         :: else -> i++;
       fi;
    :: (i >= MAX_THREAD) -> break;
  od;

  mem[sched_running].schedInfo.status = RUNNING;
  
};

// Restore_context in Threads/ia32/TMHalAsm.S
inline restore_context(){	
  d_step{				
    CPU_MODE = mem[sched_running].privilege;
    curr_id = sched_running;
    _curr_ctxt = mem[sched_running].contextPtr;
  };	
};

// Threads/TMThread.c
inline threadBuild(id/*desc id*/, ctxt /*spin pid*/, priv, schedprio, tmp){
  mem[id].privilege = priv;
  mem[id].contextPtr = ctxt;
  // initially the thread is ready and does not wait for messages
  mem[id].schedInfo.status = READY;
  mem[id].schedInfo.prio = schedprio;
  initMsgQueue(mem[id].msgQueue, tmp);
};

// install the interrupt handler
inline tmInstallHandlers(){
  int_handler_ctxt = run int_handler();
};

/*******************************/
/* Kernel Initialization model */
/*******************************/

// tmInit in Threads/TMInit.c
inline tmInit(i, tmp){
  _user_thread_init(i);
  _killed_init(i);
  hmAlloc(tmThread_id);
  i = run tmThread();
  threadBuild(tmThread_id, i, KERNEL, KERNEL_PRIORITY, tmp);
  tmInstallHandlers();
  _syst_run = true;
  sched_running = 0;
  timer_init();
  schedule(tmp);
  atomic{
    restore_context();
    run timer();
  }
};


/***************************/
/* Interrupt Handler Model */
/***************************/


// kSend Threads/ia32/TMIPC.c 
inline kSend(smsg, to ,id, reply, i){  
  if
    :: (to > MEMBLOCK_N || !used[to]) -> reply ! MSG_SENDFAILED, 0, smsg; skip;
    :: else -> 
       if
         :: (smsg.service != TM_EXIT) -> reply ! MSG_SENDOK, 0, smsg;
         :: else -> skip
       fi;
       if
         /* the thread is waiting for this message */
         :: (mem[to].msgQueue.msgPendingStatus == WAITING) && ((mem[to].msgQueue.threadIdPending == id) || (mem[to].msgQueue.threadIdPending == ANY)) ->
            mem[to].schedInfo.status = READY;
            mem[to].msgQueue.msgPendingStatus = NOT_WAITING; 			
            mem[to].msgQueue.msgPendingPtr ! MSG_RECVOK, id, smsg;
         :: else ->
            addMessageInQueue(mem[to].msgQueue, id, smsg, i);

            /* management of overflow
            if 
              :: i = TM_MSGQUEUEOVERFLOW ->
                 if
                   :: !(mem[to].privilege) -> skip;
                   :: else -> skip;
                 fi;	
              :: else -> skip
            fi;
            */
            
       fi;
  fi;                 
};					

// kRecv Threads/ia32/TMIPC.c 
inline kRecv(smsg, from, id, reply, i){
  getMessageFromQueue(mem[id].msgQueue, from, smsg, i);
  if
    :: (i == TM_NOSUCHMESSAGE) ->
       mem[id].msgQueue.threadIdPending = from;
       _reply_chan[id] = reply;
       mem[id].msgQueue.msgPendingPtr = reply;
       mem[id].schedInfo.status = BLOCKED;
       mem[id].msgQueue.msgPendingStatus = WAITING;
    :: else ->
       reply ! MSG_RECVOK, from, smsg;
  fi;
};


// _INTHandler in Threads/ia32/TMHal.c 
proctype int_handler() provided (_curr_ctxt == _pid){

  chan reply;
  service_msg smsg;	
  byte i;
  byte fromto;
  
end:do
      :: interrupt ? i;
         if
           :: (i == SOFT_INT) ->
              if 					
                :: full(syst_call) ->
                   if
                     :: syst_call ? MSG_SND, fromto, smsg, reply ->
                        kSend(smsg, fromto, curr_id, reply, i);			
                     :: syst_call ? MSG_RECV, fromto, smsg, reply -> 
                        kRecv(smsg, fromto, curr_id, reply, i);
                   fi;
                :: nfull(syst_call) -> skip
              fi;
           :: (i == TIMER_INT) ->
              skip
           :: (i == SEGFAULT_INT) ->
              mem[sched_running].schedInfo.status=BLOCKED;
         fi;
         
         schedule(i);

         atomic{
           time.counter = 0;
           restore_context();
         };
  od;			
};



/************************/
/* Kernel Threads Model */
/************************/

// iddleThread

proctype idleThread() provided (_curr_ctxt == _pid){

  do
    :: setint(SOFT_INT);
  od;

}

// thread manager thread 

//tmMain(..) in Threads/TMMain.c
proctype tmThread() provided (_curr_ctxt == _pid){

  int i,j;
  service_msg smsg;
  chan reply = [1] of {mtype, byte, service_msg};
  byte fromto, tmp;

  hmAlloc(ioThread_id);
  i = run ioThread();
  threadBuild(ioThread_id, i, KERNEL, KERNEL_PRIORITY, tmp);

  hmAlloc(j);
  i = run idleThread();
  threadBuild(j, i, KERNEL, IDLE_PRIORITY, tmp);
  
  hmAlloc(j);
  i = run uThread();
  threadBuild(j, i, USER, KERNEL_PRIORITY, tmp);
  _user_thread[j]=true;
  ut_init_ctxt = i;
  ut_init_id = j;
  
end:do
      :: fromto = ANY; recvmsg(fromto, smsg, reply); 
         if 
           :: (smsg.service == TM_START) -> 
              hmAlloc(j);
              if
                :: (j == -1) ->
                   smsg.service = TM_STARTFAILED;
                   sndmsg(fromto, smsg, reply);
                :: else ->					
                   i = run uThread();		
                   if
                     :: (i == 0)->
                        smsg.service = TM_STARTFAILED;
                        sndmsg(fromto, smsg, reply);
                     :: else ->
                        printf("new thread id:%d\n",i);
                        _killed[i]=false;
                        _spin_process = i;
                        threadBuild(j, i, USER, USER_PRIORITY, tmp);
                        _user_thread[j] = true;
                        smsg.service = TM_STARTOK;
                        smsg.arg = j;
                        sndmsg(fromto, smsg, reply);
                   fi;
              fi;
           :: (smsg.service == TM_EXIT) -> 
              _user_thread[fromto]=false;
              _killed[mem[fromto].contextPtr]=true;	
              hmFree(fromto);
           :: else -> 
              smsg.service = UNKNOWN_SYSCALL;
              sndmsg(fromto, smsg, reply);
         fi;
  od;
}

// the network is modeled as two channels

chan network_in = [1] of {byte};
chan network_out = [1] of {byte};

// a proctype that represents a network client

active proctype echo_client(){

  byte nr,na;
  
  do
    :: 	if
          :: nr = 0
          :: nr = 1
       fi;
       network_in ! nr;
       network_out ? na;
       // assert that the echo server is correct
       assert (nr == na);
  od;
}

// kernel thread that manages the network 

proctype ioThread_network(byte ioThread_network_id) provided (_curr_ctxt == _pid){

  service_msg smsg;
  chan reply = [1] of {mtype, byte, service_msg};
  byte fromto;
  
end:do
      :: fromto = ANY;
         recvmsg(fromto, smsg, reply); 
         if
           :: smsg.service == IO_READ ->
              if 
                :: empty(network_in) -> 
                   smsg.service = IO_READFAILED;
                   sndmsg(fromto, smsg, reply);
                :: nempty(network_in) ->
                   smsg.service = IO_READOK;
                   network_in ? smsg.arg;
                   sndmsg(fromto, smsg, reply);
              fi;
           :: smsg.service == IO_WRITE ->
              if 
                :: full(network_out) ->
                   smsg.service = IO_WRITEFAILED;
                   sndmsg(fromto, smsg, reply);
                :: nfull(network_out) ->
                   smsg.service = IO_WRITEOK;
                   network_out ! smsg.arg;
                   sndmsg(fromto, smsg, reply);
              fi;
           :: else ->
              smsg.service = UNKNOWN_SYSCALL;
              sndmsg(fromto, smsg, reply);
         fi;
  od;
}

//ioMain(..) in IO/IOMain.c
proctype ioThread() provided (_curr_ctxt == _pid){

  
  service_msg smsg;
  int ioThread_network_id;
  byte i, fromto;
  chan reply = [1] of {mtype, byte, service_msg};

  /* starting a "network device driver" = kernel thread */
  hmAlloc(ioThread_network_id);
  if
    :: ioThread_network_id == -1 -> skip;
    :: else ->
       i = run ioThread_network(ioThread_network_id);
       threadBuild(ioThread_network_id, i, KERNEL, KERNEL_PRIORITY, fromto);
       mem[ioThread_network_id].schedInfo.status = READY;
  fi;	
  
end:do
      :: fromto = ANY;
         recvmsg(fromto, smsg,reply); 
         if
           :: smsg.service == IO_OPEN ->
              if 
                :: ioThread_network_id == -1 -> 
                   smsg.service = IO_OPENFAILED;
                   sndmsg(fromto, smsg, reply);
                :: else ->
                   smsg.service = IO_OPENOK;
                   smsg.arg = ioThread_network_id;
                   sndmsg(fromto, smsg, reply);
              fi;
           :: smsg.service == IO_CLOSE ->
              if 
                :: ioThread_network_id == -1 -> 
                   smsg.service = IO_CLOSEFAILED;
                   sndmsg(fromto, smsg, reply);
                :: else ->
                   smsg.service = IO_CLOSEOK;
                   smsg.arg = ioThread_network_id;
                   sndmsg(fromto, smsg, reply);
              fi;
           :: else ->
              smsg.service = UNKNOWN_SYSCALL;
              sndmsg(fromto, smsg, reply);
         fi;		
  od;

}




/**********************************/
/* An example of user Application */
/**********************************/

proctype uThread() provided (_curr_ctxt == _pid || _killed[_pid]){
  service_msg smsg;
  byte fromto;
  chan reply = [1] of {mtype, byte, service_msg};
  byte nbth;

  nbth = SPIN_PROC_N - 10;

  
  // a test for memory protection
  // mutation(mem[0].contextPtr, _pid);
  
  if 
    :: _pid == ut_init_ctxt ->
       do
         :: (nbth > 0) ->
            fromto = tmThread_id;
            smsg.service = TM_START;
            genericSyscall(fromto, smsg, reply);
            
            if
              :: smsg.service == TM_STARTFAILED -> skip
              :: smsg.service == TM_STARTOK -> 
                 fromto = smsg.arg;
                 recvmsg(fromto, smsg, reply);       
            fi;
            nbth--;
         :: else ->
            break;

       od;
    :: else -> 
       fromto = ioThread_id;
       smsg.service = IO_OPEN;
       genericSyscall(fromto, smsg, reply);
       if
         :: smsg.service == IO_OPENFAILED -> skip;
         :: smsg.service == IO_OPENOK -> 
            fromto = smsg.arg;
            do
              :: smsg.service != IO_READOK ->
                 smsg.service = IO_READ;
                 genericSyscall(fromto, smsg, reply);
              :: else -> break
            od;
            do
              :: smsg.service != IO_WRITEOK -> 
                 smsg.service = IO_WRITE;
                 genericSyscall(fromto, smsg, reply);
              :: else -> break
            od;
            fromto = ioThread_id;
            smsg.service = IO_CLOSE;
            genericSyscall(fromto, smsg, reply);
       fi;
       // let my father know that I finished my task
       fromto = ut_init_id;
       sndmsg(fromto, smsg, reply);
  fi;

  // and ask to be killed to the thread manager
  fromto = tmThread_id;
  smsg.service = TM_EXIT;			
  atomic{
    syst_call ! MSG_SND, fromto, smsg, reply;
    setint(SOFT_INT);
  };

  printf("%d finish\n",_pid);
}


/*******************************/
/* Main function of the Kernel */
/*******************************/


// topsyMain() in Startup/Startup.c

init {

  _syst_run = false;

  byte i, tmp;

  // prevent thread execution before the first scheduling
  _curr_ctxt = 255;	
  bootloader();		
  hmInit(i);	
  tmInit(i, tmp);

}