From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 7 Sep 2012 01:56:39 +0000 (-0700)
Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
X-Git-Tag: pldi2013~235
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c5b57f3d98d1d14b4546995a0882753cf71a1c4b;hp=0accacf66b9f7bb4479205a0840f208dd8da6960;p=model-checker.git

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

check in my stuff...

Conflicts:
	model.cc
	threads.h
---

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 56723c7..217d642 100644
--- a/model.cc
+++ b/model.cc
@@ -9,6 +9,7 @@
 #include "clockvector.h"
 #include "cyclegraph.h"
 #include "promise.h"
+#include "datarace.h"
 
 #define INITIAL_THREAD_ID	0
 
@@ -36,7 +37,8 @@ ModelChecker::ModelChecker(struct model_params params) :
 	node_stack(new NodeStack()),
 	next_backtrack(NULL),
 	mo_graph(new CycleGraph()),
-	failed_promise(false)
+	failed_promise(false),
+	asserted(false)
 {
 }
 
@@ -77,6 +79,7 @@ void ModelChecker::reset_to_initial_state()
 	nextThread = NULL;
 	next_backtrack = NULL;
 	failed_promise = false;
+	reset_asserted();
 	snapshotObject->backTrackBeforeStep(0);
 }
 
@@ -339,7 +342,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		}
 	} else if (curr->is_write()) {
 		if (w_modification_order(curr))
-			updated = true;;
+			updated = true;
 		if (resolve_promises(curr))
 			updated = true;
 	}
@@ -370,6 +373,13 @@ 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() {
+	return promises->size()==0;
+}
+
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
 	return !mo_graph->checkForCycles() && !failed_promise;
@@ -700,6 +710,11 @@ bool ModelChecker::resolve_release_sequences(void *location)
 			it++;
 	}
 
+	// If we resolved promises or data races, see if we have realized a data race.
+	if (checkDataRaces()) {
+		model->set_assert();
+	}
+
 	return updated;
 }
 
@@ -791,6 +806,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 		} else
 			promise_index++;
 	}
+
 	return resolved;
 }
 
@@ -973,6 +989,9 @@ int ModelChecker::switch_to_master(ModelAction *act)
 bool ModelChecker::take_step() {
 	Thread *curr, *next;
 
+	if (has_asserted())
+		return false;
+
 	curr = thread_current();
 	if (curr) {
 		if (curr->get_state() == THREAD_READY) {
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: