3 #include "threads-model.h"
7 #include "clockvector.h"
9 struct ShadowTable *root;
10 std::vector<struct DataRace *> unrealizedraces;
12 /** This function initialized the data race detector. */
13 void initRaceDetector() {
14 root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1);
17 /** This function looks up the entry in the shadow table corresponding to a
19 static uint64_t * lookupAddressEntry(void * address) {
20 struct ShadowTable *currtable=root;
22 currtable=(struct ShadowTable *) currtable->array[(((uintptr_t)address)>>32)&MASK16BIT];
23 if (currtable==NULL) {
24 currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address)>>32)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowTable), 1));
28 struct ShadowBaseTable * basetable=(struct ShadowBaseTable *) currtable->array[(((uintptr_t)address)>>16)&MASK16BIT];
29 if (basetable==NULL) {
30 basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address)>>16)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowBaseTable), 1));
32 return &basetable->array[((uintptr_t)address)&MASK16BIT];
36 * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
37 * to check the potential for a data race.
38 * @param clock1 The current clock vector
39 * @param tid1 The current thread; paired with clock1
40 * @param clock2 The clock value for the potentially-racing action
41 * @param tid2 The thread ID for the potentially-racing action
42 * @return true if the current clock allows a race with the event at clock2/tid2
44 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
45 modelclock_t clock2, thread_id_t tid2)
47 return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
51 * Expands a record from the compact form to the full form. This is
52 * necessary for multiple readers or for very large thread ids or time
54 static void expandRecord(uint64_t * shadow) {
55 uint64_t shadowval=*shadow;
57 modelclock_t readClock = READVECTOR(shadowval);
58 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
59 modelclock_t writeClock = WRITEVECTOR(shadowval);
60 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
62 struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord));
63 record->writeThread=writeThread;
64 record->writeClock=writeClock;
67 record->capacity=INITCAPACITY;
68 record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t)*record->capacity);
69 record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t)*record->capacity);
71 record->thread[0]=readThread;
72 record->readClock[0]=readClock;
74 *shadow=(uint64_t) record;
77 /** This function is called when we detect a data race.*/
78 static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, void *address) {
79 struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
80 race->oldthread=oldthread;
81 race->oldclock=oldclock;
82 race->isoldwrite=isoldwrite;
83 race->newaction=newaction;
84 race->isnewwrite=isnewwrite;
85 race->address=address;
86 unrealizedraces.push_back(race);
88 /* If the race is realized, bail out now. */
89 if (checkDataRaces()) {
91 model->switch_to_master(NULL);
95 /** This function goes through the list of unrealized data races,
96 * removes the impossible ones, and print the realized ones. */
98 bool checkDataRaces() {
99 if (model->isfeasibleprefix()) {
100 /* Prune the non-racing unrealized dataraces */
101 unsigned int i,newloc=0;
102 for(i=0;i<unrealizedraces.size();i++) {
103 struct DataRace * race=unrealizedraces[i];
104 if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
105 unrealizedraces[newloc++]=race;
109 unrealizedraces.resize(newloc);
111 if (unrealizedraces.size()!=0) {
112 /* We have an actual realized race. */
113 for(i=0;i<unrealizedraces.size();i++) {
114 struct DataRace * race=unrealizedraces[i];
123 void printRace(struct DataRace *race)
125 printf("Datarace detected @ address %p:\n", race->address);
126 printf(" Access 1: %5s in thread %2d @ clock %3u\n",
127 race->isoldwrite ? "write" : "read",
128 id_to_int(race->oldthread), race->oldclock);
129 printf(" Access 2: %5s in thread %2d @ clock %3u\n",
130 race->isnewwrite ? "write" : "read",
131 id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
134 /** This function does race detection for a write on an expanded record. */
135 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
136 struct RaceRecord * record=(struct RaceRecord *) (*shadow);
138 /* Check for datarace against last read. */
140 for(int i=0;i<record->numReads;i++) {
141 modelclock_t readClock = record->readClock[i];
142 thread_id_t readThread = record->thread[i];
144 /* Note that readClock can't actuall be zero here, so it could be
147 if (clock_may_race(currClock, thread, readClock, readThread)) {
148 /* We have a datarace */
149 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
153 /* Check for datarace against last write. */
155 modelclock_t writeClock = record->writeClock;
156 thread_id_t writeThread = record->writeThread;
158 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
159 /* We have a datarace */
160 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
164 record->writeThread=thread;
165 modelclock_t ourClock = currClock->getClock(thread);
166 record->writeClock=ourClock;
169 /** This function does race detection on a write. */
170 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock) {
171 uint64_t * shadow=lookupAddressEntry(location);
172 uint64_t shadowval=*shadow;
175 if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
176 fullRaceCheckWrite(thread, location, shadow, currClock);
180 int threadid = id_to_int(thread);
181 modelclock_t ourClock = currClock->getClock(thread);
183 /* Thread ID is too large or clock is too large. */
184 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
185 expandRecord(shadow);
186 fullRaceCheckWrite(thread, location, shadow, currClock);
190 /* Check for datarace against last read. */
192 modelclock_t readClock = READVECTOR(shadowval);
193 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
195 if (clock_may_race(currClock, thread, readClock, readThread)) {
196 /* We have a datarace */
197 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
200 /* Check for datarace against last write. */
202 modelclock_t writeClock = WRITEVECTOR(shadowval);
203 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
205 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
206 /* We have a datarace */
207 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
209 *shadow = ENCODEOP(0, 0, threadid, ourClock);
212 /** This function does race detection on a read for an expanded record. */
213 void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
214 struct RaceRecord * record=(struct RaceRecord *) (*shadow);
216 /* Check for datarace against last write. */
218 modelclock_t writeClock = record->writeClock;
219 thread_id_t writeThread = record->writeThread;
221 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
222 /* We have a datarace */
223 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
226 /* Shorten vector when possible */
230 for(int i=0;i<record->numReads;i++) {
231 modelclock_t readClock = record->readClock[i];
232 thread_id_t readThread = record->thread[i];
234 /* Note that is not really a datarace check as reads cannott
235 actually race. It is just determining that this read subsumes
236 another in the sense that either this read races or neither
237 read races. Note that readClock can't actually be zero, so it
238 could be optimized. */
240 if (clock_may_race(currClock, thread, readClock, readThread)) {
241 /* Still need this read in vector */
242 if (copytoindex!=i) {
243 record->readClock[copytoindex]=record->readClock[i];
244 record->thread[copytoindex]=record->thread[i];
250 if (copytoindex>=record->capacity) {
251 int newCapacity=record->capacity*2;
252 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t)*newCapacity);
253 modelclock_t *newreadClock =( modelclock_t *)snapshot_malloc(sizeof(modelclock_t)*newCapacity);
254 std::memcpy(newthread, record->thread, record->capacity*sizeof(thread_id_t));
255 std::memcpy(newreadClock, record->readClock, record->capacity*sizeof(modelclock_t));
256 snapshot_free(record->readClock);
257 snapshot_free(record->thread);
258 record->readClock=newreadClock;
259 record->thread=newthread;
260 record->capacity=newCapacity;
263 modelclock_t ourClock = currClock->getClock(thread);
265 record->thread[copytoindex]=thread;
266 record->readClock[copytoindex]=ourClock;
267 record->numReads=copytoindex+1;
270 /** This function does race detection on a read. */
271 void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
272 uint64_t * shadow=lookupAddressEntry(location);
273 uint64_t shadowval=*shadow;
276 if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
277 fullRaceCheckRead(thread, location, shadow, currClock);
281 int threadid = id_to_int(thread);
282 modelclock_t ourClock = currClock->getClock(thread);
284 /* Thread ID is too large or clock is too large. */
285 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
286 expandRecord(shadow);
287 fullRaceCheckRead(thread, location, shadow, currClock);
291 /* Check for datarace against last write. */
293 modelclock_t writeClock = WRITEVECTOR(shadowval);
294 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
296 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
297 /* We have a datarace */
298 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
301 modelclock_t readClock = READVECTOR(shadowval);
302 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
304 if (clock_may_race(currClock, thread, readClock, readThread)) {
305 /* We don't subsume this read... Have to expand record. */
306 expandRecord(shadow);
307 fullRaceCheckRead(thread, location, shadow, currClock);
311 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);