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 struct ShadowTable *root;
  12 SnapVector<struct DataRace *> unrealizedraces;
  13 void *memory_base;
  14 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, ClockVector *currClock)
 205 {
 206         uint64_t *shadow = lookupAddressEntry(location);
 207         uint64_t shadowval = *shadow;
 208
 209         /* Do full record */
 210         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 211                 fullRaceCheckWrite(thread, location, shadow, currClock);
 212                 return;
 213         }
 214
 215         int threadid = id_to_int(thread);
 216         modelclock_t ourClock = currClock->getClock(thread);
 217
 218         /* Thread ID is too large or clock is too large. */
 219         if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 220                 expandRecord(shadow);
 221                 fullRaceCheckWrite(thread, location, shadow, currClock);
 222                 return;
 223         }
 224
 225         /* Check for datarace against last read. */
 226
 227         modelclock_t readClock = READVECTOR(shadowval);
 228         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 229
 230         if (clock_may_race(currClock, thread, readClock, readThread)) {
 231                 /* We have a datarace */
 232                 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
 233         }
 234
 235         /* Check for datarace against last write. */
 236
 237         modelclock_t writeClock = WRITEVECTOR(shadowval);
 238         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 239
 240         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 241                 /* We have a datarace */
 242                 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
 243         }
 244         *shadow = ENCODEOP(0, 0, threadid, ourClock);
 245 }
 246
 247 /** This function does race detection on a read for an expanded record. */
 248 void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
 249 {
 250         struct RaceRecord *record = (struct RaceRecord *) (*shadow);
 251
 252         /* Check for datarace against last write. */
 253
 254         modelclock_t writeClock = record->writeClock;
 255         thread_id_t writeThread = record->writeThread;
 256
 257         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 258                 /* We have a datarace */
 259                 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
 260         }
 261
 262         /* Shorten vector when possible */
 263
 264         int copytoindex = 0;
 265
 266         for (int i = 0; i < record->numReads; i++) {
 267                 modelclock_t readClock = record->readClock[i];
 268                 thread_id_t readThread = record->thread[i];
 269
 270                 /*  Note that is not really a datarace check as reads cannott
 271                                 actually race.  It is just determining that this read subsumes
 272                                 another in the sense that either this read races or neither
 273                                 read races. Note that readClock can't actually be zero, so it
 274                                 could be optimized.  */
 275
 276                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 277                         /* Still need this read in vector */
 278                         if (copytoindex != i) {
 279                                 record->readClock[copytoindex] = record->readClock[i];
 280                                 record->thread[copytoindex] = record->thread[i];
 281                         }
 282                         copytoindex++;
 283                 }
 284         }
 285
 286         if (copytoindex >= record->capacity) {
 287                 int newCapacity = record->capacity * 2;
 288                 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
 289                 modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
 290                 std::memcpy(newthread, record->thread, record->capacity * sizeof(thread_id_t));
 291                 std::memcpy(newreadClock, record->readClock, record->capacity * sizeof(modelclock_t));
 292                 snapshot_free(record->readClock);
 293                 snapshot_free(record->thread);
 294                 record->readClock = newreadClock;
 295                 record->thread = newthread;
 296                 record->capacity = newCapacity;
 297         }
 298
 299         modelclock_t ourClock = currClock->getClock(thread);
 300
 301         record->thread[copytoindex] = thread;
 302         record->readClock[copytoindex] = ourClock;
 303         record->numReads = copytoindex + 1;
 304 }
 305
 306 /** This function does race detection on a read. */
 307 void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock)
 308 {
 309         uint64_t *shadow = lookupAddressEntry(location);
 310         uint64_t shadowval = *shadow;
 311
 312         /* Do full record */
 313         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 314                 fullRaceCheckRead(thread, location, shadow, currClock);
 315                 return;
 316         }
 317
 318         int threadid = id_to_int(thread);
 319         modelclock_t ourClock = currClock->getClock(thread);
 320
 321         /* Thread ID is too large or clock is too large. */
 322         if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 323                 expandRecord(shadow);
 324                 fullRaceCheckRead(thread, location, shadow, currClock);
 325                 return;
 326         }
 327
 328         /* Check for datarace against last write. */
 329
 330         modelclock_t writeClock = WRITEVECTOR(shadowval);
 331         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 332
 333         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 334                 /* We have a datarace */
 335                 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
 336         }
 337
 338         modelclock_t readClock = READVECTOR(shadowval);
 339         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 340
 341         if (clock_may_race(currClock, thread, readClock, readThread)) {
 342                 /* We don't subsume this read... Have to expand record. */
 343                 expandRecord(shadow);
 344                 fullRaceCheckRead(thread, location, shadow, currClock);
 345                 return;
 346         }
 347
 348         *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
 349 }