X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=45fa1b20ff11462c7999090a34e34f31212b049d;hb=68690971b2a9fc95250480fb3dd4752b2f936791;hp=b8d9f7cb4ce46b7c01ed7aa08fe982985a7a9cd0;hpb=a1280c133564afec30de10cc1de12a23b02a13d0;p=c11tester.git

diff --git a/model.cc b/model.cc
index b8d9f7cb..45fa1b20 100644
--- 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();
 }
 
 /**
@@ -246,7 +244,6 @@ bool ModelChecker::next_execution()
 		if (execution->is_deadlocked())
 			assert_bug("Deadlock detected");
 
-		checkDataRaces();
 		run_trace_analyses();
 	}
 
@@ -319,6 +316,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);
@@ -350,7 +357,7 @@ bool ModelChecker::should_terminate_execution()
 	/* Infeasible -> don't take any more steps */
 	if (execution->is_infeasible())
 		return true;
-	else if (execution->isfeasibleprefix() && execution->have_bug_reports()) {
+	else if (execution->isfeasibleprefix() && execution->have_fatal_bug_reports()) {
 		execution->set_assert();
 		return true;
 	}