7 struct ShadowTable *root;
8 std::vector<struct DataRace *> unrealizedraces;
10 /** This function initialized the data race detector. */
11 void initRaceDetector() {
12 root=(struct ShadowTable *) calloc(sizeof(struct ShadowTable),1);
15 /** This function looks up the entry in the shadow table corresponding to a
17 static uint64_t * lookupAddressEntry(void * address) {
18 struct ShadowTable *currtable=root;
20 currtable=(struct ShadowTable *) currtable->array[(((uintptr_t)address)>>32)&MASK16BIT];
21 if (currtable==NULL) {
22 currtable=(struct ShadowTable *) (root->array[(((uintptr_t)address)>>32)&MASK16BIT]=calloc(sizeof(struct ShadowTable),1));
26 struct ShadowBaseTable * basetable=(struct ShadowBaseTable *) currtable->array[(((uintptr_t)address)>>16)&MASK16BIT];
27 if (basetable==NULL) {
28 basetable=(struct ShadowBaseTable *) (currtable->array[(((uintptr_t)address)>>16)&MASK16BIT]=calloc(sizeof(struct ShadowBaseTable),1));
30 return &basetable->array[((uintptr_t)address)&MASK16BIT];
34 * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
35 * to check the potential for a data race.
36 * @param clock1 The current clock vector
37 * @param tid1 The current thread; paired with clock1
38 * @param clock2 The clock value for the potentially-racing action
39 * @param tid2 The thread ID for the potentially-racing action
40 * @return true if the current clock allows a race with the event at clock2/tid2
42 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
43 modelclock_t clock2, thread_id_t tid2)
45 return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
49 * Expands a record from the compact form to the full form. This is
50 * necessary for multiple readers or for very large thread ids or time
52 static void expandRecord(uint64_t * shadow) {
53 uint64_t shadowval=*shadow;
55 modelclock_t readClock = READVECTOR(shadowval);
56 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
57 modelclock_t writeClock = WRITEVECTOR(shadowval);
58 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
60 struct RaceRecord * record=(struct RaceRecord *)calloc(1,sizeof(struct RaceRecord));
61 record->writeThread=writeThread;
62 record->writeClock=writeClock;
65 record->capacity=INITCAPACITY;
66 record->thread=(thread_id_t *) malloc(sizeof(thread_id_t)*record->capacity);
67 record->readClock=(modelclock_t *) malloc(sizeof(modelclock_t)*record->capacity);
69 record->thread[0]=readThread;
70 record->readClock[0]=readClock;
72 *shadow=(uint64_t) record;
75 /** This function is called when we detect a data race.*/
76 static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, void *address) {
77 struct DataRace * race=(struct DataRace *)malloc(sizeof(struct DataRace));
78 race->oldthread=oldthread;
79 race->oldclock=oldclock;
80 race->isoldwrite=isoldwrite;
81 race->newaction=newaction;
82 race->isnewwrite=isnewwrite;
83 race->address=address;
84 unrealizedraces.push_back(race);
86 /* If the race is realized, bail out now. */
87 if (checkDataRaces()) {
88 model->assert_thread();
92 /** This function goes through the list of unrealized data races,
93 * removes the impossible ones, and print the realized ones. */
95 bool checkDataRaces() {
96 if (model->isfeasibleprefix()) {
97 /* Prune the non-racing unrealized dataraces */
98 unsigned int i,newloc=0;
99 for(i=0;i<unrealizedraces.size();i++) {
100 struct DataRace * race=unrealizedraces[i];
101 if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
102 unrealizedraces[newloc++]=race;
106 unrealizedraces.resize(newloc);
108 if (unrealizedraces.size()!=0) {
109 /* We have an actual realized race. */
110 for(i=0;i<unrealizedraces.size();i++) {
111 struct DataRace * race=unrealizedraces[i];
120 void printRace(struct DataRace * race) {
121 printf("Datarace detected\n");
122 printf("Location %p\n", race->address);
123 printf("Initial access: thread %u clock %u, iswrite %u\n",race->oldthread,race->oldclock, race->isoldwrite);
124 printf("Second access: thread %u, iswrite %u\n", race->newaction->get_tid(), race->isnewwrite);
127 /** This function does race detection for a write on an expanded record. */
128 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
129 struct RaceRecord * record=(struct RaceRecord *) (*shadow);
131 /* Check for datarace against last read. */
133 for(int i=0;i<record->numReads;i++) {
134 modelclock_t readClock = record->readClock[i];
135 thread_id_t readThread = record->thread[i];
137 /* Note that readClock can't actuall be zero here, so it could be
140 if (clock_may_race(currClock, thread, readClock, readThread)) {
141 /* We have a datarace */
142 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
146 /* Check for datarace against last write. */
148 modelclock_t writeClock = record->writeClock;
149 thread_id_t writeThread = record->writeThread;
151 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
152 /* We have a datarace */
153 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
157 record->writeThread=thread;
158 modelclock_t ourClock = currClock->getClock(thread);
159 record->writeClock=ourClock;
162 /** This function does race detection on a write. */
163 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock) {
164 uint64_t * shadow=lookupAddressEntry(location);
165 uint64_t shadowval=*shadow;
168 if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
169 fullRaceCheckWrite(thread, location, shadow, currClock);
173 int threadid = id_to_int(thread);
174 modelclock_t ourClock = currClock->getClock(thread);
176 /* Thread ID is too large or clock is too large. */
177 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
178 expandRecord(shadow);
179 fullRaceCheckWrite(thread, location, shadow, currClock);
183 /* Check for datarace against last read. */
185 modelclock_t readClock = READVECTOR(shadowval);
186 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
188 if (clock_may_race(currClock, thread, readClock, readThread)) {
189 /* We have a datarace */
190 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
193 /* Check for datarace against last write. */
195 modelclock_t writeClock = WRITEVECTOR(shadowval);
196 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
198 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
199 /* We have a datarace */
200 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
202 *shadow = ENCODEOP(0, 0, threadid, ourClock);
205 /** This function does race detection on a read for an expanded record. */
206 void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
207 struct RaceRecord * record=(struct RaceRecord *) (*shadow);
209 /* Check for datarace against last write. */
211 modelclock_t writeClock = record->writeClock;
212 thread_id_t writeThread = record->writeThread;
214 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
215 /* We have a datarace */
216 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
219 /* Shorten vector when possible */
223 for(int i=0;i<record->numReads;i++) {
224 modelclock_t readClock = record->readClock[i];
225 thread_id_t readThread = record->thread[i];
227 /* Note that is not really a datarace check as reads cannott
228 actually race. It is just determining that this read subsumes
229 another in the sense that either this read races or neither
230 read races. Note that readClock can't actually be zero, so it
231 could be optimized. */
233 if (clock_may_race(currClock, thread, readClock, readThread)) {
234 /* Still need this read in vector */
235 if (copytoindex!=i) {
236 record->readClock[copytoindex]=record->readClock[i];
237 record->thread[copytoindex]=record->thread[i];
243 if (copytoindex>=record->capacity) {
244 int newCapacity=record->capacity*2;
245 thread_id_t *newthread=(thread_id_t *) malloc(sizeof(thread_id_t)*newCapacity);
246 modelclock_t * newreadClock=(modelclock_t *) malloc(sizeof(modelclock_t)*newCapacity);
247 std::memcpy(newthread, record->thread, record->capacity*sizeof(thread_id_t));
248 std::memcpy(newreadClock, record->readClock, record->capacity*sizeof(modelclock_t));
249 free(record->readClock);
250 free(record->thread);
251 record->readClock=newreadClock;
252 record->thread=newthread;
253 record->capacity=newCapacity;
256 modelclock_t ourClock = currClock->getClock(thread);
258 record->thread[copytoindex]=thread;
259 record->readClock[copytoindex]=ourClock;
260 record->numReads=copytoindex+1;
263 /** This function does race detection on a read. */
264 void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
265 uint64_t * shadow=lookupAddressEntry(location);
266 uint64_t shadowval=*shadow;
269 if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
270 fullRaceCheckRead(thread, location, shadow, currClock);
274 int threadid = id_to_int(thread);
275 modelclock_t ourClock = currClock->getClock(thread);
277 /* Thread ID is too large or clock is too large. */
278 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
279 expandRecord(shadow);
280 fullRaceCheckRead(thread, location, shadow, currClock);
284 /* Check for datarace against last write. */
286 modelclock_t writeClock = WRITEVECTOR(shadowval);
287 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
289 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
290 /* We have a datarace */
291 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
294 modelclock_t readClock = READVECTOR(shadowval);
295 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
297 if (clock_may_race(currClock, thread, readClock, readThread)) {
298 /* We don't subsume this read... Have to expand record. */
299 expandRecord(shadow);
300 fullRaceCheckRead(thread, location, shadow, currClock);
304 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);