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()) {
107 model->switch_to_master(NULL);
111 /** This function goes through the list of unrealized data races,
112 * removes the impossible ones, and print the realized ones. */
114 bool checkDataRaces() {
115 if (model->isfeasibleprefix()) {
116 /* Prune the non-racing unrealized dataraces */
117 unsigned int i,newloc=0;
118 for(i=0;i<unrealizedraces.size();i++) {
119 struct DataRace * race=unrealizedraces[i];
120 if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
121 unrealizedraces[newloc++]=race;
125 unrealizedraces.resize(newloc);
127 if (unrealizedraces.size()!=0) {
128 /* We have an actual realized race. */
129 for(i=0;i<unrealizedraces.size();i++) {
130 struct DataRace * race=unrealizedraces[i];
139 void printRace(struct DataRace *race)
141 printf("Datarace detected @ address %p:\n", race->address);
142 printf(" Access 1: %5s in thread %2d @ clock %3u\n",
143 race->isoldwrite ? "write" : "read",
144 id_to_int(race->oldthread), race->oldclock);
145 printf(" Access 2: %5s in thread %2d @ clock %3u\n",
146 race->isnewwrite ? "write" : "read",
147 id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
150 /** This function does race detection for a write on an expanded record. */
151 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
152 struct RaceRecord * record=(struct RaceRecord *) (*shadow);
154 /* Check for datarace against last read. */
156 for(int i=0;i<record->numReads;i++) {
157 modelclock_t readClock = record->readClock[i];
158 thread_id_t readThread = record->thread[i];
160 /* Note that readClock can't actuall be zero here, so it could be
163 if (clock_may_race(currClock, thread, readClock, readThread)) {
164 /* We have a datarace */
165 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
169 /* Check for datarace against last write. */
171 modelclock_t writeClock = record->writeClock;
172 thread_id_t writeThread = record->writeThread;
174 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
175 /* We have a datarace */
176 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
180 record->writeThread=thread;
181 modelclock_t ourClock = currClock->getClock(thread);
182 record->writeClock=ourClock;
185 /** This function does race detection on a write. */
186 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock) {
187 uint64_t * shadow=lookupAddressEntry(location);
188 uint64_t shadowval=*shadow;
191 if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
192 fullRaceCheckWrite(thread, location, shadow, currClock);
196 int threadid = id_to_int(thread);
197 modelclock_t ourClock = currClock->getClock(thread);
199 /* Thread ID is too large or clock is too large. */
200 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
201 expandRecord(shadow);
202 fullRaceCheckWrite(thread, location, shadow, currClock);
206 /* Check for datarace against last read. */
208 modelclock_t readClock = READVECTOR(shadowval);
209 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
211 if (clock_may_race(currClock, thread, readClock, readThread)) {
212 /* We have a datarace */
213 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
216 /* Check for datarace against last write. */
218 modelclock_t writeClock = WRITEVECTOR(shadowval);
219 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
221 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
222 /* We have a datarace */
223 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
225 *shadow = ENCODEOP(0, 0, threadid, ourClock);
228 /** This function does race detection on a read for an expanded record. */
229 void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t * shadow, ClockVector *currClock) {
230 struct RaceRecord * record=(struct RaceRecord *) (*shadow);
232 /* Check for datarace against last write. */
234 modelclock_t writeClock = record->writeClock;
235 thread_id_t writeThread = record->writeThread;
237 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
238 /* We have a datarace */
239 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
242 /* Shorten vector when possible */
246 for(int i=0;i<record->numReads;i++) {
247 modelclock_t readClock = record->readClock[i];
248 thread_id_t readThread = record->thread[i];
250 /* Note that is not really a datarace check as reads cannott
251 actually race. It is just determining that this read subsumes
252 another in the sense that either this read races or neither
253 read races. Note that readClock can't actually be zero, so it
254 could be optimized. */
256 if (clock_may_race(currClock, thread, readClock, readThread)) {
257 /* Still need this read in vector */
258 if (copytoindex!=i) {
259 record->readClock[copytoindex]=record->readClock[i];
260 record->thread[copytoindex]=record->thread[i];
266 if (copytoindex>=record->capacity) {
267 int newCapacity=record->capacity*2;
268 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t)*newCapacity);
269 modelclock_t *newreadClock =( modelclock_t *)snapshot_malloc(sizeof(modelclock_t)*newCapacity);
270 std::memcpy(newthread, record->thread, record->capacity*sizeof(thread_id_t));
271 std::memcpy(newreadClock, record->readClock, record->capacity*sizeof(modelclock_t));
272 snapshot_free(record->readClock);
273 snapshot_free(record->thread);
274 record->readClock=newreadClock;
275 record->thread=newthread;
276 record->capacity=newCapacity;
279 modelclock_t ourClock = currClock->getClock(thread);
281 record->thread[copytoindex]=thread;
282 record->readClock[copytoindex]=ourClock;
283 record->numReads=copytoindex+1;
286 /** This function does race detection on a read. */
287 void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock) {
288 uint64_t * shadow=lookupAddressEntry(location);
289 uint64_t shadowval=*shadow;
292 if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
293 fullRaceCheckRead(thread, location, shadow, currClock);
297 int threadid = id_to_int(thread);
298 modelclock_t ourClock = currClock->getClock(thread);
300 /* Thread ID is too large or clock is too large. */
301 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
302 expandRecord(shadow);
303 fullRaceCheckRead(thread, location, shadow, currClock);
307 /* Check for datarace against last write. */
309 modelclock_t writeClock = WRITEVECTOR(shadowval);
310 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
312 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
313 /* We have a datarace */
314 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
317 modelclock_t readClock = READVECTOR(shadowval);
318 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
320 if (clock_may_race(currClock, thread, readClock, readThread)) {
321 /* We don't subsume this read... Have to expand record. */
322 expandRecord(shadow);
323 fullRaceCheckRead(thread, location, shadow, currClock);
327 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);