Change initialize a bit
authorweiyu <weiyuluo1232@gmail.com>
Sat, 5 Sep 2020 00:24:00 +0000 (17:24 -0700)
committerweiyu <weiyuluo1232@gmail.com>
Sat, 5 Sep 2020 00:24:00 +0000 (17:24 -0700)
cmodelint.cc
model.cc
model.h
mymemory.cc
mymemory.h
pipe.cc
pthread.cc
snapshot-interface.h
snapshot.cc

index 0b9668d..205ef50 100644 (file)
@@ -15,39 +15,31 @@ memory_order orders[6] = {
        memory_order_release, memory_order_acq_rel, memory_order_seq_cst,
 };
 
        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) {
 /* ---  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) {
        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) {
        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) {
        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) { \
        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)); \
        }
 
                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) { \
 // 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();           \
                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) { \
 // 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();           \
                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) { \
 // 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();           \
                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) { \
 // 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();           \
                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
 
 void cds_func_entry(const char * funcName) {
 #ifdef NEWFUZZER
-       ensureModel();
+       createModelIfNotExist();
        thread_id_t tid = thread_current_id();
        uint32_t func_id;
 
        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
 
 void cds_func_exit(const char * funcName) {
 #ifdef NEWFUZZER
-       ensureModel();
+       createModelIfNotExist();
        thread_id_t tid = thread_current_id();
        uint32_t func_id;
 
        thread_id_t tid = thread_current_id();
        uint32_t func_id;
 
index 8f97476..2aa31e9 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -54,7 +54,14 @@ void install_handler() {
                perror("sigaction(SIGSEGV)");
                exit(EXIT_FAILURE);
        }
                perror("sigaction(SIGSEGV)");
                exit(EXIT_FAILURE);
        }
+}
 
 
+void createModelIfNotExist() {
+       if (!model) {
+               snapshot_system_init(100000);
+               model = new ModelChecker();
+               model->startChecker();
+       }
 }
 
 /** @brief Constructor */
 }
 
 /** @brief Constructor */
diff --git a/model.h b/model.h
index fd65c05..e35457e 100644 (file)
--- 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);
 extern ModelChecker *model;
 void parse_options(struct model_params *params);
 void install_trace_analyses(ModelExecution *execution);
+void createModelIfNotExist();
 
 #endif /* __MODEL_H__ */
 
 #endif /* __MODEL_H__ */
index efc36e9..dd22909 100644 (file)
 size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 };
 int nextRequest = 0;
 int howManyFreed = 0;
 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)
 {
 
 /** 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)
 {
        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)
 {
        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);
 }
 
        return mspace_realloc(sStaticSpace, ptr, size);
 }
 
index bb31392..6fb2992 100644 (file)
@@ -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);
 
 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);
 
 void * Thread_malloc(size_t size);
 void Thread_free(void *ptr);
 
diff --git a/pipe.cc b/pipe.cc
index 95a9a43..1f451dc 100644 (file)
--- a/pipe.cc
+++ b/pipe.cc
@@ -8,11 +8,7 @@
 static int (*pipe_init_p)(int filep[2]) = NULL;
 
 int pipe(int fildes[2]) {
 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();
        if (!pipe_init_p) {
                pipe_init_p = (int (*)(int fildes[2]))dlsym(RTLD_NEXT, "pipe");
                char *error = dlerror();
index e64cd13..20999ae 100644 (file)
 
 int pthread_create(pthread_t *t, const pthread_attr_t * attr,
                                                                         pthread_start_t start_routine, void * arg) {
 
 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 */
        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) {
 }
 
 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);
        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) {
 }
 
 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
        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) {
 }
 
 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;
        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
 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
        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() {
 }
 
 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();
 }
        Thread* th = model->get_current_thread();
        return (pthread_t)th->get_id();
 }
index 548ae05..d0fcbb7 100644 (file)
@@ -10,9 +10,7 @@
 typedef unsigned int snapshot_id;
 typedef void (*VoidFuncPtr)();
 
 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);
 void startExecution();
 snapshot_id take_snapshot();
 void snapshot_roll_back(snapshot_id theSnapShot);
index 0d38edc..1f0cf35 100644 (file)
@@ -106,6 +106,7 @@ static void createSharedMemory()
        fork_snap->mStackSize = STACK_SIZE_DEFAULT;
        fork_snap->mIDToRollback = -1;
        fork_snap->currSnapShotID = 0;
        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);
 }
 
        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();
 {
        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.
  */
  * @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() {
 }
 
 void startExecution() {