datarace.cc

   1 #include "datarace.h"
   2 #include "model.h"
   3 #include "threads-model.h"
   4 #include <stdio.h>
   5 #include <cstring>
   6 #include "mymemory.h"
   7 #include "clockvector.h"
   8 #include "config.h"
   9 #include "action.h"
  10 #include "execution.h"
  11 #include "stl-model.h"
  12 #include <execinfo.h>
  13
  14 static struct ShadowTable *root;
  15 static void *memory_base;
  16 static void *memory_top;
  17 static RaceSet * raceset;
  18
  19 static const ModelExecution * get_execution()
  20 {
  21         return model->get_execution();
  22 }
  23
  24 /** This function initialized the data race detector. */
  25 void initRaceDetector()
  26 {
  27         root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1);
  28         memory_base = snapshot_calloc(sizeof(struct ShadowBaseTable) * SHADOWBASETABLES, 1);
  29         memory_top = ((char *)memory_base) + sizeof(struct ShadowBaseTable) * SHADOWBASETABLES;
  30         raceset = new RaceSet();
  31 }
  32
  33 void * table_calloc(size_t size)
  34 {
  35         if ((((char *)memory_base) + size) > memory_top) {
  36                 return snapshot_calloc(size, 1);
  37         } else {
  38                 void *tmp = memory_base;
  39                 memory_base = ((char *)memory_base) + size;
  40                 return tmp;
  41         }
  42 }
  43
  44 /** This function looks up the entry in the shadow table corresponding to a
  45  * given address.*/
  46 static uint64_t * lookupAddressEntry(const void *address)
  47 {
  48         struct ShadowTable *currtable = root;
  49 #if BIT48
  50         currtable = (struct ShadowTable *) currtable->array[(((uintptr_t)address) >> 32) & MASK16BIT];
  51         if (currtable == NULL) {
  52                 currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address) >> 32) & MASK16BIT] = table_calloc(sizeof(struct ShadowTable)));
  53         }
  54 #endif
  55
  56         struct ShadowBaseTable *basetable = (struct ShadowBaseTable *)currtable->array[(((uintptr_t)address) >> 16) & MASK16BIT];
  57         if (basetable == NULL) {
  58                 basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address) >> 16) & MASK16BIT] = table_calloc(sizeof(struct ShadowBaseTable)));
  59         }
  60         return &basetable->array[((uintptr_t)address) & MASK16BIT];
  61 }
  62
  63 /**
  64  * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
  65  * to check the potential for a data race.
  66  * @param clock1 The current clock vector
  67  * @param tid1 The current thread; paired with clock1
  68  * @param clock2 The clock value for the potentially-racing action
  69  * @param tid2 The thread ID for the potentially-racing action
  70  * @return true if the current clock allows a race with the event at clock2/tid2
  71  */
  72 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
  73                                                                                                          modelclock_t clock2, thread_id_t tid2)
  74 {
  75         return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
  76 }
  77
  78 /**
  79  * Expands a record from the compact form to the full form.  This is
  80  * necessary for multiple readers or for very large thread ids or time
  81  * stamps. */
  82 static void expandRecord(uint64_t *shadow)
  83 {
  84         uint64_t shadowval = *shadow;
  85
  86         modelclock_t readClock = READVECTOR(shadowval);
  87         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
  88         modelclock_t writeClock = WRITEVECTOR(shadowval);
  89         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
  90
  91         struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord));
  92         record->writeThread = writeThread;
  93         record->writeClock = writeClock;
  94
  95         if (readClock != 0) {
  96                 record->capacity = INITCAPACITY;
  97                 record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * record->capacity);
  98                 record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * record->capacity);
  99                 record->numReads = 1;
 100                 ASSERT(readThread >= 0);
 101                 record->thread[0] = readThread;
 102                 record->readClock[0] = readClock;
 103         }
 104         *shadow = (uint64_t) record;
 105 }
 106
 107 #define FIRST_STACK_FRAME 2
 108
 109 unsigned int race_hash(struct DataRace *race) {
 110         unsigned int hash = 0;
 111         for(int i=FIRST_STACK_FRAME;i < race->numframes;i++) {
 112                 hash ^= ((uintptr_t)race->backtrace[i]);
 113                 hash = (hash >> 3) | (hash << 29);
 114         }
 115         return hash;
 116 }
 117
 118
 119 bool race_equals(struct DataRace *r1, struct DataRace *r2) {
 120         if (r1->numframes != r2->numframes)
 121                 return false;
 122         for(int i=FIRST_STACK_FRAME;i < r1->numframes;i++) {
 123                 if (r1->backtrace[i] != r2->backtrace[i])
 124                         return false;
 125         }
 126         return true;
 127 }
 128
 129 /** This function is called when we detect a data race.*/
 130 static struct DataRace * reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address)
 131 {
 132         struct DataRace *race = (struct DataRace *)model_malloc(sizeof(struct DataRace));
 133         race->oldthread = oldthread;
 134         race->oldclock = oldclock;
 135         race->isoldwrite = isoldwrite;
 136         race->newaction = newaction;
 137         race->isnewwrite = isnewwrite;
 138         race->address = address;
 139         return race;
 140 }
 141
 142 /**
 143  * @brief Assert a data race
 144  *
 145  * Asserts a data race which is currently realized, causing the execution to
 146  * end and stashing a message in the model-checker's bug list
 147  *
 148  * @param race The race to report
 149  */
 150 void assert_race(struct DataRace *race)
 151 {
 152         model_print("At location: \n");
 153         backtrace_symbols_fd(race->backtrace, race->numframes, model_out);
 154         model_print("Data race detected @ address %p:\n"
 155                                                         "    Access 1: %5s in thread %2d @ clock %3u\n"
 156                                                         "    Access 2: %5s in thread %2d @ clock %3u",
 157                                                         race->address,
 158                                                         race->isoldwrite ? "write" : "read",
 159                                                         id_to_int(race->oldthread),
 160                                                         race->oldclock,
 161                                                         race->isnewwrite ? "write" : "read",
 162                                                         id_to_int(race->newaction->get_tid()),
 163                                                         race->newaction->get_seq_number()
 164                                                         );
 165 }
 166
 167 /** This function does race detection for a write on an expanded record. */
 168 struct DataRace * fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock)
 169 {
 170         struct RaceRecord *record = (struct RaceRecord *)(*shadow);
 171         struct DataRace * race = NULL;
 172
 173         /* Check for datarace against last read. */
 174
 175         for (int i = 0;i < record->numReads;i++) {
 176                 modelclock_t readClock = record->readClock[i];
 177                 thread_id_t readThread = record->thread[i];
 178
 179                 /* Note that readClock can't actuall be zero here, so it could be
 180                          optimized. */
 181
 182                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 183                         /* We have a datarace */
 184                         race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 185                         goto Exit;
 186                 }
 187         }
 188
 189         /* Check for datarace against last write. */
 190
 191         {
 192                 modelclock_t writeClock = record->writeClock;
 193                 thread_id_t writeThread = record->writeThread;
 194
 195                 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 196                         /* We have a datarace */
 197                         race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 198                         goto Exit;
 199                 }
 200         }
 201 Exit:
 202         record->numReads = 0;
 203         record->writeThread = thread;
 204         modelclock_t ourClock = currClock->getClock(thread);
 205         record->writeClock = ourClock;
 206         return race;
 207 }
 208
 209 /** This function does race detection on a write. */
 210 void raceCheckWrite(thread_id_t thread, void *location)
 211 {
 212         uint64_t *shadow = lookupAddressEntry(location);
 213         uint64_t shadowval = *shadow;
 214         ClockVector *currClock = get_execution()->get_cv(thread);
 215         struct DataRace * race = NULL;
 216         /* Do full record */
 217         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 218                 race = fullRaceCheckWrite(thread, location, shadow, currClock);
 219                 goto Exit;
 220         }
 221
 222         {
 223                 int threadid = id_to_int(thread);
 224                 modelclock_t ourClock = currClock->getClock(thread);
 225
 226                 /* Thread ID is too large or clock is too large. */
 227                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 228                         expandRecord(shadow);
 229                         race = fullRaceCheckWrite(thread, location, shadow, currClock);
 230                         goto Exit;
 231                 }
 232
 233
 234
 235                 {
 236                         /* Check for datarace against last read. */
 237
 238                         modelclock_t readClock = READVECTOR(shadowval);
 239                         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 240
 241                         if (clock_may_race(currClock, thread, readClock, readThread)) {
 242                                 /* We have a datarace */
 243                                 race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 244                                 goto ShadowExit;
 245                         }
 246                 }
 247
 248                 {
 249                         /* Check for datarace against last write. */
 250
 251                         modelclock_t writeClock = WRITEVECTOR(shadowval);
 252                         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 253
 254                         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 255                                 /* We have a datarace */
 256                                 race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 257                                 goto ShadowExit;
 258                         }
 259                 }
 260
 261 ShadowExit:
 262                 *shadow = ENCODEOP(0, 0, threadid, ourClock);
 263         }
 264
 265 Exit:
 266         if (race) {
 267                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 268                 if (raceset->add(race))
 269                         assert_race(race);
 270                 else model_free(race);
 271         }
 272 }
 273
 274 /** This function does race detection for a write on an expanded record. */
 275 void fullRecordWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock) {
 276         struct RaceRecord *record = (struct RaceRecord *)(*shadow);
 277         record->numReads = 0;
 278         record->writeThread = thread;
 279         modelclock_t ourClock = currClock->getClock(thread);
 280         record->writeClock = ourClock;
 281 }
 282
 283 /** This function just updates metadata on atomic write. */
 284 void recordWrite(thread_id_t thread, void *location) {
 285         uint64_t *shadow = lookupAddressEntry(location);
 286         uint64_t shadowval = *shadow;
 287         ClockVector *currClock = get_execution()->get_cv(thread);
 288         /* Do full record */
 289         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 290                 fullRecordWrite(thread, location, shadow, currClock);
 291                 return;
 292         }
 293
 294         int threadid = id_to_int(thread);
 295         modelclock_t ourClock = currClock->getClock(thread);
 296
 297         /* Thread ID is too large or clock is too large. */
 298         if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 299                 expandRecord(shadow);
 300                 fullRecordWrite(thread, location, shadow, currClock);
 301                 return;
 302         }
 303
 304         *shadow = ENCODEOP(0, 0, threadid, ourClock);
 305 }
 306
 307
 308
 309 /** This function does race detection on a read for an expanded record. */
 310 struct DataRace * fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
 311 {
 312         struct RaceRecord *record = (struct RaceRecord *) (*shadow);
 313         struct DataRace * race = NULL;
 314         /* Check for datarace against last write. */
 315
 316         modelclock_t writeClock = record->writeClock;
 317         thread_id_t writeThread = record->writeThread;
 318
 319         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 320                 /* We have a datarace */
 321                 race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 322         }
 323
 324         /* Shorten vector when possible */
 325
 326         int copytoindex = 0;
 327
 328         for (int i = 0;i < record->numReads;i++) {
 329                 modelclock_t readClock = record->readClock[i];
 330                 thread_id_t readThread = record->thread[i];
 331
 332                 /*  Note that is not really a datarace check as reads cannot
 333                                 actually race.  It is just determining that this read subsumes
 334                                 another in the sense that either this read races or neither
 335                                 read races. Note that readClock can't actually be zero, so it
 336                                 could be optimized.  */
 337
 338                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 339                         /* Still need this read in vector */
 340                         if (copytoindex != i) {
 341                                 ASSERT(record->thread[i] >= 0);
 342                                 record->readClock[copytoindex] = record->readClock[i];
 343                                 record->thread[copytoindex] = record->thread[i];
 344                         }
 345                         copytoindex++;
 346                 }
 347         }
 348
 349         if (copytoindex >= record->capacity) {
 350                 if (record->capacity == 0) {
 351                         int newCapacity = INITCAPACITY;
 352                         record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
 353                         record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
 354                         record->capacity = newCapacity;
 355                 } else {
 356                         int newCapacity = record->capacity * 2;
 357                         thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
 358                         modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
 359                         std::memcpy(newthread, record->thread, record->capacity * sizeof(thread_id_t));
 360                         std::memcpy(newreadClock, record->readClock, record->capacity * sizeof(modelclock_t));
 361                         snapshot_free(record->readClock);
 362                         snapshot_free(record->thread);
 363                         record->readClock = newreadClock;
 364                         record->thread = newthread;
 365                         record->capacity = newCapacity;
 366                 }
 367         }
 368
 369         modelclock_t ourClock = currClock->getClock(thread);
 370
 371         ASSERT(thread >= 0);
 372         record->thread[copytoindex] = thread;
 373         record->readClock[copytoindex] = ourClock;
 374         record->numReads = copytoindex + 1;
 375         return race;
 376 }
 377
 378 /** This function does race detection on a read. */
 379 void raceCheckRead(thread_id_t thread, const void *location)
 380 {
 381         uint64_t *shadow = lookupAddressEntry(location);
 382         uint64_t shadowval = *shadow;
 383         ClockVector *currClock = get_execution()->get_cv(thread);
 384         struct DataRace * race = NULL;
 385
 386         /* Do full record */
 387         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 388                 race = fullRaceCheckRead(thread, location, shadow, currClock);
 389                 goto Exit;
 390         }
 391
 392         {
 393                 int threadid = id_to_int(thread);
 394                 modelclock_t ourClock = currClock->getClock(thread);
 395
 396                 /* Thread ID is too large or clock is too large. */
 397                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 398                         expandRecord(shadow);
 399                         race = fullRaceCheckRead(thread, location, shadow, currClock);
 400                         goto Exit;
 401                 }
 402
 403                 /* Check for datarace against last write. */
 404
 405                 modelclock_t writeClock = WRITEVECTOR(shadowval);
 406                 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 407
 408                 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 409                         /* We have a datarace */
 410                         race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 411                         goto ShadowExit;
 412                 }
 413
 414 ShadowExit:
 415                 {
 416                         modelclock_t readClock = READVECTOR(shadowval);
 417                         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 418
 419                         if (clock_may_race(currClock, thread, readClock, readThread)) {
 420                                 /* We don't subsume this read... Have to expand record. */
 421                                 expandRecord(shadow);
 422                                 fullRaceCheckRead(thread, location, shadow, currClock);
 423                                 goto Exit;
 424                         }
 425                 }
 426
 427                 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
 428         }
 429 Exit:
 430         if (race) {
 431                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 432                 if (raceset->add(race))
 433                         assert_race(race);
 434                 else model_free(race);
 435         }
 436 }