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                 record->thread[0] = readThread;
 100                 record->readClock[0] = readClock;
 101         }
 102         *shadow = (uint64_t) record;
 103 }
 104
 105 /** This function is called when we detect a data race.*/
 106 static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address)
 107 {
 108         struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
 109         race->oldthread = oldthread;
 110         race->oldclock = oldclock;
 111         race->isoldwrite = isoldwrite;
 112         race->newaction = newaction;
 113         race->isnewwrite = isnewwrite;
 114         race->address = address;
 115         unrealizedraces->push_back(race);
 116
 117         /* If the race is realized, bail out now. */
 118         if (checkDataRaces())
 119                 model->switch_to_master(NULL);
 120 }
 121
 122 /**
 123  * @brief Check and report data races
 124  *
 125  * If the trace is feasible (a feasible prefix), clear out the list of
 126  * unrealized data races, asserting any realized ones as execution bugs so that
 127  * the model-checker will end the execution.
 128  *
 129  * @return True if any data races were realized
 130  */
 131 bool checkDataRaces()
 132 {
 133         if (get_execution()->isfeasibleprefix()) {
 134                 bool race_asserted = false;
 135                 /* Prune the non-racing unrealized dataraces */
 136                 for (unsigned i = 0; i < unrealizedraces->size(); i++) {
 137                         struct DataRace *race = (*unrealizedraces)[i];
 138                         if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
 139                                 assert_race(race);
 140                                 race_asserted = true;
 141                         }
 142                         snapshot_free(race);
 143                 }
 144                 unrealizedraces->clear();
 145                 return race_asserted;
 146         }
 147         return false;
 148 }
 149
 150 /**
 151  * @brief Assert a data race
 152  *
 153  * Asserts a data race which is currently realized, causing the execution to
 154  * end and stashing a message in the model-checker's bug list
 155  *
 156  * @param race The race to report
 157  */
 158 void assert_race(struct DataRace *race)
 159 {
 160         model->assert_bug(
 161                         "Data race detected @ address %p:\n"
 162                         "    Access 1: %5s in thread %2d @ clock %3u\n"
 163                         "    Access 2: %5s in thread %2d @ clock %3u",
 164                         race->address,
 165                         race->isoldwrite ? "write" : "read",
 166                         id_to_int(race->oldthread),
 167                         race->oldclock,
 168                         race->isnewwrite ? "write" : "read",
 169                         id_to_int(race->newaction->get_tid()),
 170                         race->newaction->get_seq_number()
 171                 );
 172 }
 173
 174 /** This function does race detection for a write on an expanded record. */
 175 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock)
 176 {
 177         struct RaceRecord *record = (struct RaceRecord *)(*shadow);
 178
 179         /* Check for datarace against last read. */
 180
 181         for (int i = 0; i < record->numReads; i++) {
 182                 modelclock_t readClock = record->readClock[i];
 183                 thread_id_t readThread = record->thread[i];
 184
 185                 /* Note that readClock can't actuall be zero here, so it could be
 186                          optimized. */
 187
 188                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 189                         /* We have a datarace */
 190                         reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 191                 }
 192         }
 193
 194         /* Check for datarace against last write. */
 195
 196         modelclock_t writeClock = record->writeClock;
 197         thread_id_t writeThread = record->writeThread;
 198
 199         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 200                 /* We have a datarace */
 201                 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 202         }
 203
 204         record->numReads = 0;
 205         record->writeThread = thread;
 206         modelclock_t ourClock = currClock->getClock(thread);
 207         record->writeClock = ourClock;
 208 }
 209
 210 /** This function does race detection on a write. */
 211 void raceCheckWrite(thread_id_t thread, void *location)
 212 {
 213         uint64_t *shadow = lookupAddressEntry(location);
 214         uint64_t shadowval = *shadow;
 215         ClockVector *currClock = get_execution()->get_cv(thread);
 216
 217         /* Do full record */
 218         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 219                 fullRaceCheckWrite(thread, location, shadow, currClock);
 220                 return;
 221         }
 222
 223         int threadid = id_to_int(thread);
 224         modelclock_t ourClock = currClock->getClock(thread);
 225
 226         /* Thread ID is too large or clock is too large. */
 227         if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 228                 expandRecord(shadow);
 229                 fullRaceCheckWrite(thread, location, shadow, currClock);
 230                 return;
 231         }
 232
 233         /* Check for datarace against last read. */
 234
 235         modelclock_t readClock = READVECTOR(shadowval);
 236         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 237
 238         if (clock_may_race(currClock, thread, readClock, readThread)) {
 239                 /* We have a datarace */
 240                 reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 241         }
 242
 243         /* Check for datarace against last write. */
 244
 245         modelclock_t writeClock = WRITEVECTOR(shadowval);
 246         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 247
 248         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 249                 /* We have a datarace */
 250                 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 251         }
 252         *shadow = ENCODEOP(0, 0, threadid, ourClock);
 253 }
 254
 255 /** This function does race detection on a read for an expanded record. */
 256 void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
 257 {
 258         struct RaceRecord *record = (struct RaceRecord *) (*shadow);
 259
 260         /* Check for datarace against last write. */
 261
 262         modelclock_t writeClock = record->writeClock;
 263         thread_id_t writeThread = record->writeThread;
 264
 265         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 266                 /* We have a datarace */
 267                 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 268         }
 269
 270         /* Shorten vector when possible */
 271
 272         int copytoindex = 0;
 273
 274         for (int i = 0; i < record->numReads; i++) {
 275                 modelclock_t readClock = record->readClock[i];
 276                 thread_id_t readThread = record->thread[i];
 277
 278                 /*  Note that is not really a datarace check as reads cannott
 279                                 actually race.  It is just determining that this read subsumes
 280                                 another in the sense that either this read races or neither
 281                                 read races. Note that readClock can't actually be zero, so it
 282                                 could be optimized.  */
 283
 284                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 285                         /* Still need this read in vector */
 286                         if (copytoindex != i) {
 287                                 record->readClock[copytoindex] = record->readClock[i];
 288                                 record->thread[copytoindex] = record->thread[i];
 289                         }
 290                         copytoindex++;
 291                 }
 292         }
 293
 294         if (copytoindex >= record->capacity) {
 295                 int newCapacity = record->capacity * 2;
 296                 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
 297                 modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
 298                 std::memcpy(newthread, record->thread, record->capacity * sizeof(thread_id_t));
 299                 std::memcpy(newreadClock, record->readClock, record->capacity * sizeof(modelclock_t));
 300                 snapshot_free(record->readClock);
 301                 snapshot_free(record->thread);
 302                 record->readClock = newreadClock;
 303                 record->thread = newthread;
 304                 record->capacity = newCapacity;
 305         }
 306
 307         modelclock_t ourClock = currClock->getClock(thread);
 308
 309         record->thread[copytoindex] = thread;
 310         record->readClock[copytoindex] = ourClock;
 311         record->numReads = copytoindex + 1;
 312 }
 313
 314 /** This function does race detection on a read. */
 315 void raceCheckRead(thread_id_t thread, const void *location)
 316 {
 317         uint64_t *shadow = lookupAddressEntry(location);
 318         uint64_t shadowval = *shadow;
 319         ClockVector *currClock = get_execution()->get_cv(thread);
 320
 321         /* Do full record */
 322         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 323                 fullRaceCheckRead(thread, location, shadow, currClock);
 324                 return;
 325         }
 326
 327         int threadid = id_to_int(thread);
 328         modelclock_t ourClock = currClock->getClock(thread);
 329
 330         /* Thread ID is too large or clock is too large. */
 331         if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 332                 expandRecord(shadow);
 333                 fullRaceCheckRead(thread, location, shadow, currClock);
 334                 return;
 335         }
 336
 337         /* Check for datarace against last write. */
 338
 339         modelclock_t writeClock = WRITEVECTOR(shadowval);
 340         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 341
 342         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 343                 /* We have a datarace */
 344                 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 345         }
 346
 347         modelclock_t readClock = READVECTOR(shadowval);
 348         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 349
 350         if (clock_may_race(currClock, thread, readClock, readThread)) {
 351                 /* We don't subsume this read... Have to expand record. */
 352                 expandRecord(shadow);
 353                 fullRaceCheckRead(thread, location, shadow, currClock);
 354                 return;
 355         }
 356
 357         *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
 358 }
 359
 360 bool haveUnrealizedRaces()
 361 {
 362         return !unrealizedraces->empty();
 363 }