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 Exit:
 761         if (race) {
 762                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 763                 if (raceset->add(race))
 764                         assert_race(race);
 765                 else model_free(race);
 766         }
 767
 768
 769         *old_val = shadowval;
 770         *new_val = *shadow;
 771 }
 772
 773 static inline void raceCheckRead_otherIt(thread_id_t thread, const void * location, uint64_t first_shadowval, uint64_t updated_shadowval)
 774 {
 775         uint64_t *shadow = lookupAddressEntry(location);
 776         uint64_t shadowval = *shadow;
 777
 778         if (shadowval != 0 && shadowval == first_shadowval) {
 779                 *shadow = updated_shadowval;
 780                 return;
 781         }
 782
 783         ClockVector *currClock = get_execution()->get_cv(thread);
 784         if (currClock == NULL)
 785                 return;
 786
 787         struct DataRace * race = NULL;
 788
 789         /* Do full record */
 790         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 791                 race = fullRaceCheckRead(thread, location, shadow, currClock);
 792                 goto Exit;
 793         }
 794
 795         {
 796                 int threadid = id_to_int(thread);
 797                 modelclock_t ourClock = currClock->getClock(thread);
 798
 799                 /* Thread ID is too large or clock is too large. */
 800                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 801                         expandRecord(shadow);
 802                         race = fullRaceCheckRead(thread, location, shadow, currClock);
 803                         goto Exit;
 804                 }
 805
 806                 /* Check for datarace against last write. */
 807                 modelclock_t writeClock = WRITEVECTOR(shadowval);
 808                 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 809
 810                 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 811                         /* We have a datarace */
 812                         race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 813                 }
 814
 815                 modelclock_t readClock = READVECTOR(shadowval);
 816                 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 817
 818                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 819                         /* We don't subsume this read... Have to expand record. */
 820                         expandRecord(shadow);
 821                         struct RaceRecord *record = (struct RaceRecord *) (*shadow);
 822                         record->thread[1] = thread;
 823                         record->readClock[1] = ourClock;
 824                         record->numReads++;
 825
 826                         goto Exit;
 827                 }
 828
 829                 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock) | (shadowval & ATOMICMASK);
 830         }
 831 Exit:
 832         if (race) {
 833                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 834                 if (raceset->add(race))
 835                         assert_race(race);
 836                 else model_free(race);
 837         }
 838 }
 839
 840 void raceCheckRead64(thread_id_t thread, const void *location)
 841 {
 842         uint64_t old_shadowval, new_shadowval;
 843         old_shadowval = new_shadowval = 0;
 844
 845         raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
 846         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 1), old_shadowval, new_shadowval);
 847         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 2), old_shadowval, new_shadowval);
 848         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 3), old_shadowval, new_shadowval);
 849         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 4), old_shadowval, new_shadowval);
 850         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 5), old_shadowval, new_shadowval);
 851         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 6), old_shadowval, new_shadowval);
 852         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 7), old_shadowval, new_shadowval);
 853 }
 854
 855 void raceCheckRead32(thread_id_t thread, const void *location)
 856 {
 857         uint64_t old_shadowval, new_shadowval;
 858         old_shadowval = new_shadowval = 0;
 859
 860         raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
 861         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 1), old_shadowval, new_shadowval);
 862         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 2), old_shadowval, new_shadowval);
 863         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 3), old_shadowval, new_shadowval);
 864 }
 865
 866 void raceCheckRead16(thread_id_t thread, const void *location)
 867 {
 868         uint64_t old_shadowval, new_shadowval;
 869         old_shadowval = new_shadowval = 0;
 870
 871         raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
 872         raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 1), old_shadowval, new_shadowval);
 873 }
 874
 875 void raceCheckRead8(thread_id_t thread, const void *location)
 876 {
 877         uint64_t old_shadowval, new_shadowval;
 878         old_shadowval = new_shadowval = 0;
 879
 880         raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
 881 }
 882
 883 static inline void raceCheckWrite_firstIt(thread_id_t thread, void * location, uint64_t *old_val, uint64_t *new_val)
 884 {
 885         uint64_t *shadow = lookupAddressEntry(location);
 886         uint64_t shadowval = *shadow;
 887         ClockVector *currClock = get_execution()->get_cv(thread);
 888         if (currClock == NULL)
 889                 return;
 890
 891         struct DataRace * race = NULL;
 892         /* Do full record */
 893         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 894                 race = fullRaceCheckWrite(thread, location, shadow, currClock);
 895                 goto Exit;
 896         }
 897
 898         {
 899                 int threadid = id_to_int(thread);
 900                 modelclock_t ourClock = currClock->getClock(thread);
 901
 902                 /* Thread ID is too large or clock is too large. */
 903                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 904                         expandRecord(shadow);
 905                         race = fullRaceCheckWrite(thread, location, shadow, currClock);
 906                         goto Exit;
 907                 }
 908
 909                 {
 910                         /* Check for datarace against last read. */
 911                         modelclock_t readClock = READVECTOR(shadowval);
 912                         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 913
 914                         if (clock_may_race(currClock, thread, readClock, readThread)) {
 915                                 /* We have a datarace */
 916                                 race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 917                                 goto ShadowExit;
 918                         }
 919                 }
 920
 921                 {
 922                         /* Check for datarace against last write. */
 923                         modelclock_t writeClock = WRITEVECTOR(shadowval);
 924                         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 925
 926                         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 927                                 /* We have a datarace */
 928                                 race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 929                                 goto ShadowExit;
 930                         }
 931                 }
 932
 933 ShadowExit:
 934                 *shadow = ENCODEOP(0, 0, threadid, ourClock);
 935         }
 936
 937 Exit:
 938         if (race) {
 939                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 940                 if (raceset->add(race))
 941                         assert_race(race);
 942                 else model_free(race);
 943         }
 944
 945         *old_val = shadowval;
 946         *new_val = *shadow;
 947 }
 948
 949 static inline void raceCheckWrite_otherIt(thread_id_t thread, void * location, uint64_t first_shadowval, uint64_t updated_shadowval)
 950 {
 951         uint64_t *shadow = lookupAddressEntry(location);
 952         uint64_t shadowval = *shadow;
 953
 954         if (shadowval != 0 && shadowval == first_shadowval) {
 955                 *shadow = updated_shadowval;
 956                 return;
 957         }
 958
 959         ClockVector *currClock = get_execution()->get_cv(thread);
 960         if (currClock == NULL)
 961                 return;
 962
 963         struct DataRace * race = NULL;
 964         /* Do full record */
 965         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 966                 race = fullRaceCheckWrite(thread, location, shadow, currClock);
 967                 goto Exit;
 968         }
 969
 970         {
 971                 int threadid = id_to_int(thread);
 972                 modelclock_t ourClock = currClock->getClock(thread);
 973
 974                 /* Thread ID is too large or clock is too large. */
 975                 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 976                         expandRecord(shadow);
 977                         race = fullRaceCheckWrite(thread, location, shadow, currClock);
 978                         goto Exit;
 979                 }
 980
 981                 {
 982                         /* Check for datarace against last read. */
 983                         modelclock_t readClock = READVECTOR(shadowval);
 984                         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 985
 986                         if (clock_may_race(currClock, thread, readClock, readThread)) {
 987                                 /* We have a datarace */
 988                                 race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 989                                 goto ShadowExit;
 990                         }
 991                 }
 992
 993                 {
 994                         /* Check for datarace against last write. */
 995                         modelclock_t writeClock = WRITEVECTOR(shadowval);
 996                         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 997
 998                         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 999                                 /* We have a datarace */
1000                                 race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
1001                                 goto ShadowExit;
1002                         }
1003                 }
1004
1005 ShadowExit:
1006                 *shadow = ENCODEOP(0, 0, threadid, ourClock);
1007         }
1008
1009 Exit:
1010         if (race) {
1011                 race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
1012                 if (raceset->add(race))
1013                         assert_race(race);
1014                 else model_free(race);
1015         }
1016 }
1017
1018 void raceCheckWrite64(thread_id_t thread, void *location)
1019 {
1020         uint64_t old_shadowval, new_shadowval;
1021         old_shadowval = new_shadowval = 0;
1022
1023         raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
1024         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 1), old_shadowval, new_shadowval);
1025         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 2), old_shadowval, new_shadowval);
1026         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 3), old_shadowval, new_shadowval);
1027         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 4), old_shadowval, new_shadowval);
1028         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 5), old_shadowval, new_shadowval);
1029         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 6), old_shadowval, new_shadowval);
1030         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 7), old_shadowval, new_shadowval);
1031 }
1032
1033 void raceCheckWrite32(thread_id_t thread, void *location)
1034 {
1035         uint64_t old_shadowval, new_shadowval;
1036         old_shadowval = new_shadowval = 0;
1037
1038         raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
1039         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 1), old_shadowval, new_shadowval);
1040         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 2), old_shadowval, new_shadowval);
1041         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 3), old_shadowval, new_shadowval);
1042 }
1043
1044 void raceCheckWrite16(thread_id_t thread, void *location)
1045 {
1046         uint64_t old_shadowval, new_shadowval;
1047         old_shadowval = new_shadowval = 0;
1048
1049         raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
1050         raceCheckWrite_otherIt(thread, (void *)(((uintptr_t)location) + 1), old_shadowval, new_shadowval);
1051 }
1052
1053 void raceCheckWrite8(thread_id_t thread, void *location)
1054 {
1055         uint64_t old_shadowval, new_shadowval;
1056         old_shadowval = new_shadowval = 0;
1057
1058         raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
1059 }
1060
1061 /*
1062 #define RACECHECKWRITE(size) \
1063         void raceCheckWrite ## size(thread_id_t thread, void *location) {               \
1064                 uint64_t old_shadowval, new_shadowval;                                                          \
1065                 old_shadowval = new_shadowval = 0;                                                                      \
1066                 raceCheckWrite_firstit(thread, location, &old_shadowval, &new_shadowval); \
1067                 for (int i=1; i < size / 8;i++) {                                                                       \
1068                         raceCheckWrite_otherit(thread, (void *)(((char *)location) + 1), old_shadowval, new_shadowval); \
1069                 }                                                                                                                                       \
1070         }
1071
1072 RACECHECKWRITE(8)
1073 RACECHECKWRITE(16)
1074 RACECHECKWRITE(32)
1075 RACECHECKWRITE(64)
1076
1077 #define RACECHECKREAD(size) \
1078         void raceCheckRead ## size(thread_id_t thread, void *location) {                \
1079                 uint64_t old_shadowval, new_shadowval;                                                          \
1080                 old_shadowval = new_shadowval = 0;                                                                      \
1081                 raceCheckRead_firstit(thread, location, &old_shadowval, &new_shadowval); \
1082                 for (int i=1; i < size / 8;i++) {                                                                       \
1083                         raceCheckRead_otherit(thread, (void *)(((char *)location) + 1), old_shadowval, new_shadowval); \
1084                 }                                                                                                                                       \
1085         }
1086
1087 RACECHECKREAD(8)
1088 RACECHECKREAD(16)
1089 RACECHECKREAD(32)
1090 RACECHECKREAD(64)
1091 */
1092