From 02792abf9399d1dca2fab7bc511f09e934d05f1d Mon Sep 17 00:00:00 2001 From: Subramanian Ganapathy Date: Mon, 14 May 2012 18:29:08 -0700 Subject: [PATCH] Defining the interfaces to add various regions to snapshot --- .gitignore | 2 + Makefile~ | 54 ---------------- main.cc | 4 ++ model.cc | 1 - model.cc~ | 7 ++- model.h | 1 - model.h~ | 73 ---------------------- mymemory.cc | 6 ++ mymemory.cc~ | 68 --------------------- mymemory.h | 6 +- snapshot-interface.cc | 139 ++++++++++++++++++++++++++++++++++++++---- snapshot-interface.h | 53 +++++++++++++++- snapshot.h | 2 +- snapshot.h~ | 25 -------- 14 files changed, 202 insertions(+), 239 deletions(-) delete mode 100644 Makefile~ delete mode 100644 model.h~ delete mode 100644 mymemory.cc~ delete mode 100644 snapshot.h~ diff --git a/.gitignore b/.gitignore index d653bcd..6223e7e 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,8 @@ *.o .*.swp *.so +*~ +*.*~ # files in this directory /model diff --git a/Makefile~ b/Makefile~ deleted file mode 100644 index 7b10126..0000000 --- a/Makefile~ +++ /dev/null @@ -1,54 +0,0 @@ -CC=gcc -CXX=g++ - -BIN=model -LIB_NAME=model -LIB_MEM=mymemory -LIB_SO=lib$(LIB_NAME).so -LIB_MEM_SO=lib$(LIB_MEM).so - -USER_O=userprog.o -USER_H=libthreads.h libatomic.h - -MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc threads.cc tree.cc librace.cc action.cc main.cc -MODEL_O=libthreads.o schedule.o libatomic.o model.o threads.o tree.o librace.o action.o main.o -MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h - -SHMEM_CC=snapshot.cc malloc.c mymemory.cc -SHMEM_O=snapshot.o malloc.o mymemory.o -SHMEM_H=snapshot.h snapshotimp.h mymemory.h - -CPPFLAGS=-Wall -g -LDFLAGS=-ldl - -MEMCPPFLAGS=-fPIC -g -c -Wall -all: $(BIN) - -$(BIN): $(USER_O) $(LIB_SO) $(LIB_MEM_SO) - $(CXX) -o $(BIN) $(USER_O) -L. -l$(LIB_NAME) -l$(LIB_MEM) $(CPPFLAGS) - -# note: implicit rule for generating $(USER_O) (i.e., userprog.c -> userprog.o) - -$(LIB_SO): $(MODEL_O) $(MODEL_H) - $(CXX) -shared -Wl,-soname,$(LIB_SO) -o $(LIB_SO) $(MODEL_O) $(LDFLAGS) $(CPPFLAGS) - -$(LIB_MEM_SO): $(SHMEM_O) $(SHMEM_H) - $(CC) -shared -W1,rpath,"." -o $(LIB_MEM_SO) $(SHMEM_O) - -malloc.o: malloc.c - $(CC) $(MEMCPPFLAGS) -DMSPACES -DONLY_MSPACES malloc.c - -mymemory.o: mymemory.h snapshotimp.h mymemory.cc - $(CXX) $(MEMCPPFLAGS) mymemory.cc - -snapshot.o: mymemory.h snapshot.h snapshotimp.h snapshot.cc - $(CXX) $(MEMCPPFLAGS) snapshot.cc - -$(MODEL_O): $(MODEL_CC) $(MODEL_H) - $(CXX) -fPIC -c $(MODEL_CC) $(CPPFLAGS) - -clean: - rm -f $(BIN) *.o *.so - -tags:: - ctags -R diff --git a/main.cc b/main.cc index c7c348f..9af745d 100644 --- a/main.cc +++ b/main.cc @@ -11,6 +11,10 @@ /* * Return 1 if found next thread, 0 otherwise */ +int num; +int num1; +int num2; + static int thread_system_next(void) { Thread *curr, *next; diff --git a/model.cc b/model.cc index 5ecad25..51715d2 100644 --- a/model.cc +++ b/model.cc @@ -56,7 +56,6 @@ ModelChecker::ModelChecker() rootNode = new TreeNode(); currentNode = rootNode; action_trace = new action_list_t(); - global_vec = snapshot_utils::ReturnGlobalSegmentsToSnapshot(); } ModelChecker::~ModelChecker() diff --git a/model.cc~ b/model.cc~ index bd4a300..5ecad25 100644 --- a/model.cc~ +++ b/model.cc~ @@ -4,6 +4,8 @@ #include "action.h" #include "tree.h" #include "schedule.h" +#include "snapshot-interface.h" +#undef DEBUG #include "common.h" #define INITIAL_THREAD_ID 0 @@ -54,11 +56,12 @@ ModelChecker::ModelChecker() rootNode = new TreeNode(); currentNode = rootNode; action_trace = new action_list_t(); + global_vec = snapshot_utils::ReturnGlobalSegmentsToSnapshot(); } ModelChecker::~ModelChecker() { - std::map > >::iterator it; + std::map, MyAlloc< std::pair< int, class Thread * > > >::iterator it; for (it = thread_map.begin(); it != thread_map.end(); it++) delete (*it).second; thread_map.clear(); @@ -72,7 +75,7 @@ ModelChecker::~ModelChecker() void ModelChecker::reset_to_initial_state() { DEBUG("+++ Resetting to initial state +++\n"); - std::map > >::iterator it; + std::map, MyAlloc< std::pair< int, class Thread * > > >::iterator it; for (it = thread_map.begin(); it != thread_map.end(); it++) delete (*it).second; thread_map.clear(); diff --git a/model.h b/model.h index ffedb18..d3b4205 100644 --- a/model.h +++ b/model.h @@ -67,7 +67,6 @@ private: std::map, MyAlloc< std::pair< const int, class Thread * > > > thread_map; class TreeNode *rootNode, *currentNode; std::list > backtrack_list; - std::vector< std::pair< void *, size_t >, MyAlloc< std::pair< void *, size_t > > > global_vec; }; extern ModelChecker *model; diff --git a/model.h~ b/model.h~ deleted file mode 100644 index fc1f762..0000000 --- a/model.h~ +++ /dev/null @@ -1,73 +0,0 @@ -#ifndef __MODEL_H__ -#define __MODEL_H__ - -#include -#include -#include -#include - -#include "schedule.h" -#include "mymemory.h" -#include -#include "libthreads.h" -#include "libatomic.h" -#include "threads.h" -#include "action.h" - -/* Forward declaration */ -class TreeNode; -class Backtrack; - -class ModelChecker { -public: - ModelChecker(); - ~ModelChecker(); - class Scheduler *scheduler; - - void set_system_context(ucontext_t *ctxt) { system_context = ctxt; } - ucontext_t * get_system_context(void) { return system_context; } - - void set_current_action(ModelAction *act) { current_action = act; } - void check_current_action(void); - void print_summary(void); - Thread * schedule_next_thread(); - - int add_thread(Thread *t); - void remove_thread(Thread *t); - Thread * get_thread(thread_id_t tid) { return thread_map[id_to_int(tid)]; } - - thread_id_t get_next_id(); - int get_next_seq_num(); - - int switch_to_master(ModelAction *act); - - bool next_execution(); - MEMALLOC -private: - int next_thread_id; - int used_sequence_numbers; - int num_executions; - - ModelAction * get_last_conflict(ModelAction *act); - void set_backtracking(ModelAction *act); - thread_id_t advance_backtracking_state(); - thread_id_t get_next_replay_thread(); - Backtrack * get_next_backtrack(); - void reset_to_initial_state(); - - void print_list(action_list_t *list); - - class ModelAction *current_action; - Backtrack *exploring; - thread_id_t nextThread; - - ucontext_t *system_context; - action_list_t *action_trace; - std::map > > thread_map; - class TreeNode *rootNode, *currentNode; - std::list > backtrack_list; -}; - -extern ModelChecker *model; - -#endif /* __MODEL_H__ */ diff --git a/mymemory.cc b/mymemory.cc index f43f1c3..c3c67e2 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -59,6 +59,7 @@ void *malloc( size_t size ){ if( NULL == mySpace ){ //void * mem = MYMALLOC( MSPACE_SIZE ); mySpace = create_mspace( MSPACE_SIZE, 1 ); + AddUserHeapToSnapshot(); } return mspace_malloc( mySpace, size ); } @@ -67,3 +68,8 @@ void free( void * ptr ){ mspace_free( mySpace, ptr ); } +void AddUserHeapToSnapshot(){ + static bool alreadySnapshotted = false; + if( alreadySnapshotted ) return; + addMemoryRegionToSnapShot( mySpace, MSPACE_SIZE / PAGESIZE ); +} diff --git a/mymemory.cc~ b/mymemory.cc~ deleted file mode 100644 index 33a1db6..0000000 --- a/mymemory.cc~ +++ /dev/null @@ -1,68 +0,0 @@ - -#include "mymemory.h" -#include "snapshotimp.h" -#include -#include -#define MSPACE_SIZE ( 1 << 20 ) -#if !USE_CHECKPOINTING -static mspace sStaticSpace = NULL; -#endif -void *MYMALLOC(size_t size) -{ -#if USE_CHECKPOINTING - static void *(*mallocp)(size_t size); - char *error; - void *ptr; - - /* get address of libc malloc */ - if (!mallocp) { - mallocp = ( void * ( * )( size_t ) )dlsym(RTLD_NEXT, "malloc"); - if ((error = dlerror()) != NULL) { - fputs(error, stderr); - exit(1); - } - } - ptr = mallocp(size); - return ptr; -#else - if( !sTheRecord ){ - createSharedLibrary(); - } - if( NULL == sStaticSpace ) - sStaticSpace = create_mspace_with_base( ( void * )( sTheRecord->mSharedMemoryBase ), SHARED_MEMORY_DEFAULT -sizeof( struct Snapshot_t ), 1 ); - return mspace_malloc( sStaticSpace, size ); -#endif -} - -void MYFREE(void *ptr) -{ -#if USE_CHECKPOINTING - static void (*freep)(void *); - char *error; - - /* get address of libc free */ - if (!freep) { - freep = ( void ( * )( void * ) )dlsym(RTLD_NEXT, "free"); - if ((error = dlerror()) != NULL) { - fputs(error, stderr); - exit(1); - } - } - freep(ptr); -#else - mspace_free( sStaticSpace, ptr ); -#endif -} -static mspace mySpace = NULL; -void *malloc( size_t size ){ - if( NULL == mySpace ){ - //void * mem = MYMALLOC( MSPACE_SIZE ); - mySpace = create_mspace( MSPACE_SIZE, 1 ); - } - return mspace_malloc( mySpace, size ); -} - -void free( void * ptr ){ - mspace_free( mySpace, ptr ); -} - diff --git a/mymemory.h b/mymemory.h index 481e081..f2f2c2b 100644 --- a/mymemory.h +++ b/mymemory.h @@ -18,12 +18,16 @@ void *MYMALLOC(size_t size); void MYFREE(void *ptr); - +void AddUserHeapToSnapshot(); /* The following code example is taken from the book The C++ Standard Library - A Tutorial and Reference by Nicolai M. Josuttis, Addison-Wesley, 1999 © Copyright Nicolai M. Josuttis 1999 +Permission to copy, use, modify, sell and distribute this software +is granted provided this copyright notice appears in all copies. +This software is provided "as is" without express or implied +warranty, and with no claim as to its suitability for any purpose. */ template class MyAlloc { diff --git a/snapshot-interface.cc b/snapshot-interface.cc index e350bc4..b702e44 100644 --- a/snapshot-interface.cc +++ b/snapshot-interface.cc @@ -10,6 +10,8 @@ #include #include #include +#include +#include typedef std::basic_stringstream< char, std::char_traits< char >, MyAlloc< char > > MyStringStream; std::vector< MyString, MyAlloc< MyString> > splitString( MyString input, char delim ){ std::vector< MyString, MyAlloc< MyString > > splits; @@ -24,8 +26,20 @@ std::vector< MyString, MyAlloc< MyString> > splitString( MyString input, char de bool checkPermissions( MyString permStr ){ return permStr.find("w") != MyString::npos; } -std::vector< std::pair< void *, size_t >, MyAlloc< std::pair< void *, size_t > > > snapshot_utils::ReturnGlobalSegmentsToSnapshot(){ - std::vector< std::pair< void *, size_t >, MyAlloc< std::pair< void *, size_t > > > theVec; +static void takeSegmentSnapshot( const MyString & lineText ){ + std::vector< MyString, MyAlloc< MyString > > firstSplit = splitString( lineText, ' ' ); + if( checkPermissions( firstSplit[ 1 ] ) ){ + std::vector< MyString, MyAlloc< MyString > > secondSplit = splitString( firstSplit[ 0 ], '-' ); + size_t val1 = 0, val2 = 0; + sscanf( secondSplit[ 0 ].c_str(), "%zx", &val1 ); + sscanf( secondSplit[ 1 ].c_str(), "%zx", &val2 ); + size_t len = ( val2 - val1 ) / PAGESIZE; + if( 0 != len ){ + addMemoryRegionToSnapShot( ( void * )val1, len ); + } + } +} +void snapshot_utils::SnapshotGlobalSegments(){ MyString fn = PROCNAME; static char sProcessSize[ 12 ] = { 0 }; std::pair< const char *, bool > dataSect[ 3 ]; @@ -49,17 +63,118 @@ std::vector< std::pair< void *, size_t >, MyAlloc< std::pair< void *, size_t > > } if( i >= 3 || dataSect[ i ].second == true ) continue; dataSect[ i ].second = true; - if( !procName.good() )return theVec; + if( !procName.good() )return; getline( procName, line ); - std::vector< MyString, MyAlloc< MyString > > firstSplit = splitString( line, ' ' ); - if( !checkPermissions( firstSplit[ 1 ] ) ) continue; - std::vector< MyString, MyAlloc< MyString > > secondSplit = splitString( firstSplit[ 0 ], '-' ); - size_t val1 = 0, val2 = 0; - sscanf( secondSplit[ 0 ].c_str(), "%zx", &val1 ); - sscanf( secondSplit[ 1 ].c_str(), "%zx", &val2 ); - size_t len = ( val2 - val1 ) / PAGESIZE; - theVec.push_back( std::make_pair( ( void * ) val1, len ) ); + takeSegmentSnapshot( line ); } } - return theVec; } + +//class definition of snapshotTree..... +//static definitions +namespace snapshot_utils{ + snapshotTree * snapshotTree::msCurrentScope = 0; + BackTrackingParents_t snapshotTree::msRecordedParents; + SnapshotToStateMap_t snapshotTree::msSnapshottedStates; + SnapshotEdgeMap_t snapshotTree::msSnapshotEdgesMap; + unsigned int snapshotTree::msTimeCounter = 0; + void snapshotTree::EnsureRelevantRegionsSnapshotted(){ + SnapshotGlobalSegments(); + AddUserHeapToSnapshot(); + } + //declaration of constructor.... + snapshotTree::snapshotTree(){ + EnsureRelevantRegionsSnapshotted(); + } + + snapshotTree::~snapshotTree(){ + if( this == msCurrentScope ){ + msCurrentScope = 0; + } + } + + //static function definition + snapshotTree * snapshotTree::ReturnCurrentScope(){ + return msCurrentScope; + } + + MyString SerializeThreadSteps( const ThreadStepMap_t & theMap ){ + MyString newStr; + char tempArray[ 2048 ] = { 0 }; + char * ptr = tempArray; + for( ThreadStepMap_t::const_iterator myIter = theMap.begin(); myIter != theMap.end(); ++myIter ){ + sprintf( ptr, "%d:%d#", myIter->first, myIter->second ); + newStr += ptr; + ptr += strlen( ptr ); + + } + return newStr; + } + //public function definiton + /* + @funct: TakeStep( thrd_t current, thrd_t whoseNext ) + @return: bool + @Desc: this function takes a series of steps creating + new tree elements and setting the current scope. This function returns true if the step just taken leads to the parent of + an unexplored back tracking point... + */ + void snapshotTree::AddThreadStep( ThreadStepMap_t & theMap, thrd_t which ){ + if( theMap.find( which ) != theMap.end() ){ + ++theMap[ which ]; + return; + } + theMap[ which ] = 1; //implicit thread creation.... + } + bool snapshotTree::operator<( const snapshotTree & rhs ) const{ + return this->mTimeStamp < rhs.mTimeStamp; + } + bool snapshotTreeComp::operator()( const std::pair< const snapshotTree*, snapshot_id > & lhs, const std::pair< const snapshotTree*, snapshot_id > & rhs ){ + return *(lhs.first) < *(rhs.first); + } + std::pair< MyString, bool > snapshotTree::TakeStep( thrd_t which, thrd_t whoseNext ){ + assert( msCurrentScope == this ); + std::pair< MyString, bool > retVal; + ThreadStepMap_t temp = mThreadStepsTaken; + AddThreadStep( temp, which ); + MyString serialized = SerializeThreadSteps( mThreadStepsTaken ); //is it necessary to cache this with the class....? + retVal.first = serialized; + if( msSnapshotEdgesMap.find( serialized ) != msSnapshotEdgesMap.end() ){ + msCurrentScope = msSnapshotEdgesMap[ serialized ]; + } + snapshotTree * newNode = new snapshotTree(); + newNode->mThreadStepsTaken = temp; + newNode->mpParent = this; + this->mChildren.push_back( newNode ); + newNode->mNextStepTaker = whoseNext; //dont know if this will be used yet.... + newNode->mTimeStamp = msTimeCounter++; + msCurrentScope = newNode; + + //is it an actual backtracking parent.... + retVal.second = msRecordedParents.find( msCurrentScope ) != msRecordedParents.end(); + return retVal; + } + + /* + @funct: BacktrackingPointSet() + @Return: NONE + @DESC: This sets up the internal states necessary in future should we take a snapshot or something... + */ + void snapshotTree::BacktrackingPointSet(){ + assert( msCurrentScope == this ); + msRecordedParents.insert( msCurrentScope->mpParent ); + } + + /* + @funct: ReturnEarliestSnapshotID( MyString key ) + @DESC: For any key, return the snapshot id which is the latest but earlier than the transition defined by the current key.... + */ + snapshot_id snapshotTree::ReturnEarliestSnapshotID( MyString key ){ + //first return a snapshotTree * + if( msSnapshotEdgesMap.find( key ) == msSnapshotEdgesMap.end() )return -1; + //snapshotTree * theNode = msSnapshotEdgesMap[ key ]; + + //do we have a greatest snapshot id that is lesser than the current id... + return -1; + + } +}; diff --git a/snapshot-interface.h b/snapshot-interface.h index 0c2478e..6c5a8cf 100644 --- a/snapshot-interface.h +++ b/snapshot-interface.h @@ -5,8 +5,59 @@ #include #include #include +#include +#include +#include "snapshot.h" +#include "libthreads.h" typedef std::basic_string< char, std::char_traits< char >, MyAlloc< char > > MyString; namespace snapshot_utils{ - std::vector< std::pair< void *, size_t >, MyAlloc< std::pair< void *, size_t > > > ReturnGlobalSegmentsToSnapshot(); +/* +SnapshotTree defines the interfaces and ideal points that require snapshotting. +The algorithm is: When a step happens we create a new Tree node and define that node as the current scope. +when it is time to set a backtracking point, for each backtracking point we record its parent +finally when set current scope is called, we see if this state is a parent +where possible the goal is speed so we use an integer comparison to make all comparison operations required for +finding a given node O 1 +*/ + typedef std::map< thrd_t, int, std::less< thrd_t >, MyAlloc< std::pair< const thrd_t, int > > > ThreadStepMap_t; + MyString SerializeThreadSteps( const ThreadStepMap_t & theMap ); + class snapshotTree; + struct snapshotTreeComp{ + public: + bool operator()( const std::pair< const snapshotTree*, snapshot_id > & lhs, const std::pair< const snapshotTree*, snapshot_id > & rhs ); + }; + + typedef std::map< snapshotTree *, snapshot_id, snapshotTreeComp, MyAlloc< std::pair< const snapshotTree *, snapshot_id > > > SnapshotToStateMap_t; + typedef std::set< snapshotTree*, std::less< snapshotTree * >, MyAlloc< snapshotTree > > BackTrackingParents_t; + typedef std::vector< snapshotTree *, MyAlloc< snapshotTree * > > SnapshotChildren_t; + typedef std::map< MyString, snapshotTree *, std::less< MyString >, MyAlloc< std::pair< const MyString, snapshotTree * > > > SnapshotEdgeMap_t; + void SnapshotGlobalSegments(); + class snapshotTree{ + friend struct snapshotTreeComp; + public: + MEMALLOC + explicit snapshotTree( ); + ~snapshotTree(); + static snapshotTree * ReturnCurrentScope(); + std::pair< MyString, bool > TakeStep( thrd_t which, thrd_t whoseNext ); + private: + unsigned int mTimeStamp; + ThreadStepMap_t mThreadStepsTaken; + thrd_t mNextStepTaker; + snapshotTree * mpParent; + SnapshotChildren_t mChildren; + void AddThreadStep( ThreadStepMap_t & theMap, thrd_t theThread ); + static snapshotTree * msCurrentScope; + static BackTrackingParents_t msRecordedParents; + static SnapshotToStateMap_t msSnapshottedStates; + static SnapshotEdgeMap_t msSnapshotEdgesMap; //this might not actually needed, if this is blowing up memory we have to traverse and find as opposed to looking up.... + static unsigned int msTimeCounter; + void EnsureRelevantRegionsSnapshotted(); + public: + void BacktrackingPointSet(); + bool operator<( const snapshotTree & rhs ) const; + snapshot_id ReturnEarliestSnapshotID( MyString key ); + snapshot_id SnapshotNow(); + }; }; #endif diff --git a/snapshot.h b/snapshot.h index f0e36f0..c737dec 100644 --- a/snapshot.h +++ b/snapshot.h @@ -7,7 +7,7 @@ typedef unsigned int snapshot_id; typedef void (*MyFuncPtr)(); void initSnapShotLibrary(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions, MyFuncPtr entryPoint); -void addMemoryRegionToSnapShot( void * ptr, unsigned int numBytes ); +void addMemoryRegionToSnapShot( void * ptr, unsigned int numPages ); snapshot_id takeSnapshot( ); diff --git a/snapshot.h~ b/snapshot.h~ deleted file mode 100644 index 168b281..0000000 --- a/snapshot.h~ +++ /dev/null @@ -1,25 +0,0 @@ -#ifndef _SNAPSHOT_H -#define _SNAPSHOT_H -#define PAGESIZE 4096 -#define USE_CHECKPOINTING 0 -#define DEBUG 1 -typedef unsigned int snapshot_id; -typedef void (*MyFuncPtr)(); -void initSnapShotLibrary(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions, MyFuncPtr entryPoint); - -void addMemoryRegionToSnapShot( void * ptr, unsigned int numBytes ); - -snapshot_id takeSnapshot( ); - -void rollBack( snapshot_id theSnapShot ); - -void finalize(); - -#ifdef __cplusplus -extern "C" { -#endif -void createSharedLibrary(); -#ifdef __cplusplus -}; /* end of extern "C" */ -#endif -#endif -- 2.34.1