more implementation of scanalysis...
[model-checker.git] / datarace.cc
1 #include "datarace.h"
2 #include "model.h"
3 #include "threads-model.h"
4 #include <stdio.h>
5 #include <cstring>
6 #include "mymemory.h"
7 #include "clockvector.h"
8 #include "config.h"
9 #include "action.h"
10
11 struct ShadowTable *root;
12 SnapVector<struct DataRace *> unrealizedraces;
13 void *memory_base;
14 void *memory_top;
15
16
17 /** This function initialized the data race detector. */
18 void initRaceDetector()
19 {
20         root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1);
21         memory_base = snapshot_calloc(sizeof(struct ShadowBaseTable) * SHADOWBASETABLES, 1);
22         memory_top = ((char *)memory_base) + sizeof(struct ShadowBaseTable) * SHADOWBASETABLES;
23 }
24
25 void * table_calloc(size_t size)
26 {
27         if ((((char *)memory_base) + size) > memory_top) {
28                 return snapshot_calloc(size, 1);
29         } else {
30                 void *tmp = memory_base;
31                 memory_base = ((char *)memory_base) + size;
32                 return tmp;
33         }
34 }
35
36 /** This function looks up the entry in the shadow table corresponding to a
37  * given address.*/
38 static uint64_t * lookupAddressEntry(const void *address)
39 {
40         struct ShadowTable *currtable = root;
41 #if BIT48
42         currtable = (struct ShadowTable *) currtable->array[(((uintptr_t)address) >> 32) & MASK16BIT];
43         if (currtable == NULL) {
44                 currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address) >> 32) & MASK16BIT] = table_calloc(sizeof(struct ShadowTable)));
45         }
46 #endif
47
48         struct ShadowBaseTable *basetable = (struct ShadowBaseTable *)currtable->array[(((uintptr_t)address) >> 16) & MASK16BIT];
49         if (basetable == NULL) {
50                 basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address) >> 16) & MASK16BIT] = table_calloc(sizeof(struct ShadowBaseTable)));
51         }
52         return &basetable->array[((uintptr_t)address) & MASK16BIT];
53 }
54
55 /**
56  * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
57  * to check the potential for a data race.
58  * @param clock1 The current clock vector
59  * @param tid1 The current thread; paired with clock1
60  * @param clock2 The clock value for the potentially-racing action
61  * @param tid2 The thread ID for the potentially-racing action
62  * @return true if the current clock allows a race with the event at clock2/tid2
63  */
64 static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
65                            modelclock_t clock2, thread_id_t tid2)
66 {
67         return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
68 }
69
70 /**
71  * Expands a record from the compact form to the full form.  This is
72  * necessary for multiple readers or for very large thread ids or time
73  * stamps. */
74 static void expandRecord(uint64_t *shadow)
75 {
76         uint64_t shadowval = *shadow;
77
78         modelclock_t readClock = READVECTOR(shadowval);
79         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
80         modelclock_t writeClock = WRITEVECTOR(shadowval);
81         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
82
83         struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord));
84         record->writeThread = writeThread;
85         record->writeClock = writeClock;
86
87         if (readClock != 0) {
88                 record->capacity = INITCAPACITY;
89                 record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * record->capacity);
90                 record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * record->capacity);
91                 record->numReads = 1;
92                 record->thread[0] = readThread;
93                 record->readClock[0] = readClock;
94         }
95         *shadow = (uint64_t) record;
96 }
97
98 /** This function is called when we detect a data race.*/
99 static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address)
100 {
101         struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
102         race->oldthread = oldthread;
103         race->oldclock = oldclock;
104         race->isoldwrite = isoldwrite;
105         race->newaction = newaction;
106         race->isnewwrite = isnewwrite;
107         race->address = address;
108         unrealizedraces.push_back(race);
109
110         /* If the race is realized, bail out now. */
111         if (checkDataRaces())
112                 model->switch_to_master(NULL);
113 }
114
115 /**
116  * @brief Check and report data races
117  *
118  * If the trace is feasible (a feasible prefix), clear out the list of
119  * unrealized data races, asserting any realized ones as execution bugs so that
120  * the model-checker will end the execution.
121  *
122  * @return True if any data races were realized
123  */
124 bool checkDataRaces()
125 {
126         if (model->isfeasibleprefix()) {
127                 bool race_asserted = false;
128                 /* Prune the non-racing unrealized dataraces */
129                 for (unsigned i = 0; i < unrealizedraces.size(); i++) {
130                         struct DataRace *race = unrealizedraces[i];
131                         if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
132                                 assert_race(race);
133                                 race_asserted = true;
134                         }
135                         snapshot_free(race);
136                 }
137                 unrealizedraces.clear();
138                 return race_asserted;
139         }
140         return false;
141 }
142
143 /**
144  * @brief Assert a data race
145  *
146  * Asserts a data race which is currently realized, causing the execution to
147  * end and stashing a message in the model-checker's bug list
148  *
149  * @param race The race to report
150  */
151 void assert_race(struct DataRace *race)
152 {
153         model->assert_bug(
154                         "Data race detected @ address %p:\n"
155                         "    Access 1: %5s in thread %2d @ clock %3u\n"
156                         "    Access 2: %5s in thread %2d @ clock %3u",
157                         race->address,
158                         race->isoldwrite ? "write" : "read",
159                         id_to_int(race->oldthread),
160                         race->oldclock,
161                         race->isnewwrite ? "write" : "read",
162                         id_to_int(race->newaction->get_tid()),
163                         race->newaction->get_seq_number()
164                 );
165 }
166
167 /** This function does race detection for a write on an expanded record. */
168 void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock)
169 {
170         struct RaceRecord *record = (struct RaceRecord *)(*shadow);
171
172         /* Check for datarace against last read. */
173
174         for (int i = 0; i < record->numReads; i++) {
175                 modelclock_t readClock = record->readClock[i];
176                 thread_id_t readThread = record->thread[i];
177
178                 /* Note that readClock can't actuall be zero here, so it could be
179                          optimized. */
180
181                 if (clock_may_race(currClock, thread, readClock, readThread)) {
182                         /* We have a datarace */
183                         reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
184                 }
185         }
186
187         /* Check for datarace against last write. */
188
189         modelclock_t writeClock = record->writeClock;
190         thread_id_t writeThread = record->writeThread;
191
192         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
193                 /* We have a datarace */
194                 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
195         }
196
197         record->numReads = 0;
198         record->writeThread = thread;
199         modelclock_t ourClock = currClock->getClock(thread);
200         record->writeClock = ourClock;
201 }
202
203 /** This function does race detection on a write. */
204 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
205 {
206         uint64_t *shadow = lookupAddressEntry(location);
207         uint64_t shadowval = *shadow;
208
209         /* Do full record */
210         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
211                 fullRaceCheckWrite(thread, location, shadow, currClock);
212                 return;
213         }
214
215         int threadid = id_to_int(thread);
216         modelclock_t ourClock = currClock->getClock(thread);
217
218         /* Thread ID is too large or clock is too large. */
219         if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
220                 expandRecord(shadow);
221                 fullRaceCheckWrite(thread, location, shadow, currClock);
222                 return;
223         }
224
225         /* Check for datarace against last read. */
226
227         modelclock_t readClock = READVECTOR(shadowval);
228         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
229
230         if (clock_may_race(currClock, thread, readClock, readThread)) {
231                 /* We have a datarace */
232                 reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
233         }
234
235         /* Check for datarace against last write. */
236
237         modelclock_t writeClock = WRITEVECTOR(shadowval);
238         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
239
240         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
241                 /* We have a datarace */
242                 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
243         }
244         *shadow = ENCODEOP(0, 0, threadid, ourClock);
245 }
246
247 /** This function does race detection on a read for an expanded record. */
248 void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
249 {
250         struct RaceRecord *record = (struct RaceRecord *) (*shadow);
251
252         /* Check for datarace against last write. */
253
254         modelclock_t writeClock = record->writeClock;
255         thread_id_t writeThread = record->writeThread;
256
257         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
258                 /* We have a datarace */
259                 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
260         }
261
262         /* Shorten vector when possible */
263
264         int copytoindex = 0;
265
266         for (int i = 0; i < record->numReads; i++) {
267                 modelclock_t readClock = record->readClock[i];
268                 thread_id_t readThread = record->thread[i];
269
270                 /*  Note that is not really a datarace check as reads cannott
271                                 actually race.  It is just determining that this read subsumes
272                                 another in the sense that either this read races or neither
273                                 read races. Note that readClock can't actually be zero, so it
274                                 could be optimized.  */
275
276                 if (clock_may_race(currClock, thread, readClock, readThread)) {
277                         /* Still need this read in vector */
278                         if (copytoindex != i) {
279                                 record->readClock[copytoindex] = record->readClock[i];
280                                 record->thread[copytoindex] = record->thread[i];
281                         }
282                         copytoindex++;
283                 }
284         }
285
286         if (copytoindex >= record->capacity) {
287                 int newCapacity = record->capacity * 2;
288                 thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
289                 modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
290                 std::memcpy(newthread, record->thread, record->capacity * sizeof(thread_id_t));
291                 std::memcpy(newreadClock, record->readClock, record->capacity * sizeof(modelclock_t));
292                 snapshot_free(record->readClock);
293                 snapshot_free(record->thread);
294                 record->readClock = newreadClock;
295                 record->thread = newthread;
296                 record->capacity = newCapacity;
297         }
298
299         modelclock_t ourClock = currClock->getClock(thread);
300
301         record->thread[copytoindex] = thread;
302         record->readClock[copytoindex] = ourClock;
303         record->numReads = copytoindex + 1;
304 }
305
306 /** This function does race detection on a read. */
307 void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock)
308 {
309         uint64_t *shadow = lookupAddressEntry(location);
310         uint64_t shadowval = *shadow;
311
312         /* Do full record */
313         if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
314                 fullRaceCheckRead(thread, location, shadow, currClock);
315                 return;
316         }
317
318         int threadid = id_to_int(thread);
319         modelclock_t ourClock = currClock->getClock(thread);
320
321         /* Thread ID is too large or clock is too large. */
322         if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
323                 expandRecord(shadow);
324                 fullRaceCheckRead(thread, location, shadow, currClock);
325                 return;
326         }
327
328         /* Check for datarace against last write. */
329
330         modelclock_t writeClock = WRITEVECTOR(shadowval);
331         thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
332
333         if (clock_may_race(currClock, thread, writeClock, writeThread)) {
334                 /* We have a datarace */
335                 reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
336         }
337
338         modelclock_t readClock = READVECTOR(shadowval);
339         thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
340
341         if (clock_may_race(currClock, thread, readClock, readThread)) {
342                 /* We don't subsume this read... Have to expand record. */
343                 expandRecord(shadow);
344                 fullRaceCheckRead(thread, location, shadow, currClock);
345                 return;
346         }
347
348         *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
349 }