From: Brian Demsky Date: Wed, 18 Jul 2012 22:55:22 +0000 (-0700) Subject: trying to get fork based snapshotting to work X-Git-Tag: pldi2013~335 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=123c66e0c1b0f58aae2916cc22b2100143a2ceb4 trying to get fork based snapshotting to work [Amended by Brian Norris, includes some later clean up] --- diff --git a/main.cc b/main.cc index cbf93b6..73b3b0c 100644 --- a/main.cc +++ b/main.cc @@ -70,7 +70,6 @@ static void real_main() { model->set_system_context(&main_context); snapshotObject->snapshotStep(0); - do { /* Start user program */ model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL)); diff --git a/mymemory.cc b/mymemory.cc index fcc98db..e851818 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -31,11 +31,11 @@ void *MYMALLOC(size_t size) { ptr = mallocp(size); return ptr; #else - if( !sTheRecord ){ - createSharedLibrary(); + if( !snapshotrecord) { + createSharedMemory(); } if( NULL == sStaticSpace ) - sStaticSpace = create_mspace_with_base( ( void * )( sTheRecord->mSharedMemoryBase ), SHARED_MEMORY_DEFAULT -sizeof( struct Snapshot ), 1 ); + sStaticSpace = create_mspace_with_base( ( void * )( snapshotrecord->mSharedMemoryBase ), SHARED_MEMORY_DEFAULT -sizeof( struct SnapShot ), 1 ); return mspace_malloc( sStaticSpace, size ); #endif } diff --git a/snapshot.cc b/snapshot.cc index b6e20fd..9020bb7 100644 --- a/snapshot.cc +++ b/snapshot.cc @@ -26,11 +26,7 @@ #endif /* extern declaration definition */ -#if USE_MPROTECT_SNAPSHOT struct SnapShot * snapshotrecord = NULL; -#else -struct Snapshot * sTheRecord = NULL; -#endif #if !USE_MPROTECT_SNAPSHOT /** @statics @@ -112,35 +108,32 @@ static void HandlePF( int sig, siginfo_t *si, void * unused){ } #endif //nothing to handle for non snapshotting case. -void createSharedLibrary(){ #if !USE_MPROTECT_SNAPSHOT +void createSharedMemory(){ //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 ); + void * memMapBase = mmap( 0, SHARED_MEMORY_DEFAULT + STACK_SIZE_DEFAULT, PROT_READ | PROT_WRITE, MAP_SHARED|MAP_ANON, -1, 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; -#endif + + //Setup snapshot record at top of free region + snapshotrecord = ( struct SnapShot * )memMapBase; + snapshotrecord->mSharedMemoryBase = (void *)((uintptr_t)memMapBase + sizeof(struct SnapShot)); + snapshotrecord->mStackBase = (void *)((uintptr_t)memMapBase + SHARED_MEMORY_DEFAULT); + snapshotrecord->mStackSize = STACK_SIZE_DEFAULT; + snapshotrecord->mIDToRollback = -1; + snapshotrecord->currSnapShotID = 0; } +#endif + /** The initSnapShotLibrary function initializes the Snapshot library. * @param entryPoint the function that should run the program. */ +#if USE_MPROTECT_SNAPSHOT + void initSnapShotLibrary(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions, unsigned int numheappages, VoidFuncPtr entryPoint) { -#if USE_MPROTECT_SNAPSHOT /* Setup a stack for our signal handler.... */ stack_t ss; ss.ss_sp = MYMALLOC(SIGSTACKSIZE); @@ -180,17 +173,21 @@ void initSnapShotLibrary(unsigned int numbackingpages, mySpace = create_mspace_with_base(pagealignedbase, numheappages*PAGESIZE, 1 ); addMemoryRegionToSnapShot(pagealignedbase, numheappages); entryPoint(); +} #else - +void initSnapShotLibrary(unsigned int numbackingpages, + unsigned int numsnapshots, unsigned int nummemoryregions, + unsigned int numheappages, VoidFuncPtr entryPoint) { basemySpace=system_malloc((numheappages+1)*PAGESIZE); void * pagealignedbase=PageAlignAddressUpward(basemySpace); mySpace = create_mspace_with_base(pagealignedbase, numheappages*PAGESIZE, 1 ); - createSharedLibrary(); + if (!snapshotrecord) + createSharedMemory(); //step 2 setup the stack context. ucontext_t newContext; getcontext( &newContext ); - newContext.uc_stack.ss_sp = sTheRecord->mStackBase; + newContext.uc_stack.ss_sp = snapshotrecord->mStackBase; newContext.uc_stack.ss_size = STACK_SIZE_DEFAULT; makecontext( &newContext, entryPoint, 0 ); /* switch to a new entryPoint context, on a new stack */ @@ -198,42 +195,44 @@ void initSnapShotLibrary(unsigned int numbackingpages, /* switch back here when takesnapshot is called */ pid_t forkedID = 0; - snapshotid = sTheRecord->currSnapShotID; - bool swapContext = false; + snapshotid = snapshotrecord->currSnapShotID; + /* This bool indicates that the current process's snapshotid is same + as the id to which the rollback needs to occur */ + + bool rollback = false; while( true ){ - sTheRecord->currSnapShotID=snapshotid+1; + snapshotrecord->currSnapShotID=snapshotid+1; forkedID = fork(); + if( 0 == forkedID ){ - ucontext_t currentContext; - /*If the rollback bool is set{ see below }, switch to the context we need to return to during a rollback*/ - if( swapContext ) - swapcontext( ¤tContext, &( sTheRecord->mContextToRollback ) ); - else{ - /*Child process which is forked as a result of takesnapshot call should switch back to the takesnapshot context*/ - swapcontext( ¤tContext, &savedUserSnapshotContext ); + /* If the rollback bool is set, switch to the context we need to + return to during a rollback. */ + if( rollback) { + setcontext( &( snapshotrecord->mContextToRollback ) ); + } else { + /*Child process which is forked as a result of takesnapshot + call should switch back to the takesnapshot context*/ + setcontext( &savedUserSnapshotContext ); } } else { int status; int retVal; - SSDEBUG("The process id of child is %d and the process id of this process is %d and snapshot id is %d", + SSDEBUG("The process id of child is %d and the process id of this process is %d and snapshot id is %d\n", forkedID, getpid(), snapshotid ); do { retVal=waitpid( forkedID, &status, 0 ); } while( -1 == retVal && errno == EINTR ); - if( sTheRecord->mIDToRollback != snapshotid ) + if( snapshotrecord->mIDToRollback != snapshotid ) { exit(EXIT_SUCCESS); - else{ - /*This bool indicates that the current process's snapshotid is same as the id to which the rollback needs to occur*/ - swapContext = true; } + rollback = true; } } - -#endif } +#endif /** The addMemoryRegionToSnapShot function assumes that addr is page aligned. */ @@ -272,6 +271,7 @@ snapshot_id takeSnapshot( ){ return snapshot; #else swapcontext( &savedUserSnapshotContext, &savedSnapshotContext ); + SSDEBUG("TAKESNAPSHOT RETURN\n"); return snapshotid; #endif } @@ -305,24 +305,25 @@ void rollBack( snapshot_id theID ){ snapshotrecord->lastBackingPage=snapshotrecord->snapShots[theID].firstBackingPage; takeSnapshot(); //Make sure current snapshot is still good...All later ones are cleared #else - sTheRecord->mIDToRollback = theID; - int sTemp = 0; - getcontext( &sTheRecord->mContextToRollback ); + snapshotrecord->mIDToRollback = theID; + volatile int sTemp = 0; + getcontext( &snapshotrecord->mContextToRollback ); /* - * This is used to quit the process on rollback, so that - * the process which needs to rollback can quit allowing the process whose snapshotid matches the rollbackid to switch to - * this context and continue.... - */ + * This is used to quit the process on rollback, so that the process + * which needs to rollback can quit allowing the process whose + * snapshotid matches the rollbackid to switch to this context and + * continue.... + */ if( !sTemp ){ sTemp = 1; - SSDEBUG("Invoked rollback"); + SSDEBUG("Invoked rollback\n"); exit(EXIT_SUCCESS); } - /* - * This fix obviates the need for a finalize call. hence less dependences for model-checker.... - * - */ - sTheRecord->mIDToRollback = -1; + /* + * This fix obviates the need for a finalize call. hence less dependences for model-checker.... + * + */ + snapshotrecord->mIDToRollback = -1; #endif } diff --git a/snapshot.h b/snapshot.h index cbbe007..e41eb9c 100644 --- a/snapshot.h +++ b/snapshot.h @@ -17,11 +17,11 @@ #define SIGSTACKSIZE 32768 void addMemoryRegionToSnapShot( void * ptr, unsigned int numPages ); - snapshot_id takeSnapshot( ); - void rollBack( snapshot_id theSnapShot ); -void createSharedLibrary(); +#if !USE_MPROTECT_SNAPSHOT +void createSharedMemory(); +#endif #endif diff --git a/snapshotimp.h b/snapshotimp.h index e9f6d8b..e5c331a 100644 --- a/snapshotimp.h +++ b/snapshotimp.h @@ -53,17 +53,17 @@ struct SnapShot { unsigned int maxSnapShots; //Stores the total number of snapshots we allow }; -//Global reference to snapshot data structure -extern struct SnapShot * snapshotrecord; #else -struct Snapshot { +struct SnapShot { void *mSharedMemoryBase; void *mStackBase; size_t mStackSize; - snapshot_id mIDToRollback; + volatile snapshot_id mIDToRollback; ucontext_t mContextToRollback; snapshot_id currSnapShotID; }; -extern struct Snapshot * sTheRecord; #endif + +//Global reference to snapshot data structure +extern struct SnapShot * snapshotrecord; #endif