#include <sstream>
#include <cstring>
#include <cassert>
+
+/*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;
+}
#include <set>
#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<char, std::char_traits<char>, MyAlloc<char> > 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
projects / model-checker.git / commitdiff