+++ /dev/null
-#ifndef __ACTION_H__
-#define __ACTION_H__
-
-#include <list>
-#include "threads.h"
-#include "libatomic.h"
-#include "mymemory.h"
-#define VALUE_NONE -1
-
-typedef enum action_type {
- THREAD_CREATE,
- THREAD_YIELD,
- THREAD_JOIN,
- ATOMIC_READ,
- ATOMIC_WRITE
-} action_type_t;
-
-/* Forward declaration */
-class TreeNode;
-
-class ModelAction {
-public:
- ModelAction(action_type_t type, memory_order order, void *loc, int value);
- void print(void);
-
- thread_id_t get_tid() { return tid; }
- action_type get_type() { return type; }
- memory_order get_mo() { return order; }
- void * get_location() { return location; }
- int get_seq_number() { return seq_number; }
-
- TreeNode * get_node() { return node; }
- void set_node(TreeNode *n) { node = n; }
-
- bool is_read();
- bool is_write();
- bool is_acquire();
- bool is_release();
- bool same_var(ModelAction *act);
- bool same_thread(ModelAction *act);
- bool is_dependent(ModelAction *act);
- MEMALLOC
-private:
- action_type type;
- memory_order order;
- void *location;
- thread_id_t tid;
- int value;
- TreeNode *node;
- int seq_number;
-};
-
-typedef std::list<class ModelAction *> action_list_t;
-
-#endif /* __ACTION_H__ */
+++ /dev/null
-#ifndef __COMMON_H__
-#define __COMMON_H__
-
-#include <stdio.h>
-#include <stdlib.h>
-
-//#define CONFIG_DEBUG
-
-#ifdef CONFIG_DEBUG
-#define DEBUG(fmt, ...) do { printf("*** %25s(): line %-4d *** " fmt, __func__, __LINE__, ##__VA_ARGS__); } while (0)
-#define DBG() DEBUG("\n");
-#define DBG_ENABLED() (1)
-#else
-#define DEBUG(fmt, ...)
-#define DBG()
-#define DBG_ENABLED() (0)
-#endif
-
-#define ASSERT(expr) \
-do { \
- if (!(expr)) { \
- fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \
- exit(1); \
- } \
-} while (0);
-
-
-void * myMalloc(size_t size);
-void myFree(void *ptr);
-
-#define userMalloc(size) malloc(size)
-#define userFree(ptr) free(ptr)
-
-#endif /* __COMMON_H__ */
+++ /dev/null
-#include <stdio.h>
-
-#include "model.h"
-#include "action.h"
-#include "tree.h"
-#include "schedule.h"
-#include "snapshot-interface.h"
-#undef DEBUG
-#include "common.h"
-
-#define INITIAL_THREAD_ID 0
-
-class Backtrack {
-public:
- Backtrack(ModelAction *d, action_list_t *t) {
- diverge = d;
- actionTrace = t;
- iter = actionTrace->begin();
- }
- ModelAction * get_diverge() { return diverge; }
- action_list_t * get_trace() { return actionTrace; }
- void advance_state() { iter++; }
- ModelAction * get_state() {
- return iter == actionTrace->end() ? NULL : *iter;
- }
-private:
- ModelAction *diverge;
- action_list_t *actionTrace;
- /* points to position in actionTrace as we replay */
- action_list_t::iterator iter;
-};
-
-ModelChecker *model;
-
-void free_action_list(action_list_t *list)
-{
- action_list_t::iterator it;
- for (it = list->begin(); it != list->end(); it++)
- delete (*it);
- delete list;
-}
-
-ModelChecker::ModelChecker()
-{
- /* First thread created will have id INITIAL_THREAD_ID */
- this->next_thread_id = INITIAL_THREAD_ID;
- used_sequence_numbers = 0;
- /* Initialize default scheduler */
- this->scheduler = new Scheduler();
-
- num_executions = 0;
- this->current_action = NULL;
- this->exploring = NULL;
- this->nextThread = THREAD_ID_T_NONE;
-
- rootNode = new TreeNode();
- currentNode = rootNode;
- action_trace = new action_list_t();
- global_vec = snapshot_utils::ReturnGlobalSegmentsToSnapshot();
-}
-
-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++)
- delete (*it).second;
- thread_map.clear();
-
- free_action_list(action_trace);
-
- delete this->scheduler;
- delete rootNode;
-}
-
-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();
- action_trace = new action_list_t();
- currentNode = rootNode;
- current_action = NULL;
- next_thread_id = INITIAL_THREAD_ID;
- used_sequence_numbers = 0;
- /* scheduler reset ? */
-}
-
-thread_id_t ModelChecker::get_next_id()
-{
- return next_thread_id++;
-}
-
-int ModelChecker::get_next_seq_num()
-{
- return ++used_sequence_numbers;
-}
-
-Thread * ModelChecker::schedule_next_thread()
-{
- Thread *t;
- if (nextThread == THREAD_ID_T_NONE)
- return NULL;
- t = thread_map[id_to_int(nextThread)];
-
- ASSERT(t != NULL);
-
- return t;
-}
-
-/*
- * get_next_replay_thread() - Choose the next thread in the replay sequence
- *
- * If we've reached the 'diverge' point, then we pick a thread from the
- * backtracking set.
- * Otherwise, we simply return the next thread in the sequence.
- */
-thread_id_t ModelChecker::get_next_replay_thread()
-{
- ModelAction *next;
- thread_id_t tid;
-
- next = exploring->get_state();
-
- if (next == exploring->get_diverge()) {
- TreeNode *node = next->get_node();
-
- /* Reached divergence point; discard our current 'exploring' */
- DEBUG("*** Discard 'Backtrack' object ***\n");
- tid = node->getNextBacktrack();
- delete exploring;
- exploring = NULL;
- } else {
- tid = next->get_tid();
- }
- DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
- return tid;
-}
-
-thread_id_t ModelChecker::advance_backtracking_state()
-{
- /* Have we completed exploring the preselected path? */
- if (exploring == NULL)
- return THREAD_ID_T_NONE;
-
- /* Else, we are trying to replay an execution */
- exploring->advance_state();
-
- ASSERT(exploring->get_state() != NULL);
-
- return get_next_replay_thread();
-}
-
-bool ModelChecker::next_execution()
-{
- DBG();
-
- num_executions++;
- print_summary();
- if ((exploring = model->get_next_backtrack()) == NULL)
- return false;
-
- if (DBG_ENABLED()) {
- printf("Next execution will diverge at:\n");
- exploring->get_diverge()->print();
- print_list(exploring->get_trace());
- }
-
- model->reset_to_initial_state();
- nextThread = get_next_replay_thread();
- return true;
-}
-
-ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
-{
- action_type type = act->get_type();
-
- switch (type) {
- case THREAD_CREATE:
- case THREAD_YIELD:
- case THREAD_JOIN:
- return NULL;
- case ATOMIC_READ:
- case ATOMIC_WRITE:
- default:
- break;
- }
- /* linear search: from most recent to oldest */
- action_list_t::reverse_iterator rit;
- for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
- ModelAction *prev = *rit;
- if (act->is_dependent(prev))
- return prev;
- }
- return NULL;
-}
-
-void ModelChecker::set_backtracking(ModelAction *act)
-{
- ModelAction *prev;
- TreeNode *node;
- Thread *t = get_thread(act->get_tid());
-
- prev = get_last_conflict(act);
- if (prev == NULL)
- return;
-
- node = prev->get_node();
-
- while (t && !node->is_enabled(t))
- t = t->get_parent();
-
- /* Check if this has been explored already */
- if (node->hasBeenExplored(t->get_id()))
- return;
- /* If this is a new backtracking point, mark the tree */
- if (node->setBacktrack(t->get_id()) != 0)
- return;
-
- DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
- prev->get_tid(), t->get_id());
- if (DBG_ENABLED()) {
- prev->print();
- act->print();
- }
-
- Backtrack *back = new Backtrack(prev, action_trace);
- backtrack_list.push_back(back);
-}
-
-Backtrack * ModelChecker::get_next_backtrack()
-{
- Backtrack *next;
- if (backtrack_list.empty())
- return NULL;
- next = backtrack_list.back();
- backtrack_list.pop_back();
- return next;
-}
-
-void ModelChecker::check_current_action(void)
-{
- ModelAction *next = this->current_action;
-
- if (!next) {
- DEBUG("trying to push NULL action...\n");
- return;
- }
- current_action = NULL;
- nextThread = advance_backtracking_state();
- next->set_node(currentNode);
- set_backtracking(next);
- currentNode = currentNode->explore_child(next);
- this->action_trace->push_back(next);
-}
-
-void ModelChecker::print_summary(void)
-{
- printf("\n");
- printf("Number of executions: %d\n", num_executions);
- printf("Total nodes created: %d\n", TreeNode::getTotalNodes());
-
- scheduler->print();
-
- print_list(action_trace);
- printf("\n");
-
-}
-
-void ModelChecker::print_list(action_list_t *list)
-{
- action_list_t::iterator it;
-
- printf("---------------------------------------------------------------------\n");
- printf("Trace:\n");
-
- for (it = list->begin(); it != list->end(); it++) {
- (*it)->print();
- }
- printf("---------------------------------------------------------------------\n");
-}
-
-int ModelChecker::add_thread(Thread *t)
-{
- thread_map[id_to_int(t->get_id())] = t;
- scheduler->add_thread(t);
- return 0;
-}
-
-void ModelChecker::remove_thread(Thread *t)
-{
- scheduler->remove_thread(t);
-}
-
-int ModelChecker::switch_to_master(ModelAction *act)
-{
- Thread *old;
-
- DBG();
- old = thread_current();
- set_current_action(act);
- old->set_state(THREAD_READY);
- return Thread::swap(old, get_system_context());
-}
+++ /dev/null
-#!/bin/sh
-
-export LD_LIBRARY_PATH=.
-./model
+++ /dev/null
-#include "threads.h"
-#include "schedule.h"
-#include "common.h"
-#include "model.h"
-
-void Scheduler::add_thread(Thread *t)
-{
- DEBUG("thread %d\n", t->get_id());
- readyList.push_back(t);
-}
-
-void Scheduler::remove_thread(Thread *t)
-{
- if (current == t)
- current = NULL;
- else
- readyList.remove(t);
-}
-
-Thread * Scheduler::next_thread(void)
-{
- Thread *t = model->schedule_next_thread();
-
- if (t != NULL) {
- current = t;
- readyList.remove(t);
- } else if (readyList.empty()) {
- t = NULL;
- } else {
- t = readyList.front();
- current = t;
- readyList.pop_front();
- }
-
- print();
-
- return t;
-}
-
-Thread * Scheduler::get_current_thread(void)
-{
- return current;
-}
-
-void Scheduler::print()
-{
- if (current)
- DEBUG("Current thread: %d\n", current->get_id());
- else
- DEBUG("No current thread\n");
- DEBUG("Num. threads in ready list: %zu\n", readyList.size());
-
- std::list<Thread *, MyAlloc< Thread * > >::iterator it;
- for (it = readyList.begin(); it != readyList.end(); it++)
- DEBUG("In ready list: thread %d\n", (*it)->get_id());
-}
+++ /dev/null
-#ifndef __SCHEDULE_H__
-#define __SCHEDULE_H__
-
-#include <list>
-#include "mymemory.h"
-
-/* Forward declaration */
-class Thread;
-
-class Scheduler {
-public:
- void add_thread(Thread *t);
- void remove_thread(Thread *t);
- Thread * next_thread(void);
- Thread * get_current_thread(void);
- void print();
- MEMALLOC
-private:
- std::list<Thread *> readyList;
- Thread *current;
-};
-
-#endif /* __SCHEDULE_H__ */
+++ /dev/null
-#include <inttypes.h>
-#include <sys/mman.h>
-#include <unistd.h>
-#include <signal.h>
-#include <stdlib.h>
-#include <map>
-#include <set>
-#include <cstring>
-#include <cstdio>
-#include "snapshot.h"
-#include "snapshotimp.h"
-#include "mymemory.h"
-#include <fcntl.h>
-#include <assert.h>
-#include <pthread.h>
-#include <semaphore.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
-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 DEBUG
-struct timeval *starttime = NULL;
-#endif
-void DumpIntoLog( const char * filename, const char * message ){
-#if DEBUG
- 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 );
- fflush( myFile );
- fclose( myFile );
- myFile = NULL;
-#endif
-}
-static ucontext_t savedSnapshotContext;
-static ucontext_t savedUserSnapshotContext;
-static int snapshotid = 0;
-/* Initialize snapshot data structure */
-#if USE_CHECKPOINTING
-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);
- snapshotrecord->backingStoreBasePtr= ( struct SnapShotPage * )MYMALLOC( sizeof( struct SnapShotPage ) * (numbackingpages + 1) );
- //Page align the backingstorepages
- snapshotrecord->backingStore=( struct SnapShotPage * )ReturnPageAlignedAddress((void*) ((uintptr_t)(snapshotrecord->backingStoreBasePtr)+sizeof(struct SnapShotPage)-1));
- snapshotrecord->backingRecords=( struct BackingPageRecord * )MYMALLOC(sizeof(struct BackingPageRecord)*numbackingpages);
- snapshotrecord->snapShots= ( struct SnapShotRecord * )MYMALLOC(sizeof(struct SnapShotRecord)*numsnapshots);
- snapshotrecord->lastSnapShot=0;
- snapshotrecord->lastBackingPage=0;
- snapshotrecord->lastRegion=0;
- snapshotrecord->maxRegions=nummemoryregions;
- snapshotrecord->maxBackingPages=numbackingpages;
- snapshotrecord->maxSnapShots=numsnapshots;
-}
-#endif //nothing to initialize for the fork based snapshotting.
-
-void HandlePF( int sig, siginfo_t *si, void * unused){
-#if USE_CHECKPOINTING
- if( si->si_code == SEGV_MAPERR ){
- printf("Real Fault at %llx\n", ( long long )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 );
- }
-
- //copy page
- memcpy(&(snapshotrecord->backingStore[backingpage]), addr, sizeof(struct SnapShotPage));
- //remember where to copy page back to
- snapshotrecord->backingRecords[backingpage].basePtrOfPage=addr;
- //set protection to read/write
- mprotect( addr, sizeof(struct SnapShotPage), PROT_READ | PROT_WRITE );
-#endif //nothing to handle for non snapshotting case.
-}
-
-//Return a page aligned address for the address being added
-//as a side effect the numBytes are also changed.
-void * ReturnPageAlignedAddress(void * addr) {
- return (void *)(((uintptr_t)addr)&~(PAGESIZE-1));
-}
-#ifdef __cplusplus
-extern "C" {
-#endif
-void createSharedLibrary(){
-#if !USE_CHECKPOINTING
- //step 1. create shared memory.
- if( sTheRecord ) return;
- int fd = shm_open( "/ModelChecker-Snapshotter", O_RDWR | O_CREAT, 0777 ); //universal permissions.
- if( -1 == fd ) FAILURE("shm_open");
- if( -1 == ftruncate( fd, ( size_t )SHARED_MEMORY_DEFAULT + ( size_t )STACK_SIZE_DEFAULT ) ) FAILURE( "ftruncate" );
- char * memMapBase = ( char * ) mmap( 0, ( size_t )SHARED_MEMORY_DEFAULT + ( size_t )STACK_SIZE_DEFAULT, PROT_READ | PROT_WRITE, MAP_SHARED, fd, 0 );
- if( MAP_FAILED == memMapBase ) FAILURE("mmap");
- sTheRecord = ( struct Snapshot_t * )memMapBase;
- sTheRecord->mSharedMemoryBase = memMapBase + sizeof( struct Snapshot_t );
- sTheRecord->mStackBase = ( char * )memMapBase + ( size_t )SHARED_MEMORY_DEFAULT;
- sTheRecord->mStackSize = STACK_SIZE_DEFAULT;
- sTheRecord->mIDToRollback = -1;
- sTheRecord->currSnapShotID = 0;
-#endif
-}
-#ifdef __cplusplus
-}
-#endif
-void initSnapShotLibrary(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions , MyFuncPtr entryPoint){
-#if USE_CHECKPOINTING
- struct sigaction sa;
- sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART;
- sigemptyset( &sa.sa_mask );
- sa.sa_sigaction = HandlePF;
- if( sigaction( SIGSEGV, &sa, NULL ) == -1 ){
- printf("SIGACTION CANNOT BE INSTALLED\n");
- exit(-1);
- }
- initSnapShotRecord(numbackingpages, numsnapshots, nummemoryregions);
- entryPoint();
-#else
- //add a signal to indicate that the process is going to terminate.
- struct sigaction sa;
- sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART;
- sigemptyset( &sa.sa_mask );
- sa.sa_sigaction = HandlePF;
- if( sigaction( SIGUSR1, &sa, NULL ) == -1 ){
- printf("SIGACTION CANNOT BE INSTALLED\n");
- exit(-1);
- }
- createSharedLibrary();
- #if DEBUG
- starttime = &(sTheRecord->startTimeGlobal);
- gettimeofday( starttime, NULL );
-#endif
- //step 2 setup the stack context.
-
- int alreadySwapped = 0;
- getcontext( &savedSnapshotContext );
- if( !alreadySwapped ){
- alreadySwapped = 1;
- ucontext_t currentContext, swappedContext, newContext;
- getcontext( &newContext );
- newContext.uc_stack.ss_sp = sTheRecord->mStackBase;
- newContext.uc_stack.ss_size = STACK_SIZE_DEFAULT;
- newContext.uc_link = ¤tContext;
- 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;
- snapshotid = sTheRecord->currSnapShotID;
- bool swapContext = false;
- while( !sTheRecord->mbFinalize ){
- sTheRecord->currSnapShotID=snapshotid+1;
- forkedID = fork();
- if( 0 == forkedID ){
- ucontext_t currentContext;
-#if 0
- int dbg = 0;
- while( !dbg );
-#endif
- if( swapContext )
- swapcontext( ¤tContext, &( sTheRecord->mContextToRollback ) );
- else{
- swapcontext( ¤tContext, &savedUserSnapshotContext );
- }
- } else {
- int status;
- int retVal;
-#if DEBUG
- char mesg[ 1024 ] = { 0 };
- 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 {
- retVal=waitpid( forkedID, &status, 0 );
- } while( -1 == retVal && errno == EINTR );
-
- if( sTheRecord->mIDToRollback != snapshotid )
- exit(0);
- else{
- swapContext = true;
- }
- }
- }
-
-#endif
-}
-/* This function assumes that addr is page aligned */
-void addMemoryRegionToSnapShot( void * addr, unsigned int numPages) {
-#if USE_CHECKPOINTING
- 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
- 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 ){
- printf("Failed to mprotect inside of takeSnapShot\n");
- exit(-1);
- }
- }
- unsigned int snapshot=snapshotrecord->lastSnapShot++;
- if (snapshot==snapshotrecord->maxSnapShots) {
- printf("Out of snapshots\n");
- exit(-1);
- }
- snapshotrecord->snapShots[snapshot].firstBackingPage=snapshotrecord->lastBackingPage;
-
- return snapshot;
-#else
- swapcontext( &savedUserSnapshotContext, &savedSnapshotContext );
- return snapshotid;
-#endif
-}
-void rollBack( snapshot_id theID ){
-#if USE_CHECKPOINTING
- 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 ){
- 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;
- }
- else{
- duplicateMap[ snapshotrecord->backingRecords[page].basePtrOfPage ] = true;
- }
- if( !oldVal ){
- memcpy(snapshotrecord->backingRecords[page].basePtrOfPage, &snapshotrecord->backingStore[page], sizeof(struct SnapShotPage));
- }
- }
- snapshotrecord->lastSnapShot=theID;
- snapshotrecord->lastBackingPage=snapshotrecord->snapShots[theID].firstBackingPage;
- takeSnapshot(); //Make sure current snapshot is still good...All later ones are cleared
-#else
- sTheRecord->mIDToRollback = theID;
- int sTemp = 0;
- getcontext( &sTheRecord->mContextToRollback );
- if( !sTemp ){
- sTemp = 1;
-#if DEBUG
- DumpIntoLog( "ModelSnapshot", "Invoked rollback" );
-#endif
- exit( 0 );
- }
-#endif
-}
-
-void finalize(){
-#if !USE_CHECKPOINTING
- sTheRecord->mbFinalize = true;
-#endif
-}
-
+++ /dev/null
-#include <stdlib.h>
-
-#include "libthreads.h"
-#include "schedule.h"
-#include "common.h"
-#include "threads.h"
-
-/* global "model" object */
-#include "model.h"
-
-#define STACK_SIZE (1024 * 1024)
-
-static void * stack_allocate(size_t size)
-{
- return userMalloc(size);
-}
-
-static void stack_free(void *stack)
-{
- userFree(stack);
-}
-
-Thread * thread_current(void)
-{
- return model->scheduler->get_current_thread();
-}
-
-int Thread::create_context()
-{
- int ret;
-
- ret = getcontext(&context);
- if (ret)
- return ret;
-
- /* Initialize new managed context */
- stack = stack_allocate(STACK_SIZE);
- context.uc_stack.ss_sp = stack;
- context.uc_stack.ss_size = STACK_SIZE;
- context.uc_stack.ss_flags = 0;
- context.uc_link = model->get_system_context();
- makecontext(&context, start_routine, 1, arg);
-
- return 0;
-}
-
-int Thread::swap(Thread *t, ucontext_t *ctxt)
-{
- return swapcontext(&t->context, ctxt);
-}
-
-int Thread::swap(ucontext_t *ctxt, Thread *t)
-{
- return swapcontext(ctxt, &t->context);
-}
-
-void Thread::complete()
-{
- if (state != THREAD_COMPLETED) {
- DEBUG("completed thread %d\n", get_id());
- state = THREAD_COMPLETED;
- if (stack)
- stack_free(stack);
- }
-}
-
-void * Thread::operator new(size_t size) {
- return userMalloc(size);
-}
-
-void Thread::operator delete(void *ptr) {
- userFree(ptr);
-}
-
-Thread::Thread(thrd_t *t, void (*func)(), void *a) {
- int ret;
-
- user_thread = t;
- start_routine = func;
- arg = a;
-
- /* Initialize state */
- ret = create_context();
- if (ret)
- printf("Error in create_context\n");
-
- state = THREAD_CREATED;
- id = model->get_next_id();
- *user_thread = id;
- parent = thread_current();
-}
-
-Thread::~Thread()
-{
- complete();
- model->remove_thread(this);
-}
-
-thread_id_t Thread::get_id()
-{
- return id;
-}
+++ /dev/null
-#ifndef __THREADS_H__
-#define __THREADS_H__
-
-#include <ucontext.h>
-#include "mymemory.h"
-#include "libthreads.h"
-
-typedef int thread_id_t;
-
-#define THREAD_ID_T_NONE -1
-
-typedef enum thread_state {
- THREAD_CREATED,
- THREAD_RUNNING,
- THREAD_READY,
- THREAD_COMPLETED
-} thread_state;
-
-class Thread {
-public:
- Thread(thrd_t *t, void (*func)(), void *a);
- ~Thread();
- void complete();
-
- static int swap(ucontext_t *ctxt, Thread *t);
- static int swap(Thread *t, ucontext_t *ctxt);
-
- thread_state get_state() { return state; }
- void set_state(thread_state s) { state = s; }
- thread_id_t get_id();
- thrd_t get_thrd_t() { return *user_thread; }
- Thread * get_parent() { return parent; }
- MEMALLOC
-private:
- int create_context();
- Thread *parent;
-
- void (*start_routine)();
- void *arg;
- ucontext_t context;
- void *stack;
- thrd_t *user_thread;
- thread_id_t id;
- thread_state state;
-};
-
-Thread * thread_current();
-
-static inline thread_id_t thrd_to_id(thrd_t t)
-{
- return t;
-}
-
-static inline thread_id_t int_to_id(int i)
-{
- return i;
-}
-
-static inline int id_to_int(thread_id_t id)
-{
- return id;
-}
-
-#endif /* __THREADS_H__ */
+++ /dev/null
-#include "tree.h"
-#include "action.h"
-
-int TreeNode::totalNodes = 0;
-
-TreeNode::TreeNode(TreeNode *par, ModelAction *act)
-{
- TreeNode::totalNodes++;
- this->parent = par;
- if (!parent) {
- num_threads = 1;
- } else {
- num_threads = parent->num_threads;
- if (act && act->get_type() == THREAD_CREATE)
- num_threads++;
- }
-}
-
-TreeNode::~TreeNode() {
- std::map<int, class TreeNode *, std::less< int >, MyAlloc< std::pair< const int, class TreeNode * > > >::iterator it;
-
- for (it = children.begin(); it != children.end(); it++)
- delete it->second;
-}
-
-TreeNode * TreeNode::explore_child(ModelAction *act)
-{
- TreeNode *n;
- std::set<int>::iterator it;
- thread_id_t id = act->get_tid();
- int i = id_to_int(id);
-
- if (!hasBeenExplored(id)) {
- n = new TreeNode(this, act);
- children[i] = n;
- } else {
- n = children[i];
- }
- if ((it = backtrack.find(i)) != backtrack.end())
- backtrack.erase(it);
-
- return n;
-}
-
-int TreeNode::setBacktrack(thread_id_t id)
-{
- int i = id_to_int(id);
- if (backtrack.find(i) != backtrack.end())
- return 1;
- backtrack.insert(i);
- return 0;
-}
-
-thread_id_t TreeNode::getNextBacktrack()
-{
- if (backtrack.empty())
- return THREAD_ID_T_NONE;
- return int_to_id(*backtrack.begin());
-}
-
-TreeNode * TreeNode::getRoot()
-{
- if (parent)
- return parent->getRoot();
- return this;
-}
-
-bool TreeNode::is_enabled(Thread *t)
-{
- return id_to_int(t->get_id()) < num_threads;
-}
+++ /dev/null
-#ifndef __TREE_H__
-#define __TREE_H__
-#include "mymemory.h"
-#include <set>
-#include <map>
-#include <cstddef>
-#include "threads.h"
-
-class ModelAction;
-
-/*
- * An n-ary tree
- *
- * A tree with n possible branches from each node - used for recording the
- * execution paths we've executed / backtracked
- */
-class TreeNode {
-public:
- TreeNode(TreeNode *par = NULL, ModelAction *act = NULL);
- ~TreeNode();
- bool hasBeenExplored(thread_id_t id) { return children.find(id_to_int(id)) != children.end(); }
- TreeNode * explore_child(ModelAction *act);
- thread_id_t getNextBacktrack();
-
- /* Return 1 if already in backtrack, 0 otherwise */
- int setBacktrack(thread_id_t id);
- TreeNode * getRoot();
- static int getTotalNodes() { return TreeNode::totalNodes; }
-
- bool is_enabled(Thread *t);
- MEMALLOC
-private:
- TreeNode *parent;
- std::map<int, class TreeNode *, std::less< int >, MyAlloc< std::pair< const int, class TreeNode * > > > children;
- std::set<int, std::less< int >, MyAlloc< int > > backtrack;
- static int totalNodes;
- int num_threads;
-};
-
-#endif /* __TREE_H__ */
+++ /dev/null
-#include <stdio.h>
-
-#include "libthreads.h"
-#include "libatomic.h"
-
-static void a(atomic_int *obj)
-{
- int i;
- int ret;
-
- for (i = 0; i < 7; i++) {
- printf("Thread %d, loop %d\n", thrd_current(), i);
- switch (i % 2 ) {
- case 1:
- ret = atomic_load(obj);
- printf("Read value: %d\n", ret);
- break;
- case 0:
- atomic_store(obj, i);
- printf("Write value: %d\n", i);
- break;
- }
- }
-}
-
-void user_main()
-{
- thrd_t t1, t2;
- atomic_int obj;
-
- atomic_init(&obj, 0);
-
- printf("Thread %d: creating 2 threads\n", thrd_current());
- thrd_create(&t1, (thrd_start_t)&a, &obj);
- thrd_create(&t2, (thrd_start_t)&a, &obj);
-
- thrd_join(t1);
- thrd_join(t2);
- printf("Thread %d is finished\n", thrd_current());
-}
projects / model-checker.git / commitdiff