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->assert_bug("Datarace", true);
109 /** This function goes through the list of unrealized data races,
110 * removes the impossible ones, and print the realized ones. */
112 bool checkDataRaces() {
113 if (model->isfeasibleprefix()) {
114 /* Prune the non-racing unrealized dataraces */
115 unsigned int i,newloc=0;
116 for(i=0;i<unrealizedraces.size();i++) {
117 struct DataRace * race=unrealizedraces[i];
118 if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
119 unrealizedraces[newloc++]=race;
123 unrealizedraces.resize(newloc);
125 if (unrealizedraces.size()!=0) {
126 /* We have an actual realized race. */
127 for(i=0;i<unrealizedraces.size();i++) {
128 struct DataRace * race=unrealizedraces[i];
137 void printRace(struct DataRace *race)
139 printf("Datarace detected @ address %p:\n", race->address);
140 printf(" Access 1: %5s in thread %2d @ clock %3u\n",
141 race->isoldwrite ? "write" : "read",
142 id_to_int(race->oldthread), race->oldclock);
143 printf(" Access 2: %5s in thread %2d @ clock %3u\n",
144 race->isnewwrite ? "write" : "read",
145 id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
148 /** This function does race detection for a write on an expanded record. */
149 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
150 struct RaceRecord * record=(struct RaceRecord *) (*shadow);
152 /* Check for datarace against last read. */
154 for(int i=0;i<record->numReads;i++) {
155 modelclock_t readClock = record->readClock[i];
156 thread_id_t readThread = record->thread[i];
158 /* Note that readClock can't actuall be zero here, so it could be
161 if (clock_may_race(currClock, thread, readClock, readThread)) {
162 /* We have a datarace */
163 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
167 /* Check for datarace against last write. */
169 modelclock_t writeClock = record->writeClock;
170 thread_id_t writeThread = record->writeThread;
172 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
173 /* We have a datarace */
174 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
178 record->writeThread=thread;
179 modelclock_t ourClock = currClock->getClock(thread);
180 record->writeClock=ourClock;
183 /** This function does race detection on a write. */
184 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock) {
185 uint64_t * shadow=lookupAddressEntry(location);
186 uint64_t shadowval=*shadow;
189 if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
190 fullRaceCheckWrite(thread, location, shadow, currClock);
194 int threadid = id_to_int(thread);
195 modelclock_t ourClock = currClock->getClock(thread);
197 /* Thread ID is too large or clock is too large. */
198 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
199 expandRecord(shadow);
200 fullRaceCheckWrite(thread, location, shadow, currClock);
204 /* Check for datarace against last read. */
206 modelclock_t readClock = READVECTOR(shadowval);
207 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
209 if (clock_may_race(currClock, thread, readClock, readThread)) {
210 /* We have a datarace */
211 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
214 /* Check for datarace against last write. */
216 modelclock_t writeClock = WRITEVECTOR(shadowval);
217 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
219 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
220 /* We have a datarace */
221 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
223 *shadow = ENCODEOP(0, 0, threadid, ourClock);
226 /** This function does race detection on a read for an expanded record. */
227 void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t * shadow, ClockVector *currClock) {
228 struct RaceRecord * record=(struct RaceRecord *) (*shadow);
230 /* Check for datarace against last write. */
232 modelclock_t writeClock = record->writeClock;
233 thread_id_t writeThread = record->writeThread;
235 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
236 /* We have a datarace */
237 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
240 /* Shorten vector when possible */
244 for(int i=0;i<record->numReads;i++) {
245 modelclock_t readClock = record->readClock[i];
246 thread_id_t readThread = record->thread[i];
248 /* Note that is not really a datarace check as reads cannott
249 actually race. It is just determining that this read subsumes
250 another in the sense that either this read races or neither
251 read races. Note that readClock can't actually be zero, so it
252 could be optimized. */
254 if (clock_may_race(currClock, thread, readClock, readThread)) {
255 /* Still need this read in vector */
256 if (copytoindex!=i) {
257 record->readClock[copytoindex]=record->readClock[i];
258 record->thread[copytoindex]=record->thread[i];
264 if (copytoindex>=record->capacity) {
265 int newCapacity=record->capacity*2;
266 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t)*newCapacity);
267 modelclock_t *newreadClock =( modelclock_t *)snapshot_malloc(sizeof(modelclock_t)*newCapacity);
268 std::memcpy(newthread, record->thread, record->capacity*sizeof(thread_id_t));
269 std::memcpy(newreadClock, record->readClock, record->capacity*sizeof(modelclock_t));
270 snapshot_free(record->readClock);
271 snapshot_free(record->thread);
272 record->readClock=newreadClock;
273 record->thread=newthread;
274 record->capacity=newCapacity;
277 modelclock_t ourClock = currClock->getClock(thread);
279 record->thread[copytoindex]=thread;
280 record->readClock[copytoindex]=ourClock;
281 record->numReads=copytoindex+1;
284 /** This function does race detection on a read. */
285 void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock) {
286 uint64_t * shadow=lookupAddressEntry(location);
287 uint64_t shadowval=*shadow;
290 if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
291 fullRaceCheckRead(thread, location, shadow, currClock);
295 int threadid = id_to_int(thread);
296 modelclock_t ourClock = currClock->getClock(thread);
298 /* Thread ID is too large or clock is too large. */
299 if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
300 expandRecord(shadow);
301 fullRaceCheckRead(thread, location, shadow, currClock);
305 /* Check for datarace against last write. */
307 modelclock_t writeClock = WRITEVECTOR(shadowval);
308 thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
310 if (clock_may_race(currClock, thread, writeClock, writeThread)) {
311 /* We have a datarace */
312 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
315 modelclock_t readClock = READVECTOR(shadowval);
316 thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
318 if (clock_may_race(currClock, thread, readClock, readThread)) {
319 /* We don't subsume this read... Have to expand record. */
320 expandRecord(shadow);
321 fullRaceCheckRead(thread, location, shadow, currClock);
325 *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);