redo model object initialization

diff --git a/cmodelint.cc b/cmodelint.cc
index 348051a0f7f13fb736baf14f8a24c81bcfdbb4f9..c55b93866c32706d9fdd0937bf17978b7d415f72 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -2,6 +2,7 @@
 #include "model.h"
 #include "action.h"
 #include "cmodelint.h"
+#include "snapshot-interface.h"
 #include "threads-model.h"
 
 memory_order orders[6] = {
@@ -9,6 +10,13 @@ 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();
+       }
+}
+
 /** Performs a read action.*/
 uint64_t model_read_action(void * obj, memory_order ord) {
        return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
@@ -85,21 +93,25 @@ void model_rmwc_action_helper(void *obj, int atomic_index, const char *position)
 
 // cds atomic inits
 void cds_atomic_init8(void * obj, uint8_t val, const char * position) {
+       ensureModel();
        model->switch_to_master(
                new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
                );
 }
 void cds_atomic_init16(void * obj, uint16_t val, const char * position) {
+       ensureModel();
        model->switch_to_master(
                new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
                );
 }
 void cds_atomic_init32(void * obj, uint32_t val, const char * position) {
+       ensureModel();
        model->switch_to_master(
                new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
                );
 }
 void cds_atomic_init64(void * obj, uint64_t val, const char * position) {
+       ensureModel();
        model->switch_to_master(
                new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)
                );
@@ -130,21 +142,25 @@ uint64_t cds_atomic_load64(void * obj, int atomic_index, const char * position)
 
 // cds atomic stores
 void cds_atomic_store8(void * obj, uint8_t val, int atomic_index, const char * position) {
+       ensureModel();
        model->switch_to_master(
                new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
                );
 }
 void cds_atomic_store16(void * obj, uint16_t val, int atomic_index, const char * position) {
+       ensureModel();
        model->switch_to_master(
                new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
                );
 }
 void cds_atomic_store32(void * obj, uint32_t val, int atomic_index, const char * position) {
+       ensureModel();
        model->switch_to_master(
                new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
                );
 }
 void cds_atomic_store64(void * obj, uint64_t val, int atomic_index, const char * position) {
+       ensureModel();
        model->switch_to_master(
                new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val)
                );

diff --git a/include/cmodelint.h b/include/cmodelint.h
index 8530827cfe39b5cf673efa3e047a8f987f7642a1..7bc6a253c9b5fedd61b7574558c647399f0207a3 100644 (file)
--- a/include/cmodelint.h
+++ b/include/cmodelint.h
@@ -10,8 +10,11 @@
 #if __cplusplus
 using std::memory_order;
 extern "C" {
+#else
+typedef int bool;
 #endif
 
+  
 uint64_t model_read_action(void * obj, memory_order ord);
 void model_write_action(void * obj, memory_order ord, uint64_t val);
 void model_init_action(void * obj, uint64_t val);

diff --git a/main.cc b/main.cc
index 0abc80b7e766063c5b3304be14d3a86dbc049045..56ad58058d9b3b01c86d5d1af9b87d0faab28211 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -164,23 +164,6 @@ static void install_trace_analyses(ModelExecution *execution)
 /** The model_main function contains the main model checking loop. */
 static void model_main()
 {
-       struct model_params params;
-
-       param_defaults(&params);
-       register_plugins();
-
-       parse_options(&params, main_argc, main_argv);
-
-       //Initialize race detector
-       initRaceDetector();
-
-       snapshot_stack_init();
-
-       if (!model)
-               model = new ModelChecker();
-       model->setParams(params);
-       install_trace_analyses(model->get_execution());
-
        snapshot_record(0);
        model->run();
        delete model;
@@ -212,6 +195,25 @@ int main(int argc, char **argv)
        /* Configure output redirection for the model-checker */
        redirect_output();
 
-       /* Let's jump in quickly and start running stuff */
-       snapshot_system_init(10000, 1024, 1024, 40000, &model_main);
+       //Initialize snapshotting library
+       if (!model)
+               snapshot_system_init(10000, 1024, 1024, 40000);
+
+       struct model_params params;
+
+       param_defaults(&params);
+       register_plugins();
+       parse_options(&params, main_argc, main_argv);
+
+       //Initialize race detector
+       initRaceDetector();
+
+       snapshot_stack_init();
+
+       if (!model)
+               model = new ModelChecker();
+       model->setParams(params);
+       install_trace_analyses(model->get_execution());
+
+       startExecution(&model_main);
 }

diff --git a/pthread.cc b/pthread.cc
index 8c2bc076f3024edbc9042d428385b3dd36f77bc2..35af63e6a5cbbd654f663625e220aa36eb242830 100644 (file)
--- a/pthread.cc
+++ b/pthread.cc
@@ -49,6 +49,7 @@ void pthread_exit(void *value_ptr) {
 
 int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
        if (!model) {
+               snapshot_system_init(10000, 1024, 1024, 40000);
                model = new ModelChecker();
        }
 

diff --git a/snapshot-interface.h b/snapshot-interface.h
index d926c74e691dd762ccf06b2cd1bca1dfc2fd1a41..3e3ad71e02388ff1130d3da357f8321c77543a01 100644 (file)
--- a/snapshot-interface.h
+++ b/snapshot-interface.h
@@ -11,8 +11,8 @@ typedef unsigned int snapshot_id;
 typedef void (*VoidFuncPtr)();
 void snapshot_system_init(unsigned int numbackingpages,
                                                                                                        unsigned int numsnapshots, unsigned int nummemoryregions,
-                                                                                                       unsigned int numheappages, VoidFuncPtr entryPoint);
-
+                                                                                                       unsigned int numheappages);
+void startExecution(VoidFuncPtr entryPoint);
 void snapshot_stack_init();
 void snapshot_record(int seq_index);
 int snapshot_backtrack_before(int seq_index);

diff --git a/snapshot.cc b/snapshot.cc
index ce2b28fe3dc4cb0952ed9b11c8c79b923b71b021..5c1c1e25fd0599922da93a9100c9eb41f16385f7 100644 (file)
--- a/snapshot.cc
+++ b/snapshot.cc
@@ -134,7 +134,7 @@ static void mprot_handle_pf(int sig, siginfo_t *si, void *unused)
 
 static void mprot_snapshot_init(unsigned int numbackingpages,
                                                                                                                                unsigned int numsnapshots, unsigned int nummemoryregions,
-                                                                                                                               unsigned int numheappages, VoidFuncPtr entryPoint)
+                                                                                                                               unsigned int numheappages)
 {
        /* Setup a stack for our signal handler....  */
        stack_t ss;
@@ -179,7 +179,10 @@ static void mprot_snapshot_init(unsigned int numbackingpages,
        pagealignedbase = PageAlignAddressUpward(base_model_snapshot_space);
        model_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1);
        snapshot_add_memory_region(pagealignedbase, numheappages);
+}
+
 
+static void mprot_startExecution(VoidFuncPtr entryPoint) {
        entryPoint();
 }
 
@@ -363,7 +366,7 @@ mspace create_shared_mspace()
 
 static void fork_snapshot_init(unsigned int numbackingpages,
                                                                                                                         unsigned int numsnapshots, unsigned int nummemoryregions,
-                                                                                                                        unsigned int numheappages, VoidFuncPtr entryPoint)
+                                                                                                                        unsigned int numheappages)
 {
        if (!fork_snap)
                createSharedMemory();
@@ -371,7 +374,9 @@ static void fork_snapshot_init(unsigned int numbackingpages,
        void *base_model_snapshot_space = malloc((numheappages + 1) * PAGESIZE);
        void *pagealignedbase = PageAlignAddressUpward(base_model_snapshot_space);
        model_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1);
+}
 
+static void fork_startExecution(VoidFuncPtr entryPoint) {
        /* setup an "exiting" context */
        char stack[128];
        create_context(&exit_ctxt, stack, sizeof(stack), fork_exit);
@@ -437,12 +442,21 @@ static void fork_roll_back(snapshot_id theID)
  */
 void snapshot_system_init(unsigned int numbackingpages,
                                                                                                        unsigned int numsnapshots, unsigned int nummemoryregions,
-                                                                                                       unsigned int numheappages, VoidFuncPtr entryPoint)
+                                                                                                       unsigned int numheappages)
+{
+#if USE_MPROTECT_SNAPSHOT
+       mprot_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages);
+#else
+       fork_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages);
+#endif
+}
+
+void startExecution(VoidFuncPtr entryPoint)
 {
 #if USE_MPROTECT_SNAPSHOT
-       mprot_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages, entryPoint);
+       mprot_startExecution(entryPoint);
 #else
-       fork_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages, entryPoint);
+       fork_startExecution(entryPoint);
 #endif
 }