da478075c8b4f8bde0c4fdfb3bc499f44a79ace9
[model-checker.git] / snapshot.cc
1 #include <inttypes.h>
2 #include <sys/mman.h>
3 #include <unistd.h>
4 #include <signal.h>
5 #include <stdlib.h>
6 #include <string.h>
7 #include <errno.h>
8 #include <sys/wait.h>
9
10 #include "hashtable.h"
11 #include "snapshot.h"
12 #include "mymemory.h"
13 #include "common.h"
14 #include "context.h"
15
16 /** PageAlignedAdressUpdate return a page aligned address for the
17  * address being added as a side effect the numBytes are also changed.
18  */
19 static void * PageAlignAddressUpward(void *addr)
20 {
21         return (void *)((((uintptr_t)addr) + PAGESIZE - 1) & ~(PAGESIZE - 1));
22 }
23
24 #if USE_MPROTECT_SNAPSHOT
25
26 /* Each SnapShotRecord lists the firstbackingpage that must be written to
27  * revert to that snapshot */
28 struct SnapShotRecord {
29         unsigned int firstBackingPage;
30 };
31
32 /** @brief Backing store page */
33 typedef unsigned char snapshot_page_t[PAGESIZE];
34
35 /* List the base address of the corresponding page in the backing store so we
36  * know where to copy it to */
37 struct BackingPageRecord {
38         void *basePtrOfPage;
39 };
40
41 /* Struct for each memory region */
42 struct MemoryRegion {
43         void *basePtr; // base of memory region
44         int sizeInPages; // size of memory region in pages
45 };
46
47 /** ReturnPageAlignedAddress returns a page aligned address for the
48  * address being added as a side effect the numBytes are also changed.
49  */
50 static void * ReturnPageAlignedAddress(void *addr)
51 {
52         return (void *)(((uintptr_t)addr) & ~(PAGESIZE - 1));
53 }
54
55 /* Primary struct for snapshotting system */
56 struct mprot_snapshotter {
57         mprot_snapshotter(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions);
58         ~mprot_snapshotter();
59
60         struct MemoryRegion *regionsToSnapShot; //This pointer references an array of memory regions to snapshot
61         snapshot_page_t *backingStore; //This pointer references an array of snapshotpage's that form the backing store
62         void *backingStoreBasePtr; //This pointer references an array of snapshotpage's that form the backing store
63         struct BackingPageRecord *backingRecords; //This pointer references an array of backingpagerecord's (same number of elements as backingstore
64         struct SnapShotRecord *snapShots; //This pointer references the snapshot array
65
66         unsigned int lastSnapShot; //Stores the next snapshot record we should use
67         unsigned int lastBackingPage; //Stores the next backingpage we should use
68         unsigned int lastRegion; //Stores the next memory region to be used
69
70         unsigned int maxRegions; //Stores the max number of memory regions we support
71         unsigned int maxBackingPages; //Stores the total number of backing pages
72         unsigned int maxSnapShots; //Stores the total number of snapshots we allow
73
74         MEMALLOC
75 };
76
77 static struct mprot_snapshotter *mprot_snap = NULL;
78
79 mprot_snapshotter::mprot_snapshotter(unsigned int backing_pages, unsigned int snapshots, unsigned int regions) :
80         lastSnapShot(0),
81         lastBackingPage(0),
82         lastRegion(0),
83         maxRegions(regions),
84         maxBackingPages(backing_pages),
85         maxSnapShots(snapshots)
86 {
87         regionsToSnapShot = (struct MemoryRegion *)model_malloc(sizeof(struct MemoryRegion) * regions);
88         backingStoreBasePtr = (void *)model_malloc(sizeof(snapshot_page_t) * (backing_pages + 1));
89         //Page align the backingstorepages
90         backingStore = (snapshot_page_t *)PageAlignAddressUpward(backingStoreBasePtr);
91         backingRecords = (struct BackingPageRecord *)model_malloc(sizeof(struct BackingPageRecord) * backing_pages);
92         snapShots = (struct SnapShotRecord *)model_malloc(sizeof(struct SnapShotRecord) * snapshots);
93 }
94
95 mprot_snapshotter::~mprot_snapshotter()
96 {
97         model_free(regionsToSnapShot);
98         model_free(backingStoreBasePtr);
99         model_free(backingRecords);
100         model_free(snapShots);
101 }
102
103 /** mprot_handle_pf is the page fault handler for mprotect based snapshotting
104  * algorithm.
105  */
106 static void mprot_handle_pf(int sig, siginfo_t *si, void *unused)
107 {
108         if (si->si_code == SEGV_MAPERR) {
109                 model_print("Real Fault at %p\n", si->si_addr);
110                 print_trace();
111                 model_print("For debugging, place breakpoint at: %s:%d\n",
112                                 __FILE__, __LINE__);
113                 exit(EXIT_FAILURE);
114         }
115         void* addr = ReturnPageAlignedAddress(si->si_addr);
116
117         unsigned int backingpage = mprot_snap->lastBackingPage++; //Could run out of pages...
118         if (backingpage == mprot_snap->maxBackingPages) {
119                 model_print("Out of backing pages at %p\n", si->si_addr);
120                 exit(EXIT_FAILURE);
121         }
122
123         //copy page
124         memcpy(&(mprot_snap->backingStore[backingpage]), addr, sizeof(snapshot_page_t));
125         //remember where to copy page back to
126         mprot_snap->backingRecords[backingpage].basePtrOfPage = addr;
127         //set protection to read/write
128         if (mprotect(addr, sizeof(snapshot_page_t), PROT_READ | PROT_WRITE)) {
129                 perror("mprotect");
130                 // Handle error by quitting?
131         }
132 }
133
134 static void mprot_snapshot_init(unsigned int numbackingpages,
135                 unsigned int numsnapshots, unsigned int nummemoryregions,
136                 unsigned int numheappages, VoidFuncPtr entryPoint)
137 {
138         /* Setup a stack for our signal handler....  */
139         stack_t ss;
140         ss.ss_sp = PageAlignAddressUpward(model_malloc(SIGSTACKSIZE + PAGESIZE - 1));
141         ss.ss_size = SIGSTACKSIZE;
142         ss.ss_flags = 0;
143         sigaltstack(&ss, NULL);
144
145         struct sigaction sa;
146         sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART | SA_ONSTACK;
147         sigemptyset(&sa.sa_mask);
148         sa.sa_sigaction = mprot_handle_pf;
149 #ifdef MAC
150         if (sigaction(SIGBUS, &sa, NULL) == -1) {
151                 model_print("SIGACTION CANNOT BE INSTALLED\n");
152                 exit(EXIT_FAILURE);
153         }
154 #endif
155         if (sigaction(SIGSEGV, &sa, NULL) == -1) {
156                 model_print("SIGACTION CANNOT BE INSTALLED\n");
157                 exit(EXIT_FAILURE);
158         }
159
160         mprot_snap = new mprot_snapshotter(numbackingpages, numsnapshots, nummemoryregions);
161
162         // EVIL HACK: We need to make sure that calls into the mprot_handle_pf method don't cause dynamic links
163         // The problem is that we end up protecting state in the dynamic linker...
164         // Solution is to call our signal handler before we start protecting stuff...
165
166         siginfo_t si;
167         memset(&si, 0, sizeof(si));
168         si.si_addr = ss.ss_sp;
169         mprot_handle_pf(SIGSEGV, &si, NULL);
170         mprot_snap->lastBackingPage--; //remove the fake page we copied
171
172         void *basemySpace = model_malloc((numheappages + 1) * PAGESIZE);
173         void *pagealignedbase = PageAlignAddressUpward(basemySpace);
174         user_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1);
175         snapshot_add_memory_region(pagealignedbase, numheappages);
176
177         void *base_model_snapshot_space = model_malloc((numheappages + 1) * PAGESIZE);
178         pagealignedbase = PageAlignAddressUpward(base_model_snapshot_space);
179         model_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1);
180         snapshot_add_memory_region(pagealignedbase, numheappages);
181
182         entryPoint();
183 }
184
185 static void mprot_add_to_snapshot(void *addr, unsigned int numPages)
186 {
187         unsigned int memoryregion = mprot_snap->lastRegion++;
188         if (memoryregion == mprot_snap->maxRegions) {
189                 model_print("Exceeded supported number of memory regions!\n");
190                 exit(EXIT_FAILURE);
191         }
192
193         mprot_snap->regionsToSnapShot[memoryregion].basePtr = addr;
194         mprot_snap->regionsToSnapShot[memoryregion].sizeInPages = numPages;
195 }
196
197 static snapshot_id mprot_take_snapshot()
198 {
199         for (unsigned int region = 0; region < mprot_snap->lastRegion; region++) {
200                 if (mprotect(mprot_snap->regionsToSnapShot[region].basePtr, mprot_snap->regionsToSnapShot[region].sizeInPages * sizeof(snapshot_page_t), PROT_READ) == -1) {
201                         perror("mprotect");
202                         model_print("Failed to mprotect inside of takeSnapShot\n");
203                         exit(EXIT_FAILURE);
204                 }
205         }
206         unsigned int snapshot = mprot_snap->lastSnapShot++;
207         if (snapshot == mprot_snap->maxSnapShots) {
208                 model_print("Out of snapshots\n");
209                 exit(EXIT_FAILURE);
210         }
211         mprot_snap->snapShots[snapshot].firstBackingPage = mprot_snap->lastBackingPage;
212
213         return snapshot;
214 }
215
216 static void mprot_roll_back(snapshot_id theID)
217 {
218 #if USE_MPROTECT_SNAPSHOT == 2
219         if (mprot_snap->lastSnapShot == (theID + 1)) {
220                 for (unsigned int page = mprot_snap->snapShots[theID].firstBackingPage; page < mprot_snap->lastBackingPage; page++) {
221                         memcpy(mprot_snap->backingRecords[page].basePtrOfPage, &mprot_snap->backingStore[page], sizeof(snapshot_page_t));
222                 }
223                 return;
224         }
225 #endif
226
227         HashTable< void *, bool, uintptr_t, 4, model_malloc, model_calloc, model_free> duplicateMap;
228         for (unsigned int region = 0; region < mprot_snap->lastRegion; region++) {
229                 if (mprotect(mprot_snap->regionsToSnapShot[region].basePtr, mprot_snap->regionsToSnapShot[region].sizeInPages * sizeof(snapshot_page_t), PROT_READ | PROT_WRITE) == -1) {
230                         perror("mprotect");
231                         model_print("Failed to mprotect inside of takeSnapShot\n");
232                         exit(EXIT_FAILURE);
233                 }
234         }
235         for (unsigned int page = mprot_snap->snapShots[theID].firstBackingPage; page < mprot_snap->lastBackingPage; page++) {
236                 if (!duplicateMap.contains(mprot_snap->backingRecords[page].basePtrOfPage)) {
237                         duplicateMap.put(mprot_snap->backingRecords[page].basePtrOfPage, true);
238                         memcpy(mprot_snap->backingRecords[page].basePtrOfPage, &mprot_snap->backingStore[page], sizeof(snapshot_page_t));
239                 }
240         }
241         mprot_snap->lastSnapShot = theID;
242         mprot_snap->lastBackingPage = mprot_snap->snapShots[theID].firstBackingPage;
243         mprot_take_snapshot(); //Make sure current snapshot is still good...All later ones are cleared
244 }
245
246 #else /* !USE_MPROTECT_SNAPSHOT */
247
248 #define SHARED_MEMORY_DEFAULT  (100 * ((size_t)1 << 20)) // 100mb for the shared memory
249 #define STACK_SIZE_DEFAULT      (((size_t)1 << 20) * 20)  // 20 mb out of the above 100 mb for my stack
250
251 struct fork_snapshotter {
252         void *mSharedMemoryBase;
253         void *mStackBase;
254         size_t mStackSize;
255         volatile snapshot_id mIDToRollback;
256         ucontext_t mContextToRollback;
257         snapshot_id currSnapShotID;
258 };
259
260 static struct fork_snapshotter *fork_snap = NULL;
261
262 /** @statics
263 *   These variables are necessary because the stack is shared region and
264 *   there exists a race between all processes executing the same function.
265 *   To avoid the problem above, we require variables allocated in 'safe' regions.
266 *   The bug was actually observed with the forkID, these variables below are
267 *   used to indicate the various contexts to which to switch to.
268 *
269 *   @savedSnapshotContext: contains the point to which takesnapshot() call should switch to.
270 *   @savedUserSnapshotContext: contains the point to which the process whose snapshotid is equal to the rollbackid should switch to
271 *   @snapshotid: it is a running counter for the various forked processes snapshotid. it is incremented and set in a persistently shared record
272 */
273 static ucontext_t savedSnapshotContext;
274 static ucontext_t savedUserSnapshotContext;
275 static snapshot_id snapshotid = 0;
276
277 static void createSharedMemory()
278 {
279         //step 1. create shared memory.
280         void *memMapBase = mmap(0, SHARED_MEMORY_DEFAULT + STACK_SIZE_DEFAULT, PROT_READ | PROT_WRITE, MAP_SHARED | MAP_ANON, -1, 0);
281         if (memMapBase == MAP_FAILED) {
282                 perror("mmap");
283                 exit(EXIT_FAILURE);
284         }
285
286         //Setup snapshot record at top of free region
287         fork_snap = (struct fork_snapshotter *)memMapBase;
288         fork_snap->mSharedMemoryBase = (void *)((uintptr_t)memMapBase + sizeof(struct fork_snapshotter));
289         fork_snap->mStackBase = (void *)((uintptr_t)memMapBase + SHARED_MEMORY_DEFAULT);
290         fork_snap->mStackSize = STACK_SIZE_DEFAULT;
291         fork_snap->mIDToRollback = -1;
292         fork_snap->currSnapShotID = 0;
293 }
294
295 /**
296  * Create a new mspace pointer for the non-snapshotting (i.e., inter-process
297  * shared) memory region. Only for fork-based snapshotting.
298  *
299  * @return The shared memory mspace
300  */
301 mspace create_shared_mspace()
302 {
303         if (!fork_snap)
304                 createSharedMemory();
305         return create_mspace_with_base((void *)(fork_snap->mSharedMemoryBase), SHARED_MEMORY_DEFAULT - sizeof(struct fork_snapshotter), 1);
306 }
307
308 static void fork_snapshot_init(unsigned int numbackingpages,
309                 unsigned int numsnapshots, unsigned int nummemoryregions,
310                 unsigned int numheappages, VoidFuncPtr entryPoint)
311 {
312         if (!fork_snap)
313                 createSharedMemory();
314
315         void *base_model_snapshot_space = malloc((numheappages + 1) * PAGESIZE);
316         void *pagealignedbase = PageAlignAddressUpward(base_model_snapshot_space);
317         model_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1);
318
319         //step 2 setup the stack context.
320         ucontext_t newContext;
321         getcontext(&newContext);
322         newContext.uc_stack.ss_sp = fork_snap->mStackBase;
323         newContext.uc_stack.ss_size = STACK_SIZE_DEFAULT;
324         makecontext(&newContext, entryPoint, 0);
325         /* switch to a new entryPoint context, on a new stack */
326         model_swapcontext(&savedSnapshotContext, &newContext);
327
328         /* switch back here when takesnapshot is called */
329         pid_t forkedID = 0;
330         snapshotid = fork_snap->currSnapShotID;
331         /* This bool indicates that the current process's snapshotid is same
332                  as the id to which the rollback needs to occur */
333
334         bool rollback = false;
335         while (true) {
336                 fork_snap->currSnapShotID = snapshotid + 1;
337                 forkedID = fork();
338
339                 if (0 == forkedID) {
340                         /* If the rollback bool is set, switch to the context we need to
341                                  return to during a rollback. */
342                         if (rollback) {
343                                 setcontext(&(fork_snap->mContextToRollback));
344                         } else {
345                                 /*Child process which is forked as a result of takesnapshot
346                                         call should switch back to the takesnapshot context*/
347                                 setcontext(&savedUserSnapshotContext);
348                         }
349                 } else {
350                         DEBUG("parent PID: %d, child PID: %d, snapshot ID: %d\n",
351                                 getpid(), forkedID, snapshotid);
352
353                         while (waitpid(forkedID, NULL, 0) < 0) {
354                                 /* waitpid() may be interrupted */
355                                 if (errno != EINTR) {
356                                         perror("waitpid");
357                                         exit(EXIT_FAILURE);
358                                 }
359                         }
360
361                         if (fork_snap->mIDToRollback != snapshotid)
362                                 exit(EXIT_SUCCESS);
363                         rollback = true;
364                 }
365         }
366 }
367
368 static snapshot_id fork_take_snapshot()
369 {
370         model_swapcontext(&savedUserSnapshotContext, &savedSnapshotContext);
371         DEBUG("TAKESNAPSHOT RETURN\n");
372         return snapshotid;
373 }
374
375 static void fork_roll_back(snapshot_id theID)
376 {
377         fork_snap->mIDToRollback = theID;
378         volatile int sTemp = 0;
379         getcontext(&fork_snap->mContextToRollback);
380         /*
381          * This is used to quit the process on rollback, so that the process
382          * which needs to rollback can quit allowing the process whose
383          * snapshotid matches the rollbackid to switch to this context and
384          * continue....
385          */
386         if (!sTemp) {
387                 sTemp = 1;
388                 DEBUG("Invoked rollback\n");
389                 exit(EXIT_SUCCESS);
390         }
391         /*
392          * This fix obviates the need for a finalize call. hence less dependences for model-checker....
393          */
394         fork_snap->mIDToRollback = -1;
395 }
396
397 #endif /* !USE_MPROTECT_SNAPSHOT */
398
399 /**
400  * @brief Initializes the snapshot system
401  * @param entryPoint the function that should run the program.
402  */
403 void snapshot_system_init(unsigned int numbackingpages,
404                 unsigned int numsnapshots, unsigned int nummemoryregions,
405                 unsigned int numheappages, VoidFuncPtr entryPoint)
406 {
407 #if USE_MPROTECT_SNAPSHOT
408         mprot_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages, entryPoint);
409 #else
410         fork_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages, entryPoint);
411 #endif
412 }
413
414 /** Assumes that addr is page aligned. */
415 void snapshot_add_memory_region(void *addr, unsigned int numPages)
416 {
417 #if USE_MPROTECT_SNAPSHOT
418         mprot_add_to_snapshot(addr, numPages);
419 #else
420         /* not needed for fork-based snapshotting */
421 #endif
422 }
423
424 /** Takes a snapshot of memory.
425  * @return The snapshot identifier.
426  */
427 snapshot_id take_snapshot()
428 {
429 #if USE_MPROTECT_SNAPSHOT
430         return mprot_take_snapshot();
431 #else
432         return fork_take_snapshot();
433 #endif
434 }
435
436 /** Rolls the memory state back to the given snapshot identifier.
437  *  @param theID is the snapshot identifier to rollback to.
438  */
439 void snapshot_roll_back(snapshot_id theID)
440 {
441 #if USE_MPROTECT_SNAPSHOT
442         mprot_roll_back(theID);
443 #else
444         fork_roll_back(theID);
445 #endif
446 }