3 #include "threads-model.h"
7 #include "clockvector.h"
11 static struct ShadowTable *root;
12 SnapVector<struct DataRace *> unrealizedraces;
13 static void *memory_base;
14 static void *memory_top;
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)
206 uint64_t *shadow = lookupAddressEntry(location);
207 uint64_t shadowval = *shadow;
208 ClockVector *currClock = model->get_cv(thread);
211 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
212 fullRaceCheckWrite(thread, location, shadow, currClock);
216 int threadid = id_to_int(thread);
217 modelclock_t ourClock = currClock->getClock(thread);
219 /* Thread ID is too large or clock is too large. */
220 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
221 expandRecord(shadow);
222 fullRaceCheckWrite(thread, location, shadow, currClock);
226 /* Check for datarace against last read. */
228 modelclock_t readClock = READVECTOR(shadowval);
229 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
231 if (clock_may_race(currClock, thread, readClock, readThread)) {
232 /* We have a datarace */
233 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
236 /* Check for datarace against last write. */
238 modelclock_t writeClock = WRITEVECTOR(shadowval);
239 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
241 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
242 /* We have a datarace */
243 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
245 *shadow = ENCODEOP(0, 0, threadid, ourClock);
248 /** This function does race detection on a read for an expanded record. */
249 void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
251 struct RaceRecord *record = (struct RaceRecord *) (*shadow);
253 /* Check for datarace against last write. */
255 modelclock_t writeClock = record->writeClock;
256 thread_id_t writeThread = record->writeThread;
258 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
259 /* We have a datarace */
260 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
263 /* Shorten vector when possible */
267 for (int i = 0; i < record->numReads; i++) {
268 modelclock_t readClock = record->readClock[i];
269 thread_id_t readThread = record->thread[i];
271 /* Note that is not really a datarace check as reads cannott
272 actually race. It is just determining that this read subsumes
273 another in the sense that either this read races or neither
274 read races. Note that readClock can't actually be zero, so it
275 could be optimized. */
277 if (clock_may_race(currClock, thread, readClock, readThread)) {
278 /* Still need this read in vector */
279 if (copytoindex != i) {
280 record->readClock[copytoindex] = record->readClock[i];
281 record->thread[copytoindex] = record->thread[i];
287 if (copytoindex >= record->capacity) {
288 int newCapacity = record->capacity * 2;
289 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
290 modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
291 std::memcpy(newthread, record->thread, record->capacity * sizeof(thread_id_t));
292 std::memcpy(newreadClock, record->readClock, record->capacity * sizeof(modelclock_t));
293 snapshot_free(record->readClock);
294 snapshot_free(record->thread);
295 record->readClock = newreadClock;
296 record->thread = newthread;
297 record->capacity = newCapacity;
300 modelclock_t ourClock = currClock->getClock(thread);
302 record->thread[copytoindex] = thread;
303 record->readClock[copytoindex] = ourClock;
304 record->numReads = copytoindex + 1;
307 /** This function does race detection on a read. */
308 void raceCheckRead(thread_id_t thread, const void *location)
310 uint64_t *shadow = lookupAddressEntry(location);
311 uint64_t shadowval = *shadow;
312 ClockVector *currClock = model->get_cv(thread);
315 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
316 fullRaceCheckRead(thread, location, shadow, currClock);
320 int threadid = id_to_int(thread);
321 modelclock_t ourClock = currClock->getClock(thread);
323 /* Thread ID is too large or clock is too large. */
324 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
325 expandRecord(shadow);
326 fullRaceCheckRead(thread, location, shadow, currClock);
330 /* Check for datarace against last write. */
332 modelclock_t writeClock = WRITEVECTOR(shadowval);
333 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
335 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
336 /* We have a datarace */
337 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
340 modelclock_t readClock = READVECTOR(shadowval);
341 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
343 if (clock_may_race(currClock, thread, readClock, readThread)) {
344 /* We don't subsume this read... Have to expand record. */
345 expandRecord(shadow);
346 fullRaceCheckRead(thread, location, shadow, currClock);
350 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);