More code towards support non-atomic stores

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index b8d9f7cb4ce46b7c01ed7aa08fe982985a7a9cd0..4eafe4fbb321415169bf098d95ba44621de21851 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -7,7 +7,6 @@
 
 #include "model.h"
 #include "action.h"
-#include "nodestack.h"
 #include "schedule.h"
 #include "snapshot-interface.h"
 #include "common.h"
@@ -34,8 +33,7 @@ ModelChecker::ModelChecker() :
        params(),
        restart_flag(false),
        scheduler(new Scheduler()),
-       node_stack(new NodeStack()),
-       execution(new ModelExecution(this, scheduler, node_stack)),
+       execution(new ModelExecution(this, scheduler)),
        history(new ModelHistory()),
        execution_number(1),
        trace_analyses(),
@@ -47,12 +45,12 @@ ModelChecker::ModelChecker() :
        scheduler->set_current_thread(init_thread);
        execution->setParams(&params);
        param_defaults(&params);
+       initRaceDetector();
 }
 
 /** @brief Destructor */
 ModelChecker::~ModelChecker()
 {
-       delete node_stack;
        delete scheduler;
 }
 
@@ -114,7 +112,7 @@ Thread * ModelChecker::get_next_thread()
         * Have we completed exploring the preselected path? Then let the
         * scheduler decide
         */
-       return scheduler->select_next_thread(node_stack->get_head());
+       return scheduler->select_next_thread();
 }
 
 /**
@@ -319,6 +317,16 @@ void ModelChecker::switch_from_master(Thread *thread)
  */
 uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
+       if (forklock) {
+               static bool fork_message_printed = false;
+
+               if (!fork_message_printed) {
+                       model_print("Fork handler trying to call into model checker...\n");
+                       fork_message_printed = true;
+               }
+               delete act;
+               return 0;
+       }
        DBG();
        Thread *old = thread_current();
        scheduler->set_current_thread(NULL);