pthread.cc

   1 #include "common.h"
   2 #include "threads-model.h"
   3 #include "action.h"
   4 #include "pthread.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
  17 static void param_defaults(struct model_params *params)
  18 {
  19         params->maxreads = 0;
  20         params->maxfuturedelay = 6;
  21         params->fairwindow = 0;
  22         params->yieldon = false;
  23         params->yieldblock = false;
  24         params->enabledcount = 1;
  25         params->bound = 0;
  26         params->maxfuturevalues = 0;
  27         params->expireslop = 4;
  28         params->verbose = !!DBG_ENABLED();
  29         params->uninitvalue = 0;
  30         params->maxexecutions = 0;
  31 }
  32
  33 static void model_main()
  34 {
  35         struct model_params params;
  36
  37         param_defaults(&params);
  38
  39         //parse_options(&params, main_argc, main_argv);
  40
  41         //Initialize race detector
  42         initRaceDetector();
  43
  44         snapshot_stack_init();
  45
  46         model = new ModelChecker(params);       // L: Model thread is created
  47 //      install_trace_analyses(model->get_execution());         L: disable plugin
  48
  49         snapshot_record(0);
  50         model->run();
  51         delete model;
  52
  53         DEBUG("Exiting\n");
  54 }
  55
  56 int pthread_create(pthread_t *t, const pthread_attr_t * attr,
  57           pthread_start_t start_routine, void * arg) {
  58         struct pthread_params params = { start_routine, arg };
  59
  60         ModelAction *act = new ModelAction(PTHREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)&params);
  61
  62         /* seq_cst is just a 'don't care' parameter */
  63         model->switch_to_master(act);
  64
  65         return 0;
  66 }
  67
  68 int pthread_join(pthread_t t, void **value_ptr) {
  69 //      Thread *th = model->get_pthread(t);
  70         ModelExecution *execution = model->get_execution();
  71         Thread *th = execution->get_pthread(t);
  72
  73         model->switch_to_master(new ModelAction(PTHREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(th->get_id())));
  74
  75         if ( value_ptr ) {
  76                 // store return value
  77                 void *rtval = th->get_pthread_return();
  78                 *value_ptr = rtval;
  79         }
  80         return 0;
  81 }
  82
  83 void pthread_exit(void *value_ptr) {
  84         Thread * th = thread_current();
  85         model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, th));
  86 }
  87
  88 int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
  89         if (!model) {
  90                 snapshot_system_init(10000, 1024, 1024, 40000, &model_main);
  91         }
  92
  93         cdsc::mutex *m = new cdsc::mutex();
  94
  95         ModelExecution *execution = model->get_execution();
  96         execution->getMutexMap()->put(p_mutex, m);
  97         return 0;
  98 }
  99
 100 int pthread_mutex_lock(pthread_mutex_t *p_mutex) {
 101         ModelExecution *execution = model->get_execution();
 102
 103         /* to protect the case where PTHREAD_MUTEX_INITIALIZER is used
 104            instead of pthread_mutex_init, or where *p_mutex is not stored
 105            in the execution->mutex_map for some reason. */
 106         if (!execution->getMutexMap()->contains(p_mutex)) {
 107                 pthread_mutex_init(p_mutex, NULL);
 108         }
 109
 110         cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
 111
 112         if (m != NULL) {
 113                 m->lock();
 114         } else {
 115                 printf("ah\n");
 116         }
 117
 118         return 0;
 119 }
 120
 121 int pthread_mutex_trylock(pthread_mutex_t *p_mutex) {
 122         ModelExecution *execution = model->get_execution();
 123         cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
 124         return m->try_lock();
 125 }
 126 int pthread_mutex_unlock(pthread_mutex_t *p_mutex) {
 127         ModelExecution *execution = model->get_execution();
 128         cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
 129
 130         if (m != NULL) {
 131                 m->unlock();
 132         } else {
 133                 printf("try to unlock an untracked pthread_mutex\n");
 134         }
 135
 136         return 0;
 137 }
 138
 139 int pthread_mutex_timedlock (pthread_mutex_t *__restrict p_mutex,
 140                                 const struct timespec *__restrict abstime) {
 141 // timedlock just gives the option of giving up the lock, so return and let the scheduler decide which thread goes next
 142
 143 /*
 144         ModelExecution *execution = model->get_execution();
 145         if (!execution->mutex_map.contains(p_mutex)) {
 146                 pthread_mutex_init(p_mutex, NULL);
 147         }
 148         cdsc::mutex *m = execution->mutex_map.get(p_mutex);
 149
 150         if (m != NULL) {
 151                 m->lock();
 152         } else {
 153                 printf("something is wrong with pthread_mutex_timedlock\n");
 154         }
 155
 156         printf("pthread_mutex_timedlock is called. It is currently implemented as a normal lock operation without no timeout\n");
 157 */
 158         return 0;
 159 }
 160
 161 pthread_t pthread_self() {
 162         Thread* th = model->get_current_thread();
 163         return th->get_id();
 164 }
 165
 166 int pthread_key_delete(pthread_key_t) {
 167         model_print("key_delete is called\n");
 168         return 0;
 169 }
 170
 171 int pthread_cond_init(pthread_cond_t *p_cond, const pthread_condattr_t *attr) {
 172         cdsc::condition_variable *v = new cdsc::condition_variable();
 173
 174         ModelExecution *execution = model->get_execution();
 175         execution->getCondMap()->put(p_cond, v);
 176         return 0;
 177 }
 178
 179 int pthread_cond_wait(pthread_cond_t *p_cond, pthread_mutex_t *p_mutex) {
 180         ModelExecution *execution = model->get_execution();
 181         if ( !execution->getCondMap()->contains(p_cond) )
 182                 pthread_cond_init(p_cond, NULL);
 183
 184         cdsc::condition_variable *v = execution->getCondMap()->get(p_cond);
 185         cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
 186
 187         v->wait(*m);
 188         return 0;
 189 }
 190
 191 int pthread_cond_timedwait(pthread_cond_t *p_cond,
 192     pthread_mutex_t *p_mutex, const struct timespec *abstime) {
 193 // implement cond_timedwait as a noop and let the scheduler decide which thread goes next
 194         ModelExecution *execution = model->get_execution();
 195
 196         if ( !execution->getCondMap()->contains(p_cond) )
 197                 pthread_cond_init(p_cond, NULL);
 198         if ( !execution->getMutexMap()->contains(p_mutex) )
 199                 pthread_mutex_init(p_mutex, NULL);
 200
 201         cdsc::condition_variable *v = execution->getCondMap()->get(p_cond);
 202         cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
 203
 204         model->switch_to_master(new ModelAction(NOOP, std::memory_order_seq_cst, v, NULL));
 205 //      v->wait(*m);
 206 //      printf("timed_wait called\n");
 207         return 0;
 208 }
 209
 210 int pthread_cond_signal(pthread_cond_t *p_cond) {
 211         // notify only one blocked thread
 212         ModelExecution *execution = model->get_execution();
 213         if ( !execution->getCondMap()->contains(p_cond) )
 214                 pthread_cond_init(p_cond, NULL);
 215
 216         cdsc::condition_variable *v = execution->getCondMap()->get(p_cond);
 217
 218         v->notify_one();
 219         return 0;
 220 }