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