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