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