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() {
18 root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1);
19 memory_base = snapshot_calloc(sizeof(struct ShadowBaseTable)*SHADOWBASETABLES, 1);
20 memory_top = ((char *)memory_base) + sizeof(struct ShadowBaseTable)*SHADOWBASETABLES;
23 void * table_calloc(size_t size) {
24 if ((((char *)memory_base)+size)>memory_top) {
25 return snapshot_calloc(size, 1);
27 void *tmp=memory_base;
28 memory_base=((char *)memory_base)+size;
33 /** This function looks up the entry in the shadow table corresponding to a
35 static uint64_t * lookupAddressEntry(const void * address) {
36 struct ShadowTable *currtable=root;
38 currtable=(struct ShadowTable *) currtable->array[(((uintptr_t)address)>>32)&MASK16BIT];
39 if (currtable==NULL) {
40 currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address)>>32)&MASK16BIT] = table_calloc(sizeof(struct ShadowTable)));
44 struct ShadowBaseTable * basetable=(struct ShadowBaseTable *) currtable->array[(((uintptr_t)address)>>16)&MASK16BIT];
45 if (basetable==NULL) {
46 basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address)>>16)&MASK16BIT] = table_calloc(sizeof(struct ShadowBaseTable)));
48 return &basetable->array[((uintptr_t)address)&MASK16BIT];
52 * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
53 * to check the potential for a data race.
54 * @param clock1 The current clock vector
55 * @param tid1 The current thread; paired with clock1
56 * @param clock2 The clock value for the potentially-racing action
57 * @param tid2 The thread ID for the potentially-racing action
58 * @return true if the current clock allows a race with the event at clock2/tid2
60 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
61 modelclock_t clock2, thread_id_t tid2)
63 return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
67 * Expands a record from the compact form to the full form. This is
68 * necessary for multiple readers or for very large thread ids or time
70 static void expandRecord(uint64_t * shadow) {
71 uint64_t shadowval=*shadow;
73 modelclock_t readClock = READVECTOR(shadowval);
74 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
75 modelclock_t writeClock = WRITEVECTOR(shadowval);
76 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
78 struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord));
79 record->writeThread=writeThread;
80 record->writeClock=writeClock;
83 record->capacity=INITCAPACITY;
84 record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t)*record->capacity);
85 record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t)*record->capacity);
87 record->thread[0]=readThread;
88 record->readClock[0]=readClock;
90 *shadow=(uint64_t) record;
93 /** This function is called when we detect a data race.*/
94 static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address) {
95 struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
96 race->oldthread=oldthread;
97 race->oldclock=oldclock;
98 race->isoldwrite=isoldwrite;
99 race->newaction=newaction;
100 race->isnewwrite=isnewwrite;
101 race->address=address;
102 unrealizedraces.push_back(race);
104 /* If the race is realized, bail out now. */
105 if (checkDataRaces())
106 model->switch_to_master(NULL);
110 * @brief Check and report data races
112 * If the trace is feasible (a feasible prefix), clear out the list of
113 * unrealized data races, asserting any realized ones as execution bugs so that
114 * the model-checker will end the execution.
116 * @return True if any data races were realized
118 bool checkDataRaces() {
119 if (model->isfeasibleprefix()) {
120 bool race_asserted = false;
121 /* Prune the non-racing unrealized dataraces */
122 for (unsigned i = 0; i < unrealizedraces.size(); i++) {
123 struct DataRace *race = unrealizedraces[i];
124 if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
126 race_asserted = true;
130 unrealizedraces.clear();
131 return race_asserted;
137 * @brief Assert a data race
139 * Asserts a data race which is currently realized, causing the execution to
140 * end and stashing a message in the model-checker's bug list
142 * @param race The race to report
144 void assert_race(struct DataRace *race)
148 ptr += sprintf(ptr, "Data race detected @ address %p:\n", race->address);
149 ptr += sprintf(ptr, " Access 1: %5s in thread %2d @ clock %3u\n",
150 race->isoldwrite ? "write" : "read",
151 id_to_int(race->oldthread), race->oldclock);
152 ptr += sprintf(ptr, " Access 2: %5s in thread %2d @ clock %3u",
153 race->isnewwrite ? "write" : "read",
154 id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
155 model->assert_bug(buf);
158 /** This function does race detection for a write on an expanded record. */
159 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
160 struct RaceRecord * record=(struct RaceRecord *) (*shadow);
162 /* Check for datarace against last read. */
164 for(int i=0;i<record->numReads;i++) {
165 modelclock_t readClock = record->readClock[i];
166 thread_id_t readThread = record->thread[i];
168 /* Note that readClock can't actuall be zero here, so it could be
171 if (clock_may_race(currClock, thread, readClock, readThread)) {
172 /* We have a datarace */
173 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
177 /* Check for datarace against last write. */
179 modelclock_t writeClock = record->writeClock;
180 thread_id_t writeThread = record->writeThread;
182 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
183 /* We have a datarace */
184 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
188 record->writeThread=thread;
189 modelclock_t ourClock = currClock->getClock(thread);
190 record->writeClock=ourClock;
193 /** This function does race detection on a write. */
194 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock) {
195 uint64_t * shadow=lookupAddressEntry(location);
196 uint64_t shadowval=*shadow;
199 if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
200 fullRaceCheckWrite(thread, location, shadow, currClock);
204 int threadid = id_to_int(thread);
205 modelclock_t ourClock = currClock->getClock(thread);
207 /* Thread ID is too large or clock is too large. */
208 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
209 expandRecord(shadow);
210 fullRaceCheckWrite(thread, location, shadow, currClock);
214 /* Check for datarace against last read. */
216 modelclock_t readClock = READVECTOR(shadowval);
217 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
219 if (clock_may_race(currClock, thread, readClock, readThread)) {
220 /* We have a datarace */
221 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
224 /* Check for datarace against last write. */
226 modelclock_t writeClock = WRITEVECTOR(shadowval);
227 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
229 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
230 /* We have a datarace */
231 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
233 *shadow = ENCODEOP(0, 0, threadid, ourClock);
236 /** This function does race detection on a read for an expanded record. */
237 void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t * shadow, ClockVector *currClock) {
238 struct RaceRecord * record=(struct RaceRecord *) (*shadow);
240 /* Check for datarace against last write. */
242 modelclock_t writeClock = record->writeClock;
243 thread_id_t writeThread = record->writeThread;
245 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
246 /* We have a datarace */
247 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
250 /* Shorten vector when possible */
254 for(int i=0;i<record->numReads;i++) {
255 modelclock_t readClock = record->readClock[i];
256 thread_id_t readThread = record->thread[i];
258 /* Note that is not really a datarace check as reads cannott
259 actually race. It is just determining that this read subsumes
260 another in the sense that either this read races or neither
261 read races. Note that readClock can't actually be zero, so it
262 could be optimized. */
264 if (clock_may_race(currClock, thread, readClock, readThread)) {
265 /* Still need this read in vector */
266 if (copytoindex!=i) {
267 record->readClock[copytoindex]=record->readClock[i];
268 record->thread[copytoindex]=record->thread[i];
274 if (copytoindex>=record->capacity) {
275 int newCapacity=record->capacity*2;
276 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t)*newCapacity);
277 modelclock_t *newreadClock =( modelclock_t *)snapshot_malloc(sizeof(modelclock_t)*newCapacity);
278 std::memcpy(newthread, record->thread, record->capacity*sizeof(thread_id_t));
279 std::memcpy(newreadClock, record->readClock, record->capacity*sizeof(modelclock_t));
280 snapshot_free(record->readClock);
281 snapshot_free(record->thread);
282 record->readClock=newreadClock;
283 record->thread=newthread;
284 record->capacity=newCapacity;
287 modelclock_t ourClock = currClock->getClock(thread);
289 record->thread[copytoindex]=thread;
290 record->readClock[copytoindex]=ourClock;
291 record->numReads=copytoindex+1;
294 /** This function does race detection on a read. */
295 void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock) {
296 uint64_t * shadow=lookupAddressEntry(location);
297 uint64_t shadowval=*shadow;
300 if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
301 fullRaceCheckRead(thread, location, shadow, currClock);
305 int threadid = id_to_int(thread);
306 modelclock_t ourClock = currClock->getClock(thread);
308 /* Thread ID is too large or clock is too large. */
309 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
310 expandRecord(shadow);
311 fullRaceCheckRead(thread, location, shadow, currClock);
315 /* Check for datarace against last write. */
317 modelclock_t writeClock = WRITEVECTOR(shadowval);
318 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
320 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
321 /* We have a datarace */
322 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
325 modelclock_t readClock = READVECTOR(shadowval);
326 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
328 if (clock_may_race(currClock, thread, readClock, readThread)) {
329 /* We don't subsume this read... Have to expand record. */
330 expandRecord(shadow);
331 fullRaceCheckRead(thread, location, shadow, currClock);
335 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);