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 !(ATOMICMASK & shadowval);
  70         } else {
  71                 if (shadowval == 0)
  72                         return true;
  73                 struct RaceRecord *record = (struct RaceRecord *)shadowval;
  74                 return !record->isAtomic;
  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                         *shadow = ATOMICMASK | ENCODEOP(0, 0, 0, 0);
  86                         return;
  87                 }
  88                 struct RaceRecord *record = (struct RaceRecord *)shadowval;
  89                 record->isAtomic = 1;
  90         }
  91 }
  92
  93 void getStoreThreadAndClock(const void *address, thread_id_t * thread, modelclock_t * clock) {
  94         uint64_t * shadow = lookupAddressEntry(address);
  95         uint64_t shadowval = *shadow;
  96         if (ISSHORTRECORD(shadowval) || shadowval == 0) {
  97                 //Do we have a non atomic write with a non-zero clock
  98                 *thread = WRTHREADID(shadowval);
  99                 *clock = WRITEVECTOR(shadowval);
 100         } else {
 101                 struct RaceRecord *record = (struct RaceRecord *)shadowval;
 102                 *thread = record->writeThread;
 103                 *clock = record->writeClock;
 104         }
 105 }
 106
 107 /**
 108  * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
 109  * to check the potential for a data race.
 110  * @param clock1 The current clock vector
 111  * @param tid1 The current thread; paired with clock1
 112  * @param clock2 The clock value for the potentially-racing action
 113  * @param tid2 The thread ID for the potentially-racing action
 114  * @return true if the current clock allows a race with the event at clock2/tid2
 115  */
 116 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
 117                                                                                                          modelclock_t clock2, thread_id_t tid2)
 118 {
 119         return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
 120 }
 121
 122 /**
 123  * Expands a record from the compact form to the full form.  This is
 124  * necessary for multiple readers or for very large thread ids or time
 125  * stamps. */
 126 static void expandRecord(uint64_t *shadow)
 127 {
 128         uint64_t shadowval = *shadow;
 129
 130         modelclock_t readClock = READVECTOR(shadowval);
 131         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 132         modelclock_t writeClock = WRITEVECTOR(shadowval);
 133         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 134
 135         struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord));
 136         record->writeThread = writeThread;
 137         record->writeClock = writeClock;
 138
 139         if (readClock != 0) {
 140                 record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * INITCAPACITY);
 141                 record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * INITCAPACITY);
 142                 record->numReads = 1;
 143                 ASSERT(readThread >= 0);
 144                 record->thread[0] = readThread;
 145                 record->readClock[0] = readClock;
 146         }
 147         if (shadowval & ATOMICMASK)
 148                 record->isAtomic = 1;
 149         *shadow = (uint64_t) record;
 150 }
 151
 152 #define FIRST_STACK_FRAME 2
 153
 154 unsigned int race_hash(struct DataRace *race) {
 155         unsigned int hash = 0;
 156         for(int i=FIRST_STACK_FRAME;i < race->numframes;i++) {
 157                 hash ^= ((uintptr_t)race->backtrace[i]);
 158                 hash = (hash >> 3) | (hash << 29);
 159         }
 160         return hash;
 161 }
 162
 163
 164 bool race_equals(struct DataRace *r1, struct DataRace *r2) {
 165         if (r1->numframes != r2->numframes)
 166                 return false;
 167         for(int i=FIRST_STACK_FRAME;i < r1->numframes;i++) {
 168                 if (r1->backtrace[i] != r2->backtrace[i])
 169                         return false;
 170         }
 171         return true;
 172 }
 173
 174 /** This function is called when we detect a data race.*/
 175 static struct DataRace * reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address)
 176 {
 177         struct DataRace *race = (struct DataRace *)model_malloc(sizeof(struct DataRace));
 178         race->oldthread = oldthread;
 179         race->oldclock = oldclock;
 180         race->isoldwrite = isoldwrite;
 181         race->newaction = newaction;
 182         race->isnewwrite = isnewwrite;
 183         race->address = address;
 184         return race;
 185 }
 186
 187 /**
 188  * @brief Assert a data race
 189  *
 190  * Asserts a data race which is currently realized, causing the execution to
 191  * end and stashing a message in the model-checker's bug list
 192  *
 193  * @param race The race to report
 194  */
 195 void assert_race(struct DataRace *race)
 196 {
 197         model_print("Race detected at location: \n");
 198         backtrace_symbols_fd(race->backtrace, race->numframes, model_out);
 199         model_print("\nData race detected @ address %p:\n"
 200                                                         "    Access 1: %5s in thread %2d @ clock %3u\n"
 201                                                         "    Access 2: %5s in thread %2d @ clock %3u\n\n",
 202                                                         race->address,
 203                                                         race->isoldwrite ? "write" : "read",
 204                                                         id_to_int(race->oldthread),
 205                                                         race->oldclock,
 206                                                         race->isnewwrite ? "write" : "read",
 207                                                         id_to_int(race->newaction->get_tid()),
 208                                                         race->newaction->get_seq_number()
 209                                                         );
 210 }
 211
 212 /** This function does race detection for a write on an expanded record. */
 213 struct DataRace * fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock)
 214 {
 215         struct RaceRecord *record = (struct RaceRecord *)(*shadow);
 216         struct DataRace * race = NULL;
 217
 218         /* Check for datarace against last read. */
 219
 220         for (int i = 0;i < record->numReads;i++) {
 221                 modelclock_t readClock = record->readClock[i];
 222                 thread_id_t readThread = record->thread[i];
 223
 224                 /* Note that readClock can't actuall be zero here, so it could be
 225                          optimized. */
 226
 227                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 228                         /* We have a datarace */
 229                         race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 230                         goto Exit;
 231                 }
 232         }
 233
 234         /* Check for datarace against last write. */
 235
 236         {
 237                 modelclock_t writeClock = record->writeClock;
 238                 thread_id_t writeThread = record->writeThread;
 239
 240                 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 241                         /* We have a datarace */
 242                         race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 243                         goto Exit;
 244                 }
 245         }
 246 Exit:
 247         record->numReads = 0;
 248         record->writeThread = thread;
 249         record->isAtomic = 0;
 250         modelclock_t ourClock = currClock->getClock(thread);
 251         record->writeClock = ourClock;
 252         return race;
 253 }
 254
 255 /** This function does race detection on a write. */
 256 void raceCheckWrite(thread_id_t thread, void *location)
 257 {
 258         uint64_t *shadow = lookupAddressEntry(location);
 259         uint64_t shadowval = *shadow;
 260         ClockVector *currClock = get_execution()->get_cv(thread);
 261         if (currClock == NULL)
 262                 return;
 263
 264         struct DataRace * race = NULL;
 265         /* Do full record */
 266         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 267                 race = fullRaceCheckWrite(thread, location, shadow, currClock);
 268                 goto Exit;
 269         }
 270
 271         {
 272                 int threadid = id_to_int(thread);
 273                 modelclock_t ourClock = currClock->getClock(thread);
 274
 275                 /* Thread ID is too large or clock is too large. */
 276                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 277                         expandRecord(shadow);
 278                         race = fullRaceCheckWrite(thread, location, shadow, currClock);
 279                         goto Exit;
 280                 }
 281
 282
 283
 284                 {
 285                         /* Check for datarace against last read. */
 286                         modelclock_t readClock = READVECTOR(shadowval);
 287                         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 288
 289                         if (clock_may_race(currClock, thread, readClock, readThread)) {
 290                                 /* We have a datarace */
 291                                 race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 292                                 goto ShadowExit;
 293                         }
 294                 }
 295
 296                 {
 297                         /* Check for datarace against last write. */
 298
 299                         modelclock_t writeClock = WRITEVECTOR(shadowval);
 300                         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 301
 302                         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 303                                 /* We have a datarace */
 304                                 race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 305                                 goto ShadowExit;
 306                         }
 307                 }
 308
 309 ShadowExit:
 310                 *shadow = ENCODEOP(0, 0, threadid, ourClock);
 311         }
 312
 313 Exit:
 314         if (race) {
 315                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 316                 if (raceset->add(race))
 317                         assert_race(race);
 318                 else model_free(race);
 319         }
 320 }
 321
 322
 323 /** This function does race detection for a write on an expanded record. */
 324 struct DataRace * atomfullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock)
 325 {
 326         struct RaceRecord *record = (struct RaceRecord *)(*shadow);
 327         struct DataRace * race = NULL;
 328
 329         if (record->isAtomic)
 330                 goto Exit;
 331
 332         /* Check for datarace against last read. */
 333
 334         for (int i = 0;i < record->numReads;i++) {
 335                 modelclock_t readClock = record->readClock[i];
 336                 thread_id_t readThread = record->thread[i];
 337
 338                 /* Note that readClock can't actuall be zero here, so it could be
 339                          optimized. */
 340
 341                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 342                         /* We have a datarace */
 343                         race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 344                         goto Exit;
 345                 }
 346         }
 347
 348         /* Check for datarace against last write. */
 349
 350         {
 351                 modelclock_t writeClock = record->writeClock;
 352                 thread_id_t writeThread = record->writeThread;
 353
 354                 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 355                         /* We have a datarace */
 356                         race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 357                         goto Exit;
 358                 }
 359         }
 360 Exit:
 361         record->numReads = 0;
 362         record->writeThread = thread;
 363         record->isAtomic = 1;
 364         modelclock_t ourClock = currClock->getClock(thread);
 365         record->writeClock = ourClock;
 366         return race;
 367 }
 368
 369 /** This function does race detection on a write. */
 370 void atomraceCheckWrite(thread_id_t thread, void *location)
 371 {
 372         uint64_t *shadow = lookupAddressEntry(location);
 373         uint64_t shadowval = *shadow;
 374         ClockVector *currClock = get_execution()->get_cv(thread);
 375         if (currClock == NULL)
 376                 return;
 377
 378         struct DataRace * race = NULL;
 379         /* Do full record */
 380         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 381                 race = atomfullRaceCheckWrite(thread, location, shadow, currClock);
 382                 goto Exit;
 383         }
 384
 385         {
 386                 int threadid = id_to_int(thread);
 387                 modelclock_t ourClock = currClock->getClock(thread);
 388
 389                 /* Thread ID is too large or clock is too large. */
 390                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 391                         expandRecord(shadow);
 392                         race = atomfullRaceCheckWrite(thread, location, shadow, currClock);
 393                         goto Exit;
 394                 }
 395
 396                 /* Can't race with atomic */
 397                 if (shadowval & ATOMICMASK)
 398                         goto ShadowExit;
 399
 400                 {
 401                         /* Check for datarace against last read. */
 402
 403                         modelclock_t readClock = READVECTOR(shadowval);
 404                         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 405
 406                         if (clock_may_race(currClock, thread, readClock, readThread)) {
 407                                 /* We have a datarace */
 408                                 race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 409                                 goto ShadowExit;
 410                         }
 411                 }
 412
 413                 {
 414                         /* Check for datarace against last write. */
 415
 416                         modelclock_t writeClock = WRITEVECTOR(shadowval);
 417                         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 418
 419                         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 420                                 /* We have a datarace */
 421                                 race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 422                                 goto ShadowExit;
 423                         }
 424                 }
 425
 426 ShadowExit:
 427                 *shadow = ENCODEOP(0, 0, threadid, ourClock) | ATOMICMASK;
 428         }
 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 }
 438
 439 /** This function does race detection for a write on an expanded record. */
 440 void fullRecordWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock) {
 441         struct RaceRecord *record = (struct RaceRecord *)(*shadow);
 442         record->numReads = 0;
 443         record->writeThread = thread;
 444         modelclock_t ourClock = currClock->getClock(thread);
 445         record->writeClock = ourClock;
 446         record->isAtomic = 1;
 447 }
 448
 449 /** This function does race detection for a write on an expanded record. */
 450 void fullRecordWriteNonAtomic(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock) {
 451         struct RaceRecord *record = (struct RaceRecord *)(*shadow);
 452         record->numReads = 0;
 453         record->writeThread = thread;
 454         modelclock_t ourClock = currClock->getClock(thread);
 455         record->writeClock = ourClock;
 456         record->isAtomic = 0;
 457 }
 458
 459 /** This function just updates metadata on atomic write. */
 460 void recordWrite(thread_id_t thread, void *location) {
 461         uint64_t *shadow = lookupAddressEntry(location);
 462         uint64_t shadowval = *shadow;
 463         ClockVector *currClock = get_execution()->get_cv(thread);
 464         /* Do full record */
 465         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 466                 fullRecordWrite(thread, location, shadow, currClock);
 467                 return;
 468         }
 469
 470         int threadid = id_to_int(thread);
 471         modelclock_t ourClock = currClock->getClock(thread);
 472
 473         /* Thread ID is too large or clock is too large. */
 474         if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 475                 expandRecord(shadow);
 476                 fullRecordWrite(thread, location, shadow, currClock);
 477                 return;
 478         }
 479
 480         *shadow = ENCODEOP(0, 0, threadid, ourClock) | ATOMICMASK;
 481 }
 482
 483 /** This function just updates metadata on atomic write. */
 484 void recordCalloc(void *location, size_t size) {
 485         thread_id_t thread = thread_current()->get_id();
 486         for(;size != 0;size--) {
 487                 uint64_t *shadow = lookupAddressEntry(location);
 488                 uint64_t shadowval = *shadow;
 489                 ClockVector *currClock = get_execution()->get_cv(thread);
 490                 /* Do full record */
 491                 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 492                         fullRecordWriteNonAtomic(thread, location, shadow, currClock);
 493                         return;
 494                 }
 495
 496                 int threadid = id_to_int(thread);
 497                 modelclock_t ourClock = currClock->getClock(thread);
 498
 499                 /* Thread ID is too large or clock is too large. */
 500                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 501                         expandRecord(shadow);
 502                         fullRecordWriteNonAtomic(thread, location, shadow, currClock);
 503                         return;
 504                 }
 505
 506                 *shadow = ENCODEOP(0, 0, threadid, ourClock);
 507                 location = (void *)(((char *) location) + 1);
 508         }
 509 }
 510
 511
 512
 513 /** This function does race detection on a read for an expanded record. */
 514 struct DataRace * fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
 515 {
 516         struct RaceRecord *record = (struct RaceRecord *) (*shadow);
 517         struct DataRace * race = NULL;
 518         /* Check for datarace against last write. */
 519
 520         modelclock_t writeClock = record->writeClock;
 521         thread_id_t writeThread = record->writeThread;
 522
 523         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 524                 /* We have a datarace */
 525                 race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 526         }
 527
 528         /* Shorten vector when possible */
 529
 530         int copytoindex = 0;
 531
 532         for (int i = 0;i < record->numReads;i++) {
 533                 modelclock_t readClock = record->readClock[i];
 534                 thread_id_t readThread = record->thread[i];
 535
 536                 /*  Note that is not really a datarace check as reads cannot
 537                                 actually race.  It is just determining that this read subsumes
 538                                 another in the sense that either this read races or neither
 539                                 read races. Note that readClock can't actually be zero, so it
 540                                 could be optimized.  */
 541
 542                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 543                         /* Still need this read in vector */
 544                         if (copytoindex != i) {
 545                                 ASSERT(record->thread[i] >= 0);
 546                                 record->readClock[copytoindex] = record->readClock[i];
 547                                 record->thread[copytoindex] = record->thread[i];
 548                         }
 549                         copytoindex++;
 550                 }
 551         }
 552
 553         if (__builtin_popcount(copytoindex) <= 1) {
 554                 if (copytoindex == 0) {
 555                         int newCapacity = INITCAPACITY;
 556                         record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
 557                         record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
 558                 } else if (copytoindex>=INITCAPACITY) {
 559                         int newCapacity = copytoindex * 2;
 560                         thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
 561                         modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
 562                         std::memcpy(newthread, record->thread, copytoindex * sizeof(thread_id_t));
 563                         std::memcpy(newreadClock, record->readClock, copytoindex * sizeof(modelclock_t));
 564                         snapshot_free(record->readClock);
 565                         snapshot_free(record->thread);
 566                         record->readClock = newreadClock;
 567                         record->thread = newthread;
 568                 }
 569         }
 570
 571         modelclock_t ourClock = currClock->getClock(thread);
 572
 573         ASSERT(thread >= 0);
 574         record->thread[copytoindex] = thread;
 575         record->readClock[copytoindex] = ourClock;
 576         record->numReads = copytoindex + 1;
 577         return race;
 578 }
 579
 580 /** This function does race detection on a read. */
 581 void raceCheckRead(thread_id_t thread, const void *location)
 582 {
 583         uint64_t *shadow = lookupAddressEntry(location);
 584         uint64_t shadowval = *shadow;
 585         ClockVector *currClock = get_execution()->get_cv(thread);
 586         if (currClock == NULL)
 587                 return;
 588
 589         struct DataRace * race = NULL;
 590
 591         /* Do full record */
 592         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 593                 race = fullRaceCheckRead(thread, location, shadow, currClock);
 594                 goto Exit;
 595         }
 596
 597         {
 598                 int threadid = id_to_int(thread);
 599                 modelclock_t ourClock = currClock->getClock(thread);
 600
 601                 /* Thread ID is too large or clock is too large. */
 602                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 603                         expandRecord(shadow);
 604                         race = fullRaceCheckRead(thread, location, shadow, currClock);
 605                         goto Exit;
 606                 }
 607
 608                 /* Check for datarace against last write. */
 609
 610                 modelclock_t writeClock = WRITEVECTOR(shadowval);
 611                 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 612
 613                 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 614                         /* We have a datarace */
 615                         race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 616                         goto ShadowExit;
 617                 }
 618
 619 ShadowExit:
 620                 {
 621                         modelclock_t readClock = READVECTOR(shadowval);
 622                         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 623
 624                         if (clock_may_race(currClock, thread, readClock, readThread)) {
 625                                 /* We don't subsume this read... Have to expand record. */
 626                                 expandRecord(shadow);
 627                                 fullRaceCheckRead(thread, location, shadow, currClock);
 628                                 goto Exit;
 629                         }
 630                 }
 631
 632                 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock) | (shadowval & ATOMICMASK);
 633         }
 634 Exit:
 635         if (race) {
 636                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 637                 if (raceset->add(race))
 638                         assert_race(race);
 639                 else model_free(race);
 640         }
 641 }
 642
 643
 644 /** This function does race detection on a read for an expanded record. */
 645 struct DataRace * atomfullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
 646 {
 647         struct RaceRecord *record = (struct RaceRecord *) (*shadow);
 648         struct DataRace * race = NULL;
 649         /* Check for datarace against last write. */
 650         if (record->isAtomic)
 651                 return NULL;
 652
 653         modelclock_t writeClock = record->writeClock;
 654         thread_id_t writeThread = record->writeThread;
 655
 656         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 657                 /* We have a datarace */
 658                 race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 659         }
 660         return race;
 661 }
 662
 663 /** This function does race detection on a read. */
 664 void atomraceCheckRead(thread_id_t thread, const void *location)
 665 {
 666         uint64_t *shadow = lookupAddressEntry(location);
 667         uint64_t shadowval = *shadow;
 668         ClockVector *currClock = get_execution()->get_cv(thread);
 669         if (currClock == NULL)
 670                 return;
 671
 672         struct DataRace * race = NULL;
 673
 674         /* Do full record */
 675         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 676                 race = atomfullRaceCheckRead(thread, location, shadow, currClock);
 677                 goto Exit;
 678         }
 679
 680         if (shadowval & ATOMICMASK)
 681                 return;
 682
 683         {
 684                 /* Check for datarace against last write. */
 685
 686                 modelclock_t writeClock = WRITEVECTOR(shadowval);
 687                 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 688
 689                 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 690                         /* We have a datarace */
 691                         race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 692                         goto Exit;
 693                 }
 694
 695
 696         }
 697 Exit:
 698         if (race) {
 699                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 700                 if (raceset->add(race))
 701                         assert_race(race);
 702                 else model_free(race);
 703         }
 704 }
 705
 706 static inline void raceCheckRead_firstIt(thread_id_t thread, const void * location, uint64_t *old_val, uint64_t *new_val)
 707 {
 708         uint64_t *shadow = lookupAddressEntry(location);
 709         uint64_t shadowval = *shadow;
 710
 711         ClockVector *currClock = get_execution()->get_cv(thread);
 712         if (currClock == NULL)
 713                 return;
 714
 715         struct DataRace * race = NULL;
 716
 717         /* Do full record */
 718         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 719                 race = fullRaceCheckRead(thread, location, shadow, currClock);
 720                 goto Exit;
 721         }
 722
 723         {
 724                 int threadid = id_to_int(thread);
 725                 modelclock_t ourClock = currClock->getClock(thread);
 726
 727                 /* Thread ID is too large or clock is too large. */
 728                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 729                         expandRecord(shadow);
 730                         race = fullRaceCheckRead(thread, location, shadow, currClock);
 731                         goto Exit;
 732                 }
 733
 734                 /* Check for datarace against last write. */
 735
 736                 modelclock_t writeClock = WRITEVECTOR(shadowval);
 737                 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 738
 739                 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 740                         /* We have a datarace */
 741                         race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 742                 }
 743
 744                 modelclock_t readClock = READVECTOR(shadowval);
 745                 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 746
 747                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 748                         /* We don't subsume this read... Have to expand record. */
 749                         expandRecord(shadow);
 750                         struct RaceRecord *record = (struct RaceRecord *) (*shadow);
 751                         record->thread[1] = thread;
 752                         record->readClock[1] = ourClock;
 753                         record->numReads++;
 754
 755                         goto Exit;
 756                 }
 757
 758                 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock) | (shadowval & ATOMICMASK);
 759
 760                 *old_val = shadowval;
 761                 *new_val = *shadow;
 762         }
 763 Exit:
 764         if (race) {
 765                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 766                 if (raceset->add(race))
 767                         assert_race(race);
 768                 else model_free(race);
 769         }
 770 }
 771
 772 static inline void raceCheckRead_otherIt(thread_id_t thread, const void * location, uint64_t first_shadowval, uint64_t updated_shadowval)
 773 {
 774         uint64_t *shadow = lookupAddressEntry(location);
 775         uint64_t shadowval = *shadow;
 776
 777         if (shadowval == first_shadowval) {
 778                 *shadow = updated_shadowval;
 779                 return;
 780         }
 781
 782         ClockVector *currClock = get_execution()->get_cv(thread);
 783         if (currClock == NULL)
 784                 return;
 785
 786         struct DataRace * race = NULL;
 787
 788         /* Do full record */
 789         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 790                 race = fullRaceCheckRead(thread, location, shadow, currClock);
 791                 goto Exit;
 792         }
 793
 794         {
 795                 int threadid = id_to_int(thread);
 796                 modelclock_t ourClock = currClock->getClock(thread);
 797
 798                 /* Thread ID is too large or clock is too large. */
 799                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 800                         expandRecord(shadow);
 801                         race = fullRaceCheckRead(thread, location, shadow, currClock);
 802                         goto Exit;
 803                 }
 804
 805                 /* Check for datarace against last write. */
 806                 modelclock_t writeClock = WRITEVECTOR(shadowval);
 807                 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 808
 809                 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 810                         /* We have a datarace */
 811                         race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 812                 }
 813
 814                 modelclock_t readClock = READVECTOR(shadowval);
 815                 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 816
 817                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 818                         /* We don't subsume this read... Have to expand record. */
 819                         expandRecord(shadow);
 820                         struct RaceRecord *record = (struct RaceRecord *) (*shadow);
 821                         record->thread[1] = thread;
 822                         record->readClock[1] = ourClock;
 823                         record->numReads++;
 824
 825                         goto Exit;
 826                 }
 827
 828                 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock) | (shadowval & ATOMICMASK);
 829         }
 830 Exit:
 831         if (race) {
 832                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 833                 if (raceset->add(race))
 834                         assert_race(race);
 835                 else model_free(race);
 836         }
 837 }
 838
 839 void raceCheckRead64(thread_id_t thread, const void *location)
 840 {
 841         uint64_t old_shadowval, new_shadowval;
 842         old_shadowval = new_shadowval = INVALIDSHADOWVAL;
 843
 844         raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
 845         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 1), old_shadowval, new_shadowval);
 846         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 2), old_shadowval, new_shadowval);
 847         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 3), old_shadowval, new_shadowval);
 848         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 4), old_shadowval, new_shadowval);
 849         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 5), old_shadowval, new_shadowval);
 850         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 6), old_shadowval, new_shadowval);
 851         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 7), old_shadowval, new_shadowval);
 852 }
 853
 854 void raceCheckRead32(thread_id_t thread, const void *location)
 855 {
 856         uint64_t old_shadowval, new_shadowval;
 857         old_shadowval = new_shadowval = INVALIDSHADOWVAL;
 858
 859         raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
 860         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 1), old_shadowval, new_shadowval);
 861         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 2), old_shadowval, new_shadowval);
 862         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 3), old_shadowval, new_shadowval);
 863 }
 864
 865 void raceCheckRead16(thread_id_t thread, const void *location)
 866 {
 867         uint64_t old_shadowval, new_shadowval;
 868         old_shadowval = new_shadowval = INVALIDSHADOWVAL;
 869
 870         raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
 871         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 1), old_shadowval, new_shadowval);
 872 }
 873
 874 void raceCheckRead8(thread_id_t thread, const void *location)
 875 {
 876         uint64_t old_shadowval, new_shadowval;
 877         old_shadowval = new_shadowval = INVALIDSHADOWVAL;
 878
 879         raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
 880 }
 881
 882 static inline void raceCheckWrite_firstIt(thread_id_t thread, void * location, uint64_t *old_val, uint64_t *new_val)
 883 {
 884         uint64_t *shadow = lookupAddressEntry(location);
 885         uint64_t shadowval = *shadow;
 886         ClockVector *currClock = get_execution()->get_cv(thread);
 887         if (currClock == NULL)
 888                 return;
 889
 890         struct DataRace * race = NULL;
 891         /* Do full record */
 892         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 893                 race = fullRaceCheckWrite(thread, location, shadow, currClock);
 894                 goto Exit;
 895         }
 896
 897         {
 898                 int threadid = id_to_int(thread);
 899                 modelclock_t ourClock = currClock->getClock(thread);
 900
 901                 /* Thread ID is too large or clock is too large. */
 902                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 903                         expandRecord(shadow);
 904                         race = fullRaceCheckWrite(thread, location, shadow, currClock);
 905                         goto Exit;
 906                 }
 907
 908                 {
 909                         /* Check for datarace against last read. */
 910                         modelclock_t readClock = READVECTOR(shadowval);
 911                         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 912
 913                         if (clock_may_race(currClock, thread, readClock, readThread)) {
 914                                 /* We have a datarace */
 915                                 race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 916                                 goto ShadowExit;
 917                         }
 918                 }
 919
 920                 {
 921                         /* Check for datarace against last write. */
 922                         modelclock_t writeClock = WRITEVECTOR(shadowval);
 923                         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 924
 925                         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 926                                 /* We have a datarace */
 927                                 race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 928                                 goto ShadowExit;
 929                         }
 930                 }
 931
 932 ShadowExit:
 933                 *shadow = ENCODEOP(0, 0, threadid, ourClock);
 934
 935                 *old_val = shadowval;
 936                 *new_val = *shadow;
 937         }
 938
 939 Exit:
 940         if (race) {
 941                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 942                 if (raceset->add(race))
 943                         assert_race(race);
 944                 else model_free(race);
 945         }
 946 }
 947
 948 static inline void raceCheckWrite_otherIt(thread_id_t thread, void * location, uint64_t first_shadowval, uint64_t updated_shadowval)
 949 {
 950         uint64_t *shadow = lookupAddressEntry(location);
 951         uint64_t shadowval = *shadow;
 952
 953         if (shadowval == first_shadowval) {
 954                 *shadow = updated_shadowval;
 955                 return;
 956         }
 957
 958         ClockVector *currClock = get_execution()->get_cv(thread);
 959         if (currClock == NULL)
 960                 return;
 961
 962         struct DataRace * race = NULL;
 963         /* Do full record */
 964         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 965                 race = fullRaceCheckWrite(thread, location, shadow, currClock);
 966                 goto Exit;
 967         }
 968
 969         {
 970                 int threadid = id_to_int(thread);
 971                 modelclock_t ourClock = currClock->getClock(thread);
 972
 973                 /* Thread ID is too large or clock is too large. */
 974                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 975                         expandRecord(shadow);
 976                         race = fullRaceCheckWrite(thread, location, shadow, currClock);
 977                         goto Exit;
 978                 }
 979
 980                 {
 981                         /* Check for datarace against last read. */
 982                         modelclock_t readClock = READVECTOR(shadowval);
 983                         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 984
 985                         if (clock_may_race(currClock, thread, readClock, readThread)) {
 986                                 /* We have a datarace */
 987                                 race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 988                                 goto ShadowExit;
 989                         }
 990                 }
 991
 992                 {
 993                         /* Check for datarace against last write. */
 994                         modelclock_t writeClock = WRITEVECTOR(shadowval);
 995                         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 996
 997                         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 998                                 /* We have a datarace */
 999                                 race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
1000                                 goto ShadowExit;
1001                         }
1002                 }
1003
1004 ShadowExit:
1005                 *shadow = ENCODEOP(0, 0, threadid, ourClock);
1006         }
1007
1008 Exit:
1009         if (race) {
1010                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
1011                 if (raceset->add(race))
1012                         assert_race(race);
1013                 else model_free(race);
1014         }
1015 }
1016
1017 void raceCheckWrite64(thread_id_t thread, void *location)
1018 {
1019         uint64_t old_shadowval, new_shadowval;
1020         old_shadowval = new_shadowval = INVALIDSHADOWVAL;
1021
1022         raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
1023         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 1), old_shadowval, new_shadowval);
1024         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 2), old_shadowval, new_shadowval);
1025         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 3), old_shadowval, new_shadowval);
1026         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 4), old_shadowval, new_shadowval);
1027         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 5), old_shadowval, new_shadowval);
1028         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 6), old_shadowval, new_shadowval);
1029         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 7), old_shadowval, new_shadowval);
1030 }
1031
1032 void raceCheckWrite32(thread_id_t thread, void *location)
1033 {
1034         uint64_t old_shadowval, new_shadowval;
1035         old_shadowval = new_shadowval = INVALIDSHADOWVAL;
1036
1037         raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
1038         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 1), old_shadowval, new_shadowval);
1039         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 2), old_shadowval, new_shadowval);
1040         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 3), old_shadowval, new_shadowval);
1041 }
1042
1043 void raceCheckWrite16(thread_id_t thread, void *location)
1044 {
1045         uint64_t old_shadowval, new_shadowval;
1046         old_shadowval = new_shadowval = INVALIDSHADOWVAL;
1047
1048         raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
1049         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 1), old_shadowval, new_shadowval);
1050 }
1051
1052 void raceCheckWrite8(thread_id_t thread, void *location)
1053 {
1054         uint64_t old_shadowval, new_shadowval;
1055         old_shadowval = new_shadowval = INVALIDSHADOWVAL;
1056
1057         raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
1058 }
1059
1060 /*
1061 #define RACECHECKWRITE(size) \
1062         void raceCheckWrite ## size(thread_id_t thread, void *location) {               \
1063                 uint64_t old_shadowval, new_shadowval;                                                          \
1064                 old_shadowval = new_shadowval = 0;                                                                      \
1065                 raceCheckWrite_firstit(thread, location, &old_shadowval, &new_shadowval); \
1066                 for (int i=1; i < size / 8;i++) {                                                                       \
1067                         raceCheckWrite_otherit(thread, (void *)(((char *)location) + 1), old_shadowval, new_shadowval); \
1068                 }                                                                                                                                       \
1069         }
1070
1071 RACECHECKWRITE(8)
1072 RACECHECKWRITE(16)
1073 RACECHECKWRITE(32)
1074 RACECHECKWRITE(64)
1075
1076 #define RACECHECKREAD(size) \
1077         void raceCheckRead ## size(thread_id_t thread, void *location) {                \
1078                 uint64_t old_shadowval, new_shadowval;                                                          \
1079                 old_shadowval = new_shadowval = 0;                                                                      \
1080                 raceCheckRead_firstit(thread, location, &old_shadowval, &new_shadowval); \
1081                 for (int i=1; i < size / 8;i++) {                                                                       \
1082                         raceCheckRead_otherit(thread, (void *)(((char *)location) + 1), old_shadowval, new_shadowval); \
1083                 }                                                                                                                                       \
1084         }
1085
1086 RACECHECKREAD(8)
1087 RACECHECKREAD(16)
1088 RACECHECKREAD(32)
1089 RACECHECKREAD(64)
1090 */
1091