3 #include "threads-model.h"
7 #include "clockvector.h"
10 struct ShadowTable *root;
11 std::vector<struct DataRace *> unrealizedraces;
16 /** This function initialized the data race detector. */
17 void initRaceDetector()
19 root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1);
20 memory_base = snapshot_calloc(sizeof(struct ShadowBaseTable) * SHADOWBASETABLES, 1);
21 memory_top = ((char *)memory_base) + sizeof(struct ShadowBaseTable) * SHADOWBASETABLES;
24 void * table_calloc(size_t size)
26 if ((((char *)memory_base) + size) > memory_top) {
27 return snapshot_calloc(size, 1);
29 void *tmp = memory_base;
30 memory_base = ((char *)memory_base) + size;
35 /** This function looks up the entry in the shadow table corresponding to a
37 static uint64_t * lookupAddressEntry(const void *address)
39 struct ShadowTable *currtable = root;
41 currtable = (struct ShadowTable *) currtable->array[(((uintptr_t)address) >> 32) & MASK16BIT];
42 if (currtable == NULL) {
43 currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address) >> 32) & MASK16BIT] = table_calloc(sizeof(struct ShadowTable)));
47 struct ShadowBaseTable *basetable = (struct ShadowBaseTable *)currtable->array[(((uintptr_t)address) >> 16) & MASK16BIT];
48 if (basetable == NULL) {
49 basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address) >> 16) & MASK16BIT] = table_calloc(sizeof(struct ShadowBaseTable)));
51 return &basetable->array[((uintptr_t)address) & MASK16BIT];
55 * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
56 * to check the potential for a data race.
57 * @param clock1 The current clock vector
58 * @param tid1 The current thread; paired with clock1
59 * @param clock2 The clock value for the potentially-racing action
60 * @param tid2 The thread ID for the potentially-racing action
61 * @return true if the current clock allows a race with the event at clock2/tid2
63 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
64 modelclock_t clock2, thread_id_t tid2)
66 return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
70 * Expands a record from the compact form to the full form. This is
71 * necessary for multiple readers or for very large thread ids or time
73 static void expandRecord(uint64_t *shadow)
75 uint64_t shadowval = *shadow;
77 modelclock_t readClock = READVECTOR(shadowval);
78 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
79 modelclock_t writeClock = WRITEVECTOR(shadowval);
80 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
82 struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord));
83 record->writeThread = writeThread;
84 record->writeClock = writeClock;
87 record->capacity = INITCAPACITY;
88 record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * record->capacity);
89 record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * record->capacity);
91 record->thread[0] = readThread;
92 record->readClock[0] = readClock;
94 *shadow = (uint64_t) record;
97 /** This function is called when we detect a data race.*/
98 static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address)
100 struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
101 race->oldthread = oldthread;
102 race->oldclock = oldclock;
103 race->isoldwrite = isoldwrite;
104 race->newaction = newaction;
105 race->isnewwrite = isnewwrite;
106 race->address = address;
107 unrealizedraces.push_back(race);
109 /* If the race is realized, bail out now. */
110 if (checkDataRaces())
111 model->switch_to_master(NULL);
115 * @brief Check and report data races
117 * If the trace is feasible (a feasible prefix), clear out the list of
118 * unrealized data races, asserting any realized ones as execution bugs so that
119 * the model-checker will end the execution.
121 * @return True if any data races were realized
123 bool checkDataRaces()
125 if (model->isfeasibleprefix()) {
126 bool race_asserted = false;
127 /* Prune the non-racing unrealized dataraces */
128 for (unsigned i = 0; i < unrealizedraces.size(); i++) {
129 struct DataRace *race = unrealizedraces[i];
130 if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
132 race_asserted = true;
136 unrealizedraces.clear();
137 return race_asserted;
143 * @brief Assert a data race
145 * Asserts a data race which is currently realized, causing the execution to
146 * end and stashing a message in the model-checker's bug list
148 * @param race The race to report
150 void assert_race(struct DataRace *race)
154 ptr += sprintf(ptr, "Data race detected @ address %p:\n", race->address);
155 ptr += sprintf(ptr, " Access 1: %5s in thread %2d @ clock %3u\n",
156 race->isoldwrite ? "write" : "read",
157 id_to_int(race->oldthread), race->oldclock);
158 ptr += sprintf(ptr, " Access 2: %5s in thread %2d @ clock %3u",
159 race->isnewwrite ? "write" : "read",
160 id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
161 model->assert_bug(buf);
164 /** This function does race detection for a write on an expanded record. */
165 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock)
167 struct RaceRecord *record = (struct RaceRecord *)(*shadow);
169 /* Check for datarace against last read. */
171 for (int i = 0; i < record->numReads; i++) {
172 modelclock_t readClock = record->readClock[i];
173 thread_id_t readThread = record->thread[i];
175 /* Note that readClock can't actuall be zero here, so it could be
178 if (clock_may_race(currClock, thread, readClock, readThread)) {
179 /* We have a datarace */
180 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
184 /* Check for datarace against last write. */
186 modelclock_t writeClock = record->writeClock;
187 thread_id_t writeThread = record->writeThread;
189 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
190 /* We have a datarace */
191 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
194 record->numReads = 0;
195 record->writeThread = thread;
196 modelclock_t ourClock = currClock->getClock(thread);
197 record->writeClock = ourClock;
200 /** This function does race detection on a write. */
201 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
203 uint64_t *shadow = lookupAddressEntry(location);
204 uint64_t shadowval = *shadow;
207 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
208 fullRaceCheckWrite(thread, location, shadow, currClock);
212 int threadid = id_to_int(thread);
213 modelclock_t ourClock = currClock->getClock(thread);
215 /* Thread ID is too large or clock is too large. */
216 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
217 expandRecord(shadow);
218 fullRaceCheckWrite(thread, location, shadow, currClock);
222 /* Check for datarace against last read. */
224 modelclock_t readClock = READVECTOR(shadowval);
225 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
227 if (clock_may_race(currClock, thread, readClock, readThread)) {
228 /* We have a datarace */
229 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
232 /* Check for datarace against last write. */
234 modelclock_t writeClock = WRITEVECTOR(shadowval);
235 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
237 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
238 /* We have a datarace */
239 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
241 *shadow = ENCODEOP(0, 0, threadid, ourClock);
244 /** This function does race detection on a read for an expanded record. */
245 void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
247 struct RaceRecord *record = (struct RaceRecord *) (*shadow);
249 /* Check for datarace against last write. */
251 modelclock_t writeClock = record->writeClock;
252 thread_id_t writeThread = record->writeThread;
254 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
255 /* We have a datarace */
256 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
259 /* Shorten vector when possible */
263 for (int i = 0; i < record->numReads; i++) {
264 modelclock_t readClock = record->readClock[i];
265 thread_id_t readThread = record->thread[i];
267 /* Note that is not really a datarace check as reads cannott
268 actually race. It is just determining that this read subsumes
269 another in the sense that either this read races or neither
270 read races. Note that readClock can't actually be zero, so it
271 could be optimized. */
273 if (clock_may_race(currClock, thread, readClock, readThread)) {
274 /* Still need this read in vector */
275 if (copytoindex != i) {
276 record->readClock[copytoindex] = record->readClock[i];
277 record->thread[copytoindex] = record->thread[i];
283 if (copytoindex >= record->capacity) {
284 int newCapacity = record->capacity * 2;
285 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
286 modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
287 std::memcpy(newthread, record->thread, record->capacity * sizeof(thread_id_t));
288 std::memcpy(newreadClock, record->readClock, record->capacity * sizeof(modelclock_t));
289 snapshot_free(record->readClock);
290 snapshot_free(record->thread);
291 record->readClock = newreadClock;
292 record->thread = newthread;
293 record->capacity = newCapacity;
296 modelclock_t ourClock = currClock->getClock(thread);
298 record->thread[copytoindex] = thread;
299 record->readClock[copytoindex] = ourClock;
300 record->numReads = copytoindex + 1;
303 /** This function does race detection on a read. */
304 void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock)
306 uint64_t *shadow = lookupAddressEntry(location);
307 uint64_t shadowval = *shadow;
310 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
311 fullRaceCheckRead(thread, location, shadow, currClock);
315 int threadid = id_to_int(thread);
316 modelclock_t ourClock = currClock->getClock(thread);
318 /* Thread ID is too large or clock is too large. */
319 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
320 expandRecord(shadow);
321 fullRaceCheckRead(thread, location, shadow, currClock);
325 /* Check for datarace against last write. */
327 modelclock_t writeClock = WRITEVECTOR(shadowval);
328 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
330 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
331 /* We have a datarace */
332 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
335 modelclock_t readClock = READVECTOR(shadowval);
336 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
338 if (clock_may_race(currClock, thread, readClock, readThread)) {
339 /* We don't subsume this read... Have to expand record. */
340 expandRecord(shadow);
341 fullRaceCheckRead(thread, location, shadow, currClock);
345 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);