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)
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);
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)
168 struct RaceRecord *record = (struct RaceRecord *)(*shadow);
170 /* Check for datarace against last read. */
172 for (int i = 0; i < record->numReads; i++) {
173 modelclock_t readClock = record->readClock[i];
174 thread_id_t readThread = record->thread[i];
176 /* Note that readClock can't actuall be zero here, so it could be
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);
185 /* Check for datarace against last write. */
187 modelclock_t writeClock = record->writeClock;
188 thread_id_t writeThread = record->writeThread;
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);
195 record->numReads = 0;
196 record->writeThread = thread;
197 modelclock_t ourClock = currClock->getClock(thread);
198 record->writeClock = ourClock;
201 /** This function does race detection on a write. */
202 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
204 uint64_t *shadow = lookupAddressEntry(location);
205 uint64_t shadowval = *shadow;
208 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
209 fullRaceCheckWrite(thread, location, shadow, currClock);
213 int threadid = id_to_int(thread);
214 modelclock_t ourClock = currClock->getClock(thread);
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);
223 /* Check for datarace against last read. */
225 modelclock_t readClock = READVECTOR(shadowval);
226 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
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);
233 /* Check for datarace against last write. */
235 modelclock_t writeClock = WRITEVECTOR(shadowval);
236 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
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);
242 *shadow = ENCODEOP(0, 0, threadid, ourClock);
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)
248 struct RaceRecord *record = (struct RaceRecord *) (*shadow);
250 /* Check for datarace against last write. */
252 modelclock_t writeClock = record->writeClock;
253 thread_id_t writeThread = record->writeThread;
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);
260 /* Shorten vector when possible */
264 for (int i = 0; i < record->numReads; i++) {
265 modelclock_t readClock = record->readClock[i];
266 thread_id_t readThread = record->thread[i];
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. */
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];
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;
297 modelclock_t ourClock = currClock->getClock(thread);
299 record->thread[copytoindex] = thread;
300 record->readClock[copytoindex] = ourClock;
301 record->numReads = copytoindex + 1;
304 /** This function does race detection on a read. */
305 void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock)
307 uint64_t *shadow = lookupAddressEntry(location);
308 uint64_t shadowval = *shadow;
311 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
312 fullRaceCheckRead(thread, location, shadow, currClock);
316 int threadid = id_to_int(thread);
317 modelclock_t ourClock = currClock->getClock(thread);
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);
326 /* Check for datarace against last write. */
328 modelclock_t writeClock = WRITEVECTOR(shadowval);
329 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
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);
336 modelclock_t readClock = READVECTOR(shadowval);
337 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
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);
346 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);