3 #include "threads-model.h"
7 #include "clockvector.h"
10 #include "execution.h"
11 #include "stl-model.h"
13 static struct ShadowTable *root;
14 static SnapVector<DataRace *> *unrealizedraces;
15 static void *memory_base;
16 static void *memory_top;
18 static const ModelExecution * get_execution()
20 return model->get_execution();
23 /** This function initialized the data race detector. */
24 void initRaceDetector()
26 root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1);
27 memory_base = snapshot_calloc(sizeof(struct ShadowBaseTable) * SHADOWBASETABLES, 1);
28 memory_top = ((char *)memory_base) + sizeof(struct ShadowBaseTable) * SHADOWBASETABLES;
29 unrealizedraces = new SnapVector<DataRace *>();
32 void * table_calloc(size_t size)
34 if ((((char *)memory_base) + size) > memory_top) {
35 return snapshot_calloc(size, 1);
37 void *tmp = memory_base;
38 memory_base = ((char *)memory_base) + size;
43 /** This function looks up the entry in the shadow table corresponding to a
45 static uint64_t * lookupAddressEntry(const void *address)
47 struct ShadowTable *currtable = root;
49 currtable = (struct ShadowTable *) currtable->array[(((uintptr_t)address) >> 32) & MASK16BIT];
50 if (currtable == NULL) {
51 currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address) >> 32) & MASK16BIT] = table_calloc(sizeof(struct ShadowTable)));
55 struct ShadowBaseTable *basetable = (struct ShadowBaseTable *)currtable->array[(((uintptr_t)address) >> 16) & MASK16BIT];
56 if (basetable == NULL) {
57 basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address) >> 16) & MASK16BIT] = table_calloc(sizeof(struct ShadowBaseTable)));
59 return &basetable->array[((uintptr_t)address) & MASK16BIT];
63 * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
64 * to check the potential for a data race.
65 * @param clock1 The current clock vector
66 * @param tid1 The current thread; paired with clock1
67 * @param clock2 The clock value for the potentially-racing action
68 * @param tid2 The thread ID for the potentially-racing action
69 * @return true if the current clock allows a race with the event at clock2/tid2
71 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
72 modelclock_t clock2, thread_id_t tid2)
74 return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
78 * Expands a record from the compact form to the full form. This is
79 * necessary for multiple readers or for very large thread ids or time
81 static void expandRecord(uint64_t *shadow)
83 uint64_t shadowval = *shadow;
85 modelclock_t readClock = READVECTOR(shadowval);
86 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
87 modelclock_t writeClock = WRITEVECTOR(shadowval);
88 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
90 struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord));
91 record->writeThread = writeThread;
92 record->writeClock = writeClock;
95 record->capacity = INITCAPACITY;
96 record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * record->capacity);
97 record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * record->capacity);
99 record->thread[0] = readThread;
100 record->readClock[0] = readClock;
102 *shadow = (uint64_t) record;
105 /** This function is called when we detect a data race.*/
106 static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address)
108 struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
109 race->oldthread = oldthread;
110 race->oldclock = oldclock;
111 race->isoldwrite = isoldwrite;
112 race->newaction = newaction;
113 race->isnewwrite = isnewwrite;
114 race->address = address;
115 unrealizedraces->push_back(race);
117 /* If the race is realized, bail out now. */
118 if (checkDataRaces())
119 model->switch_to_master(NULL);
123 * @brief Check and report data races
125 * If the trace is feasible (a feasible prefix), clear out the list of
126 * unrealized data races, asserting any realized ones as execution bugs so that
127 * the model-checker will end the execution.
129 * @return True if any data races were realized
131 bool checkDataRaces()
133 if (get_execution()->isfeasibleprefix()) {
134 bool race_asserted = false;
135 /* Prune the non-racing unrealized dataraces */
136 for (unsigned i = 0; i < unrealizedraces->size(); i++) {
137 struct DataRace *race = (*unrealizedraces)[i];
138 if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
140 race_asserted = true;
144 unrealizedraces->clear();
145 return race_asserted;
151 * @brief Assert a data race
153 * Asserts a data race which is currently realized, causing the execution to
154 * end and stashing a message in the model-checker's bug list
156 * @param race The race to report
158 void assert_race(struct DataRace *race)
161 "Data race detected @ address %p:\n"
162 " Access 1: %5s in thread %2d @ clock %3u\n"
163 " Access 2: %5s in thread %2d @ clock %3u",
165 race->isoldwrite ? "write" : "read",
166 id_to_int(race->oldthread),
168 race->isnewwrite ? "write" : "read",
169 id_to_int(race->newaction->get_tid()),
170 race->newaction->get_seq_number()
174 /** This function does race detection for a write on an expanded record. */
175 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock)
177 struct RaceRecord *record = (struct RaceRecord *)(*shadow);
179 /* Check for datarace against last read. */
181 for (int i = 0; i < record->numReads; i++) {
182 modelclock_t readClock = record->readClock[i];
183 thread_id_t readThread = record->thread[i];
185 /* Note that readClock can't actuall be zero here, so it could be
188 if (clock_may_race(currClock, thread, readClock, readThread)) {
189 /* We have a datarace */
190 reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
194 /* Check for datarace against last write. */
196 modelclock_t writeClock = record->writeClock;
197 thread_id_t writeThread = record->writeThread;
199 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
200 /* We have a datarace */
201 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
204 record->numReads = 0;
205 record->writeThread = thread;
206 modelclock_t ourClock = currClock->getClock(thread);
207 record->writeClock = ourClock;
210 /** This function does race detection on a write. */
211 void raceCheckWrite(thread_id_t thread, void *location)
213 uint64_t *shadow = lookupAddressEntry(location);
214 uint64_t shadowval = *shadow;
215 ClockVector *currClock = get_execution()->get_cv(thread);
218 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
219 fullRaceCheckWrite(thread, location, shadow, currClock);
223 int threadid = id_to_int(thread);
224 modelclock_t ourClock = currClock->getClock(thread);
226 /* Thread ID is too large or clock is too large. */
227 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
228 expandRecord(shadow);
229 fullRaceCheckWrite(thread, location, shadow, currClock);
233 /* Check for datarace against last read. */
235 modelclock_t readClock = READVECTOR(shadowval);
236 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
238 if (clock_may_race(currClock, thread, readClock, readThread)) {
239 /* We have a datarace */
240 reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
243 /* Check for datarace against last write. */
245 modelclock_t writeClock = WRITEVECTOR(shadowval);
246 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
248 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
249 /* We have a datarace */
250 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
252 *shadow = ENCODEOP(0, 0, threadid, ourClock);
255 /** This function does race detection on a read for an expanded record. */
256 void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
258 struct RaceRecord *record = (struct RaceRecord *) (*shadow);
260 /* Check for datarace against last write. */
262 modelclock_t writeClock = record->writeClock;
263 thread_id_t writeThread = record->writeThread;
265 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
266 /* We have a datarace */
267 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
270 /* Shorten vector when possible */
274 for (int i = 0; i < record->numReads; i++) {
275 modelclock_t readClock = record->readClock[i];
276 thread_id_t readThread = record->thread[i];
278 /* Note that is not really a datarace check as reads cannott
279 actually race. It is just determining that this read subsumes
280 another in the sense that either this read races or neither
281 read races. Note that readClock can't actually be zero, so it
282 could be optimized. */
284 if (clock_may_race(currClock, thread, readClock, readThread)) {
285 /* Still need this read in vector */
286 if (copytoindex != i) {
287 record->readClock[copytoindex] = record->readClock[i];
288 record->thread[copytoindex] = record->thread[i];
294 if (copytoindex >= record->capacity) {
295 int newCapacity = record->capacity * 2;
296 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
297 modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
298 std::memcpy(newthread, record->thread, record->capacity * sizeof(thread_id_t));
299 std::memcpy(newreadClock, record->readClock, record->capacity * sizeof(modelclock_t));
300 snapshot_free(record->readClock);
301 snapshot_free(record->thread);
302 record->readClock = newreadClock;
303 record->thread = newthread;
304 record->capacity = newCapacity;
307 modelclock_t ourClock = currClock->getClock(thread);
309 record->thread[copytoindex] = thread;
310 record->readClock[copytoindex] = ourClock;
311 record->numReads = copytoindex + 1;
314 /** This function does race detection on a read. */
315 void raceCheckRead(thread_id_t thread, const void *location)
317 uint64_t *shadow = lookupAddressEntry(location);
318 uint64_t shadowval = *shadow;
319 ClockVector *currClock = get_execution()->get_cv(thread);
322 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
323 fullRaceCheckRead(thread, location, shadow, currClock);
327 int threadid = id_to_int(thread);
328 modelclock_t ourClock = currClock->getClock(thread);
330 /* Thread ID is too large or clock is too large. */
331 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
332 expandRecord(shadow);
333 fullRaceCheckRead(thread, location, shadow, currClock);
337 /* Check for datarace against last write. */
339 modelclock_t writeClock = WRITEVECTOR(shadowval);
340 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
342 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
343 /* We have a datarace */
344 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
347 modelclock_t readClock = READVECTOR(shadowval);
348 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
350 if (clock_may_race(currClock, thread, readClock, readThread)) {
351 /* We don't subsume this read... Have to expand record. */
352 expandRecord(shadow);
353 fullRaceCheckRead(thread, location, shadow, currClock);
357 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
360 bool haveUnrealizedRaces()
362 return !unrealizedraces->empty();