model: build up 'may_read_from' set
[c11tester.git] / snapshot.cc
index 51d2a3adbb4842902db2fab53ceda4f61dbb48d9..a50835d1cca27ecd2c28aac29e798791dce3f69c 100644 (file)
@@ -28,9 +28,8 @@
 /* extern declaration definition */
 #if USE_MPROTECT_SNAPSHOT
 struct SnapShot * snapshotrecord = NULL;
-struct Snapshot_t * sTheRecord = NULL;
 #else
-struct Snapshot_t * sTheRecord = NULL;
+struct Snapshot * sTheRecord = NULL;
 #endif
 
 #if !USE_MPROTECT_SNAPSHOT
@@ -39,12 +38,26 @@ static ucontext_t savedUserSnapshotContext;
 static snapshot_id snapshotid = 0;
 #endif
 
+/** PageAlignedAdressUpdate return a page aligned address for the
+ * address being added as a side effect the numBytes are also changed.
+ */
+static void * PageAlignAddressUpward(void * addr) {
+       return (void *)((((uintptr_t)addr)+PAGESIZE-1)&~(PAGESIZE-1));
+}
+
 #if USE_MPROTECT_SNAPSHOT
 
+/** ReturnPageAlignedAddress returns a page aligned address for the
+ * address being added as a side effect the numBytes are also changed.
+ */
+static void * ReturnPageAlignedAddress(void * addr) {
+       return (void *)(((uintptr_t)addr)&~(PAGESIZE-1));
+}
+
 /** The initSnapShotRecord method initialized the snapshotting data
  *  structures for the mprotect based snapshot. 
  */
-void initSnapShotRecord(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions) {
+static void initSnapShotRecord(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions) {
        snapshotrecord=( struct SnapShot * )MYMALLOC(sizeof(struct SnapShot));
        snapshotrecord->regionsToSnapShot=( struct MemoryRegion * )MYMALLOC(sizeof(struct MemoryRegion)*nummemoryregions);
        snapshotrecord->backingStoreBasePtr= ( struct SnapShotPage * )MYMALLOC( sizeof( struct SnapShotPage ) * (numbackingpages + 1) );
@@ -59,14 +72,11 @@ void initSnapShotRecord(unsigned int numbackingpages, unsigned int numsnapshots,
        snapshotrecord->maxBackingPages=numbackingpages;
        snapshotrecord->maxSnapShots=numsnapshots;
 }
-#endif //nothing to initialize for the fork based snapshotting.
 
 /** HandlePF is the page fault handler for mprotect based snapshotting
  * algorithm.
  */
-
-void HandlePF( int sig, siginfo_t *si, void * unused){
-#if USE_MPROTECT_SNAPSHOT
+static void HandlePF( int sig, siginfo_t *si, void * unused){
        if( si->si_code == SEGV_MAPERR ){
                printf("Real Fault at %p\n", si->si_addr);
                exit( EXIT_FAILURE );
@@ -88,48 +98,31 @@ void HandlePF( int sig, siginfo_t *si, void * unused){
                perror("mprotect");
                // Handle error by quitting?
        }
-#endif //nothing to handle for non snapshotting case.
-}
-
-/** ReturnPageAlignedAddress returns a page aligned address for the
- * address being added as a side effect the numBytes are also changed.
- */
-
-void * ReturnPageAlignedAddress(void * addr) {
-       return (void *)(((uintptr_t)addr)&~(PAGESIZE-1));
 }
+#endif //nothing to handle for non snapshotting case.
 
-/** PageAlignedAdressUpdate return a page aligned address for the
- * address being added as a side effect the numBytes are also changed.
- */
-
-void * PageAlignAddressUpward(void * addr) {
-       return (void *)((((uintptr_t)addr)+PAGESIZE-1)&~(PAGESIZE-1));
-}
-#ifdef __cplusplus
-extern "C" {
-#endif
-       void createSharedLibrary(){
+void createSharedLibrary(){
 #if !USE_MPROTECT_SNAPSHOT
-               //step 1. create shared memory.
-               if( sTheRecord ) return;
-               int fd = shm_open( "/ModelChecker-Snapshotter", O_RDWR | O_CREAT, 0777 ); //universal permissions.
-               if( -1 == fd ) FAILURE("shm_open");
-               if( -1 == ftruncate( fd, ( size_t )SHARED_MEMORY_DEFAULT + ( size_t )STACK_SIZE_DEFAULT ) ) FAILURE( "ftruncate" );
-               char * memMapBase = ( char * ) mmap( 0, ( size_t )SHARED_MEMORY_DEFAULT + ( size_t )STACK_SIZE_DEFAULT, PROT_READ | PROT_WRITE, MAP_SHARED, fd, 0 );
-               if( MAP_FAILED == memMapBase ) FAILURE("mmap");
-               sTheRecord = ( struct Snapshot_t * )memMapBase;
-               sTheRecord->mSharedMemoryBase = memMapBase + sizeof( struct Snapshot_t );
-               sTheRecord->mStackBase = ( char * )memMapBase + ( size_t )SHARED_MEMORY_DEFAULT;
-               sTheRecord->mStackSize = STACK_SIZE_DEFAULT;
-               sTheRecord->mIDToRollback = -1;
-               sTheRecord->currSnapShotID = 0;
-               sTheRecord->mbFinalize = false;
+       //step 1. create shared memory.
+       if ( sTheRecord )
+               return;
+       int fd = shm_open( "/ModelChecker-Snapshotter", O_RDWR | O_CREAT, 0777 ); //universal permissions.
+       if ( -1 == fd )
+               FAILURE("shm_open");
+       if ( -1 == ftruncate( fd, SHARED_MEMORY_DEFAULT + STACK_SIZE_DEFAULT ) )
+               FAILURE( "ftruncate" );
+       void * memMapBase = mmap( 0, SHARED_MEMORY_DEFAULT + STACK_SIZE_DEFAULT, PROT_READ | PROT_WRITE, MAP_SHARED, fd, 0 );
+       if( MAP_FAILED == memMapBase )
+               FAILURE("mmap");
+       sTheRecord = ( struct Snapshot * )memMapBase;
+       sTheRecord->mSharedMemoryBase = (void *)((uintptr_t)memMapBase + sizeof(struct Snapshot));
+       sTheRecord->mStackBase = (void *)((uintptr_t)memMapBase + SHARED_MEMORY_DEFAULT);
+       sTheRecord->mStackSize = STACK_SIZE_DEFAULT;
+       sTheRecord->mIDToRollback = -1;
+       sTheRecord->currSnapShotID = 0;
+       sTheRecord->mbFinalize = false;
 #endif
-       }
-#ifdef __cplusplus
 }
-#endif
 
 /** The initSnapShotLibrary function initializes the Snapshot library.
  *  @param entryPoint the function that should run the program.
@@ -185,19 +178,13 @@ void initSnapShotLibrary(unsigned int numbackingpages,
        createSharedLibrary();
 
        //step 2 setup the stack context.
-
-       int alreadySwapped = 0;
-       getcontext( &savedSnapshotContext );
-       if( !alreadySwapped ){
-               alreadySwapped = 1;
-               ucontext_t currentContext, swappedContext, newContext;
-               getcontext( &newContext );
-               newContext.uc_stack.ss_sp = sTheRecord->mStackBase;
-               newContext.uc_stack.ss_size = STACK_SIZE_DEFAULT;
-               newContext.uc_link = &currentContext;
-               makecontext( &newContext, entryPoint, 0 );
-               swapcontext( &swappedContext, &newContext );
-       }
+       ucontext_t newContext;
+       getcontext( &newContext );
+       newContext.uc_stack.ss_sp = sTheRecord->mStackBase;
+       newContext.uc_stack.ss_size = STACK_SIZE_DEFAULT;
+       makecontext( &newContext, entryPoint, 0 );
+       /* switch to a new entryPoint context, on a new stack */
+       swapcontext(&savedSnapshotContext, &newContext);
 
        //add the code to take a snapshot here...
        //to return to user process, do a second swapcontext...
@@ -258,7 +245,6 @@ void addMemoryRegionToSnapShot( void * addr, unsigned int numPages) {
 /** The takeSnapshot function takes a snapshot.
  * @return The snapshot identifier.
  */
-
 snapshot_id takeSnapshot( ){
 #if USE_MPROTECT_SNAPSHOT
        for(unsigned int region=0; region<snapshotrecord->lastRegion;region++) {
@@ -285,7 +271,6 @@ snapshot_id takeSnapshot( ){
 /** The rollBack function rollback to the given snapshot identifier.
  *  @param theID is the snapshot identifier to rollback to.
  */
-
 void rollBack( snapshot_id theID ){
 #if USE_MPROTECT_SNAPSHOT
        std::map< void *, bool, std::less< void * >, MyAlloc< std::pair< const void *, bool > > > duplicateMap;
@@ -326,10 +311,8 @@ void rollBack( snapshot_id theID ){
 /** The finalize method shuts down the snapshotting system.  */
 //Subramanian -- remove this function from the external interface and
 //have us call it internally
-
 void finalize(){
 #if !USE_MPROTECT_SNAPSHOT
        sTheRecord->mbFinalize = true;
 #endif
 }
-