source: CIVL/examples/pthread/pthread.cvh@ 00dbbe9

/*
  All specification references correspond to pages in the Standard for Information Technology
Portable Operating System Interface (POSIX)IEEE Computer Society Base Specifications, Issue 7.

Standard modifications to each translation:
header files are altered
errors are changed to assertion violations with appropriate messages
appropriate definitions are changed to input variables
*/

#include <civlc.h>
#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <stdbool.h>

//Mutex types
#define PTHREAD_MUTEX_DEFAULT   0
#define PTHREAD_MUTEX_NORMAL    0
#define PTHREAD_MUTEX_RECURSIVE 1
#define PTHREAD_MUTEX_ERRORCHECK 2

//Mutex Robustness Types
#define PTHREAD_MUTEX_STALLED 0
#define PTHREAD_MUTEX_ROBUST 1

//Attribute Constants
#define PTHREAD_CREATE_DETACHED 0
#define PTHREAD_CREATE_JOINABLE 1

//Mutex initializer
#define __LOCK_INITIALIZER      0
#define PTHREAD_MUTEX_INITIALIZER       {0,0,0,PTHREAD_MUTEX_NORMAL,__LOCK_INITIALIZER}
#define PTHREAD_COND_INITIALIZER        {__LOCK_INITIALIZER,0}

//Error definitions
#define EINVAL 1       //Designates an invalid value
#define ENOTSUP 2
#define EOWNERDEAD 3   //Designates the termination of the owning thread




/* Struct definitions */

/* pthread_attr_t struct definition
  Description: This struct corresponds to the pthread_attr_t which is the attribute of a pthread_t. It's fields
  define the way the pthread_t is able to interact (join/detach), (memory capacity), (scope) etc.
  
  Fields: void * stackaddr: The address of the attr's stack in memory
  size_t stacksize: The memory capacity for the attr's stack
  size_t guardsize: The guardsize attribute controls the size of the guard area for the created thread' stack. The
                    guardsize attribute provides protection against overflow of the stack pointer.
  int detachstate: Defines a threads ability to join with two values: PTHREAD_CREATE_DETACHED and PTHREAD_CREATE_JOINABLE
  int inheritsched: The inheritance scheduling policy of the thread
  int contentionscope: Defines the contention scope of the thread
  int schedpolicy: Determines the scheduling policy of the thread
  
*/

typedef struct {
  void *stackaddr;
  size_t stacksize;
  size_t guardsize;
  int detachstate;
  int inheritsched;
  int contentionscope;
  int schedpolicy;
} pthread_attr_t;

/* pthread_mutexattr_t struct definition
  Description: The pthread_mutexattr_t defines multiple attributes of a mutex and controls its interactions with threads 
  Fields: robust: defines the robustness of the mutex; if robust and the owning thread terminates, it will notify the 
          next thread of this to prevent deadlocks and other errors
          pshared: defines the process shared element of the thread and which processes can interact with the mutex
          protocol: defines the priority protocol of the mutex and which threads may interact first
          type: defines the type of the mutex as either PTHREAD_MUTEX_DEFAULT/NORMAL, PTHREAD_MUTEX_ERRORCHECK, or 
          PTHREAD_MUTEX_RECURSIVE, each explained in pthread_mutex_lock below
          prioceiling: defines the lowest priority the mutex's critical section can be at
*/

typedef struct {
  int robust;
  int pshared;
  int protocol;
  int type;
  int prioceiling;
}pthread_mutexattr_t;

/* pthread_mutex_t struct definition
  Description: The pthread_mutex_t is a locking mechanism for threads to interact with in order to control the scheduling
  of the threads. It can be locked, which allows for blocking of other threads waiting on the mutex and unlocked, allowing
  access. It has a pthread_mutexattr_t which defines its behavior.
  Fields: count - used for recursive mutex, incremented when locked, decremented when unlocked, mutex released when count is 0
  owner - current process owner of the mutex
  lock - int of 0 or 1, respectively 0 if unlocked, 1 if locked
  prioceiling - allows locking without adherence to the priority ceiling
  attr - see above
*/

typedef struct {
  int count;
  $proc owner;
  int lock;
  int prioceiling;
  pthread_mutexattr_t *attr;
} pthread_mutex_t;

//Unimplemented
/*
typedef struct {
  int pshared;
  clockid_t clock_id;
}pthread_condattr_t;
*/

/* pthread_cond_t struct definition
  Description: The pthread_cond_t is another locking mechanism which interacts with the mutex variable. When
  the mutex is locked, the condition can be accessed, leading the accessing thread to unlock it, and sleep
  until the signal is given
  Fields: proccount - specifies the number of processes/threads still waiting on this condition variable
  signal - Boolean value stating whether the condition is satisfied (indicated by 1) or not (0)
*/

typedef struct {
  int proccount;
  _Bool signal;
} pthread_cond_t;

/* pthread_t struct definition
  Description: The pthread_t is a struct containing a $proc variable as well as a thread attribute which defines
  its interactions with other threads. It encapsulates the $proc and allows attributes to apply to it.
  Fields: thr: the $proc variable that is the heart of the thread
  attr: see above
*/

typedef struct {
  $proc thr;
  const pthread_attr_t *attr;
} pthread_t;

/* pthread_attr_init method definition
  The pthread_attr_init() initializes an attribute with the default values defined for it by an implementation.  
  At the moment, the pthread_attr_t is very basic, only supporting joining/detaching but will be improved 
  upon at a later date.
  Corresponding specification: p. 153
*/ 

int pthread_attr_init(pthread_attr_t *attr){
  attr->stacksize = 0;
  attr->guardsize = 0;
  attr->detachstate = PTHREAD_CREATE_DETACHED;
  //attr->inheritsched = PTHREAD_EXPLICIT_SCHED;
  //attr->scope = PTHREAD_SCOPE_SYSTEM;
  attr->stackaddr = NULL;
  //attr->schedpolicy = SCHED_OTHER;
  return 0;
}

/* pthread_attr_destroy method definition
  This implementation effectively uninitializes the attr variable, which works accordingly with the specification's requirements.
  Corresponding specification: p. 153/4
*/
int pthread_attr_destroy(pthread_attr_t *attr)
{ 
  pthread_attr_t blank;
  
  *attr = blank;
  return 0; 
}

//Set the detachstate attribute
//Corresponding specification: p. 153/4 
int pthread_attr_setdetachstate(pthread_attr_t *attr, int detachstate)
{
  attr->detachstate = detachstate;
  return 0;
}

//Return the detachstate attribute
//Corresponding specification: p. 153/4 
int pthread_attr_getdetachstate(const pthread_attr_t *attr, int *detachstate)
{
  *detachstate = attr->detachstate;
  return 0;
}

//Set scheduling inheritance 
//Corresponding specification: p. 153/4 
int pthread_attr_setinheritsched(pthread_attr_t *attr, int inheritsched)
{
  attr->inheritsched = inheritsched;
  return 0;
}

//Return the scheduling inheritance 
//Corresponding specification: p. 153/4 
int pthread_attr_getinheritsched(const pthread_attr_t *attr, int *inheritsched)
{
  *inheritsched = attr->inheritsched;
  return 0;
}

/*Set scheduling contention scope 
//Corresponding specification: p. 153/4 
int pthread_attr_setscope(pthread_attr_t *attr, int contentionscope)
{
  attr->scope = contentionscope;
  return 0;
}

//Return the scheduling contention scope 
//Corresponding specification: p. 153/4 
int pthread_attr_getscope(const pthread_attr_t *attr, int *contentionscope)
{
  *contentionscope = attr->scope;
  return 0;
}
*/

// Set the stack size and stack address of the specified pthread_attr_t
// Corresponding specification p.1548
int pthread_attr_setstack(pthread_attr_t *attr, void * stackaddr, size_t stacksize){ 
  attr->stackaddr = stackaddr;
  attr->stacksize = stacksize;
  return 0;
}

// Get the stack size and stack address of the specified pthread_attr_t
// Corresponding specification p.1548
int pthread_attr_getstack(const pthread_attr_t *attr, void ** stackaddr, size_t *stacksize){
{
  *stackaddr = attr->stackaddr;
  *stacksize = attr->stacksize;
  return 0;
}

//Set guard size
//Corresponding specification: p. 153/4 
int pthread_attr_setguardsize(pthread_attr_t *attr, size_t guardsize)
{
  attr->guardsize = guardsize;
  return 0;
}

// Return guard size
//Corresponding specification: p. 153/4 
int pthread_attr_getguardsize(const pthread_attr_t *attr, size_t *guardsize)
{
  *guardsize = attr->guardsize;
  return 0;
}

//Set scheduling policy
//Corresponding specification: p. 153/4 
int pthread_attr_setschedpolicy(pthread_attr_t *attr, int policy)
{
  attr->schedpolicy = policy;
  return 0;
}

// Return scheduling policy
//Corresponding specification: p. 153/4
int pthread_attr_getschedpolicy(const pthread_attr_t *attr, int *policy)
{
  *policy = attr->schedpolicy;
  return 0;
}

/* pthread_mutexattr_init method definition
  This method defines the default values for each of the mutexattr's field
  //Corresponding specification: p. 165
*/

int pthread_mutexattr_init(pthread_mutexattr_t *attr){
  attr->robust = 0;
  attr->pshared = 0;
  attr->protocol = 0;
  attr->type = 0;
  attr->prioceiling = 0;
  return 0;
}

/* pthread_mutexattr_destroy method definition
  This implementation effectively uninitializes the attr variable, which works accordingly with the specification's requirements.
  //Corresponding specification: p. 165
*/

int pthread_mutexattr_destroy(pthread_mutexattr_t *attr){
  pthread_mutexattr_t blank;
  
  *attr = blank;
  return 0;
}

int pthread_mutexattr_getrobust(const pthread_mutexattr_t *attr, int *robust){
  *robust = attr->robust;
  return 0;
}

int pthread mutexattr_setrobust(pthread_mutexattr_t *attr, int robust){
  attr->robust = robust;
  return 0;
}

int pthread_mutexattr_getpshared(const pthread_mutexattr_t *attr, int *pshared){
  *pshared = attr->pshared;
  return 0;
}

int pthread mutexattr_setpshared(pthread_mutexattr_t *attr, int pshared){
  attr->pshared = pshared;
  return 0;
}

int pthread_mutexattr_getprotocol(const pthread_mutexattr_t *attr, int *protocol){
  *protocol = attr->protocol;
  return 0;
}

int pthread mutexattr_setprotocol(pthread_mutexattr_t *attr, int protocol){
  attr->protocol = protocol;
  return 0;
}

int pthread_mutexattr_gettype(const pthread_mutexattr_t *attr, int *type){
  *type = attr->type;
  return 0;
}

int pthread mutexattr_settype(pthread_mutexattr_t *attr, int type){
  attr->type = type;
  return 0;
}

int pthread_mutexattr_getprioceiling(const pthread_mutexattr_t *attr, int *prioceiling){
  *prioceiling = attr->prioceiling;
  return 0;
}

int pthread mutexattr_setprioceiling(pthread_mutexattr_t *attr, int prioceiling){
  attr->prioceiling = prioceiling;
  return 0;
}


/* pthread_mutex_init method definition
  This method initializes each of the mutex's default values as well as being able to take values from another attribute
  if desired, otherwise the attribute field may be NULL
  //Corresponding specification: p. 164
*/

int pthread_mutex_init(pthread_mutex_t *mutex, const pthread_mutexattr_t *attr){
  if(attr == NULL){
    mutex->attr = (pthread_mutexattr_t *)malloc(sizeof(pthread_mutexattr_t));
    mutex->attr->robust = 0;
    mutex->attr->pshared = 0;
    mutex->attr->protocol = 0;
    mutex->attr->type = PTHREAD_MUTEX_DEFAULT;
    mutex->attr->prioceiling = 0;
  }
  else{
    mutex->attr = (pthread_mutexattr_t *)malloc(sizeof(pthread_mutexattr_t));
    mutex->attr = attr;
  }
  mutex->lock = 0;
  mutex->count = 0;
  mutex->owner = $proc_null;
  return 0;
}

/* pthread_mutex_destroy method definition
  This implementation effectively uninitializes the mutex variable, which works accordingly with the specification's requirements.
  //Corresponding specification: p. 164 
*/

int pthread_mutex_destroy(pthread_mutex_t *mutex){
  pthread_mutex_t blank;
  
  *mutex = blank;
  return 0;
}

/* pthread_cond_init method definition 
  Initializes the condition variable so that it begins with 0 processes waiting on it as well as a signal set to be zero
   **Needs to be modified to work with condition attributes as the second parameter
  //Corresponding specification: p. 158 
*/

void pthread_cond_init(pthread_cond_t *cond, void *arg){
  cond->proccount = 0;
  cond->signal = 0;
}



/* pthread_cond_destroy method definition
  This implementation effectively uninitializes the cond variable, which works accordingly with the specification's requirements.
  If any threads are still waiting on the condition upon destruction, an error is returned.
  //Corresponding specification: p. 158 
*/

int pthread_cond_destroy(pthread_cond_t *cond){
  if(cond->proccount != 0){
    $assert($false, "ERROR: Threads still waiting on specified condition variable");
  }
  else{
    pthread_cond_t blank;
    *cond = blank;
  }
  return 0;
}

/* pthread_create method definition
  Description: Defines a pthread_t by assigning it an attribute value (by value so the original attribute's state is
  irrelevant), and spawning a process as the thr field with arguments void *arg
  //Corresponding specification: p. 160
*/

int pthread_create(pthread_t *thread, const pthread_attr_t *attr, void *(*start_routine)(void*), void *arg){
  thread->thr = $spawn start_routine(arg);
  if(attr == NULL){
    thread->attr = (pthread_attr_t *)malloc(sizeof(pthread_attr_t));
    thread->attr->stackaddr = NULL;
    thread->attr->stacksize = 0;
    thread->attr->guardsize = 0;
    thread->attr->detachstate = 1;
    thread->attr->inheritsched = 0;
    thread->attr->contentionscope = 0;
    thread->attr->schedpolicy = 0;
  }
  else{
    thread->attr = (pthread_attr_t *)malloc(sizeof(pthread_attr_t));
    thread->attr->stackaddr = attr->stackaddr;
    thread->attr->stacksize = attr->stacksize;
    thread->attr->guardsize = attr->guardsize;
    thread->attr->detachstate = attr->detachstate;
    thread->attr->inheritsched = attr->inheritsched;
    thread->attr->contentionscope = attr->contentionscope;
    thread->attr->schedpolicy = attr->schedpolicy;
  }
  return 0;
}

/* pthread_join method definition 
  Description: Causes current thread to wait on thread specified as a parameter. If specified thread's detachstate field is set as PTHREAD_CREATE_DETACHED,
  error will be returned stating the the thread cannot be joined.
  //Corresponding specification: p. 160
*/ 

int pthread_join(pthread_t thread, void **value_ptr){
  if(thread.attr != NULL){
    if(thread.attr->detachstate == 0){
      $assert($false, "Thread is designated as unjoinable");
      return 1;
    }
  }
  $wait(thread.thr);
  return 0;
}

/* pthread_exit method definition
  Description: Causes current thread to immediately terminate; if currently in the main method as specified by the 
  isMain parameter, the main method will wait for each thread to terminate before it terminates
  //Corresponding specification: p. 160 
*/

int pthread_exit(void *arg, _Bool isMain, pthread_t *arr, int len){
  if(isMain){
    for(int i = 0; i<len; i++)
      $wait(arr[i].thr);
  }
  $exit();
  return 0;
}

//Unimplemented
int pthread_detach(pthread_t thread);

/* pthread_mutex_lock method definition
  Description: pthread_mutex_lock takes in a mutex variable and acts accordingly to its current state and type
  PTHREAD_MUTEX_NORMAL: Checks to see whether mutex is already locked and behaves accordingly
    locked and owner: Relock error, returns 0
    locked and not owner: Waits until mutex is unlocked and then locks and becomes owner
    unlocked and not owner: Locks the mutex and becomes owner
  PTHREAD_MUTEX_RECURSIVE: A recursive mutex increments its count when it is locked and decremented when
  it is unlocked and the lock is released when the count reaches 0.
  PTHREAD_MUTEX_ERRORCHECK: Currently implemented similarly to PTHREAD_MUTEX_NORMAL
  //Corresponding specification: p. 163 
*/

int pthread_mutex_lock(pthread_mutex_t *mutex){
  $atomic{
    if (mutex->attr->type == PTHREAD_MUTEX_NORMAL){
      if (mutex->lock != 0) {
        if(mutex->owner == $proc_null){
          if(mutex->attr->robust == PTHREAD_MUTEX_ROBUST){
            $when(mutex->lock == 0);
          }
          else{
            $assert($false);
            return EOWNERDEAD;
          }
        }
        else{
          if(mutex->owner == $self){
            $assert($false);
            return 0;
          }
          else{
            $when(mutex->lock == 0); 
          }
        }
      }
      mutex->owner = $self;
      mutex->lock = 1;
    } 
    else {
      int tmp = mutex->lock;
      
      mutex->lock = 1;
      if (tmp == 0) { // Attempts lock and checks for whether lock is already locked
        mutex->count = 1; 
        mutex->owner = $self;
      } 
      else {
        //Checks for ownership, otherwise returns error
        if(mutex->owner == $self){
          // Checks for recursive mutex, otherwise returns an error 
          if (mutex->attr->type == PTHREAD_MUTEX_RECURSIVE) {
            mutex->count++;
          }
          else {
            $assert($false);
            return 0;
          }
        }
        else {
          $assert($false, "ERROR: Relock attempted on non-recursive mutex\n");
          return 0;
        }
      }
    }
    return 0;
  }
}

/* pthread_mutex_lock method definition
  Description: pthread_mutex_trylock takes in a mutex variable and acts similarly to pthread_mutex_lock except that 
  if the mutex is locked, success will be returned immediately. In the case of a recursive mutex, the count will
  be incremented and will return successfully.
  //Corresponding specification: p. 163 
*/

int pthread_mutex_trylock(pthread_mutex_t *mutex){
  $atomic{
    if (mutex->attr->type == PTHREAD_MUTEX_NORMAL){
      if (mutex->lock != 0) {
        return 0;
      }
      mutex->owner = $self;
      mutex->lock = 1;
    } 
    else {
      int tmp = mutex->lock;
      
      mutex->lock = 1;
      if (tmp == 0) { // Attempts lock and checks for whether lock is already locked
        mutex->count = 1; 
        mutex->owner = $self;
      } 
      else {
        //Checks for ownership, otherwise returns error
        if(mutex->owner == $self){
          // Checks for recursive mutex, otherwise returns an error 
          if (mutex->attr->type == PTHREAD_MUTEX_RECURSIVE) {
            mutex->count++;
          }
          else {
            $assert($false);
            return 0;
          }
        }
        else {
          return 0;
        }
      }
    }
    return 0;
  }
}

/* pthread_mutex_lock method definition
  Description: pthread_mutex_lock takes in a mutex variable and acts accordingly to its current state and type
  PTHREAD_MUTEX_NORMAL: Checks to see whether mutex is already unlocked and behaves accordingly
    unlocked: returns error
    locked: unlocks
  PTHREAD_MUTEX_RECURSIVE: A recursive mutex increments its count when it is locked and decremented when
  it is unlocked and the lock is released when the count reaches 0.
  PTHREAD_MUTEX_ERRORCHECK: Currently implemented similarly to PTHREAD_MUTEX_NORMAL
  //Corresponding specification: p. 163 
*/

int pthread_mutex_unlock(pthread_mutex_t *mutex){
  $atomic{
    if (mutex->attr->type == 0 || mutex->attr->type == 2) {
      int idx;
      
      // Attempts unlock, if already unlocked, returns error
      if (mutex->lock == 0 && mutex->attr->type == PTHREAD_MUTEX_DEFAULT) {
        $assert($false);
        return 0;
      }
      else if (mutex->lock == 0 && mutex->attr->type == PTHREAD_MUTEX_ERRORCHECK){
        $assert($false, "Attempting to unlock unlocked lock\n");
        return 0;
      }
      else {
        mutex->lock = 0;
        mutex->owner = $proc_null;
      }
    } 
    else {
      //Checks for ownership of thread, if not, returns error
      if(mutex->owner == $self)
      {
        //Checks for recursive mutex
        _Bool tmp = !(mutex->attr->type == 1);
        
        if (--mutex->count == 0){
          mutex->lock = 0;
          mutex->owner = $proc_null;
        }
      }
      else {
        $assert($false);
        return 0;
      }
    }
    return 0;
  }
}

/* pthread_mutex_consistent method definition
  Description: Checks for robustness of mutex: if robust, the mutex is unlocked, otherwise an error is caused
  and EINVAL is returned
*/
int pthread_mutex_consistent(pthread_mutex_t *mutex){
  if(mutex->attr->robust == PTHREAD_MUTEX_ROBUST){
    mutex->lock = 0;
    return 0;
  }
  $assert($false);
  return EINVAL;
}

/* pthread_cond_wait method definition
  Description: Checks for calling thread as owner of the mutex, then increments proccount, unlocks the mutex 
  and sleeps. Awakens upon signal and decrements proccount and locks mutex.
  //Corresponding specification: p. 158
*/

int pthread_cond_wait(pthread_cond_t *cond, pthread_mutex_t *mutex){
  if(mutex->owner != $self){
    printf("Mutex not owned by thread");
    $assert($false);
    return 0;
  }
  
  cond->proccount= cond->proccount+1;
  pthread_mutex_unlock(mutex);
  
  $when(cond->signal);
  cond->signal = false;
  --cond->proccount;
  $when(mutex->lock == 0){pthread_mutex_lock(mutex);}
  return 0;
}

/* pthread_cond_signal method definition
  Description: Signals the condition by setting the signal to true
  //Corresponding specification: p. 158
*/

int pthread_cond_signal(pthread_cond_t *cond){
  cond->signal = true;
  return 0;
}

/* pthread_cond_broadcast method definition
  Description: Repeated signals the condition until all processes waiting have been signalled and awoken
  //Corresponding specification: p. 157 
*/

int pthread_cond_broadcast(pthread_cond_t *cond){
  while(cond->proccount > 0){
    cond->signal = true;
  }
  return 0;
}