X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=datarace.cc;h=653039b3307e3ebfb195e2dc99efda36ae123a7c;hp=5174c042e177a52773eee7d7668e010ed38a5e54;hb=f0b1d5cb87fd3ae41c325045b6bbf9554e7116f9;hpb=c123ef2c7d98d23474d2d2b121b56b502d75665b

diff --git a/datarace.cc b/datarace.cc
index 5174c04..653039b 100644
--- a/datarace.cc
+++ b/datarace.cc
@@ -7,12 +7,18 @@
 #include "clockvector.h"
 #include "config.h"
 #include "action.h"
+#include "execution.h"
+#include "stl-model.h"
 
 static struct ShadowTable *root;
-SnapVector<struct DataRace *> unrealizedraces;
+static SnapVector<DataRace *> *unrealizedraces;
 static void *memory_base;
 static void *memory_top;
 
+static const ModelExecution * get_execution()
+{
+	return model->get_execution();
+}
 
 /** This function initialized the data race detector. */
 void initRaceDetector()
@@ -20,6 +26,7 @@ void initRaceDetector()
 	root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1);
 	memory_base = snapshot_calloc(sizeof(struct ShadowBaseTable) * SHADOWBASETABLES, 1);
 	memory_top = ((char *)memory_base) + sizeof(struct ShadowBaseTable) * SHADOWBASETABLES;
+	unrealizedraces = new SnapVector<DataRace *>();
 }
 
 void * table_calloc(size_t size)
@@ -105,7 +112,7 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
 	race->newaction = newaction;
 	race->isnewwrite = isnewwrite;
 	race->address = address;
-	unrealizedraces.push_back(race);
+	unrealizedraces->push_back(race);
 
 	/* If the race is realized, bail out now. */
 	if (checkDataRaces())
@@ -123,18 +130,18 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
  */
 bool checkDataRaces()
 {
-	if (model->isfeasibleprefix()) {
+	if (get_execution()->isfeasibleprefix()) {
 		bool race_asserted = false;
 		/* Prune the non-racing unrealized dataraces */
-		for (unsigned i = 0; i < unrealizedraces.size(); i++) {
-			struct DataRace *race = unrealizedraces[i];
+		for (unsigned i = 0; i < unrealizedraces->size(); i++) {
+			struct DataRace *race = (*unrealizedraces)[i];
 			if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
 				assert_race(race);
 				race_asserted = true;
 			}
 			snapshot_free(race);
 		}
-		unrealizedraces.clear();
+		unrealizedraces->clear();
 		return race_asserted;
 	}
 	return false;
@@ -180,7 +187,7 @@ void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl
 
 		if (clock_may_race(currClock, thread, readClock, readThread)) {
 			/* We have a datarace */
-			reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
+			reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 		}
 	}
 
@@ -191,7 +198,7 @@ void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl
 
 	if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 		/* We have a datarace */
-		reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
+		reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 	}
 
 	record->numReads = 0;
@@ -205,7 +212,7 @@ void raceCheckWrite(thread_id_t thread, void *location)
 {
 	uint64_t *shadow = lookupAddressEntry(location);
 	uint64_t shadowval = *shadow;
-	ClockVector *currClock = model->get_cv(thread);
+	ClockVector *currClock = get_execution()->get_cv(thread);
 
 	/* Do full record */
 	if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
@@ -230,7 +237,7 @@ void raceCheckWrite(thread_id_t thread, void *location)
 
 	if (clock_may_race(currClock, thread, readClock, readThread)) {
 		/* We have a datarace */
-		reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
+		reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 	}
 
 	/* Check for datarace against last write. */
@@ -240,7 +247,7 @@ void raceCheckWrite(thread_id_t thread, void *location)
 
 	if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 		/* We have a datarace */
-		reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
+		reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 	}
 	*shadow = ENCODEOP(0, 0, threadid, ourClock);
 }
@@ -257,7 +264,7 @@ void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shado
 
 	if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 		/* We have a datarace */
-		reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
+		reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 	}
 
 	/* Shorten vector when possible */
@@ -309,7 +316,7 @@ void raceCheckRead(thread_id_t thread, const void *location)
 {
 	uint64_t *shadow = lookupAddressEntry(location);
 	uint64_t shadowval = *shadow;
-	ClockVector *currClock = model->get_cv(thread);
+	ClockVector *currClock = get_execution()->get_cv(thread);
 
 	/* Do full record */
 	if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
@@ -334,7 +341,7 @@ void raceCheckRead(thread_id_t thread, const void *location)
 
 	if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 		/* We have a datarace */
-		reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
+		reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 	}
 
 	modelclock_t readClock = READVECTOR(shadowval);
@@ -349,3 +356,8 @@ void raceCheckRead(thread_id_t thread, const void *location)
 
 	*shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
 }
+
+bool haveUnrealizedRaces()
+{
+	return !unrealizedraces->empty();
+}