all: $(BIN)
+debug: CPPFLAGS += -DCONFIG_DEBUG
+debug: all
+
$(BIN): $(USER_O) $(LIB_SO)
$(CXX) -o $(BIN) $(USER_O) -L. -l$(LIB_NAME)
#include "model.h"
#include "action.h"
+#include "clockvector.h"
+#include "common.h"
ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
{
act->tid = t->get_id();
act->value = value;
act->seq_number = model->get_next_seq_num();
+
+ cv = NULL;
+}
+
+ModelAction::~ModelAction()
+{
+ if (cv)
+ delete cv;
}
bool ModelAction::is_read()
bool ModelAction::same_var(ModelAction *act)
{
- return true;
- // TODO: fix stack allocation... return location == act->location;
+ return location == act->location;
}
bool ModelAction::same_thread(ModelAction *act)
return false;
}
+void ModelAction::create_cv(ModelAction *parent)
+{
+ if (cv)
+ return;
+
+ if (parent)
+ cv = new ClockVector(parent->cv, this);
+ else
+ cv = new ClockVector(NULL, this);
+}
+
+void ModelAction::read_from(ModelAction *act)
+{
+ ASSERT(cv);
+ if (act->is_release() && this->is_acquire())
+ cv->merge(act->cv);
+ value = act->value;
+}
+
void ModelAction::print(void)
{
const char *type_str;
type_str = "unknown type";
}
- printf("(%4d) Thread: %d\tAction: %s\tMO: %d\tLoc: %14p\tValue: %d\n",
+ printf("(%3d) Thread: %-2d Action: %-13s MO: %d Loc: %14p Value: %d",
seq_number, id_to_int(tid), type_str, order, location, value);
+ if (cv) {
+ printf("\t");
+ cv->print();
+ } else
+ printf("\n");
}
#define __ACTION_H__
#include <list>
+#include <cstddef>
+
#include "threads.h"
#include "libatomic.h"
#include "mymemory.h"
/* Forward declaration */
class Node;
+class ClockVector;
class ModelAction {
public:
ModelAction(action_type_t type, memory_order order, void *loc, int value);
+ ~ModelAction();
void print(void);
thread_id_t get_tid() { return tid; }
bool same_thread(ModelAction *act);
bool is_dependent(ModelAction *act);
+ void create_cv(ModelAction *parent = NULL);
+ void read_from(ModelAction *act);
+
inline bool operator <(const ModelAction& act) const {
return get_seq_number() < act.get_seq_number();
}
int value;
Node *node;
int seq_number;
+
+ ClockVector *cv;
};
-typedef std::list<class ModelAction *, MyAlloc< class ModelAction * > > action_list_t;
+typedef std::list<class ModelAction *> action_list_t;
#endif /* __ACTION_H__ */
#include <algorithm>
#include <cstring>
+#include <stdlib.h>
#include "model.h"
#include "action.h"
ClockVector::ClockVector(ClockVector *parent, ModelAction *act)
{
- num_threads = parent ? parent->num_threads : 1;
- if (act && act->get_type() == THREAD_CREATE)
- num_threads++;
+ num_threads = model->get_num_threads();
clock = (int *)MYMALLOC(num_threads * sizeof(int));
+ memset(clock, 0, num_threads * sizeof(int));
if (parent)
std::memcpy(clock, parent->clock, parent->num_threads * sizeof(int));
- else
- clock[0] = 0;
if (act)
clock[id_to_int(act->get_tid())] = act->get_seq_number();
return act->get_seq_number() < clock[i];
return false;
}
+
+void ClockVector::print()
+{
+ int i;
+ printf("CV: (");
+ for (i = 0; i < num_threads; i++)
+ printf("%2d%s", clock[i], (i == num_threads - 1) ? ")\n" : ", ");
+}
#define __CLOCKVECTOR_H__
#include "threads.h"
+#include "mymemory.h"
/* Forward declaration */
class ModelAction;
~ClockVector();
void merge(ClockVector *cv);
bool happens_before(ModelAction *act, thread_id_t id);
+
+ void print();
+
+ MEMALLOC
private:
int *clock;
int num_threads;
#define __COMMON_H__
#include <stdio.h>
-#include <stdlib.h>
-#include "mymemory.h"
-//#define CONFIG_DEBUG
+/*
+#ifndef CONFIG_DEBUG
+#define CONFIG_DEBUG
+#endif
+*/
#ifdef CONFIG_DEBUG
#define DEBUG(fmt, ...) do { printf("*** %25s(): line %-4d *** " fmt, __func__, __LINE__, ##__VA_ARGS__); } while (0)
} \
} while (0);
-
-#define userMalloc(size) malloc(size)
-#define userFree(ptr) free(ptr)
-
#endif /* __COMMON_H__ */
*/
int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg)
{
+ Thread *thread;
int ret;
DBG();
- ret = model->add_thread(new Thread(t, start_routine, arg));
+ thread = new Thread(t, start_routine, arg);
+ ret = model->add_thread(thread);
DEBUG("create thread %d\n", id_to_int(thrd_to_id(*t)));
/* seq_cst is just a 'don't care' parameter */
- model->switch_to_master(new ModelAction(THREAD_CREATE, memory_order_seq_cst, NULL, VALUE_NONE));
+ model->switch_to_master(new ModelAction(THREAD_CREATE, memory_order_seq_cst, thread, VALUE_NONE));
return ret;
}
/* global "model" object */
#include "model.h"
-#include "snapshot.h"
#include "snapshot-interface.h"
/*
thrd_t user_thread;
ucontext_t main_context;
- //Create the singleton snapshotStack object
- snapshotObject = new snapshotStack();
+ //Create the singleton SnapshotStack object
+ snapshotObject = new SnapshotStack();
model = new ModelChecker();
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));
diverge(NULL),
nextThread(THREAD_ID_T_NONE),
action_trace(new action_list_t()),
+ thread_map(new std::map<int, class Thread *>),
+ obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
+ thrd_last_action(new std::vector<ModelAction *>(1)),
node_stack(new NodeStack()),
next_backtrack(NULL)
{
ModelChecker::~ModelChecker()
{
- 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++)
+ std::map<int, class Thread *>::iterator it;
+ for (it = thread_map->begin(); it != thread_map->end(); it++)
delete (*it).second;
- thread_map.clear();
+ delete thread_map;
+ delete obj_thrd_map;
delete action_trace;
-
+ delete thrd_last_action;
delete node_stack;
delete scheduler;
}
void ModelChecker::reset_to_initial_state()
{
DEBUG("+++ Resetting to initial state +++\n");
- 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();
- delete action_trace;
- action_trace = new action_list_t();
node_stack->reset_execution();
current_action = NULL;
next_thread_id = INITIAL_THREAD_ID;
used_sequence_numbers = 0;
nextThread = 0;
next_backtrack = NULL;
- /* scheduler reset ? */
+ snapshotObject->backTrackBeforeStep(0);
}
thread_id_t ModelChecker::get_next_id()
return next_thread_id++;
}
+int ModelChecker::get_num_threads()
+{
+ return next_thread_id;
+}
+
int ModelChecker::get_next_seq_num()
{
return ++used_sequence_numbers;
Thread *t;
if (nextThread == THREAD_ID_T_NONE)
return NULL;
- t = thread_map[id_to_int(nextThread)];
+ t = (*thread_map)[id_to_int(nextThread)];
ASSERT(t != NULL);
}
curr = node_stack->explore_action(curr);
+ curr->create_cv(get_parent_action(curr->get_tid()));
+
+ /* Assign 'creation' parent */
+ if (curr->get_type() == THREAD_CREATE) {
+ Thread *th = (Thread *)curr->get_location();
+ th->set_creation(curr);
+ }
+
nextThread = get_next_replay_thread();
currnode = curr->get_node();
next_backtrack = curr;
set_backtracking(curr);
- this->action_trace->push_back(curr);
+
+ add_action_to_lists(curr);
+}
+
+void ModelChecker::add_action_to_lists(ModelAction *act)
+{
+ action_trace->push_back(act);
+
+ std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
+ if (id_to_int(act->get_tid()) >= (int)vec->size())
+ vec->resize(next_thread_id);
+ (*vec)[id_to_int(act->get_tid())].push_back(act);
+
+ (*thrd_last_action)[id_to_int(act->get_tid())] = act;
+}
+
+ModelAction * ModelChecker::get_last_action(thread_id_t tid)
+{
+ int nthreads = get_num_threads();
+ if ((int)thrd_last_action->size() < nthreads)
+ thrd_last_action->resize(nthreads);
+ return (*thrd_last_action)[id_to_int(tid)];
+}
+
+ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
+{
+ ModelAction *parent = get_last_action(tid);
+ if (!parent)
+ parent = get_thread(tid)->get_creation();
+ return parent;
}
void ModelChecker::print_summary(void)
int ModelChecker::add_thread(Thread *t)
{
- thread_map[id_to_int(t->get_id())] = t;
+ (*thread_map)[id_to_int(t->get_id())] = t;
scheduler->add_thread(t);
return 0;
}
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 * get_thread(thread_id_t tid) { return (*thread_map)[id_to_int(tid)]; }
thread_id_t get_next_id();
+ int get_num_threads();
int get_next_seq_num();
int switch_to_master(ModelAction *act);
ModelAction * get_next_backtrack();
void reset_to_initial_state();
+ void add_action_to_lists(ModelAction *act);
+ ModelAction * get_last_action(thread_id_t tid);
+ ModelAction * get_parent_action(thread_id_t tid);
+
void print_list(action_list_t *list);
ModelAction *current_action;
ucontext_t *system_context;
action_list_t *action_trace;
- std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< const int, class Thread * > > > thread_map;
+ std::map<int, class Thread *> *thread_map;
+ std::map<void *, std::vector<action_list_t> > *obj_thrd_map;
+ std::vector<ModelAction *> *thrd_last_action;
class NodeStack *node_stack;
ModelAction *next_backtrack;
};
#include "snapshotimp.h"
#include <stdio.h>
#include <dlfcn.h>
-#if !USE_CHECKPOINTING
+#if !USE_MPROTECT_SNAPSHOT
static mspace sStaticSpace = NULL;
#endif
void *MYMALLOC(size_t size) {
-#if USE_CHECKPOINTING
+#if USE_MPROTECT_SNAPSHOT
static void *(*mallocp)(size_t size);
char *error;
void *ptr;
}
void MYFREE(void *ptr) {
-#if USE_CHECKPOINTING
+#if USE_MPROTECT_SNAPSHOT
static void (*freep)(void *);
char *error;
}
void * operator new(size_t size) throw(std::bad_alloc) {
- return MYMALLOC(size);
+ return malloc(size);
}
void operator delete(void *p) throw() {
- MYFREE(p);
+ free(p);
+}
+
+void * operator new[](size_t size) throw(std::bad_alloc) {
+ return malloc(size);
+}
+
+void operator delete[](void *p, size_t size) {
+ free(p);
}
#include "nodestack.h"
#include "action.h"
#include "common.h"
+#include "model.h"
int Node::total_nodes = 0;
-Node::Node(ModelAction *act, Node *parent)
+Node::Node(ModelAction *act, int nthreads)
: action(act),
- num_threads(parent ? parent->num_threads : 1),
+ num_threads(nthreads),
explored_children(num_threads),
backtrack(num_threads)
{
total_nodes++;
- if (act && act->get_type() == THREAD_CREATE) {
- num_threads++;
- explored_children.resize(num_threads);
- backtrack.resize(num_threads);
- }
}
Node::~Node()
/* Record action */
get_head()->explore_child(act);
- node_list.push_back(new Node(act, get_head()));
+ node_list.push_back(new Node(act, model->get_num_threads()));
iter++;
}
return (*iter)->get_action();
class Node {
public:
- Node(ModelAction *act = NULL, Node *parent = NULL);
+ Node(ModelAction *act = NULL, int nthreads = 1);
~Node();
/* return true = thread choice has already been explored */
bool has_been_explored(thread_id_t tid);
static int total_nodes;
ModelAction *action;
int num_threads;
- std::vector<bool> explored_children;
- std::vector<bool> backtrack;
+ std::vector< bool, MyAlloc<bool> > explored_children;
+ std::vector< bool, MyAlloc<bool> > backtrack;
};
-typedef std::list<class Node *> node_list_t;
+typedef std::list<class Node *, MyAlloc< class Node * > > node_list_t;
class NodeStack {
public:
Thread * get_current_thread(void);
void print();
- MEMALLOC
+ SNAPSHOTALLOC
private:
- std::list<Thread *, MyAlloc< Thread * > > readyList;
+ std::list<Thread *> readyList;
Thread *current;
};
#include "snapshot-interface.h"
+#include "snapshot.h"
#include <iostream>
#include <fstream>
#include <unistd.h>
#include <sys/types.h>
#include <sstream>
#include <cstring>
+#include <string>
#include <cassert>
+#include <vector>
+#include <utility>
#define MYBINARYNAME "model"
#define MYLIBRARYNAME "libmodel.so"
#define PROCNAME "/proc/*/maps"
#define REPLACEPOS 6
-#define PAGESIZE 4096
-snapshotStack * snapshotObject;
+typedef std::basic_string<char, std::char_traits<char>, MyAlloc<char> > MyString;
+
+SnapshotStack * snapshotObject;
/*This looks like it might leak memory... Subramanian should fix this. */
MyString line;
while( procName.good() ){
getline( procName, line );
- int i = 0;
- for( i = 0; i < 3; ++i ){
+ int i;
+ for( i = 0; i < 2; ++i ){
if( MyString::npos != line.find( dataSect[ i ].first ) ) break;
}
- if( i >= 3 || dataSect[ i ].second == true ) continue;
+ if( i >= 2 || dataSect[ i ].second == true ) continue;
dataSect[ i ].second = true;
if( !procName.good() )return;
getline( procName, line );
}
}
-//class definition of snapshotStack.....
+//class definition of SnapshotStack.....
//declaration of constructor....
-snapshotStack::snapshotStack(){
+SnapshotStack::SnapshotStack(){
SnapshotGlobalSegments();
stack=NULL;
}
-snapshotStack::~snapshotStack(){
+SnapshotStack::~SnapshotStack(){
}
-int snapshotStack::backTrackBeforeStep(int seqindex) {
+int SnapshotStack::backTrackBeforeStep(int seqindex) {
while(true) {
if (stack->index<=seqindex) {
//have right entry
}
}
-void snapshotStack::snapshotStep(int seqindex) {
+void SnapshotStack::snapshotStep(int seqindex) {
struct stackEntry *tmp=(struct stackEntry *)MYMALLOC(sizeof(struct stackEntry));
tmp->next=stack;
tmp->index=seqindex;
#ifndef __SNAPINTERFACE_H
#define __SNAPINTERFACE_H
-#include "snapshot.h"
#include "mymemory.h"
-#include <vector>
-#include <utility>
-#include <string>
-#include <map>
-#include <set>
-#include "snapshot.h"
-#include "libthreads.h"
-class snapshotStack;
-typedef std::basic_string<char, std::char_traits<char>, MyAlloc<char> > MyString;
+typedef unsigned int snapshot_id;
+
+typedef void (*VoidFuncPtr)();
+void initSnapShotLibrary(unsigned int numbackingpages,
+ unsigned int numsnapshots, unsigned int nummemoryregions,
+ unsigned int numheappages, VoidFuncPtr entryPoint);
void SnapshotGlobalSegments();
int index;
};
-class snapshotStack {
+class SnapshotStack {
public:
MEMALLOC
- snapshotStack( );
- ~snapshotStack();
+ SnapshotStack( );
+ ~SnapshotStack();
int backTrackBeforeStep(int seq_index);
void snapshotStep(int seq_index);
/* Not sure what it even means to have more than one snapshot object,
so let's just make a global reference to it.*/
-extern snapshotStack * snapshotObject;
+extern SnapshotStack * snapshotObject;
#endif
#include <signal.h>
#include <stdlib.h>
#include <map>
-#include <set>
#include <cstring>
#include <cstdio>
#include "snapshot.h"
#include <errno.h>
#include <sys/wait.h>
#include <ucontext.h>
-#include <sys/time.h>
+
//extern declaration definition
#define FAILURE(mesg) { printf("failed in the API: %s with errno relative message: %s\n", mesg, strerror( errno ) ); exit( -1 ); }
-#if USE_CHECKPOINTING
+#if USE_MPROTECT_SNAPSHOT
struct SnapShot * snapshotrecord = NULL;
struct Snapshot_t * sTheRecord = NULL;
#else
struct Snapshot_t * sTheRecord = NULL;
#endif
-void BeginOperation( struct timeval * theStartTime ){
-#if 1
- gettimeofday( theStartTime, NULL );
-#endif
-}
-#if SSDEBUG
-struct timeval *starttime = NULL;
-#endif
void DumpIntoLog( const char * filename, const char * message ){
#if SSDEBUG
static pid_t thePID = getpid();
char newFn[ 1024 ] ={ 0 };
sprintf( newFn,"%s-%d.txt", filename, thePID );
FILE * myFile = fopen( newFn, "w+" );
- struct timeval theEndTime;
- BeginOperation( &theEndTime );
- double elapsed = ( theEndTime.tv_sec - starttime->tv_sec ) + ( theEndTime.tv_usec - starttime->tv_usec ) / 1000000.0;
- fprintf( myFile, "The timestamp %f:--> the message %s: the process id %d\n", elapsed, message, thePID );
+ fprintf( myFile, "the message %s: the process id %d\n", message, thePID );
fflush( myFile );
fclose( myFile );
myFile = NULL;
#endif
}
-#if !USE_CHECKPOINTING
+#if !USE_MPROTECT_SNAPSHOT
static ucontext_t savedSnapshotContext;
static ucontext_t savedUserSnapshotContext;
-static int snapshotid = 0;
+static snapshot_id snapshotid = 0;
#endif
/* Initialize snapshot data structure */
-#if USE_CHECKPOINTING
+#if USE_MPROTECT_SNAPSHOT
void initSnapShotRecord(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions) {
snapshotrecord=( struct SnapShot * )MYMALLOC(sizeof(struct SnapShot));
snapshotrecord->regionsToSnapShot=( struct MemoryRegion * )MYMALLOC(sizeof(struct MemoryRegion)*nummemoryregions);
#endif //nothing to initialize for the fork based snapshotting.
void HandlePF( int sig, siginfo_t *si, void * unused){
-#if USE_CHECKPOINTING
+#if USE_MPROTECT_SNAPSHOT
if( si->si_code == SEGV_MAPERR ){
- printf("Real Fault at %llx\n", ( long long )si->si_addr);
- exit( EXIT_FAILURE );
+ printf("Real Fault at %p\n", si->si_addr);
+ exit( EXIT_FAILURE );
}
void* addr = ReturnPageAlignedAddress(si->si_addr);
unsigned int backingpage=snapshotrecord->lastBackingPage++; //Could run out of pages...
if (backingpage==snapshotrecord->maxBackingPages) {
- printf("Out of backing pages at %llx\n", ( long long )si->si_addr);
- exit( EXIT_FAILURE );
+ printf("Out of backing pages at %p\n", si->si_addr);
+ exit( EXIT_FAILURE );
}
//copy page
extern "C" {
#endif
void createSharedLibrary(){
-#if !USE_CHECKPOINTING
+#if !USE_MPROTECT_SNAPSHOT
//step 1. create shared memory.
if( sTheRecord ) return;
int fd = shm_open( "/ModelChecker-Snapshotter", O_RDWR | O_CREAT, 0777 ); //universal permissions.
#ifdef __cplusplus
}
#endif
-void initSnapShotLibrary(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions, unsigned int numheappages, MyFuncPtr entryPoint){
-#if USE_CHECKPOINTING
+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);
+ ss.ss_size = SIGSTACKSIZE;
+ ss.ss_flags = 0;
+ sigaltstack(&ss, NULL);
+
struct sigaction sa;
- sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART;
+ sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART | SA_ONSTACK;
sigemptyset( &sa.sa_mask );
sa.sa_sigaction = HandlePF;
if( sigaction( SIGSEGV, &sa, NULL ) == -1 ){
exit(-1);
}
initSnapShotRecord(numbackingpages, numsnapshots, nummemoryregions);
-
+
basemySpace=MYMALLOC((numheappages+1)*PAGESIZE);
void * pagealignedbase=PageAlignAddressUpward(basemySpace);
mySpace = create_mspace_with_base(pagealignedbase, numheappages*PAGESIZE, 1 );
exit(-1);
}
createSharedLibrary();
-#if SSDEBUG
- starttime = &(sTheRecord->startTimeGlobal);
- gettimeofday( starttime, NULL );
-#endif
+
//step 2 setup the stack context.
-
+
int alreadySwapped = 0;
getcontext( &savedSnapshotContext );
if( !alreadySwapped ){
makecontext( &newContext, entryPoint, 0 );
swapcontext( &swappedContext, &newContext );
}
-
+
//add the code to take a snapshot here...
//to return to user process, do a second swapcontext...
pid_t forkedID = 0;
while( !sTheRecord->mbFinalize ){
sTheRecord->currSnapShotID=snapshotid+1;
forkedID = fork();
- if( 0 == forkedID ){
+ if( 0 == forkedID ){
ucontext_t currentContext;
#if 0
int dbg = 0;
if( swapContext )
swapcontext( ¤tContext, &( sTheRecord->mContextToRollback ) );
else{
- swapcontext( ¤tContext, &savedUserSnapshotContext );
+ swapcontext( ¤tContext, &savedUserSnapshotContext );
}
} else {
int status;
sprintf( mesg, "The process id of child is %d and the process id of this process is %d and snapshot id is %d", forkedID, getpid(), snapshotid );
DumpIntoLog( "ModelSnapshot", mesg );
#endif
- do {
+ do {
retVal=waitpid( forkedID, &status, 0 );
} while( -1 == retVal && errno == EINTR );
}
}
}
-
+
#endif
}
/* This function assumes that addr is page aligned */
void addMemoryRegionToSnapShot( void * addr, unsigned int numPages) {
-#if USE_CHECKPOINTING
+#if USE_MPROTECT_SNAPSHOT
unsigned int memoryregion=snapshotrecord->lastRegion++;
if (memoryregion==snapshotrecord->maxRegions) {
printf("Exceeded supported number of memory regions!\n");
exit(-1);
}
-
+
snapshotrecord->regionsToSnapShot[ memoryregion ].basePtr=addr;
snapshotrecord->regionsToSnapShot[ memoryregion ].sizeInPages=numPages;
#endif //NOT REQUIRED IN THE CASE OF FORK BASED SNAPSHOTS.
}
//take snapshot
snapshot_id takeSnapshot( ){
-#if USE_CHECKPOINTING
+#if USE_MPROTECT_SNAPSHOT
for(unsigned int region=0; region<snapshotrecord->lastRegion;region++) {
if( mprotect(snapshotrecord->regionsToSnapShot[region].basePtr, snapshotrecord->regionsToSnapShot[region].sizeInPages*sizeof(struct SnapShotPage), PROT_READ ) == -1 ){
perror("mprotect");
printf("Failed to mprotect inside of takeSnapShot\n");
exit(-1);
- }
+ }
}
unsigned int snapshot=snapshotrecord->lastSnapShot++;
if (snapshot==snapshotrecord->maxSnapShots) {
exit(-1);
}
snapshotrecord->snapShots[snapshot].firstBackingPage=snapshotrecord->lastBackingPage;
-
+
return snapshot;
#else
swapcontext( &savedUserSnapshotContext, &savedSnapshotContext );
#endif
}
void rollBack( snapshot_id theID ){
-#if USE_CHECKPOINTING
+#if USE_MPROTECT_SNAPSHOT
std::map< void *, bool, std::less< void * >, MyAlloc< std::pair< const void *, bool > > > duplicateMap;
for(unsigned int region=0; region<snapshotrecord->lastRegion;region++) {
if( mprotect(snapshotrecord->regionsToSnapShot[region].basePtr, snapshotrecord->regionsToSnapShot[region].sizeInPages*sizeof(struct SnapShotPage), PROT_READ | PROT_WRITE ) == -1 ){
perror("mprotect");
printf("Failed to mprotect inside of takeSnapShot\n");
exit(-1);
- }
+ }
}
for(unsigned int page=snapshotrecord->snapShots[theID].firstBackingPage; page<snapshotrecord->lastBackingPage; page++) {
bool oldVal = false;
if( duplicateMap.find( snapshotrecord->backingRecords[page].basePtrOfPage ) != duplicateMap.end() ){
- oldVal = true;
+ oldVal = true;
}
else{
- duplicateMap[ snapshotrecord->backingRecords[page].basePtrOfPage ] = true;
+ duplicateMap[ snapshotrecord->backingRecords[page].basePtrOfPage ] = true;
}
if( !oldVal ){
memcpy(snapshotrecord->backingRecords[page].basePtrOfPage, &snapshotrecord->backingStore[page], sizeof(struct SnapShotPage));
if( !sTemp ){
sTemp = 1;
#if SSDEBUG
- DumpIntoLog( "ModelSnapshot", "Invoked rollback" );
+ DumpIntoLog( "ModelSnapshot", "Invoked rollback" );
#endif
exit( 0 );
}
}
void finalize(){
-#if !USE_CHECKPOINTING
+#if !USE_MPROTECT_SNAPSHOT
sTheRecord->mbFinalize = true;
#endif
}
#ifndef _SNAPSHOT_H
#define _SNAPSHOT_H
+
+#include "snapshot-interface.h"
+
#define PAGESIZE 4096
-#define USE_CHECKPOINTING 1
+/* If USE_MPROTECT_SNAPSHOT=1, then snapshot by using mmap() and mprotect()
+ If USE_MPROTECT_SNAPSHOT=0, then snapshot by using fork() */
+#define USE_MPROTECT_SNAPSHOT 1
-typedef unsigned int snapshot_id;
-typedef void (*MyFuncPtr)();
-void initSnapShotLibrary(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions, unsigned int numheappages, MyFuncPtr entryPoint);
+/* Size of signal stack */
+#define SIGSTACKSIZE 16384
void addMemoryRegionToSnapShot( void * ptr, unsigned int numPages );
#define SHARED_MEMORY_DEFAULT ( 100 * ( 1 << 20 ) ) // 100mb for the shared memory
#define STACK_SIZE_DEFAULT ( ( 1 << 20 ) * 20 ) //20 mb out of the above 100 mb for my stack.
-#if USE_CHECKPOINTING
+#if USE_MPROTECT_SNAPSHOT
//Each snapshotrecord lists the firstbackingpage that must be written to revert to that snapshot
struct SnapShotRecord {
unsigned int firstBackingPage;
snapshot_id mIDToRollback;
ucontext_t mContextToRollback;
snapshot_id currSnapShotID;
-#if SSDEBUG
-struct timeval startTimeGlobal;
-#endif
volatile bool mbFinalize;
};
extern struct Snapshot_t * sTheRecord;
static void * stack_allocate(size_t size)
{
- return userMalloc(size);
+ return malloc(size);
}
static void stack_free(void *stack)
{
- userFree(stack);
+ free(stack);
}
Thread * thread_current(void)
THREAD_COMPLETED
} thread_state;
+class ModelAction;
+
class Thread {
public:
Thread(thrd_t *t, void (*func)(void *), void *a);
thrd_t get_thrd_t() { return *user_thread; }
Thread * get_parent() { return parent; }
+ void set_creation(ModelAction *act) { creation = act; }
+ ModelAction * get_creation() { return creation; }
+
friend void thread_startup();
- MEMALLOC
+ SNAPSHOTALLOC
private:
int create_context();
Thread *parent;
+ ModelAction *creation;
void (*start_routine)(void *);
void *arg;
projects / c11tester.git / commitdiff