*.o
.*.swp
*.so
+*~
+*.*~
# files in this directory
/model
+++ /dev/null
-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
/*
* Return 1 if found next thread, 0 otherwise
*/
+int num;
+int num1;
+int num2;
+
static int thread_system_next(void)
{
Thread *curr, *next;
rootNode = new TreeNode();
currentNode = rootNode;
action_trace = new action_list_t();
- global_vec = snapshot_utils::ReturnGlobalSegmentsToSnapshot();
}
ModelChecker::~ModelChecker()
#include "action.h"
#include "tree.h"
#include "schedule.h"
+#include "snapshot-interface.h"
+#undef DEBUG
#include "common.h"
#define INITIAL_THREAD_ID 0
rootNode = new TreeNode();
currentNode = rootNode;
action_trace = new action_list_t();
+ global_vec = snapshot_utils::ReturnGlobalSegmentsToSnapshot();
}
ModelChecker::~ModelChecker()
{
- std::map<int, class Thread *, MyAlloc< std::pair< int, class Thread * > > >::iterator it;
+ std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< int, class Thread * > > >::iterator it;
for (it = thread_map.begin(); it != thread_map.end(); it++)
delete (*it).second;
thread_map.clear();
void ModelChecker::reset_to_initial_state()
{
DEBUG("+++ Resetting to initial state +++\n");
- std::map<int, class Thread *, MyAlloc< std::pair< int, class Thread * > > >::iterator it;
+ std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< int, class Thread * > > >::iterator it;
for (it = thread_map.begin(); it != thread_map.end(); it++)
delete (*it).second;
thread_map.clear();
std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< const int, class Thread * > > > thread_map;
class TreeNode *rootNode, *currentNode;
std::list<class Backtrack *, MyAlloc< class Backtrack * > > backtrack_list;
- std::vector< std::pair< void *, size_t >, MyAlloc< std::pair< void *, size_t > > > global_vec;
};
extern ModelChecker *model;
+++ /dev/null
-#ifndef __MODEL_H__
-#define __MODEL_H__
-
-#include <list>
-#include <map>
-#include <cstddef>
-#include <ucontext.h>
-
-#include "schedule.h"
-#include "mymemory.h"
-#include <utility>
-#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<int, class Thread *, MyAlloc< std::pair< const int, class Thread * > > > thread_map;
- class TreeNode *rootNode, *currentNode;
- std::list<class Backtrack *, MyAlloc< class Backtrack * > > backtrack_list;
-};
-
-extern ModelChecker *model;
-
-#endif /* __MODEL_H__ */
if( NULL == mySpace ){
//void * mem = MYMALLOC( MSPACE_SIZE );
mySpace = create_mspace( MSPACE_SIZE, 1 );
+ AddUserHeapToSnapshot();
}
return mspace_malloc( mySpace, size );
}
mspace_free( mySpace, ptr );
}
+void AddUserHeapToSnapshot(){
+ static bool alreadySnapshotted = false;
+ if( alreadySnapshotted ) return;
+ addMemoryRegionToSnapShot( mySpace, MSPACE_SIZE / PAGESIZE );
+}
+++ /dev/null
-
-#include "mymemory.h"
-#include "snapshotimp.h"
-#include <stdio.h>
-#include <dlfcn.h>
-#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 );
-}
-
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 T>
class MyAlloc {
#include <unistd.h>
#include <sys/types.h>
#include <sstream>
+#include <cstring>
+#include <cassert>
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;
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 ];
}
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;
+
+ }
+};
#include <vector>
#include <utility>
#include <string>
+#include <map>
+#include <set>
+#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
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( );
+++ /dev/null
-#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
projects / model-checker.git / commitdiff