source: CIVL/include/impls/pthread.cvl@ 4e993a9

#ifndef __CIVL_PTHREAD__
#define __CIVL_PTHREAD__

#include <civlc.cvh>
#include <stdbool.h>
#include <concurrency.cvh>
#include <pthread.h>
#include <seq.cvh>

const $scope _root = $here;
struct pthread_mutexattr_t{
  int robust;
  int pshared;
  int protocol;
  int type;
  int prioceiling;
};

struct pthread_mutex_t{
  int count;
  $proc ownerid;
  int lock;
  int prioceiling;
  pthread_mutexattr_t attr;
};

/* pthread_barrierattr_t
*/
struct pthread_barrierattr_t{ 
  int pshared;
};

/* pthread_barrier_t
  A structure which contains a global barrier which each of the threads must key into.
*/
struct pthread_barrier_t{
  pthread_barrierattr_t attr;
  int numThrds;
  int size;
  $gbarrier barr;
};
  
/* pthread_spinlock_t
  Very simple locking mechanism, spins until the lock is free.
*/
struct pthread_spinlock_t{
  $proc owner;
  _Bool lock;
  int pshared;
};

/* Implemented struct definitions */

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

struct _pthread_t{
  $proc thr;
  const pthread_attr_t attr;
  _Bool terminated;
  void** exitValue;
};

/* 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:
  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
  
*/
struct _pthread_attr_t{
  int detachstate;
  int inheritsched;
  int contentionscope;
  int schedpolicy;
  //sched_param param;
};

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


/* pthread_rwlockattr_t
*/
struct pthread_rwlockattr_t{
  int pshared;
};

/* pthread_rwlock_t struct definition
  Description: Reader-writer lock. When a reader has the lock other readers may operate, but not the writer.
  Only a single writer can operate at one time and locks out readers
*/
struct pthread_rwlock_t{
  $proc rdowners[];
  int rdlocks[];
  _Bool empty;
  $proc wrowner;
  _Bool wrlock;
  pthread_rwlockattr_t attr;
};


/* 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)
*/

struct pthread_cond_t{
  _Bool signal;
  _Bool broadcast;
};

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

struct pthread_t{
  $proc thr;
  const pthread_attr_t attr;
  _Bool terminated;
  void** exitValue;
};

extern pthread_mutex_t PTHREAD_MUTEX_INITIALIZER = {0,$proc_null,0,0,{0,0,0,0,0}};
$pthread_gpool_t $pthread_gpool = $pthread_gpool_create($here);

/**
  * Initializes a spinlock with the default values defined for it by an implementation
  * Corresponding specification: p. 
  *
  * @param *slock
  *            The spinlock to be initialized.
  * @param pshared
  *            The process shared attribute that the spinlock shall take as its field
  *
  * @return Returns 0 upon successful completion
  */

int pthread_spin_init(pthread_spinlock_t *slock, int pshared){
  slock->owner = $proc_null;
  slock->lock = true;
  slock->pshared = 0;
  return 0;
}

int pthread_spin_destroy(pthread_spinlock_t *slock){
  pthread_spinlock_t blank;
  *slock = blank;
  return 0;
}

int pthread_spin_lock(pthread_spinlock_t *slock){
  $atomic{
    $when(!slock->lock && slock->owner == $proc_null){
      slock->lock = true;
      slock->owner == $self;
    }
  }
  return 0;
}

int pthread_spin_unlock(pthread_spinlock_t *slock){
  $atomic{
    slock->owner = $proc_null;
    slock->lock = false;
  }
  return 0;
}

int pthread_rwlock_init(pthread_rwlock_t *rwlock, const pthread_rwlockattr_t * attr){
  if(attr==NULL){
    rwlock->attr.pshared = PTHREAD_PROCESS_PRIVATE;
  }
  else{
    rwlock->attr = *attr;
  }
  int zero = 0;
  $proc nu = $proc_null;
  rwlock->wrowner = $proc_null;
  rwlock->wrlock = false;
  rwlock->empty = true;
  return 0;
}

int pthread_rwlock_destroy(pthread_rwlock_t *rwlock){
  pthread_rwlock_t blank;

  *rwlock = blank;
  return 0;
}

int pthread_rwlock_rdlock(pthread_rwlock_t *rwlock){
  $when(!rwlock->wrlock){
  // Remove any function calls
    $atomic{
      int len = $seq_length(&(rwlock->rdowners));
      int one = 1;
      _Bool found = false;

      for(int x = 0; x < len; x++){
        if(rwlock->rdowners[x] == $self){
          found = true;
          rwlock->rdlocks[x]++;
          break;
        }
      }

      if(!found){
        $proc s = $self;
        $seq_insert(&(rwlock->rdowners), len, &s, 1);
        $seq_insert(&(rwlock->rdlocks), len, &one, 1);
      }
      rwlock->empty = false;
    }
  }
  return 0;
}

int pthread_rwlock_unlock(pthread_rwlock_t *rwlock){
  // Remove function calls from atomic
  $atomic{
    _Bool found = false;
    int len = $seq_length(&(rwlock->rdowners));
    for(int x = 0; x < len; x++){      
      if(rwlock->rdowners[x] == $self){
        found = true;
        rwlock->rdlocks[x]--;
        if(rwlock->rdlocks[x] == 0){
          $seq_remove(&(rwlock->rdowners), x, NULL, 1);
          $seq_remove(&(rwlock->rdlocks), x, NULL, 1);
          len--;
          x--;
          break;
        }
      }
    }
    if(!found){
      if(rwlock->wrowner == $self){
        rwlock->wrowner = $proc_null;
        rwlock->wrlock = false;
      }
    }
    if($seq_length(&(rwlock->rdowners)) == 0){
      rwlock->empty = true;
    }
    return 0;
  }
}

int pthread_rwlock_wrlock(pthread_rwlock_t *rwlock){
  $when(rwlock->empty && !(rwlock->wrlock)){
    $atomic{
      rwlock->wrlock = true;
      rwlock->wrowner = $self;
    }
  }
  return 0;
}


int pthread_barrierattr_init(pthread_barrierattr_t *attr){
  attr->pshared = 0;
  return 0;
}

int pthread_barrierattr_destroy(pthread_barrierattr_t *attr){
  pthread_barrierattr_t blank;
  *attr = blank;
  return 0;
}

/**
  * Initializes a barrier with the default values defined for it by an implementation
  * or with the values defined by the barrier attribute parameter
  * Corresponding specification: p. 
  *
  * @param *barrier
  *            The barrier 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_barrier_init(pthread_barrier_t *barrier, const pthread_barrierattr_t *attr, int count){
  if(attr == NULL){
    barrier->attr.pshared = 0;
  }
  else{
    barrier->attr = *attr;
  }
  barrier->barr = $gbarrier_create(_root, count);
  barrier->size = count;
  barrier->numThrds = 0;
  return 0;
}

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

int pthread_barrier_destroy(pthread_barrier_t *barrier){
  $gbarrier_destroy(barrier->barr);
  pthread_barrier_t blank;
  *barrier = blank;
  return 0;
}

/**
  * Creates local barrier for a thead and places it in the global barrier. It then proceeds to call the
  * $barrier_call, forcing the thread to wait until the release of the global barrier. The global barrier
  * and local barrier are then destroyed.
  *
  * @param *barrier
  *            The barrier containing the global barrier to be waited upon
  *
  * @return Returns PTHREAD_BARRIER_SERIAL_THREAD from one exiting thread, and 0 from each of the rest
  */

int pthread_barrier_wait(pthread_barrier_t *barrier){
  $barrier locbarr;
  //Remove function calls from atomic
  $atomic{
    locbarr = $barrier_create($here, barrier->barr, barrier->numThrds);
    barrier->numThrds++;
    $barrier_call(locbarr);
    
    $barrier_destroy(locbarr);
    $gbarrier_destroy(barrier->barr);
    if(barrier->numThrds == barrier->size){
      barrier->numThrds--;
      return PTHREAD_BARRIER_SERIAL_THREAD;
    }
    else{
      return 0;
    }
  }
}


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

/**
  * 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.robust = 0;
    mutex->attr.pshared = 0;
    mutex->attr.protocol = 0;
    mutex->attr.type = PTHREAD_MUTEX_NORMAL;
    mutex->attr.prioceiling = 0;
  }
  else{
    mutex->attr = *attr;
  }
  mutex->lock = 0;
  mutex->count = 0;
  mutex->ownerid = $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 * restrict cond, const pthread_condattr_t * restrict arg){
  cond->signal = 0;
  cond->broadcast = 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){
  pthread_cond_t blank;
  *cond = blank;
  return 0;
}

int pthread_equal(pthread_t t1, pthread_t t2){
  if(t1.thr==$proc_null || t2.thr==$proc_null)
    return 0;
  if(t1.thr == t2.thr){
    return 1;
  }
  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){
  //Remove function calls from atomic
  $atomic{
    thread->thr = $spawn start_routine(arg);
    if(attr == NULL){
      thread->attr.detachstate = PTHREAD_CREATE_JOINABLE;
      thread->attr.inheritsched = 0;
      thread->attr.contentionscope = 0;
      thread->attr.schedpolicy = 0;
    }
    else{
      thread->attr = *attr;
    }
    thread->terminated = false;
    thread->exitValue = NULL;
    $pthread_gpool_add($pthread_gpool, 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){
  //#ifndef _SVCOMP
  if(&thread.attr != NULL){
    if(thread.attr.detachstate == PTHREAD_CREATE_DETACHED){
      $assert($false, "Thread is designated as unjoinable");
      return 1;
    }
  }
  //#endif
  $wait(thread.thr);
  if(value_ptr!=NULL)
    *value_ptr = thread.exitValue;
  return 0;
}

void pthread_exit(void *value_ptr){
  return;
}

/**
  * 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
  */
/*void $pthread_exit(void *value_ptr, $pthread_pool_t $pthread_pool);
{
  $pthread_pool_terminates($pthread_pool, value_ptr);
  $free($pthread_pool);
  $exit();
}*/

void $pthread_exit_main(void *value_ptr, $pthread_pool_t $pthread_pool){
  $free($pthread_pool);
  $pthread_gpool_join($pthread_gpool);
  /*int len = $pthread_gpool_size($pthread_gpool);
  
  for(int i = 0; i<len; i++){
    $proc tid = $pthread_gpool_thread($pthread_gpool, i);
      
    $wait(tid);
    }    
  $free($pthread_gpool);
  */
  //$exit();
}

pthread_t $pthread_self($pthread_pool_t pool){
  return $pthread_pool_thread(pool);
}


/**
  * 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, $pthread_pool_t $pthread_pool){
  _Bool owner_term = $pthread_pool_is_terminated($pthread_pool, mutex->ownerid);
  
  $atomic{
    if (owner_term)
      if (mutex->attr.robust != PTHREAD_MUTEX_ROBUST)
        $assert($false, "Deadlock: owner terminated without robust mutex");
      else
        return EOWNERDEAD;    
    if(mutex->lock==0) {
      mutex->ownerid = $self;
      mutex->lock = 1;
      mutex->count = 1;
      return 0;
    } 
    // lock != 0:    
    if (mutex->attr.type == PTHREAD_MUTEX_NORMAL) {
      if (mutex->ownerid == $self)
        $assert($false, "Deadlock: attempted to relock a lock with PTHREAD_MUTEX_NORMAL"
                " attribute");
    } else if (mutex->attr.type == PTHREAD_MUTEX_ERRORCHECK) {
      if (mutex->ownerid == $self)
        return EDEADLK;
    } else if (mutex->ownerid == $self) {
      if (mutex->attr.type == PTHREAD_MUTEX_RECURSIVE) {
        mutex->count++;
        return 0;
      } else
        $assert($false, "Undefined behavior: attempted to relock a lock with"
                " PTHREAD_MUTEX_DEFAULT attribute");
    }
  }
  // wait for the lock:
  $when(mutex->lock == 0) 
    return $pthread_mutex_lock(mutex, $pthread_pool);
  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
  */
//Manchun: check me
int pthread_mutex_trylock(pthread_mutex_t *mutex){
  $atomic{
    if (mutex->attr.type == PTHREAD_MUTEX_NORMAL){
      if (mutex->lock != 0) {
        return EBUSY;
      }
      mutex->ownerid = $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->ownerid = $self;
      } 
      else {
        //Checks for ownership, otherwise returns error
        if(mutex->ownerid == $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 == PTHREAD_MUTEX_NORMAL || mutex->attr.type == PTHREAD_MUTEX_ERRORCHECK) {
      // 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->ownerid = $proc_null;
      }
    } 
    else {
      //Checks for ownership of thread, if not, returns error
      if(mutex->ownerid == $self)
      {
        if (--mutex->count == 0){
          mutex->lock = 0;
          mutex->ownerid = $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, $pthread_pool_t $pthread_pool){
  if(mutex->ownerid != $self){
    $assert(($false));
    return 0;
  }
  cond->signal = false;
  pthread_mutex_unlock(mutex);
  $when(cond->signal != 0 || cond->broadcast != 0)
    cond->signal = false;
  $when(mutex->lock == 0){$pthread_mutex_lock(mutex, $pthread_pool);}
  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){
  cond->broadcast = true;
  return 0;
}

#endif