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;
31 void * table_calloc(size_t size)
33 if ((((char *)memory_base) + size) > memory_top) {
34 return snapshot_calloc(size, 1);
36 void *tmp = memory_base;
37 memory_base = ((char *)memory_base) + size;
42 /** This function looks up the entry in the shadow table corresponding to a
44 static uint64_t * lookupAddressEntry(const void *address)
46 struct ShadowTable *currtable = root;
48 currtable = (struct ShadowTable *) currtable->array[(((uintptr_t)address) >> 32) & MASK16BIT];
49 if (currtable == NULL) {
50 currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address) >> 32) & MASK16BIT] = table_calloc(sizeof(struct ShadowTable)));
54 struct ShadowBaseTable *basetable = (struct ShadowBaseTable *)currtable->array[(((uintptr_t)address) >> 16) & MASK16BIT];
55 if (basetable == NULL) {
56 basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address) >> 16) & MASK16BIT] = table_calloc(sizeof(struct ShadowBaseTable)));
58 return &basetable->array[((uintptr_t)address) & MASK16BIT];
62 * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
63 * to check the potential for a data race.
64 * @param clock1 The current clock vector
65 * @param tid1 The current thread; paired with clock1
66 * @param clock2 The clock value for the potentially-racing action
67 * @param tid2 The thread ID for the potentially-racing action
68 * @return true if the current clock allows a race with the event at clock2/tid2
70 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
71 modelclock_t clock2, thread_id_t tid2)
73 return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
77 * Expands a record from the compact form to the full form. This is
78 * necessary for multiple readers or for very large thread ids or time
80 static void expandRecord(uint64_t *shadow)
82 uint64_t shadowval = *shadow;
84 modelclock_t readClock = READVECTOR(shadowval);
85 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
86 modelclock_t writeClock = WRITEVECTOR(shadowval);
87 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
89 struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord));
90 record->writeThread = writeThread;
91 record->writeClock = writeClock;
94 record->capacity = INITCAPACITY;
95 record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * record->capacity);
96 record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * record->capacity);
98 record->thread[0] = readThread;
99 record->readClock[0] = readClock;
101 *shadow = (uint64_t) record;
104 /** This function is called when we detect a data race.*/
105 static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address)
107 struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
108 race->oldthread = oldthread;
109 race->oldclock = oldclock;
110 race->isoldwrite = isoldwrite;
111 race->newaction = newaction;
112 race->isnewwrite = isnewwrite;
113 race->address = address;
114 unrealizedraces.push_back(race);
116 /* If the race is realized, bail out now. */
117 if (checkDataRaces())
118 model->switch_to_master(NULL);
122 * @brief Check and report data races
124 * If the trace is feasible (a feasible prefix), clear out the list of
125 * unrealized data races, asserting any realized ones as execution bugs so that
126 * the model-checker will end the execution.
128 * @return True if any data races were realized
130 bool checkDataRaces()
132 if (get_execution()->isfeasibleprefix()) {
133 bool race_asserted = false;
134 /* Prune the non-racing unrealized dataraces */
135 for (unsigned i = 0; i < unrealizedraces.size(); i++) {
136 struct DataRace *race = unrealizedraces[i];
137 if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
139 race_asserted = true;
143 unrealizedraces.clear();
144 return race_asserted;
150 * @brief Assert a data race
152 * Asserts a data race which is currently realized, causing the execution to
153 * end and stashing a message in the model-checker's bug list
155 * @param race The race to report
157 void assert_race(struct DataRace *race)
160 "Data race detected @ address %p:\n"
161 " Access 1: %5s in thread %2d @ clock %3u\n"
162 " Access 2: %5s in thread %2d @ clock %3u",
164 race->isoldwrite ? "write" : "read",
165 id_to_int(race->oldthread),
167 race->isnewwrite ? "write" : "read",
168 id_to_int(race->newaction->get_tid()),
169 race->newaction->get_seq_number()
173 /** This function does race detection for a write on an expanded record. */
174 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock)
176 struct RaceRecord *record = (struct RaceRecord *)(*shadow);
178 /* Check for datarace against last read. */
180 for (int i = 0; i < record->numReads; i++) {
181 modelclock_t readClock = record->readClock[i];
182 thread_id_t readThread = record->thread[i];
184 /* Note that readClock can't actuall be zero here, so it could be
187 if (clock_may_race(currClock, thread, readClock, readThread)) {
188 /* We have a datarace */
189 reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
193 /* Check for datarace against last write. */
195 modelclock_t writeClock = record->writeClock;
196 thread_id_t writeThread = record->writeThread;
198 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
199 /* We have a datarace */
200 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
203 record->numReads = 0;
204 record->writeThread = thread;
205 modelclock_t ourClock = currClock->getClock(thread);
206 record->writeClock = ourClock;
209 /** This function does race detection on a write. */
210 void raceCheckWrite(thread_id_t thread, void *location)
212 uint64_t *shadow = lookupAddressEntry(location);
213 uint64_t shadowval = *shadow;
214 ClockVector *currClock = get_execution()->get_cv(thread);
217 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
218 fullRaceCheckWrite(thread, location, shadow, currClock);
222 int threadid = id_to_int(thread);
223 modelclock_t ourClock = currClock->getClock(thread);
225 /* Thread ID is too large or clock is too large. */
226 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
227 expandRecord(shadow);
228 fullRaceCheckWrite(thread, location, shadow, currClock);
232 /* Check for datarace against last read. */
234 modelclock_t readClock = READVECTOR(shadowval);
235 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
237 if (clock_may_race(currClock, thread, readClock, readThread)) {
238 /* We have a datarace */
239 reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
242 /* Check for datarace against last write. */
244 modelclock_t writeClock = WRITEVECTOR(shadowval);
245 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
247 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
248 /* We have a datarace */
249 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
251 *shadow = ENCODEOP(0, 0, threadid, ourClock);
254 /** This function does race detection on a read for an expanded record. */
255 void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
257 struct RaceRecord *record = (struct RaceRecord *) (*shadow);
259 /* Check for datarace against last write. */
261 modelclock_t writeClock = record->writeClock;
262 thread_id_t writeThread = record->writeThread;
264 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
265 /* We have a datarace */
266 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
269 /* Shorten vector when possible */
273 for (int i = 0; i < record->numReads; i++) {
274 modelclock_t readClock = record->readClock[i];
275 thread_id_t readThread = record->thread[i];
277 /* Note that is not really a datarace check as reads cannott
278 actually race. It is just determining that this read subsumes
279 another in the sense that either this read races or neither
280 read races. Note that readClock can't actually be zero, so it
281 could be optimized. */
283 if (clock_may_race(currClock, thread, readClock, readThread)) {
284 /* Still need this read in vector */
285 if (copytoindex != i) {
286 record->readClock[copytoindex] = record->readClock[i];
287 record->thread[copytoindex] = record->thread[i];
293 if (copytoindex >= record->capacity) {
294 int newCapacity = record->capacity * 2;
295 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
296 modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
297 std::memcpy(newthread, record->thread, record->capacity * sizeof(thread_id_t));
298 std::memcpy(newreadClock, record->readClock, record->capacity * sizeof(modelclock_t));
299 snapshot_free(record->readClock);
300 snapshot_free(record->thread);
301 record->readClock = newreadClock;
302 record->thread = newthread;
303 record->capacity = newCapacity;
306 modelclock_t ourClock = currClock->getClock(thread);
308 record->thread[copytoindex] = thread;
309 record->readClock[copytoindex] = ourClock;
310 record->numReads = copytoindex + 1;
313 /** This function does race detection on a read. */
314 void raceCheckRead(thread_id_t thread, const void *location)
316 uint64_t *shadow = lookupAddressEntry(location);
317 uint64_t shadowval = *shadow;
318 ClockVector *currClock = get_execution()->get_cv(thread);
321 if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
322 fullRaceCheckRead(thread, location, shadow, currClock);
326 int threadid = id_to_int(thread);
327 modelclock_t ourClock = currClock->getClock(thread);
329 /* Thread ID is too large or clock is too large. */
330 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
331 expandRecord(shadow);
332 fullRaceCheckRead(thread, location, shadow, currClock);
336 /* Check for datarace against last write. */
338 modelclock_t writeClock = WRITEVECTOR(shadowval);
339 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
341 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
342 /* We have a datarace */
343 reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
346 modelclock_t readClock = READVECTOR(shadowval);
347 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
349 if (clock_may_race(currClock, thread, readClock, readThread)) {
350 /* We don't subsume this read... Have to expand record. */
351 expandRecord(shadow);
352 fullRaceCheckRead(thread, location, shadow, currClock);
356 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
359 bool haveUnrealizedRaces()
361 return !unrealizedraces.empty();