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