More changes

diff --git a/cmodelint.cc b/cmodelint.cc
index c55b93866c32706d9fdd0937bf17978b7d415f72..96cd1c49ef78f56a1a75eb6da46423fe3504123f 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -1,5 +1,6 @@
 #include <stdio.h>
 #include "model.h"
 #include <stdio.h>
 #include "model.h"

+#include "execution.h"

 #include "action.h"
 #include "cmodelint.h"
 #include "snapshot-interface.h"
 #include "action.h"
 #include "cmodelint.h"
 #include "snapshot-interface.h"


@@ -10,10 +11,15 @@ 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() {
+static void ensureModel(ModelAction * action) {

        if (!model) {
        if (!model) {

-               snapshot_system_init(10000, 1024, 1024, 40000);
-               model = new ModelChecker();
+               if (!model_init) {
+                       snapshot_system_init(10000, 1024, 1024, 40000);
+                       model_init = new ModelChecker();
+               }
+               model_init->get_execution()->check_current_action(action);
+       } else {
+               model->switch_to_master(action);

        }
 }
 
        }
 }
 


@@ -93,26 +99,22 @@ 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) {
 
 // cds atomic inits
 void cds_atomic_init8(void * obj, uint8_t val, const char * position) {

-       ensureModel();
-       model->switch_to_master(
+       ensureModel(

                new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
                );
 }
 void cds_atomic_init16(void * obj, uint16_t val, const char * position) {
                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(
+       ensureModel(

                new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
                );
 }
 void cds_atomic_init32(void * obj, uint32_t val, const char * position) {
                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(
+       ensureModel(

                new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
                );
 }
 void cds_atomic_init64(void * obj, uint64_t val, const char * position) {
                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(
+       ensureModel(

                new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)
                );
 }
                new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)
                );
 }


@@ -142,26 +144,22 @@ 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) {
 
 // cds atomic stores
 void cds_atomic_store8(void * obj, uint8_t val, int atomic_index, const char * position) {

-       ensureModel();
-       model->switch_to_master(
+       ensureModel(

                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) {
                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(
+       ensureModel(

                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) {
                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(
+       ensureModel(

                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) {
                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(
+       ensureModel(

                new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val)
                );
 }
                new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val)
                );
 }

diff --git a/execution.h b/execution.h
index 20bbfdc67f6466fe1ba47b46af00e1b6ad84d31e..4d5ef866ae72b7831bb3ab70e0311ee45f363e2e 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -105,6 +105,7 @@ public:
        CycleGraph * const get_mo_graph() { return mo_graph; }
        HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> * getCondMap() {return &cond_map;}
        HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> * getMutexMap() {return &mutex_map;}
        CycleGraph * const get_mo_graph() { return mo_graph; }
        HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> * getCondMap() {return &cond_map;}
        HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> * getMutexMap() {return &mutex_map;}

+       ModelAction * check_current_action(ModelAction *curr);

 
        SNAPSHOTALLOC
 private:
 
        SNAPSHOTALLOC
 private:


@@ -124,7 +125,6 @@ private:
        modelclock_t get_next_seq_num();
 
        bool next_execution();
        modelclock_t get_next_seq_num();
 
        bool next_execution();

-       ModelAction * check_current_action(ModelAction *curr);

        bool initialize_curr_action(ModelAction **curr);
        void process_read(ModelAction *curr, SnapVector<const ModelAction *> * rf_set);
        void process_write(ModelAction *curr);
        bool initialize_curr_action(ModelAction **curr);
        void process_read(ModelAction *curr, SnapVector<const ModelAction *> * rf_set);
        void process_write(ModelAction *curr);

diff --git a/main.cc b/main.cc
index 56ad58058d9b3b01c86d5d1af9b87d0faab28211..cc3fcbf081316cf3958cf1f59915e4b3ca8d9e9a 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -196,7 +196,7 @@ int main(int argc, char **argv)
        redirect_output();
 
        //Initialize snapshotting library
        redirect_output();
 
        //Initialize snapshotting library

-       if (!model)
+       if (!model_init)

                snapshot_system_init(10000, 1024, 1024, 40000);
 
        struct model_params params;
                snapshot_system_init(10000, 1024, 1024, 40000);
 
        struct model_params params;


@@ -210,8 +210,11 @@ int main(int argc, char **argv)
 
        snapshot_stack_init();
 
 
        snapshot_stack_init();
 

-       if (!model)
+       if (!model_init)

                model = new ModelChecker();
                model = new ModelChecker();

+       else
+               model = model_init;
+

        model->setParams(params);
        install_trace_analyses(model->get_execution());
 
        model->setParams(params);
        install_trace_analyses(model->get_execution());
 

diff --git a/model.cc b/model.cc
index 84a60a510456fbea7cd6f0e4e6df87499c40ee48..4b159aa5d35f879da883571c0bbc203d68a1c6d5 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -18,7 +18,14 @@
 #include "execution.h"
 #include "bugmessage.h"
 
 #include "execution.h"
 #include "bugmessage.h"
 

-ModelChecker *model;
+ModelChecker *model = NULL;
+ModelChecker *model_init = NULL;
+
+/** Wrapper to run the user's main function, with appropriate arguments */
+void user_main_wrapper(void *)
+{
+       user_main(model->params.argc, model->params.argv);
+}

 
 /** @brief Constructor */
 ModelChecker::ModelChecker() :
 
 /** @brief Constructor */
 ModelChecker::ModelChecker() :


@@ -33,6 +40,9 @@ ModelChecker::ModelChecker() :
        inspect_plugin(NULL)
 {
        memset(&stats,0,sizeof(struct execution_stats));
        inspect_plugin(NULL)
 {
        memset(&stats,0,sizeof(struct execution_stats));

+       init_thread = new Thread(execution->get_next_id(), (thrd_t *) malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL);  // L: user_main_wrapper passes the user program
+       execution->add_thread(init_thread);
+       scheduler->set_current_thread(init_thread);

 }
 
 /** @brief Destructor */
 }
 
 /** @brief Destructor */


@@ -313,10 +323,11 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        Thread *old = thread_current();
        scheduler->set_current_thread(NULL);
        ASSERT(!old->get_pending());
        Thread *old = thread_current();
        scheduler->set_current_thread(NULL);
        ASSERT(!old->get_pending());

-/* W: No plugin
-        if (inspect_plugin != NULL) {
-                inspect_plugin->inspectModelAction(act);
-        }*/
+
+       if (inspect_plugin != NULL) {
+               inspect_plugin->inspectModelAction(act);
+       }
+

        old->set_pending(act);
        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");
        old->set_pending(act);
        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");


@@ -325,12 +336,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        return old->get_return_value();
 }
 
        return old->get_return_value();
 }
 

-/** Wrapper to run the user's main function, with appropriate arguments */
-void user_main_wrapper(void *)
-{
-       user_main(model->params.argc, model->params.argv);
-}
-

 bool ModelChecker::should_terminate_execution()
 {
        /* Infeasible -> don't take any more steps */
 bool ModelChecker::should_terminate_execution()
 {
        /* Infeasible -> don't take any more steps */


@@ -367,10 +372,8 @@ void ModelChecker::run()
        initstate(423121, random_state, sizeof(random_state));
 
        for(int exec = 0;exec < params.maxexecutions;exec++) {
        initstate(423121, random_state, sizeof(random_state));
 
        for(int exec = 0;exec < params.maxexecutions;exec++) {

-               thrd_t user_thread;
-               Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
-               execution->add_thread(t);
-               //Need to seed random number generator, otherwise its state gets reset
+               Thread * t = init_thread;
+

                do {
                        /*
                         * Stash next pending action(s) for thread(s). There
                do {
                        /*
                         * Stash next pending action(s) for thread(s). There

diff --git a/model.h b/model.h
index 2a505c3d0251064710a85f1b75aca17d912bd23e..46c2454319d94b115381e41ad4248cd197732cef 100644 (file)
--- a/model.h
+++ b/model.h
@@ -72,6 +72,7 @@ private:
        Scheduler * const scheduler;
        NodeStack * const node_stack;
        ModelExecution *execution;
        Scheduler * const scheduler;
        NodeStack * const node_stack;
        ModelExecution *execution;

+       Thread * init_thread;

 
        int execution_number;
 
 
        int execution_number;
 


@@ -103,5 +104,6 @@ private:
 };
 
 extern ModelChecker *model;
 };
 
 extern ModelChecker *model;

+extern ModelChecker *model_init;

 
 #endif /* __MODEL_H__ */
 
 #endif /* __MODEL_H__ */

diff --git a/pthread.cc b/pthread.cc
index 35af63e6a5cbbd654f663625e220aa36eb242830..79e904257b38ef69973ce4733cb55ab3ed1ce527 100644 (file)
--- a/pthread.cc
+++ b/pthread.cc
@@ -48,15 +48,19 @@ void pthread_exit(void *value_ptr) {
 }
 
 int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
 }
 
 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();
-       }
-

        cdsc::mutex *m = new cdsc::mutex();
        cdsc::mutex *m = new cdsc::mutex();

+       ModelExecution *execution;

 
 

-       ModelExecution *execution = model->get_execution();
+       if (!model) {
+               if (!model_init) {
+                       snapshot_system_init(10000, 1024, 1024, 40000);
+                       model_init = new ModelChecker();
+               }
+               execution = model_init->get_execution();
+       } else
+               execution = model->get_execution();

        execution->getMutexMap()->put(p_mutex, m);
        execution->getMutexMap()->put(p_mutex, m);

+

        return 0;
 }
 
        return 0;
 }