source: CIVL/examples/pthread/pthread.cvh@ 37bfb99

#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}

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

/* pthread_t struct definition
Contains a $proc and a pthread_attr_t which describes how it interacts with other threads and certain methods
*/
typedef struct {
  $proc thr;
  const pthread_attr_t *attr;
} pthread_t;

/* pthread_attr_init method definition
  As stated in the specification, 'The pthread_attr_init( ) function shall initialize a thread attributes object attr with the default
  value for all of the individual attributes used by a given implementation.' At the moment, the pthread_attr_t is very basic, but will
  be improved upon at a later date.
*/ 
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->policy = SCHED_OTHER;
  return 0;
}

/* pthread_attr_destroy method definition
  As stated in the specification, 'The pthread_attr_destroy( ) function shall destroy a thread attributes object. An implementation
  may cause pthread_attr_destroy( ) to set attr to an implementation-defined invalid value. A
  destroyed attr attributes object can be reinitialized using pthread_attr_init( ); the results of
  otherwise referencing the object after it has been destroyed are undefined.'
  This implementation effectively uninitializes the attr variable, which works according with the specification's requirements.
*/
int pthread_attr_destroy(pthread_attr_t *attr)
{ 
  pthread_attr_t blank;
  *attr = blank;
  return 0; 
}

//Set the detachstate attribute 
int pthread_attr_setdetachstate(pthread_attr_t *attr, int detachstate)
{
  attr->detachstate = detachstate;
  return 0;
}

//Return the detachstate attribute
int pthread_attr_getdetachstate(const pthread_attr_t *attr, int *detachstate)
{
  *detachstate = attr->detachstate;
  return 0;
}

//Set scheduling inheritance 
int pthread_attr_setinheritsched(pthread_attr_t *attr, int inheritsched)
{
  attr->inheritsched = inheritsched;
  return 0;
}

//Return the scheduling inheritance 
int pthread_attr_getinheritsched(const pthread_attr_t *attr, int *inheritsched)
{
  *inheritsched = attr->inheritsched;
  return 0;
}

/*Set scheduling contention scope 
int pthread_attr_setscope(pthread_attr_t *attr, int contentionscope)
{
  attr->scope = contentionscope;
  return 0;
}

//Return the scheduling contention scope 
int pthread_attr_getscope(const pthread_attr_t *attr, int *contentionscope)
{
  *contentionscope = attr->scope;
  return 0;
}
*/
 
//Set the starting address of the stack of the thread
int pthread_attr_setstackaddr(pthread_attr_t *attr, void *stackaddr)
{
  attr->stackaddr = stackaddr;
  return 0;
}
 
//Return the address for the stack
int pthread_attr_getstackaddr(const pthread_attr_t *attr, void **stackaddr)
{
  *stackaddr = attr->stackaddr;
  return 0;
}

//Set stack size
int pthread_attr_setstacksize(pthread_attr_t *attr, size_t stacksize)
{
  attr->stacksize = stacksize;
  return 0;
}

//Return the stack size
int pthread_attr_getstacksize(const pthread_attr_t *attr, size_t *stacksize)
{
  *stacksize = attr->stacksize;
  return 0;
}

//Set guard size
int pthread_attr_setguardsize(pthread_attr_t *attr, size_t guardsize)
{
  attr->guardsize = guardsize;
  return 0;
}

// Return guard size
int pthread_attr_getguardsize(const pthread_attr_t *attr, size_t *guardsize)
{
  *guardsize = attr->guardsize;
  return 0;
}

//Set scheduling policy
int pthread_attr_setschedpolicy(pthread_attr_t *attr, int policy)
{
  attr->policy = policy;
  return 0;
}

// Return scheduling policy
int pthread_attr_getschedpolicy(const pthread_attr_t *attr, int *policy)
{
  *policy = attr->policy;
  return 0;
}

/* pthread_mutexattr_t struct definition
Fields: robust: defines the robustness of the mutex


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

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;
}

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

/* pthread_mutex_t struct definition
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
*/
typedef struct {
  int count;
  $proc owner;
  int lock;
  int prioceiling;
  pthread_mutexattr_t *attr;
} pthread_mutex_t;

//Initializes mutex as unlocked and with attributes defined by attr
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;
}

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

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

/* pthread_cond_t struct definition
Fields: procount - 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;

/* 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
*/
void pthread_cond_init(pthread_cond_t *cond, void *arg){
  cond->proccount = 0;
  cond->signal = 0;
}

/* Unitializes the condition parameter and then frees the data used to store it. If certains threads are still waiting when 
   pthread_cond_destroy is called, an error will be triggered.
*/
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;
}

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->policy = 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->policy = attr->policy;
  }
  return 0;
}

/* Causes current thread to wait on thread specified as a paremeter. If specified thread's detachstate field is set as PTHREAD_CREATE_DETACHED,
   error will be returned stating the the thread cannot be joined.
*/ 
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;
}

/* Calls CIVL $exit method causing the current thread to immediately terminate

*/
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;
}

int pthread_detach(pthread_t thread);

/* 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
*/
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){
        $when(mutex->lock == 0);
      }
      else{
        if(mutex->owner == $self){
          $assert($false, "ERROR: Relock attempted");
          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 == 1) {
          mutex->count++;
          if(mutex->count==0){
            mutex->lock = 0;
            mutex->owner = $proc_null;
          }
        }
        else {
          $assert($false);
          return 0;
        }
      }
      else {
        $assert($false);
        return 0;
      }
    }
  }
  return 0;
  }
}


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) {
      $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;
  }
}


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;
  }
  $atomic{
  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;
  }
}

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

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