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