Change initialize a bit

diff --git a/cmodelint.cc b/cmodelint.cc
index 0b9668d16a56c96f20322205e4a7a4cdb599fca4..205ef507a060f9bb392070a358332de4ccc62cb4 100644 (file)
--- 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 8f974762043065de618aea980d89ac2321ec9dcd..2aa31e9b596d9e46f5b147536134e3648bc9d498 100644 (file)
--- 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 fd65c0503b0ecd32ff16536a601a12c5fb9fab68..e35457e1eea77c9dd653db444303d6284caa7279 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);
+void createModelIfNotExist();
 
 #endif /* __MODEL_H__ */

diff --git a/mymemory.cc b/mymemory.cc
index efc36e98c8be4b607bb0927936beed7e6769712f..dd22909c9bb31a32405070cb2e6873ac5d584e95 100644 (file)
--- 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 bb313928fbab6a04138afea45cbef9face71b1f3..6fb2992bd4e4e93abce31d6002957830575c7081 100644 (file)
--- 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 95a9a43970f524d9be415e45776303cd0b50bf30..1f451dcbe41ee85473494bad7896206594a57afc 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]) {
-       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 e64cd134b91f4b4aebf0723adc78e283154b7c50..20999aea4899c61f6fb20e0f6707d29e16737dde 100644 (file)
--- 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 548ae05335ac89ed6cd9c1cd530b9eeb5b3fda49..d0fcbb70fc9e137daae11d04f5443310d101a319 100644 (file)
--- 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 0d38edc1c1cbc7ee0b34d393aeee50baa2e05ee8..1f0cf352d2e214c0e5218818addb29fab2a37330 100644 (file)
--- 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() {