X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=datarace.cc;h=1cc407bb991889545210f54ec313ae84c49cf412;hb=f94de5b6daa067501562ed3047bfb6b4939f9435;hp=5ab52fc49eefa87ea1d2ad4e3c8c1a4b607f15f5;hpb=620c53f1b91d3f9b51424ff57c652d247f6fbaac;p=model-checker.git

diff --git a/datarace.cc b/datarace.cc
index 5ab52fc..1cc407b 100644
--- a/datarace.cc
+++ b/datarace.cc
@@ -82,14 +82,19 @@ 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->set_assert();
+		model->switch_to_master(NULL);
+	}
 }
 
 /** 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,18 +105,24 @@ 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) {
 	printf("Datarace detected\n");
 	printf("Location %p\n", race->address);
 	printf("Initial access: thread %u clock %u, iswrite %u\n",race->oldthread,race->oldclock, race->isoldwrite);
-	printf("Second access: thread %u, iswrite %u\n", race->newaction->get_tid(), race->isnewwrite);
+	printf("Second access: thread %u clock %u, iswrite %u\n", race->newaction->get_tid(), race->newaction->get_seq_number() , race->isnewwrite);
 }
 
 /** This function does race detection for a write on an expanded record. */