8 struct ShadowTable *root;
9 std::vector<struct DataRace *> unrealizedraces;
11 /** This function initialized the data race detector. */
12 void initRaceDetector() {
13 root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1);
16 /** This function looks up the entry in the shadow table corresponding to a
18 static uint64_t * lookupAddressEntry(void * address) {
19 struct ShadowTable *currtable=root;
21 currtable=(struct ShadowTable *) currtable->array[(((uintptr_t)address)>>32)&MASK16BIT];
22 if (currtable==NULL) {
23 currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address)>>32)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowTable), 1));
27 struct ShadowBaseTable * basetable=(struct ShadowBaseTable *) currtable->array[(((uintptr_t)address)>>16)&MASK16BIT];
28 if (basetable==NULL) {
29 basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address)>>16)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowBaseTable), 1));
31 return &basetable->array[((uintptr_t)address)&MASK16BIT];
35 * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
36 * to check the potential for a data race.
37 * @param clock1 The current clock vector
38 * @param tid1 The current thread; paired with clock1
39 * @param clock2 The clock value for the potentially-racing action
40 * @param tid2 The thread ID for the potentially-racing action
41 * @return true if the current clock allows a race with the event at clock2/tid2
43 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
44 modelclock_t clock2, thread_id_t tid2)
46 return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
50 * Expands a record from the compact form to the full form. This is
51 * necessary for multiple readers or for very large thread ids or time
53 static void expandRecord(uint64_t * shadow) {
54 uint64_t shadowval=*shadow;
56 modelclock_t readClock = READVECTOR(shadowval);
57 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
58 modelclock_t writeClock = WRITEVECTOR(shadowval);
59 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
61 struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord));
62 record->writeThread=writeThread;
63 record->writeClock=writeClock;
66 record->capacity=INITCAPACITY;
67 record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t)*record->capacity);
68 record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t)*record->capacity);
70 record->thread[0]=readThread;
71 record->readClock[0]=readClock;
73 *shadow=(uint64_t) record;
76 /** This function is called when we detect a data race.*/
77 static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, void *address) {
78 struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
79 race->oldthread=oldthread;
80 race->oldclock=oldclock;
81 race->isoldwrite=isoldwrite;
82 race->newaction=newaction;
83 race->isnewwrite=isnewwrite;
84 race->address=address;
85 unrealizedraces.push_back(race);
87 /* If the race is realized, bail out now. */
88 if (checkDataRaces()) {
90 model->switch_to_master(NULL);
94 /** This function goes through the list of unrealized data races,
95 * removes the impossible ones, and print the realized ones. */
97 bool checkDataRaces() {
98 if (model->isfeasibleprefix()) {
99 /* Prune the non-racing unrealized dataraces */
100 unsigned int i,newloc=0;
101 for(i=0;i<unrealizedraces.size();i++) {
102 struct DataRace * race=unrealizedraces[i];
103 if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
104 unrealizedraces[newloc++]=race;
108 unrealizedraces.resize(newloc);
110 if (unrealizedraces.size()!=0) {
111 /* We have an actual realized race. */
112 for(i=0;i<unrealizedraces.size();i++) {
113 struct DataRace * race=unrealizedraces[i];
122 void printRace(struct DataRace * race) {
123 printf("Datarace detected\n");
124 printf("Location %p\n", race->address);
125 printf("Initial access: thread %u clock %u, iswrite %u\n",race->oldthread,race->oldclock, race->isoldwrite);
126 printf("Second access: thread %u clock %u, iswrite %u\n", race->newaction->get_tid(), race->newaction->get_seq_number() , race->isnewwrite);
129 /** This function does race detection for a write on an expanded record. */
130 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
131 struct RaceRecord * record=(struct RaceRecord *) (*shadow);
133 /* Check for datarace against last read. */
135 for(int i=0;i<record->numReads;i++) {
136 modelclock_t readClock = record->readClock[i];
137 thread_id_t readThread = record->thread[i];
139 /* Note that readClock can't actuall be zero here, so it could be
142 if (clock_may_race(currClock, thread, readClock, readThread)) {
143 /* We have a datarace */
144 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
148 /* Check for datarace against last write. */
150 modelclock_t writeClock = record->writeClock;
151 thread_id_t writeThread = record->writeThread;
153 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
154 /* We have a datarace */
155 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
159 record->writeThread=thread;
160 modelclock_t ourClock = currClock->getClock(thread);
161 record->writeClock=ourClock;
164 /** This function does race detection on a write. */
165 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock) {
166 uint64_t * shadow=lookupAddressEntry(location);
167 uint64_t shadowval=*shadow;
170 if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
171 fullRaceCheckWrite(thread, location, shadow, currClock);
175 int threadid = id_to_int(thread);
176 modelclock_t ourClock = currClock->getClock(thread);
178 /* Thread ID is too large or clock is too large. */
179 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
180 expandRecord(shadow);
181 fullRaceCheckWrite(thread, location, shadow, currClock);
185 /* Check for datarace against last read. */
187 modelclock_t readClock = READVECTOR(shadowval);
188 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
190 if (clock_may_race(currClock, thread, readClock, readThread)) {
191 /* We have a datarace */
192 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
195 /* Check for datarace against last write. */
197 modelclock_t writeClock = WRITEVECTOR(shadowval);
198 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
200 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
201 /* We have a datarace */
202 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
204 *shadow = ENCODEOP(0, 0, threadid, ourClock);
207 /** This function does race detection on a read for an expanded record. */
208 void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
209 struct RaceRecord * record=(struct RaceRecord *) (*shadow);
211 /* Check for datarace against last write. */
213 modelclock_t writeClock = record->writeClock;
214 thread_id_t writeThread = record->writeThread;
216 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
217 /* We have a datarace */
218 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
221 /* Shorten vector when possible */
225 for(int i=0;i<record->numReads;i++) {
226 modelclock_t readClock = record->readClock[i];
227 thread_id_t readThread = record->thread[i];
229 /* Note that is not really a datarace check as reads cannott
230 actually race. It is just determining that this read subsumes
231 another in the sense that either this read races or neither
232 read races. Note that readClock can't actually be zero, so it
233 could be optimized. */
235 if (clock_may_race(currClock, thread, readClock, readThread)) {
236 /* Still need this read in vector */
237 if (copytoindex!=i) {
238 record->readClock[copytoindex]=record->readClock[i];
239 record->thread[copytoindex]=record->thread[i];
245 if (copytoindex>=record->capacity) {
246 int newCapacity=record->capacity*2;
247 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t)*newCapacity);
248 modelclock_t *newreadClock =( modelclock_t *)snapshot_malloc(sizeof(modelclock_t)*newCapacity);
249 std::memcpy(newthread, record->thread, record->capacity*sizeof(thread_id_t));
250 std::memcpy(newreadClock, record->readClock, record->capacity*sizeof(modelclock_t));
251 snapshot_free(record->readClock);
252 snapshot_free(record->thread);
253 record->readClock=newreadClock;
254 record->thread=newthread;
255 record->capacity=newCapacity;
258 modelclock_t ourClock = currClock->getClock(thread);
260 record->thread[copytoindex]=thread;
261 record->readClock[copytoindex]=ourClock;
262 record->numReads=copytoindex+1;
265 /** This function does race detection on a read. */
266 void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
267 uint64_t * shadow=lookupAddressEntry(location);
268 uint64_t shadowval=*shadow;
271 if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
272 fullRaceCheckRead(thread, location, shadow, currClock);
276 int threadid = id_to_int(thread);
277 modelclock_t ourClock = currClock->getClock(thread);
279 /* Thread ID is too large or clock is too large. */
280 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
281 expandRecord(shadow);
282 fullRaceCheckRead(thread, location, shadow, currClock);
286 /* Check for datarace against last write. */
288 modelclock_t writeClock = WRITEVECTOR(shadowval);
289 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
291 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
292 /* We have a datarace */
293 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
296 modelclock_t readClock = READVECTOR(shadowval);
297 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
299 if (clock_may_race(currClock, thread, readClock, readThread)) {
300 /* We don't subsume this read... Have to expand record. */
301 expandRecord(shadow);
302 fullRaceCheckRead(thread, location, shadow, currClock);
306 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);