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