From: Brian Demsky Date: Tue, 15 May 2012 18:21:20 +0000 (-0700) Subject: fix this stuff... X-Git-Tag: pldi2013~435^2 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=8c24abefd5f4c7528a245ec786309f96601b5c58 fix this stuff... --- diff --git a/snapshot-interface.cc b/snapshot-interface.cc index b702e44..2ee01a4 100644 --- a/snapshot-interface.cc +++ b/snapshot-interface.cc @@ -12,169 +12,95 @@ #include #include #include + +/*This looks like it might leak memory... Subramanian should fix this. */ + 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; - MyStringStream ss( input ); - MyString item; - while( std::getline( ss, item, delim ) ){ - splits.push_back( item ); - } - return splits; + std::vector< MyString, MyAlloc< MyString > > splits; + MyStringStream ss( input ); + MyString item; + while( std::getline( ss, item, delim ) ){ + splits.push_back( item ); + } + return splits; } bool checkPermissions( MyString permStr ){ - return permStr.find("w") != MyString::npos; + return permStr.find("w") != MyString::npos; } 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 ); - } + 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 ]; - dataSect[ 0 ] = std::make_pair( MYBINARYNAME, false ); - dataSect[ 1 ] = std::make_pair( MYLIBRARYNAME, false ); - dataSect[ 2 ] = std::make_pair( MYALLOCNAME, false ); - static pid_t sProcID = 0; - if( 0 == sProcID ) { - sProcID = getpid(); - sprintf( sProcessSize, "%d", sProcID ); - } - fn.replace( REPLACEPOS, 1, sProcessSize ); - std::ifstream procName( fn.c_str() ); - if( procName.is_open() ){ - MyString line; - while( procName.good() ){ - getline( procName, line ); - int i = 0; - for( i = 0; i < 3; ++i ){ - if( MyString::npos != line.find( dataSect[ i ].first ) ) break; - } - if( i >= 3 || dataSect[ i ].second == true ) continue; - dataSect[ i ].second = true; - if( !procName.good() )return; - getline( procName, line ); - takeSegmentSnapshot( line ); - } - } +void SnapshotGlobalSegments(){ + MyString fn = PROCNAME; + static char sProcessSize[ 12 ] = { 0 }; + std::pair< const char *, bool > dataSect[ 3 ]; + dataSect[ 0 ] = std::make_pair( MYBINARYNAME, false ); + dataSect[ 1 ] = std::make_pair( MYLIBRARYNAME, false ); + dataSect[ 2 ] = std::make_pair( MYALLOCNAME, false ); + static pid_t sProcID = 0; + if( 0 == sProcID ) { + sProcID = getpid(); + sprintf( sProcessSize, "%d", sProcID ); + } + fn.replace( REPLACEPOS, 1, sProcessSize ); + std::ifstream procName( fn.c_str() ); + if( procName.is_open() ){ + MyString line; + while( procName.good() ){ + getline( procName, line ); + int i = 0; + for( i = 0; i < 3; ++i ){ + if( MyString::npos != line.find( dataSect[ i ].first ) ) break; + } + if( i >= 3 || dataSect[ i ].second == true ) continue; + dataSect[ i ].second = true; + if( !procName.good() )return; + getline( procName, line ); + takeSegmentSnapshot( line ); + } + } } -//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(); - } +//class definition of snapshotStack..... +//declaration of constructor.... +snapshotStack::snapshotStack(){ + SnapshotGlobalSegments(); + AddUserHeapToSnapshot(); + stack=NULL; +} - snapshotTree::~snapshotTree(){ - if( this == msCurrentScope ){ - msCurrentScope = 0; - } - } +snapshotStack::~snapshotStack(){ +} - //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 ); - } +int snapshotStack::backTrackBeforeStep(int seqindex) { + while(true) { + if (stack->index<=seqindex) { + //have right entry + rollBack(stack->snapshotid); + return stack->index; + } + struct stackEntry *tmp=stack; + free(tmp); + stack=stack->next; + } +} - /* - @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; - - } -}; +void snapshotStack::snapshotStep(int seqindex) { + struct stackEntry *tmp=(struct stackEntry *)malloc(sizeof(struct stackEntry)); + tmp->next=stack; + tmp->index=seqindex; + tmp->snapshotid=takeSnapshot(); + stack=tmp; +} diff --git a/snapshot-interface.h b/snapshot-interface.h index 6c5a8cf..5f5f4ea 100644 --- a/snapshot-interface.h +++ b/snapshot-interface.h @@ -9,55 +9,27 @@ #include #include "snapshot.h" #include "libthreads.h" -typedef std::basic_string< char, std::char_traits< char >, MyAlloc< char > > MyString; -namespace snapshot_utils{ -/* -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(); - }; + +class snapshotStack; +typedef std::basic_string, MyAlloc > MyString; + +void SnapshotGlobalSegments(); + +struct stackEntry { + struct stackEntry *next; + snapshot_id snapshotid; + int index; +}; + +class snapshotStack { + public: + MEMALLOC + snapshotStack( ); + ~snapshotStack(); + int backTrackBeforeStep(int seq_index); + void snapshotStep(int seq_index); + + private: + struct stackEntry * stack; }; #endif