From: Brian Demsky Date: Tue, 15 May 2012 17:08:02 +0000 (-0700) Subject: don't check in useless files X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6a76a17766bc7808ad258ee941c0045d58839f25;p=c11tester.git don't check in useless files --- diff --git a/action.h~ b/action.h~ deleted file mode 100644 index 73817c09..00000000 --- a/action.h~ +++ /dev/null @@ -1,55 +0,0 @@ -#ifndef __ACTION_H__ -#define __ACTION_H__ - -#include -#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 action_list_t; - -#endif /* __ACTION_H__ */ diff --git a/common.h~ b/common.h~ deleted file mode 100644 index bb66c3a7..00000000 --- a/common.h~ +++ /dev/null @@ -1,34 +0,0 @@ -#ifndef __COMMON_H__ -#define __COMMON_H__ - -#include -#include - -//#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__ */ diff --git a/model.cc~ b/model.cc~ deleted file mode 100644 index 5ecad250..00000000 --- a/model.cc~ +++ /dev/null @@ -1,305 +0,0 @@ -#include - -#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, 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, 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()); -} diff --git a/run.sh~ b/run.sh~ deleted file mode 100644 index 9c7af2fb..00000000 --- a/run.sh~ +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/sh - -export LD_LIBRARY_PATH=. -./model diff --git a/schedule.cc~ b/schedule.cc~ deleted file mode 100644 index 40f9894e..00000000 --- a/schedule.cc~ +++ /dev/null @@ -1,56 +0,0 @@ -#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 >::iterator it; - for (it = readyList.begin(); it != readyList.end(); it++) - DEBUG("In ready list: thread %d\n", (*it)->get_id()); -} diff --git a/schedule.h~ b/schedule.h~ deleted file mode 100644 index 750bc1d4..00000000 --- a/schedule.h~ +++ /dev/null @@ -1,23 +0,0 @@ -#ifndef __SCHEDULE_H__ -#define __SCHEDULE_H__ - -#include -#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 readyList; - Thread *current; -}; - -#endif /* __SCHEDULE_H__ */ diff --git a/snapshot.cc~ b/snapshot.cc~ deleted file mode 100644 index d07d8015..00000000 --- a/snapshot.cc~ +++ /dev/null @@ -1,285 +0,0 @@ -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include "snapshot.h" -#include "snapshotimp.h" -#include "mymemory.h" -#include -#include -#include -#include -#include -#include -#include -#include -//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; regionlastRegion;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; regionlastRegion;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; pagelastBackingPage; 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 -} - diff --git a/threads.cc~ b/threads.cc~ deleted file mode 100644 index 946b5e4f..00000000 --- a/threads.cc~ +++ /dev/null @@ -1,102 +0,0 @@ -#include - -#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; -} diff --git a/threads.h~ b/threads.h~ deleted file mode 100644 index b592804d..00000000 --- a/threads.h~ +++ /dev/null @@ -1,64 +0,0 @@ -#ifndef __THREADS_H__ -#define __THREADS_H__ - -#include -#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__ */ diff --git a/tree.cc~ b/tree.cc~ deleted file mode 100644 index 9684d7d5..00000000 --- a/tree.cc~ +++ /dev/null @@ -1,71 +0,0 @@ -#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, 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::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; -} diff --git a/tree.h~ b/tree.h~ deleted file mode 100644 index e107a7ef..00000000 --- a/tree.h~ +++ /dev/null @@ -1,40 +0,0 @@ -#ifndef __TREE_H__ -#define __TREE_H__ -#include "mymemory.h" -#include -#include -#include -#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, MyAlloc< std::pair< const int, class TreeNode * > > > children; - std::set, MyAlloc< int > > backtrack; - static int totalNodes; - int num_threads; -}; - -#endif /* __TREE_H__ */ diff --git a/userprog.c~ b/userprog.c~ deleted file mode 100644 index 3f45ac97..00000000 --- a/userprog.c~ +++ /dev/null @@ -1,40 +0,0 @@ -#include - -#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()); -}