3 #include "threads-model.h"
7 #include "clockvector.h"
11 struct ShadowTable *root;
12 SnapVector<struct DataRace *> unrealizedraces;
17 /** This function initialized the data race detector. */
18 void initRaceDetector()
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;
25 void * table_calloc(size_t size)
27 if ((((char *)memory_base) + size) > memory_top) {
28 return snapshot_calloc(size, 1);
30 void *tmp = memory_base;
31 memory_base = ((char *)memory_base) + size;
36 /** This function looks up the entry in the shadow table corresponding to a
38 static uint64_t * lookupAddressEntry(const void *address)
40 struct ShadowTable *currtable = root;
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)));
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)));
52 return &basetable->array[((uintptr_t)address) & MASK16BIT];
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
64 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
65 modelclock_t clock2, thread_id_t tid2)
67 return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
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
74 static void expandRecord(uint64_t *shadow)
76 uint64_t shadowval = *shadow;
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));
83 struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord));
84 record->writeThread = writeThread;
85 record->writeClock = writeClock;
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);
92 record->thread[0] = readThread;
93 record->readClock[0] = readClock;
95 *shadow = (uint64_t) record;
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)
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);
110 /* If the race is realized, bail out now. */
111 if (checkDataRaces())
112 model->switch_to_master(NULL);
116 * @brief Check and report data races
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.
122 * @return True if any data races were realized
124 bool checkDataRaces()
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)) {
133 race_asserted = true;
137 unrealizedraces.clear();
138 return race_asserted;
144 * @brief Assert a data race
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
149 * @param race The race to report
151 void assert_race(struct DataRace *race)
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",
158 race->isoldwrite ? "write" : "read",
159 id_to_int(race->oldthread),
161 race->isnewwrite ? "write" : "read",
162 id_to_int(race->newaction->get_tid()),
163 race->newaction->get_seq_number()
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)
170 struct RaceRecord *record = (struct RaceRecord *)(*shadow);
172 /* Check for datarace against last read. */
174 for (int i = 0; i < record->numReads; i++) {
175 modelclock_t readClock = record->readClock[i];
176 thread_id_t readThread = record->thread[i];
178 /* Note that readClock can't actuall be zero here, so it could be
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);
187 /* Check for datarace against last write. */
189 modelclock_t writeClock = record->writeClock;
190 thread_id_t writeThread = record->writeThread;
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);
197 record->numReads = 0;
198 record->writeThread = thread;
199 modelclock_t ourClock = currClock->getClock(thread);
200 record->writeClock = ourClock;
203 /** This function does race detection on a write. */
204 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
206 uint64_t *shadow = lookupAddressEntry(location);
207 uint64_t shadowval = *shadow;
210 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
211 fullRaceCheckWrite(thread, location, shadow, currClock);
215 int threadid = id_to_int(thread);
216 modelclock_t ourClock = currClock->getClock(thread);
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);
225 /* Check for datarace against last read. */
227 modelclock_t readClock = READVECTOR(shadowval);
228 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
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);
235 /* Check for datarace against last write. */
237 modelclock_t writeClock = WRITEVECTOR(shadowval);
238 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
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);
244 *shadow = ENCODEOP(0, 0, threadid, ourClock);
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)
250 struct RaceRecord *record = (struct RaceRecord *) (*shadow);
252 /* Check for datarace against last write. */
254 modelclock_t writeClock = record->writeClock;
255 thread_id_t writeThread = record->writeThread;
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);
262 /* Shorten vector when possible */
266 for (int i = 0; i < record->numReads; i++) {
267 modelclock_t readClock = record->readClock[i];
268 thread_id_t readThread = record->thread[i];
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. */
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];
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;
299 modelclock_t ourClock = currClock->getClock(thread);
301 record->thread[copytoindex] = thread;
302 record->readClock[copytoindex] = ourClock;
303 record->numReads = copytoindex + 1;
306 /** This function does race detection on a read. */
307 void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock)
309 uint64_t *shadow = lookupAddressEntry(location);
310 uint64_t shadowval = *shadow;
313 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
314 fullRaceCheckRead(thread, location, shadow, currClock);
318 int threadid = id_to_int(thread);
319 modelclock_t ourClock = currClock->getClock(thread);
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);
328 /* Check for datarace against last write. */
330 modelclock_t writeClock = WRITEVECTOR(shadowval);
331 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
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);
338 modelclock_t readClock = READVECTOR(shadowval);
339 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
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);
348 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);