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