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->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * INITCAPACITY);
  97                 record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * INITCAPACITY);
  98                 record->numReads = 1;
  99                 ASSERT(readThread >= 0);
 100                 record->thread[0] = readThread;
 101                 record->readClock[0] = readClock;
 102         }
 103         if (shadowval & ATOMICMASK)
 104                 record->isAtomic = 1;
 105         *shadow = (uint64_t) record;
 106 }
 107
 108 #define FIRST_STACK_FRAME 2
 109
 110 unsigned int race_hash(struct DataRace *race) {
 111         unsigned int hash = 0;
 112         for(int i=FIRST_STACK_FRAME;i < race->numframes;i++) {
 113                 hash ^= ((uintptr_t)race->backtrace[i]);
 114                 hash = (hash >> 3) | (hash << 29);
 115         }
 116         return hash;
 117 }
 118
 119
 120 bool race_equals(struct DataRace *r1, struct DataRace *r2) {
 121         if (r1->numframes != r2->numframes)
 122                 return false;
 123         for(int i=FIRST_STACK_FRAME;i < r1->numframes;i++) {
 124                 if (r1->backtrace[i] != r2->backtrace[i])
 125                         return false;
 126         }
 127         return true;
 128 }
 129
 130 /** This function is called when we detect a data race.*/
 131 static struct DataRace * reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address)
 132 {
 133         struct DataRace *race = (struct DataRace *)model_malloc(sizeof(struct DataRace));
 134         race->oldthread = oldthread;
 135         race->oldclock = oldclock;
 136         race->isoldwrite = isoldwrite;
 137         race->newaction = newaction;
 138         race->isnewwrite = isnewwrite;
 139         race->address = address;
 140         return race;
 141 }
 142
 143 /**
 144  * @brief Assert a data race
 145  *
 146  * Asserts a data race which is currently realized, causing the execution to
 147  * end and stashing a message in the model-checker's bug list
 148  *
 149  * @param race The race to report
 150  */
 151 void assert_race(struct DataRace *race)
 152 {
 153         model_print("At location: \n");
 154         backtrace_symbols_fd(race->backtrace, race->numframes, model_out);
 155         model_print("Data race detected @ address %p:\n"
 156                                                         "    Access 1: %5s in thread %2d @ clock %3u\n"
 157                                                         "    Access 2: %5s in thread %2d @ clock %3u",
 158                                                         race->address,
 159                                                         race->isoldwrite ? "write" : "read",
 160                                                         id_to_int(race->oldthread),
 161                                                         race->oldclock,
 162                                                         race->isnewwrite ? "write" : "read",
 163                                                         id_to_int(race->newaction->get_tid()),
 164                                                         race->newaction->get_seq_number()
 165                                                         );
 166 }
 167
 168 /** This function does race detection for a write on an expanded record. */
 169 struct DataRace * fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock)
 170 {
 171         struct RaceRecord *record = (struct RaceRecord *)(*shadow);
 172         struct DataRace * race = NULL;
 173
 174         /* Check for datarace against last read. */
 175
 176         for (int i = 0;i < record->numReads;i++) {
 177                 modelclock_t readClock = record->readClock[i];
 178                 thread_id_t readThread = record->thread[i];
 179
 180                 /* Note that readClock can't actuall be zero here, so it could be
 181                          optimized. */
 182
 183                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 184                         /* We have a datarace */
 185                         race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 186                         goto Exit;
 187                 }
 188         }
 189
 190         /* Check for datarace against last write. */
 191
 192         {
 193                 modelclock_t writeClock = record->writeClock;
 194                 thread_id_t writeThread = record->writeThread;
 195
 196                 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 197                         /* We have a datarace */
 198                         race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 199                         goto Exit;
 200                 }
 201         }
 202 Exit:
 203         record->numReads = 0;
 204         record->writeThread = thread;
 205         record->isAtomic = 0;
 206         modelclock_t ourClock = currClock->getClock(thread);
 207         record->writeClock = ourClock;
 208         return race;
 209 }
 210
 211 /** This function does race detection on a write. */
 212 void raceCheckWrite(thread_id_t thread, void *location)
 213 {
 214         uint64_t *shadow = lookupAddressEntry(location);
 215         uint64_t shadowval = *shadow;
 216         ClockVector *currClock = get_execution()->get_cv(thread);
 217         struct DataRace * race = NULL;
 218         /* Do full record */
 219         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 220                 race = fullRaceCheckWrite(thread, location, shadow, currClock);
 221                 goto Exit;
 222         }
 223
 224         {
 225                 int threadid = id_to_int(thread);
 226                 modelclock_t ourClock = currClock->getClock(thread);
 227
 228                 /* Thread ID is too large or clock is too large. */
 229                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 230                         expandRecord(shadow);
 231                         race = fullRaceCheckWrite(thread, location, shadow, currClock);
 232                         goto Exit;
 233                 }
 234
 235
 236
 237                 {
 238                         /* Check for datarace against last read. */
 239
 240                         modelclock_t readClock = READVECTOR(shadowval);
 241                         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 242
 243                         if (clock_may_race(currClock, thread, readClock, readThread)) {
 244                                 /* We have a datarace */
 245                                 race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 246                                 goto ShadowExit;
 247                         }
 248                 }
 249
 250                 {
 251                         /* Check for datarace against last write. */
 252
 253                         modelclock_t writeClock = WRITEVECTOR(shadowval);
 254                         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 255
 256                         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 257                                 /* We have a datarace */
 258                                 race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 259                                 goto ShadowExit;
 260                         }
 261                 }
 262
 263 ShadowExit:
 264                 *shadow = ENCODEOP(0, 0, threadid, ourClock);
 265         }
 266
 267 Exit:
 268         if (race) {
 269                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 270                 if (raceset->add(race))
 271                         assert_race(race);
 272                 else model_free(race);
 273         }
 274 }
 275
 276 /** This function does race detection for a write on an expanded record. */
 277 void fullRecordWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock) {
 278         struct RaceRecord *record = (struct RaceRecord *)(*shadow);
 279         record->numReads = 0;
 280         record->writeThread = thread;
 281         modelclock_t ourClock = currClock->getClock(thread);
 282         record->writeClock = ourClock;
 283         record->isAtomic = 1;
 284 }
 285
 286 /** This function just updates metadata on atomic write. */
 287 void recordWrite(thread_id_t thread, void *location) {
 288         uint64_t *shadow = lookupAddressEntry(location);
 289         uint64_t shadowval = *shadow;
 290         ClockVector *currClock = get_execution()->get_cv(thread);
 291         /* Do full record */
 292         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 293                 fullRecordWrite(thread, location, shadow, currClock);
 294                 return;
 295         }
 296
 297         int threadid = id_to_int(thread);
 298         modelclock_t ourClock = currClock->getClock(thread);
 299
 300         /* Thread ID is too large or clock is too large. */
 301         if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 302                 expandRecord(shadow);
 303                 fullRecordWrite(thread, location, shadow, currClock);
 304                 return;
 305         }
 306
 307         *shadow = ENCODEOP(0, 0, threadid, ourClock) | ATOMICMASK;
 308 }
 309
 310
 311
 312 /** This function does race detection on a read for an expanded record. */
 313 struct DataRace * fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
 314 {
 315         struct RaceRecord *record = (struct RaceRecord *) (*shadow);
 316         struct DataRace * race = NULL;
 317         /* Check for datarace against last write. */
 318
 319         modelclock_t writeClock = record->writeClock;
 320         thread_id_t writeThread = record->writeThread;
 321
 322         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 323                 /* We have a datarace */
 324                 race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 325         }
 326
 327         /* Shorten vector when possible */
 328
 329         int copytoindex = 0;
 330
 331         for (int i = 0;i < record->numReads;i++) {
 332                 modelclock_t readClock = record->readClock[i];
 333                 thread_id_t readThread = record->thread[i];
 334
 335                 /*  Note that is not really a datarace check as reads cannot
 336                                 actually race.  It is just determining that this read subsumes
 337                                 another in the sense that either this read races or neither
 338                                 read races. Note that readClock can't actually be zero, so it
 339                                 could be optimized.  */
 340
 341                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 342                         /* Still need this read in vector */
 343                         if (copytoindex != i) {
 344                                 ASSERT(record->thread[i] >= 0);
 345                                 record->readClock[copytoindex] = record->readClock[i];
 346                                 record->thread[copytoindex] = record->thread[i];
 347                         }
 348                         copytoindex++;
 349                 }
 350         }
 351
 352         if (__builtin_popcount(copytoindex) <= 1) {
 353                 if (copytoindex == 0) {
 354                         int newCapacity = INITCAPACITY;
 355                         record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
 356                         record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
 357                 } else if (copytoindex>=INITCAPACITY) {
 358                         int newCapacity = copytoindex * 2;
 359                         thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
 360                         modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
 361                         std::memcpy(newthread, record->thread, copytoindex * sizeof(thread_id_t));
 362                         std::memcpy(newreadClock, record->readClock, copytoindex * sizeof(modelclock_t));
 363                         snapshot_free(record->readClock);
 364                         snapshot_free(record->thread);
 365                         record->readClock = newreadClock;
 366                         record->thread = newthread;
 367                 }
 368         }
 369
 370         modelclock_t ourClock = currClock->getClock(thread);
 371
 372         ASSERT(thread >= 0);
 373         record->thread[copytoindex] = thread;
 374         record->readClock[copytoindex] = ourClock;
 375         record->numReads = copytoindex + 1;
 376         return race;
 377 }
 378
 379 /** This function does race detection on a read. */
 380 void raceCheckRead(thread_id_t thread, const void *location)
 381 {
 382         uint64_t *shadow = lookupAddressEntry(location);
 383         uint64_t shadowval = *shadow;
 384         ClockVector *currClock = get_execution()->get_cv(thread);
 385         struct DataRace * race = NULL;
 386
 387         /* Do full record */
 388         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 389                 race = fullRaceCheckRead(thread, location, shadow, currClock);
 390                 goto Exit;
 391         }
 392
 393         {
 394                 int threadid = id_to_int(thread);
 395                 modelclock_t ourClock = currClock->getClock(thread);
 396
 397                 /* Thread ID is too large or clock is too large. */
 398                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 399                         expandRecord(shadow);
 400                         race = fullRaceCheckRead(thread, location, shadow, currClock);
 401                         goto Exit;
 402                 }
 403
 404                 /* Check for datarace against last write. */
 405
 406                 modelclock_t writeClock = WRITEVECTOR(shadowval);
 407                 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 408
 409                 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 410                         /* We have a datarace */
 411                         race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 412                         goto ShadowExit;
 413                 }
 414
 415 ShadowExit:
 416                 {
 417                         modelclock_t readClock = READVECTOR(shadowval);
 418                         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 419
 420                         if (clock_may_race(currClock, thread, readClock, readThread)) {
 421                                 /* We don't subsume this read... Have to expand record. */
 422                                 expandRecord(shadow);
 423                                 fullRaceCheckRead(thread, location, shadow, currClock);
 424                                 goto Exit;
 425                         }
 426                 }
 427
 428                 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock) | (shadowval & ATOMICMASK);
 429         }
 430 Exit:
 431         if (race) {
 432                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 433                 if (raceset->add(race))
 434                         assert_race(race);
 435                 else model_free(race);
 436         }
 437 }