pthread.cc

   1 #include "common.h"
   2 #include "threads-model.h"
   3 #include "action.h"
   4 #include "mypthread.h"
   5
   6 #include "snapshot-interface.h"
   7 #include "datarace.h"
   8
   9 #include "mutex.h"
  10 #include <condition_variable>
  11
  12 /* global "model" object */
  13 #include "model.h"
  14 #include "execution.h"
  15 #include <errno.h>
  16
  17 int pthread_create(pthread_t *t, const pthread_attr_t * attr,
  18          pthread_start_t start_routine, void * arg) {
  19         if (!model) {
  20                 snapshot_system_init(10000, 1024, 1024, 40000);
  21                 model = new ModelChecker();
  22                 model->startChecker();
  23         }
  24
  25         struct pthread_params params = { start_routine, arg };
  26
  27         ModelAction *act = new ModelAction(PTHREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)&params);
  28
  29         /* seq_cst is just a 'don't care' parameter */
  30         model->switch_to_master(act);
  31
  32         return 0;
  33 }
  34
  35 int pthread_join(pthread_t t, void **value_ptr) {
  36         ModelExecution *execution = model->get_execution();
  37         Thread *th = execution->get_pthread(t);
  38
  39         model->switch_to_master(new ModelAction(PTHREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(th->get_id())));
  40
  41         if ( value_ptr ) {
  42                 // store return value
  43                 void *rtval = th->get_pthread_return();
  44                 *value_ptr = rtval;
  45         }
  46         return 0;
  47 }
  48
  49 int pthread_detach(pthread_t t) {
  50         //Doesn't do anything
  51         //Return success
  52         return 0;
  53 }
  54
  55 void pthread_exit(void *value_ptr) {
  56         Thread * th = thread_current();
  57         th->set_pthread_return(value_ptr);
  58         model->switch_to_master(new ModelAction(THREADONLY_FINISH, std::memory_order_seq_cst, th));
  59         //Need to exit so we don't return to the program
  60         real_pthread_exit(NULL);
  61 }
  62
  63 int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
  64         if (!model) {
  65                 snapshot_system_init(10000, 1024, 1024, 40000);
  66                 model = new ModelChecker();
  67                 model->startChecker();
  68         }
  69         cdsc::snapmutex *m = new cdsc::snapmutex();
  70
  71         ModelExecution *execution = model->get_execution();
  72         execution->getMutexMap()->put(p_mutex, m);
  73
  74         return 0;
  75 }
  76
  77 int pthread_mutex_lock(pthread_mutex_t *p_mutex) {
  78         if (!model) {
  79                 snapshot_system_init(10000, 1024, 1024, 40000);
  80                 model = new ModelChecker();
  81                 model->startChecker();
  82         }
  83
  84         ModelExecution *execution = model->get_execution();
  85
  86         /* to protect the case where PTHREAD_MUTEX_INITIALIZER is used
  87            instead of pthread_mutex_init, or where *p_mutex is not stored
  88            in the execution->mutex_map for some reason. */
  89         if (!execution->getMutexMap()->contains(p_mutex)) {
  90                 pthread_mutex_init(p_mutex, NULL);
  91         }
  92
  93         cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
  94
  95         if (m != NULL) {
  96                 m->lock();
  97         } else {
  98                 return 1;
  99         }
 100
 101         return 0;
 102 }
 103
 104 int pthread_mutex_trylock(pthread_mutex_t *p_mutex) {
 105         if (!model) {
 106                 snapshot_system_init(10000, 1024, 1024, 40000);
 107                 model = new ModelChecker();
 108                 model->startChecker();
 109         }
 110
 111         ModelExecution *execution = model->get_execution();
 112         cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
 113         return m->try_lock();
 114 }
 115 int pthread_mutex_unlock(pthread_mutex_t *p_mutex) {
 116         ModelExecution *execution = model->get_execution();
 117         cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
 118
 119         if (m != NULL) {
 120                 m->unlock();
 121         } else {
 122                 printf("try to unlock an untracked pthread_mutex\n");
 123                 return 1;
 124         }
 125
 126         return 0;
 127 }
 128
 129 int pthread_mutex_timedlock (pthread_mutex_t *__restrict p_mutex,
 130          const struct timespec *__restrict abstime) {
 131 // timedlock just gives the option of giving up the lock, so return and let the scheduler decide which thread goes next
 132
 133         if (!model) {
 134                 snapshot_system_init(10000, 1024, 1024, 40000);
 135                 model = new ModelChecker();
 136                 model->startChecker();
 137         }
 138
 139         ModelExecution *execution = model->get_execution();
 140
 141         /* to protect the case where PTHREAD_MUTEX_INITIALIZER is used
 142            instead of pthread_mutex_init, or where *p_mutex is not stored
 143            in the execution->mutex_map for some reason. */
 144         if (!execution->getMutexMap()->contains(p_mutex)) {
 145                 pthread_mutex_init(p_mutex, NULL);
 146         }
 147
 148         cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
 149
 150         if (m != NULL) {
 151                 m->lock();
 152                 return 0;
 153         }
 154
 155         return 1;
 156 }
 157
 158 pthread_t pthread_self() {
 159         Thread* th = model->get_current_thread();
 160         return (pthread_t)th->get_id();
 161 }
 162
 163 int pthread_key_delete(pthread_key_t) {
 164         model_print("key_delete is called\n");
 165         return 0;
 166 }
 167
 168 int pthread_cond_init(pthread_cond_t *p_cond, const pthread_condattr_t *attr) {
 169         cdsc::snapcondition_variable *v = new cdsc::snapcondition_variable();
 170
 171         ModelExecution *execution = model->get_execution();
 172         execution->getCondMap()->put(p_cond, v);
 173         return 0;
 174 }
 175
 176 int pthread_cond_wait(pthread_cond_t *p_cond, pthread_mutex_t *p_mutex) {
 177         ModelExecution *execution = model->get_execution();
 178         if ( !execution->getCondMap()->contains(p_cond) )
 179                 pthread_cond_init(p_cond, NULL);
 180         if ( !execution->getMutexMap()->contains(p_mutex) )
 181                 pthread_mutex_init(p_mutex, NULL);
 182
 183         cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);
 184         cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
 185
 186         v->wait(*m);
 187         return 0;
 188 }
 189
 190 int pthread_cond_timedwait(pthread_cond_t *p_cond,
 191         pthread_mutex_t *p_mutex, const struct timespec *abstime) {
 192         ModelExecution *execution = model->get_execution();
 193
 194         if ( !execution->getCondMap()->contains(p_cond) )
 195                 pthread_cond_init(p_cond, NULL);
 196         if ( !execution->getMutexMap()->contains(p_mutex) )
 197                 pthread_mutex_init(p_mutex, NULL);
 198
 199         cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);
 200         cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
 201
 202         model->switch_to_master(new ModelAction(ATOMIC_TIMEDWAIT, std::memory_order_seq_cst, v, (uint64_t) m));
 203         m->lock();
 204
 205         // model_print("Timed_wait is called\n");
 206         return 0;
 207 }
 208
 209 int pthread_cond_signal(pthread_cond_t *p_cond) {
 210         // notify only one blocked thread
 211         ModelExecution *execution = model->get_execution();
 212         if ( !execution->getCondMap()->contains(p_cond) )
 213                 pthread_cond_init(p_cond, NULL);
 214
 215         cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);
 216
 217         v->notify_one();
 218         return 0;
 219 }
 220
 221 int pthread_cond_broadcast(pthread_cond_t *p_cond) {
 222         // notify all blocked threads
 223         ModelExecution *execution = model->get_execution();
 224         if ( !execution->getCondMap()->contains(p_cond) )
 225                 pthread_cond_init(p_cond, NULL);
 226
 227         cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);
 228
 229         v->notify_all();
 230         return 0;
 231 }
 232
 233 int pthread_cond_destroy(pthread_cond_t *p_cond) {
 234         ModelExecution *execution = model->get_execution();
 235
 236         if (execution->getCondMap()->contains(p_cond)) {
 237                 cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);
 238                 delete v;
 239                 execution->getCondMap()->remove(p_cond);
 240         }
 241         return 0;
 242 }