Merge branch 'new_fuzzer' of /home/git/random-fuzzer into new_fuzzer

diff --git a/cmodelint.cc b/cmodelint.cc
index 348051a0f7f13fb736baf14f8a24c81bcfdbb4f9..96cd1c49ef78f56a1a75eb6da46423fe3504123f 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -1,7 +1,9 @@
 #include <stdio.h>
 #include "model.h"
+#include "execution.h"
 #include "action.h"
 #include "cmodelint.h"
+#include "snapshot-interface.h"
 #include "threads-model.h"
 
 memory_order orders[6] = {
@@ -9,6 +11,18 @@ memory_order orders[6] = {
        memory_order_release, memory_order_acq_rel, memory_order_seq_cst
 };
 
+static void ensureModel(ModelAction * action) {
+       if (!model) {
+               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);
+       }
+}
+
 /** 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,22 +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) {
-       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) {
-       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) {
-       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) {
-       model->switch_to_master(
+       ensureModel(
                new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)
                );
 }
@@ -130,22 +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) {
-       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) {
-       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) {
-       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) {
-       model->switch_to_master(
+       ensureModel(
                new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val)
                );
 }

diff --git a/execution.cc b/execution.cc
index d75499f1349a4e24c69a1c01c90aa8bb599240d5..2c08711eee0d1a655272bd56f1adf0d900ef599d 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -778,9 +778,6 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
 
        /* Last SC fence in the current thread */
        ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
-       ModelAction *last_sc_write = NULL;
-       if (curr->is_seqcst())
-               last_sc_write = get_last_seq_cst_write(curr);
 
        int tid = curr->get_tid();
        ModelAction *prev_same_thread = NULL;

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;}
+       ModelAction * check_current_action(ModelAction *curr);
 
        SNAPSHOTALLOC
 private:
@@ -124,7 +125,6 @@ private:
        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);

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..cc3fcbf081316cf3958cf1f59915e4b3ca8d9e9a 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,28 @@ 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_init)
+               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_init)
+               model = new ModelChecker();
+       else
+               model = model_init;
+
+       model->setParams(params);
+       install_trace_analyses(model->get_execution());
+
+       startExecution(&model_main);
 }

diff --git a/model.cc b/model.cc
index 61d0b64c8ba4042e31a8945b9ecce5f8a20f1136..c468d0deb3e8b6972673d3910670e99eff42052f 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -18,7 +18,14 @@
 #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() :
@@ -33,6 +40,9 @@ ModelChecker::ModelChecker() :
        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 */
@@ -310,10 +320,11 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        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");
@@ -322,12 +333,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        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 */
@@ -363,10 +368,8 @@ void ModelChecker::run()
        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

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;
+       Thread * init_thread;
 
        int execution_number;
 
@@ -103,5 +104,6 @@ private:
 };
 
 extern ModelChecker *model;
+extern ModelChecker *model_init;
 
 #endif /* __MODEL_H__ */

diff --git a/pthread.cc b/pthread.cc
index 8c2bc076f3024edbc9042d428385b3dd36f77bc2..79e904257b38ef69973ce4733cb55ab3ed1ce527 100644 (file)
--- a/pthread.cc
+++ b/pthread.cc
@@ -48,14 +48,19 @@ void pthread_exit(void *value_ptr) {
 }
 
 int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
-       if (!model) {
-               model = new ModelChecker();
-       }
-
        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);
+
        return 0;
 }
 

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
 }
 

diff --git a/test/condvar.cc b/test/condvar.cc
index fcfd59a8825f5b0946fb4fd3786d9347b26a364e..0457c41479d33eab3bee952fa6883f1d6f007628 100644 (file)
--- a/test/condvar.cc
+++ b/test/condvar.cc
@@ -3,11 +3,11 @@
 #include "threads.h"
 #include "librace.h"
 #include "stdatomic.h"
-#include <mutex>
+#include <mutex.h>
 #include <condition_variable>
 
-std::mutex * m;
-std::condition_variable *v;
+cdsc::mutex * m;
+cdsc::condition_variable *v;
 int shareddata;
 
 static void a(void *obj)
@@ -32,8 +32,8 @@ int user_main(int argc, char **argv)
 {
        thrd_t t1, t2;
        store_32(&shareddata, (unsigned int) 0);
-       m=new std::mutex();
-       v=new std::condition_variable();
+       m=new cdsc::mutex();
+       v=new cdsc::condition_variable();
 
        thrd_create(&t1, (thrd_start_t)&a, NULL);
        thrd_create(&t2, (thrd_start_t)&b, NULL);