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 std::vector<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         char buf[200];
 154         char *ptr = buf;
 155         ptr += sprintf(ptr, "Data race detected @ address %p:\n", race->address);
 156         ptr += sprintf(ptr, "    Access 1: %5s in thread %2d @ clock %3u\n",
 157                         race->isoldwrite ? "write" : "read",
 158                         id_to_int(race->oldthread), race->oldclock);
 159         ptr += sprintf(ptr, "    Access 2: %5s in thread %2d @ clock %3u",
 160                         race->isnewwrite ? "write" : "read",
 161                         id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
 162         model->assert_bug(buf);
 163 }
 164
 165 /** This function does race detection for a write on an expanded record. */
 166 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock)
 167 {
 168         struct RaceRecord *record = (struct RaceRecord *)(*shadow);
 169
 170         /* Check for datarace against last read. */
 171
 172         for (int i = 0; i < record->numReads; i++) {
 173                 modelclock_t readClock = record->readClock[i];
 174                 thread_id_t readThread = record->thread[i];
 175
 176                 /* Note that readClock can't actuall be zero here, so it could be
 177                          optimized. */
 178
 179                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 180                         /* We have a datarace */
 181                         reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
 182                 }
 183         }
 184
 185         /* Check for datarace against last write. */
 186
 187         modelclock_t writeClock = record->writeClock;
 188         thread_id_t writeThread = record->writeThread;
 189
 190         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 191                 /* We have a datarace */
 192                 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
 193         }
 194
 195         record->numReads = 0;
 196         record->writeThread = thread;
 197         modelclock_t ourClock = currClock->getClock(thread);
 198         record->writeClock = ourClock;
 199 }
 200
 201 /** This function does race detection on a write. */
 202 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
 203 {
 204         uint64_t *shadow = lookupAddressEntry(location);
 205         uint64_t shadowval = *shadow;
 206
 207         /* Do full record */
 208         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 209                 fullRaceCheckWrite(thread, location, shadow, currClock);
 210                 return;
 211         }
 212
 213         int threadid = id_to_int(thread);
 214         modelclock_t ourClock = currClock->getClock(thread);
 215
 216         /* Thread ID is too large or clock is too large. */
 217         if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 218                 expandRecord(shadow);
 219                 fullRaceCheckWrite(thread, location, shadow, currClock);
 220                 return;
 221         }
 222
 223         /* Check for datarace against last read. */
 224
 225         modelclock_t readClock = READVECTOR(shadowval);
 226         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 227
 228         if (clock_may_race(currClock, thread, readClock, readThread)) {
 229                 /* We have a datarace */
 230                 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
 231         }
 232
 233         /* Check for datarace against last write. */
 234
 235         modelclock_t writeClock = WRITEVECTOR(shadowval);
 236         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 237
 238         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 239                 /* We have a datarace */
 240                 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
 241         }
 242         *shadow = ENCODEOP(0, 0, threadid, ourClock);
 243 }
 244
 245 /** This function does race detection on a read for an expanded record. */
 246 void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
 247 {
 248         struct RaceRecord *record = (struct RaceRecord *) (*shadow);
 249
 250         /* Check for datarace against last write. */
 251
 252         modelclock_t writeClock = record->writeClock;
 253         thread_id_t writeThread = record->writeThread;
 254
 255         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 256                 /* We have a datarace */
 257                 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
 258         }
 259
 260         /* Shorten vector when possible */
 261
 262         int copytoindex = 0;
 263
 264         for (int i = 0; i < record->numReads; i++) {
 265                 modelclock_t readClock = record->readClock[i];
 266                 thread_id_t readThread = record->thread[i];
 267
 268                 /*  Note that is not really a datarace check as reads cannott
 269                                 actually race.  It is just determining that this read subsumes
 270                                 another in the sense that either this read races or neither
 271                                 read races. Note that readClock can't actually be zero, so it
 272                                 could be optimized.  */
 273
 274                 if (clock_may_race(currClock, thread, readClock, readThread)) {
 275                         /* Still need this read in vector */
 276                         if (copytoindex != i) {
 277                                 record->readClock[copytoindex] = record->readClock[i];
 278                                 record->thread[copytoindex] = record->thread[i];
 279                         }
 280                         copytoindex++;
 281                 }
 282         }
 283
 284         if (copytoindex >= record->capacity) {
 285                 int newCapacity = record->capacity * 2;
 286                 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
 287                 modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
 288                 std::memcpy(newthread, record->thread, record->capacity * sizeof(thread_id_t));
 289                 std::memcpy(newreadClock, record->readClock, record->capacity * sizeof(modelclock_t));
 290                 snapshot_free(record->readClock);
 291                 snapshot_free(record->thread);
 292                 record->readClock = newreadClock;
 293                 record->thread = newthread;
 294                 record->capacity = newCapacity;
 295         }
 296
 297         modelclock_t ourClock = currClock->getClock(thread);
 298
 299         record->thread[copytoindex] = thread;
 300         record->readClock[copytoindex] = ourClock;
 301         record->numReads = copytoindex + 1;
 302 }
 303
 304 /** This function does race detection on a read. */
 305 void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock)
 306 {
 307         uint64_t *shadow = lookupAddressEntry(location);
 308         uint64_t shadowval = *shadow;
 309
 310         /* Do full record */
 311         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
 312                 fullRaceCheckRead(thread, location, shadow, currClock);
 313                 return;
 314         }
 315
 316         int threadid = id_to_int(thread);
 317         modelclock_t ourClock = currClock->getClock(thread);
 318
 319         /* Thread ID is too large or clock is too large. */
 320         if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
 321                 expandRecord(shadow);
 322                 fullRaceCheckRead(thread, location, shadow, currClock);
 323                 return;
 324         }
 325
 326         /* Check for datarace against last write. */
 327
 328         modelclock_t writeClock = WRITEVECTOR(shadowval);
 329         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 330
 331         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 332                 /* We have a datarace */
 333                 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
 334         }
 335
 336         modelclock_t readClock = READVECTOR(shadowval);
 337         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 338
 339         if (clock_may_race(currClock, thread, readClock, readThread)) {
 340                 /* We don't subsume this read... Have to expand record. */
 341                 expandRecord(shadow);
 342                 fullRaceCheckRead(thread, location, shadow, currClock);
 343                 return;
 344         }
 345
 346         *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
 347 }