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 ASSERT(readThread >= 0);
100 record->thread[0] = readThread;
101 record->readClock[0] = readClock;
103 *shadow = (uint64_t) record;
106 /** This function is called when we detect a data race.*/
107 static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address)
109 struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
110 race->oldthread = oldthread;
111 race->oldclock = oldclock;
112 race->isoldwrite = isoldwrite;
113 race->newaction = newaction;
114 race->isnewwrite = isnewwrite;
115 race->address = address;
116 unrealizedraces->push_back(race);
118 /* If the race is realized, bail out now. */
119 if (checkDataRaces())
120 model->switch_to_master(NULL);
124 * @brief Check and report data races
126 * If the trace is feasible (a feasible prefix), clear out the list of
127 * unrealized data races, asserting any realized ones as execution bugs so that
128 * the model-checker will end the execution.
130 * @return True if any data races were realized
132 bool checkDataRaces()
134 if (get_execution()->isfeasibleprefix()) {
135 bool race_asserted = false;
136 /* Prune the non-racing unrealized dataraces */
137 for (unsigned i = 0;i < unrealizedraces->size();i++) {
138 struct DataRace *race = (*unrealizedraces)[i];
139 if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
141 race_asserted = true;
145 unrealizedraces->clear();
146 return race_asserted;
152 * @brief Assert a data race
154 * Asserts a data race which is currently realized, causing the execution to
155 * end and stashing a message in the model-checker's bug list
157 * @param race The race to report
159 void assert_race(struct DataRace *race)
162 "Data race detected @ address %p:\n"
163 " Access 1: %5s in thread %2d @ clock %3u\n"
164 " Access 2: %5s in thread %2d @ clock %3u",
166 race->isoldwrite ? "write" : "read",
167 id_to_int(race->oldthread),
169 race->isnewwrite ? "write" : "read",
170 id_to_int(race->newaction->get_tid()),
171 race->newaction->get_seq_number()
175 /** This function does race detection for a write on an expanded record. */
176 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock)
178 struct RaceRecord *record = (struct RaceRecord *)(*shadow);
180 /* Check for datarace against last read. */
182 for (int i = 0;i < record->numReads;i++) {
183 modelclock_t readClock = record->readClock[i];
184 thread_id_t readThread = record->thread[i];
186 /* Note that readClock can't actuall be zero here, so it could be
189 if (clock_may_race(currClock, thread, readClock, readThread)) {
190 /* We have a datarace */
191 reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
195 /* Check for datarace against last write. */
197 modelclock_t writeClock = record->writeClock;
198 thread_id_t writeThread = record->writeThread;
200 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
201 /* We have a datarace */
202 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
205 record->numReads = 0;
206 record->writeThread = thread;
207 modelclock_t ourClock = currClock->getClock(thread);
208 record->writeClock = ourClock;
211 /** This function does race detection on a write. */
212 void raceCheckWrite(thread_id_t thread, void *location)
214 uint64_t *shadow = lookupAddressEntry(location);
215 uint64_t shadowval = *shadow;
216 ClockVector *currClock = get_execution()->get_cv(thread);
219 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
220 fullRaceCheckWrite(thread, location, shadow, currClock);
224 int threadid = id_to_int(thread);
225 modelclock_t ourClock = currClock->getClock(thread);
227 /* Thread ID is too large or clock is too large. */
228 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
229 expandRecord(shadow);
230 fullRaceCheckWrite(thread, location, shadow, currClock);
234 /* Check for datarace against last read. */
236 modelclock_t readClock = READVECTOR(shadowval);
237 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
239 if (clock_may_race(currClock, thread, readClock, readThread)) {
240 /* We have a datarace */
241 reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
244 /* Check for datarace against last write. */
246 modelclock_t writeClock = WRITEVECTOR(shadowval);
247 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
249 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
250 /* We have a datarace */
251 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
253 *shadow = ENCODEOP(0, 0, threadid, ourClock);
256 /** This function does race detection on a read for an expanded record. */
257 void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
259 struct RaceRecord *record = (struct RaceRecord *) (*shadow);
261 /* Check for datarace against last write. */
263 modelclock_t writeClock = record->writeClock;
264 thread_id_t writeThread = record->writeThread;
266 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
267 /* We have a datarace */
268 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
271 /* Shorten vector when possible */
275 for (int i = 0;i < record->numReads;i++) {
276 modelclock_t readClock = record->readClock[i];
277 thread_id_t readThread = record->thread[i];
279 /* Note that is not really a datarace check as reads cannott
280 actually race. It is just determining that this read subsumes
281 another in the sense that either this read races or neither
282 read races. Note that readClock can't actually be zero, so it
283 could be optimized. */
285 if (clock_may_race(currClock, thread, readClock, readThread)) {
286 /* Still need this read in vector */
287 if (copytoindex != i) {
288 ASSERT(record->thread[i] >= 0);
289 record->readClock[copytoindex] = record->readClock[i];
290 record->thread[copytoindex] = record->thread[i];
296 if (copytoindex >= record->capacity) {
297 int newCapacity = record->capacity * 2;
298 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
299 modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
300 std::memcpy(newthread, record->thread, record->capacity * sizeof(thread_id_t));
301 std::memcpy(newreadClock, record->readClock, record->capacity * sizeof(modelclock_t));
302 snapshot_free(record->readClock);
303 snapshot_free(record->thread);
304 record->readClock = newreadClock;
305 record->thread = newthread;
306 record->capacity = newCapacity;
309 modelclock_t ourClock = currClock->getClock(thread);
312 record->thread[copytoindex] = thread;
313 record->readClock[copytoindex] = ourClock;
314 record->numReads = copytoindex + 1;
317 /** This function does race detection on a read. */
318 void raceCheckRead(thread_id_t thread, const void *location)
320 uint64_t *shadow = lookupAddressEntry(location);
321 uint64_t shadowval = *shadow;
322 ClockVector *currClock = get_execution()->get_cv(thread);
325 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
326 fullRaceCheckRead(thread, location, shadow, currClock);
330 int threadid = id_to_int(thread);
331 modelclock_t ourClock = currClock->getClock(thread);
333 /* Thread ID is too large or clock is too large. */
334 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
335 expandRecord(shadow);
336 fullRaceCheckRead(thread, location, shadow, currClock);
340 /* Check for datarace against last write. */
342 modelclock_t writeClock = WRITEVECTOR(shadowval);
343 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
345 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
346 /* We have a datarace */
347 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
350 modelclock_t readClock = READVECTOR(shadowval);
351 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
353 if (clock_may_race(currClock, thread, readClock, readThread)) {
354 /* We don't subsume this read... Have to expand record. */
355 expandRecord(shadow);
356 fullRaceCheckRead(thread, location, shadow, currClock);
360 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
363 bool haveUnrealizedRaces()
365 return !unrealizedraces->empty();