From: weiyu Date: Sat, 5 Sep 2020 00:24:00 +0000 (-0700) Subject: Change initialize a bit X-Git-Url: http://demsky.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=7742256df627848c1c375f979f5369a45c92057b Change initialize a bit --- diff --git a/cmodelint.cc b/cmodelint.cc index 0b9668d1..205ef507 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -15,39 +15,31 @@ memory_order orders[6] = { memory_order_release, memory_order_acq_rel, memory_order_seq_cst, }; -static void ensureModel() { - if (!model) { - snapshot_system_init(10000, 1024, 1024, 40000); - model = new ModelChecker(); - model->startChecker(); - } -} - /* --- helper functions --- */ uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldval, int size, const char *position) { - ensureModel(); + createModelIfNotExist(); return model->switch_thread(new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size)); } uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) { - ensureModel(); + createModelIfNotExist(); return model->switch_thread(new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj)); } void model_rmw_action_helper(void *obj, uint64_t val, int atomic_index, const char * position) { - ensureModel(); + createModelIfNotExist(); model->switch_thread(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val)); } void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) { - ensureModel(); + createModelIfNotExist(); model->switch_thread(new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj)); } // cds volatile loads #define VOLATILELOAD(size) \ uint ## size ## _t cds_volatile_load ## size(void * obj, const char * position) { \ - ensureModel(); \ + createModelIfNotExist(); \ return (uint ## size ## _t)model->switch_thread(new ModelAction(ATOMIC_READ, position, memory_order_volatile_load, obj)); \ } @@ -59,7 +51,7 @@ VOLATILELOAD(64) // cds volatile stores #define VOLATILESTORE(size) \ void cds_volatile_store ## size (void * obj, uint ## size ## _t val, const char * position) { \ - ensureModel(); \ + createModelIfNotExist(); \ model->switch_thread(new ModelAction(ATOMIC_WRITE, position, memory_order_volatile_store, obj, (uint64_t) val)); \ *((volatile uint ## size ## _t *)obj) = val; \ thread_id_t tid = thread_current_id(); \ @@ -76,7 +68,7 @@ VOLATILESTORE(64) // cds atomic inits #define CDSATOMICINT(size) \ void cds_atomic_init ## size (void * obj, uint ## size ## _t val, const char * position) { \ - ensureModel(); \ + createModelIfNotExist(); \ model->switch_thread(new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)); \ *((volatile uint ## size ## _t *)obj) = val; \ thread_id_t tid = thread_current_id(); \ @@ -93,7 +85,7 @@ CDSATOMICINT(64) // cds atomic loads #define CDSATOMICLOAD(size) \ uint ## size ## _t cds_atomic_load ## size(void * obj, int atomic_index, const char * position) { \ - ensureModel(); \ + createModelIfNotExist(); \ uint ## size ## _t val = (uint ## size ## _t)model->switch_thread( \ new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj)); \ thread_id_t tid = thread_current_id(); \ @@ -111,7 +103,7 @@ CDSATOMICLOAD(64) // cds atomic stores #define CDSATOMICSTORE(size) \ void cds_atomic_store ## size(void * obj, uint ## size ## _t val, int atomic_index, const char * position) { \ - ensureModel(); \ + createModelIfNotExist(); \ model->switch_thread(new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)); \ *((volatile uint ## size ## _t *)obj) = val; \ thread_id_t tid = thread_current_id(); \ @@ -292,7 +284,7 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) { void cds_func_entry(const char * funcName) { #ifdef NEWFUZZER - ensureModel(); + createModelIfNotExist(); thread_id_t tid = thread_current_id(); uint32_t func_id; @@ -319,7 +311,7 @@ void cds_func_entry(const char * funcName) { void cds_func_exit(const char * funcName) { #ifdef NEWFUZZER - ensureModel(); + createModelIfNotExist(); thread_id_t tid = thread_current_id(); uint32_t func_id; diff --git a/model.cc b/model.cc index 8f974762..2aa31e9b 100644 --- a/model.cc +++ b/model.cc @@ -54,7 +54,14 @@ void install_handler() { perror("sigaction(SIGSEGV)"); exit(EXIT_FAILURE); } +} +void createModelIfNotExist() { + if (!model) { + snapshot_system_init(100000); + model = new ModelChecker(); + model->startChecker(); + } } /** @brief Constructor */ diff --git a/model.h b/model.h index fd65c050..e35457e1 100644 --- a/model.h +++ b/model.h @@ -107,5 +107,6 @@ private: extern ModelChecker *model; void parse_options(struct model_params *params); void install_trace_analyses(ModelExecution *execution); +void createModelIfNotExist(); #endif /* __MODEL_H__ */ diff --git a/mymemory.cc b/mymemory.cc index efc36e98..dd22909c 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -18,29 +18,23 @@ size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 }; int nextRequest = 0; int howManyFreed = 0; -static mspace sStaticSpace = NULL; +mspace sStaticSpace = NULL; /** Non-snapshotting calloc for our use. */ void *model_calloc(size_t count, size_t size) { - if (!sStaticSpace) - sStaticSpace = create_shared_mspace(); return mspace_calloc(sStaticSpace, count, size); } /** Non-snapshotting malloc for our use. */ void *model_malloc(size_t size) { - if (!sStaticSpace) - sStaticSpace = create_shared_mspace(); return mspace_malloc(sStaticSpace, size); } /** Non-snapshotting malloc for our use. */ void *model_realloc(void *ptr, size_t size) { - if (!sStaticSpace) - sStaticSpace = create_shared_mspace(); return mspace_realloc(sStaticSpace, ptr, size); } diff --git a/mymemory.h b/mymemory.h index bb313928..6fb2992b 100644 --- a/mymemory.h +++ b/mymemory.h @@ -57,6 +57,9 @@ void * snapshot_calloc(size_t count, size_t size); void * snapshot_realloc(void *ptr, size_t size); void snapshot_free(void *ptr); +typedef void * mspace; +extern mspace sStaticSpace; + void * Thread_malloc(size_t size); void Thread_free(void *ptr); diff --git a/pipe.cc b/pipe.cc index 95a9a439..1f451dcb 100644 --- a/pipe.cc +++ b/pipe.cc @@ -8,11 +8,7 @@ static int (*pipe_init_p)(int filep[2]) = NULL; int pipe(int fildes[2]) { - if (!model) { - snapshot_system_init(10000, 1024, 1024, 40000); - model = new ModelChecker(); - model->startChecker(); - } + createModelIfNotExist(); if (!pipe_init_p) { pipe_init_p = (int (*)(int fildes[2]))dlsym(RTLD_NEXT, "pipe"); char *error = dlerror(); diff --git a/pthread.cc b/pthread.cc index e64cd134..20999aea 100644 --- a/pthread.cc +++ b/pthread.cc @@ -16,12 +16,7 @@ int pthread_create(pthread_t *t, const pthread_attr_t * attr, pthread_start_t start_routine, void * arg) { - if (!model) { - snapshot_system_init(10000, 1024, 1024, 40000); - model = new ModelChecker(); - model->startChecker(); - } - + createModelIfNotExist(); struct pthread_params params = { start_routine, arg }; /* seq_cst is just a 'don't care' parameter */ @@ -65,12 +60,7 @@ void pthread_exit(void *value_ptr) { } int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t * attr) { - if (!model) { - snapshot_system_init(10000, 1024, 1024, 40000); - model = new ModelChecker(); - model->startChecker(); - } - + createModelIfNotExist(); int mutex_type = PTHREAD_MUTEX_DEFAULT; if (attr != NULL) pthread_mutexattr_gettype(attr, &mutex_type); @@ -84,12 +74,7 @@ int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t * att } int pthread_mutex_lock(pthread_mutex_t *p_mutex) { - if (!model) { - snapshot_system_init(10000, 1024, 1024, 40000); - model = new ModelChecker(); - model->startChecker(); - } - + createModelIfNotExist(); ModelExecution *execution = model->get_execution(); /* to protect the case where PTHREAD_MUTEX_INITIALIZER is used @@ -111,12 +96,7 @@ int pthread_mutex_lock(pthread_mutex_t *p_mutex) { } int pthread_mutex_trylock(pthread_mutex_t *p_mutex) { - if (!model) { - snapshot_system_init(10000, 1024, 1024, 40000); - model = new ModelChecker(); - model->startChecker(); - } - + createModelIfNotExist(); ModelExecution *execution = model->get_execution(); cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex); return m->try_lock() ? 0 : EBUSY; @@ -138,13 +118,7 @@ int pthread_mutex_unlock(pthread_mutex_t *p_mutex) { int pthread_mutex_timedlock (pthread_mutex_t *__restrict p_mutex, const struct timespec *__restrict abstime) { // timedlock just gives the option of giving up the lock, so return and let the scheduler decide which thread goes next - - if (!model) { - snapshot_system_init(10000, 1024, 1024, 40000); - model = new ModelChecker(); - model->startChecker(); - } - + createModelIfNotExist(); ModelExecution *execution = model->get_execution(); /* to protect the case where PTHREAD_MUTEX_INITIALIZER is used @@ -165,12 +139,7 @@ int pthread_mutex_timedlock (pthread_mutex_t *__restrict p_mutex, } pthread_t pthread_self() { - if (!model) { - snapshot_system_init(10000, 1024, 1024, 40000); - model = new ModelChecker(); - model->startChecker(); - } - + createModelIfNotExist(); Thread* th = model->get_current_thread(); return (pthread_t)th->get_id(); } diff --git a/snapshot-interface.h b/snapshot-interface.h index 548ae053..d0fcbb70 100644 --- a/snapshot-interface.h +++ b/snapshot-interface.h @@ -10,9 +10,7 @@ typedef unsigned int snapshot_id; typedef void (*VoidFuncPtr)(); -void snapshot_system_init(unsigned int numbackingpages, - unsigned int numsnapshots, unsigned int nummemoryregions, - unsigned int numheappages); +void snapshot_system_init(unsigned int numheappages); void startExecution(); snapshot_id take_snapshot(); void snapshot_roll_back(snapshot_id theSnapShot); diff --git a/snapshot.cc b/snapshot.cc index 0d38edc1..1f0cf352 100644 --- a/snapshot.cc +++ b/snapshot.cc @@ -106,6 +106,7 @@ static void createSharedMemory() fork_snap->mStackSize = STACK_SIZE_DEFAULT; fork_snap->mIDToRollback = -1; fork_snap->currSnapShotID = 0; + sStaticSpace = create_shared_mspace(); } /** @@ -121,9 +122,7 @@ mspace create_shared_mspace() return create_mspace_with_base((void *)(fork_snap->mSharedMemoryBase), SHARED_MEMORY_DEFAULT - sizeof(*fork_snap), 1); } -static void fork_snapshot_init(unsigned int numbackingpages, - unsigned int numsnapshots, unsigned int nummemoryregions, - unsigned int numheappages) +static void fork_snapshot_init(unsigned int numheappages) { if (!fork_snap) createSharedMemory(); @@ -192,11 +191,9 @@ static void fork_roll_back(snapshot_id theID) * @brief Initializes the snapshot system * @param entryPoint the function that should run the program. */ -void snapshot_system_init(unsigned int numbackingpages, - unsigned int numsnapshots, unsigned int nummemoryregions, - unsigned int numheappages) +void snapshot_system_init(unsigned int numheappages) { - fork_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages); + fork_snapshot_init(numheappages); } void startExecution() {