source: CIVL/text/include/pthread-c.cvl@ aef8b11

extern void *value = NULL;
__pthread_pool_t _pool={.len = 0};

/*void _add_thread(__pthread_pool_t* pool, pthread_t* thread){
  $atomic{
  int len = pool->len;
  pthread_t** newThreads = (pthread_t**) malloc(sizeof(pthread_t*) * (len+1));
  
  if(pool->threads != NULL)
    for(int i = 0; i < len - 1; i++)
      *(newThreads+i) = *(pool->threads+i);
  *(newThreads+len) = thread;
  pool->threads = newThreads;
  pool->len = len + 1;
  }
}*/

/**
  * Initializes an attribute with the default values defined for it by an implementation.
  * Corresponding specification: p. 1532-4
  *
  * @param *attr
  *            The attribute to be initialized.
  * @return Returns 0 upon successful completion
  */

int pthread_attr_init(pthread_attr_t *attr){
  attr->detachstate = PTHREAD_CREATE_DETACHED;
  //attr->inheritsched = PTHREAD_EXPLICIT_SCHED;
  attr->contentionscope = PTHREAD_SCOPE_SYSTEM;
  //attr->schedpolicy = SCHED_OTHER;
  return 0;
}

/**
  * Uninitializes the specified attr variable.
  * Corresponding specification: p. 1532-4
  *
  * @param *attr
  *            The attribute to be uninitialized.
  * @return Returns 0 upon successful completion
  */

int pthread_attr_destroy(pthread_attr_t *attr)
{ 
  pthread_attr_t blank;
  
  *attr = blank;
  return 0; 
}


/**
  * Sets the detachstate field of the attribute
  * Corresponding specification: p. 1535-6
  *
  * @param *attr
  *            The attribute to have it's detachstate set
  * @param detachstate
  *            The detachstate to which the attribute's detachstate is set  
  * @return Returns 0 upon successful completion
  */

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

/**
  * Stores the detachstate value of the attribute in an alternate location
  * Corresponding specification: p. 1535-6
  *
  * @param *attr
  *            The attribute whose detachstate is to be stored
  * @param *detachstate
  *            The location at which the detachstate is to be stored  
  * @return Returns 0 upon successful completion
  */
  
int pthread_attr_getdetachstate(const pthread_attr_t *attr, int *detachstate)
{
  *detachstate = attr->detachstate;
  return 0;
}

/**
  * Set scheduling inheritance 
  * Corresponding specification: p. 1540-1
  *
  * @param *attr
  *            The attribute to have it's inheritsched set
  * @param inheritsched
  *            The inheritsched to which the attribute's inheritsched is set 
  * @return Returns 0 upon successful completion
  */

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

/**
  * Stores the inheritsched value of the attribute in an alternate location
  * Corresponding specification: p. 1540-1
  *
  * @param *attr
  *            The attribute whose inheritsched is to be stored
  * @param *intheritsched
  *            The location at which the attribute's inheritsched is to be stored  
  * @return Returns 0 upon successful completion
  */

int pthread_attr_getinheritsched(const pthread_attr_t *attr, int *inheritsched)
{
  *inheritsched = attr->inheritsched;
  return 0;
}

/**
  * Set contentionscope field of the attribute
  * Corresponding specification: p. 1546-7
  *
  * @param *attr
  *            The attribute to have it's contentionscope set
  * @param contentionscope
  *            The contentionscope to which the attribute's contentionscope is set  
  * @return Returns 0 upon successful completion
  */
 
int pthread_attr_setscope(pthread_attr_t *attr, int contentionscope)
{
  attr->contentionscope = contentionscope;
  return 0;
}

/**
  * Stores the contentionscope value of the attribute in an alternate location
  * Corresponding specification: p. 1546-7
  *
  * @param *attr
  *            The attribute whose contentionscope is to be stored
  * @param *contentionscope
  *            The location at which the attribute's contentionscope is to be stored  
  * @return Returns 0 upon successful completion
  */

int pthread_attr_getscope(const pthread_attr_t *attr, int *contentionscope)
{
  *contentionscope = attr->contentionscope;
  return 0;
}

/**
  * Sets the scheduling policy field of the attribute
  * Corresponding specification: p. 1544-45
  *
  * @param *attr
  *            The attribute to have it's scheduling policy set
  * @param policy
  *            The scheduling policy to which the attribute's scheduling policy is set  
  * @return Returns 0 upon successful completion
  */

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

/**
  * Stores the scheduling policy value in an alternate location
  * Corresponding specification: p. 1544-45
  *
  * @param *attr
  *            The attribute whose scheduling policy is to be stored
  * @param *policy
  *            The location at which the attribute's scheduling policy is to be stored  
  * @return Returns 0 upon successful completion
  */

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

/**
  * Initializes an attribute with the default values defined for it by an implementation.
  * Corresponding specification: p. 1647-51
  *
  * @param *attr
  *            The attribute to be initialized.
  * @return Returns 0 upon successful completion
  */

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

/**
  * Uninitializes the specified attr variable.
  * Corresponding specification: p. 1647-51
  *
  * @param *attr
  *            The attribute to be uninitialized.
  * @return Returns 0 upon successful completion
  */

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

/**
  * Stores the robustness value in an alternate location
  * Corresponding specification: p. 1659-1660
  *
  * @param *attr
  *            The attribute whose robustness is to be stored
  * @param *robust
  *            The location at which the attribute's robustness is to be stored  
  * @return Returns 0 upon successful completion
  */

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

/**
  * Sets the robustness field of the attribute
  * Corresponding specification: p. 1659-1660
  *
  * @param *attr
  *            The attribute to have it's robustness set
  * @param robust
  *            The robustness to which the attribute's robustness is set  
  * @return Returns 0 upon successful completion
  */
  
int pthread_mutexattr_setrobust(pthread_mutexattr_t *attr, int robust){
  attr->robust = robust;
  return 0;
}

/**
  * Stores the process shared variable in an alternate location
  * Corresponding specification: p. 1657-8
  *
  * @param *attr
  *            The attribute whose process shared variable is to be stored
  * @param *detachstate
  *            The location at which the attribute's process shared variable is to be stored  
  * @return Returns 0 upon successful completion
  */
  
int pthread_mutexattr_getpshared(const pthread_mutexattr_t *attr, int *pshared){
  *pshared = attr->pshared;
  return 0;
}

/**
  * Sets the process shared variable field of the attribute
  * Corresponding specification: p. 1657-8
  *
  * @param *attr
  *            The attribute to have it's process shared variable set
  * @param detachstate
  *            The process shared variable to which the attribute's process shared variable is set  
  * @return Returns 0 upon successful completion
  */
  
int pthread_mutexattr_setpshared(pthread_mutexattr_t *attr, int pshared){
  attr->pshared = pshared;
  return 0;
}

/**
  * Stores the protocol value in an alternate location
  * Corresponding specification: p. 1654-56
  *
  * @param *attr
  *            The attribute whose protocol is to be stored
  * @param *detachstate
  *            The location at which the attribute's protocol is to be stored  
  * @return Returns 0 upon successful completion
  */
  
int pthread_mutexattr_getprotocol(const pthread_mutexattr_t *attr, int *protocol){
  *protocol = attr->protocol;
  return 0;
}

/**
  * Sets the protocol field of the attribute
  * Corresponding specification: p. 1654-56
  *
  * @param *attr
  *            The protocol to have it's protocol set
  * @param detachstate
  *            The protocol to which the attribute's protocol is set  
  * @return Returns 0 upon successful completion
  */
int pthread_mutexattr_setprotocol(pthread_mutexattr_t *attr, int protocol){
  attr->protocol = protocol;
  return 0;
}

/**
  * Stores the type value in an alternate location
  * Corresponding specification: p. 1709-10
  *
  * @param *attr
  *            The attribute whose type is to be stored
  * @param *detachstate
  *            The location at which the attribute's type is to be stored  
  * @return Returns 0 upon successful completion
  */
int pthread_mutexattr_gettype(const pthread_mutexattr_t *attr, int *type){
  *type = attr->type;
  return 0;
}

/**
  * Sets the type field of the attribute
  * Corresponding specification: p. 1709-10
  *
  * @param *attr
  *            The attribute to have it's type set
  * @param detachstate
  *            The type to which the attribute's type is set  
  * @return Returns 0 upon successful completion
  */
int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type){
  attr->type = type;
  return 0;
}

/**
  * Stores the priority ceiling value in an alternate location
  * Corresponding specification: p. 1700-1
  *
  * @param *attr
  *            The attribute whose priority ceiling is to be stored
  * @param *detachstate
  *            The location at which the attribute's priority ceiling is to be stored  
  * @return Returns 0 upon successful completion
  */
  
int pthread_mutexattr_getprioceiling(const pthread_mutexattr_t *attr, int *prioceiling){
  *prioceiling = attr->prioceiling;
  return 0;
}

/**
  * Sets the priority ceiling field of the attribute
  * Corresponding specification: p. 1700-1
  *
  * @param *attr
  *            The attribute to have it's priority ceiling set
  * @param detachstate
  *            The priority ceiling to which the attribute's priority ceiling is set  
  * @return Returns 0 upon successful completion
  */
  
int pthread_mutexattr_setprioceiling(pthread_mutexattr_t *attr, int prioceiling){
  attr->prioceiling = prioceiling;
  return 0;
}


/**
  * Initializes a mutex with the default values defined for it by an implementation
  * or with the values defined by the mutex attribute parameter
  * Corresponding specification: p. 1676-81
  *
  * @param *mutex
  *            The mutex to be initialized.
  * @param *attr
  *            The mutex attribute which the mutex shall take as it's field. May also
  *            be null for default values to be initialized.
  * @return Returns 0 upon successful completion
  */

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

/**
  * Uninitializes the specified mutex variable.
  * Corresponding specification: p. 1676-81
  *
  * @param *mutex
  *            The mutex to be uninitialized.
  * @return Returns 0 upon successful completion
  */

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

/**
  * Initializes an condition with the default values defined for it by an implementation.
  * Corresponding specification: p. 1630-32
  *
  * @param *cond
  *            The condition to be initialized.
  * @param *arg
  *            Should be changed to condition attribute
  * @return Returns 0 upon successful completion
  */

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


/**
  * Uninitializes the specified cond variable.
  * Corresponding specification: p. 1630-2
  *
  * @param *cond
  *            The condition to be uninitialized.
  * @return Returns 0 upon successful completion
  */

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

/**
  * 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. 1649-51
  *
  * @param *thread
  *            The thread to be created with fields set from the other parameters.
  * @param *attr
  *            The attribute to be assigned to the thread
  * @param *startroutine
  *            The process to be spawned as the thread's actual 'thread'
  * @param *arg
  *            The argument to be passed to the spawned function
  *
  * @return Returns 0 upon successful completion
  */

int pthread_create(pthread_t *thread, const pthread_attr_t *attr, void *(*start_routine)(void*), void *arg){
  $atomic{
  thread->thr = $spawn start_routine(arg);
  if(attr == NULL){
    thread->attr = (pthread_attr_t *)malloc(sizeof(pthread_attr_t));
    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->detachstate = attr->detachstate;
    thread->attr->inheritsched = attr->inheritsched;
    thread->attr->contentionscope = attr->contentionscope;
    thread->attr->schedpolicy = attr->schedpolicy;
  }
  _add_thread(&_pool, thread);
  }
  return 0;
}

/**
  * 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. The value_ptr of pthread_exit shall be passed to any joining thread to the 
  * terminated thread using pthread_join's value_ptr
  * Corresponding specification: p. 1617-9
  *
  * @param thread
  *            The thread to be waited on by the current thread.
  * @param **value_ptr
  *            The location at which the pthread_exit output is accessible
  *
  * @return Returns 0 upon successful completion
  */

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);
  if(value_ptr!=NULL)
    value_ptr = &value;
  return 0;
}

/**
  * 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. The value
  * value_ptr will be made accessible in the location stated in pthread_join
  * Corresponding specification: p. 1655-6
  *
  * @param *value_ptr
  *            The value to be stored in the location stated by pthread_join
  * @param isMain
  *            Is this thread the main thread?
  * @param *arr 
  *            The array of threads which need to be waited upon by the main thread
  * @param len
  *            The length of the array of threads to be waited upon
  * @return Returns 0 upon successful completion
  */

int _pthread_exit(void *value_ptr, _Bool isMain){
  if(isMain){
    for(int i = 0; i<_pool.len; i++)
    if($proc_defined(_pool.threads[i]->thr))
      $wait(_pool.threads[i]->thr);
    $exit();
    return 0;
  }
  else{
    value = value_ptr;
    $exit();
    return 0;
  }
}

//Unimplemented
int pthread_detach(pthread_t thread);

/**
  * 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: Implemented similarly to PTHREAD_MUTEX_NORMAL, but notifies the user of errors
  * Corresponding specification: p. 1686-9
  *
  * @param *mutex
  *            The mutex to be locked
  * @return Returns 0 upon successful completion, EOWNERDEAD upon termination of owner, 
  */

/*
int pthread_mutex_lock(pthread_mutex_t *mutex){
  $choose{
    $when((mutex->attr->type == PTHREAD_MUTEX_NORMAL || mutex->attr->type == PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner == $proc_null && mutex->attr->robust == PTHREAD_MUTEX_ROBUST && mutex->lock == 0)
    {
      $atomic{
        mutex->lock = 1;
        mutex->count = 1;
        mutex->owner = $self;
      }
    }
    $when((mutex->attr->type == PTHREAD_MUTEX_NORMAL || mutex->attr->type == PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner != $proc_null && mutex->owner != $self && mutex->lock == 0)
    {
      $atomic{
        mutex->lock = 1;
        mutex->count = 1;
        mutex->owner = $self;
      }
    }
    $when((mutex->attr->type != PTHREAD_MUTEX_NORMAL && mutex->attr->type != PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner != $self && mutex->owner != $proc_null && mutex->lock == 0)
    {
      $atomic{
        mutex->lock = 1;
        mutex->count = 1;
        mutex->owner = $self;
      }
    }
    $when((mutex->attr->type == PTHREAD_MUTEX_NORMAL || mutex->attr->type == PTHREAD_MUTEX_ERRORCHECK) && mutex->lock == 0 && mutex->owner == $proc_null)
    {
      $atomic{
        mutex->lock = 1;
        mutex->count = 1;
        mutex->owner = $self;
      }
    }
    $when((mutex->attr->type == PTHREAD_MUTEX_NORMAL || mutex->attr->type == PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner == $proc_null && mutex->attr->robust != PTHREAD_MUTEX_ROBUST)
    {
      $assert($false, "Owner terminated without releasing mutex and was not robust");
      return EOWNERDEAD;
    }
    $when((mutex->attr->type == PTHREAD_MUTEX_NORMAL || mutex->attr->type == PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner != $proc_null && mutex->owner== $self)
    {
      $assert($false, "Attempting to relock locked lock");
      return EDEADLK;
    }
    $when((mutex->attr->type != PTHREAD_MUTEX_NORMAL && mutex->attr->type != PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner == $self)
    {
      mutex->count++;
    }
    $when((mutex->attr->type != PTHREAD_MUTEX_NORMAL && mutex->attr->type != PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner != $self && mutex->owner == $proc_null && mutex->attr->robust != PTHREAD_MUTEX_ROBUST)
    { 
      $assert($false, "Attempting to relock locked lock");
      return EDEADLK;
    }
  }
  return 0;
}
*/
/**
  * Takes in a mutex variable and acts similarly to pthread_mutex_lock except that 
  * if the mutex is locked, it will return immeditately. In the case of a recursive mutex, the count will
  * be incremented and will return successfully.
  * Corresponding specification: p. 1686-9
  *
  * @param *mutex
  *            The mutex to be locked
  * @return Returns 0 upon successful completion
  */

int pthread_mutex_trylock(pthread_mutex_t *mutex){
  $atomic{
    if (mutex->attr->type == PTHREAD_MUTEX_NORMAL){
      if (mutex->lock != 0) {
        return EBUSY;
      }
      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 EBUSY;
        }
      }
    }
    return 0;
  }
}

/**
  * 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. 1686-9 
  *
  * @param *mutex
  *            The mutex to be unlocked
  * @return Returns 0 upon successful completion
  */

int pthread_mutex_unlock(pthread_mutex_t *mutex){
  $atomic{
    if (mutex->attr->type == 0 || mutex->attr->type == 2) {
      // 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)
      {
        if (--mutex->count == 0){
          mutex->lock = 0;
          mutex->owner = $proc_null;
        }
      }
      else {
        $assert($false);
        return 0;
      }
    }
    return 0;
  }
}

/**
  * Checks for robustness of mutex: if robust, the mutex is unlocked, otherwise an error is caused
  * and EINVAL is returned
  * Corresponding specification: p. 1674-5
  *
  * @param *mutex
  *            The mutex to be marked as consistent
  * @return Returns 0 upon successful completion, EINVAL upon non-robust mutex input 
  */

int pthread_mutex_consistent(pthread_mutex_t *mutex){
  if(mutex->attr->robust == PTHREAD_MUTEX_ROBUST){
    mutex->lock = 0;
    return 0;
  }
  $assert($false);
  return EINVAL;
}

/**
  * 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. 1634-9
  *
  * @param *cond
  *            The condition to be waited upon until a signal is given
  * @param *mutex
  *            The mutex used to lock other threads out
  * @return Returns 0 upon successful completion, EINVAL upon non-robust mutex input 
  */

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);
  
  cond->signal = false;
  $when(cond->signal);
  cond->signal = false;
  --cond->proccount;
  $when(mutex->lock == 0){pthread_mutex_lock(mutex);}
  return 0;
}

/**
  * Signals the condition by setting the signal to true
  * Corresponding specification: p. 1627-30
  *
  * @param *cond
  *            The condition to be signalled
  * @return Returns 0 upon successful completion 
  */

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

/**
  * Repeated signals the condition until all processes waiting have been signalled and awoken
  * Corresponding specification: p. 1627-30
  *
  * @param *cond
  *            The condition to be signalled repeatedly
  * @return Returns 0 upon successful completion 
  */

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