From 7c003db5218470054490a6777c97c6611b933a12 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Thu, 6 Sep 2012 18:32:56 -0700
Subject: [PATCH] changes

---
 datarace.cc | 22 ++++++++++++++++------
 datarace.h  |  2 +-
 model.cc    | 17 +++++++++++++++++
 model.h     |  2 ++
 threads.h   |  1 +
 5 files changed, 37 insertions(+), 7 deletions(-)

diff --git a/datarace.cc b/datarace.cc
index 5ab52fc..34060fa 100644
--- a/datarace.cc
+++ b/datarace.cc
@@ -82,14 +82,18 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
 	race->isnewwrite=isnewwrite;
 	race->address=address;
 	unrealizedraces.push_back(race);
-	checkDataRaces();
+
+	/* If the race is realized, bail out now. */
+	if (checkDataRaces()) {
+		model->assert_thread();
+	}
 }
 
 /** This function goes through the list of unrealized data races,
  *	removes the impossible ones, and print the realized ones. */
 
-void checkDataRaces() {
-	if (true) {
+bool checkDataRaces() {
+	if (model->isfeasibleprefix()) {
 		/* Prune the non-racing unrealized dataraces */
 		unsigned int i,newloc=0;
 		for(i=0;i<unrealizedraces.size();i++) {
@@ -100,11 +104,17 @@ void checkDataRaces() {
 		}
 		if (newloc!=i)
 			unrealizedraces.resize(newloc);
-		for(i=0;i<unrealizedraces.size();i++) {
-			struct DataRace * race=unrealizedraces[i];
-			printRace(race);
+
+		if (unrealizedraces.size()!=0) {
+			/* We have an actual realized race. */
+			for(i=0;i<unrealizedraces.size();i++) {
+				struct DataRace * race=unrealizedraces[i];
+				printRace(race);
+			}
+			return true;
 		}
 	}
+	return false;
 }
 
 void printRace(struct DataRace * race) {
diff --git a/datarace.h b/datarace.h
index b2f7099..5bfcb8a 100644
--- a/datarace.h
+++ b/datarace.h
@@ -40,7 +40,7 @@ struct DataRace {
 void initRaceDetector();
 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock);
 void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock);
-void checkDataRaces();
+bool checkDataRaces();
 void printRace(struct DataRace *race);
 
 extern std::vector<struct DataRace *> unrealizedraces;
diff --git a/model.cc b/model.cc
index ec953ef..0e2b818 100644
--- a/model.cc
+++ b/model.cc
@@ -357,6 +357,12 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		return get_next_replay_thread();
 }
 
+/** @returns whether the current partial trace must be a prefix of a
+ * feasible trace. */
+
+bool ModelChecker::isfeasibleprefix() {
+}
+
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
 	return !mo_graph->checkForCycles() && !failed_promise;
@@ -956,6 +962,14 @@ int ModelChecker::switch_to_master(ModelAction *act)
 	return Thread::swap(old, &system_context);
 }
 
+void ModelChecker::assert_thread() {
+	DBG();
+	Thread *old = thread_current();
+	set_current_action(NULL);
+	old->set_state(THREAD_ASSERTED);
+	return Thread::swap(old, &system_context);
+}
+
 /**
  * Takes the next step in the execution, if possible.
  * @return Returns true (success) if a step was taken and false otherwise.
@@ -974,6 +988,9 @@ bool ModelChecker::take_step() {
 		} else if (curr->get_state() == THREAD_RUNNING) {
 			/* Stopped while running; i.e., completed */
 			curr->complete();
+		} else if (curr->get_state()==THREAD_ASSERTED) {
+			/* Something bad happened.  Stop taking steps. */
+			return false;
 		} else {
 			ASSERT(false);
 		}
diff --git a/model.h b/model.h
index 9eb9aa6..9235f8f 100644
--- a/model.h
+++ b/model.h
@@ -53,6 +53,7 @@ public:
 	/** @return The currently executing Thread. */
 	Thread * get_current_thread() { return scheduler->get_current_thread(); }
 
+	void assert_thread();
 	int switch_to_master(ModelAction *act);
 	ClockVector * get_cv(thread_id_t tid);
 	ModelAction * get_parent_action(thread_id_t tid);
@@ -64,6 +65,7 @@ public:
 	                std::vector<const ModelAction *> *release_heads);
 
 	void finish_execution();
+	bool isfeasibleprefix();
 
 	MEMALLOC
 private:
diff --git a/threads.h b/threads.h
index e7cd792..6872ffa 100644
--- a/threads.h
+++ b/threads.h
@@ -27,6 +27,7 @@ typedef enum thread_state {
 	 * context.
 	 */
 	THREAD_READY,
+	THREAD_ASSERTED,
 	/** Thread has completed its execution */
 	THREAD_COMPLETED
 } thread_state;
-- 
2.34.1