X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=datarace.cc;h=bdfade358e60595d1157e94cd2fcd0b5a18d0b86;hb=05d91de8ac8098425d51e9af2704eb91e04a7f9b;hp=732d6ff748b6e77187c10f0bf5dcd6b6b834b025;hpb=caa1df880547acce2804221c8e6995170a5121eb;p=model-checker.git

diff --git a/datarace.cc b/datarace.cc
index 732d6ff..bdfade3 100644
--- a/datarace.cc
+++ b/datarace.cc
@@ -32,7 +32,7 @@ void * table_calloc(size_t size) {
 
 /** This function looks up the entry in the shadow table corresponding to a
  * given address.*/
-static uint64_t * lookupAddressEntry(void * address) {
+static uint64_t * lookupAddressEntry(const void * address) {
 	struct ShadowTable *currtable=root;
 #if BIT48
 	currtable=(struct ShadowTable *) currtable->array[(((uintptr_t)address)>>32)&MASK16BIT];
@@ -91,7 +91,7 @@ static void expandRecord(uint64_t * shadow) {
 }
 
 /** This function is called when we detect a data race.*/
-static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, void *address) {
+static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address) {
 	struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
 	race->oldthread=oldthread;
 	race->oldclock=oldclock;
@@ -102,49 +102,57 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
 	unrealizedraces.push_back(race);
 
 	/* If the race is realized, bail out now. */
-	if (checkDataRaces()) {
-		model->set_assert();
+	if (checkDataRaces())
 		model->switch_to_master(NULL);
-	}
 }
 
-/** This function goes through the list of unrealized data races,
- *	removes the impossible ones, and print the realized ones. */
-
+/**
+ * @brief Check and report data races
+ *
+ * If the trace is feasible (a feasible prefix), clear out the list of
+ * unrealized data races, asserting any realized ones as execution bugs so that
+ * the model-checker will end the execution.
+ *
+ * @return True if any data races were realized
+ */
 bool checkDataRaces() {
 	if (model->isfeasibleprefix()) {
+		bool race_asserted = false;
 		/* Prune the non-racing unrealized dataraces */
-		unsigned int i,newloc=0;
-		for(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)) {
-				unrealizedraces[newloc++]=race;
+				assert_race(race);
+				race_asserted = true;
 			}
+			snapshot_free(race);
 		}
-		if (newloc!=i)
-			unrealizedraces.resize(newloc);
-
-		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;
-		}
+		unrealizedraces.clear();
+		return race_asserted;
 	}
 	return false;
 }
 
-void printRace(struct DataRace *race)
+/**
+ * @brief Assert a data race
+ *
+ * Asserts a data race which is currently realized, causing the execution to
+ * end and stashing a message in the model-checker's bug list
+ *
+ * @param race The race to report
+ */
+void assert_race(struct DataRace *race)
 {
-	printf("Datarace detected @ address %p:\n", race->address);
-	printf("    Access 1: %5s in thread %2d @ clock %3u\n",
+	char buf[200];
+	char *ptr = buf;
+	ptr += sprintf(ptr, "Data race detected @ address %p:\n", race->address);
+	ptr += sprintf(ptr, "    Access 1: %5s in thread %2d @ clock %3u\n",
 			race->isoldwrite ? "write" : "read",
 			id_to_int(race->oldthread), race->oldclock);
-	printf("    Access 2: %5s in thread %2d @ clock %3u\n",
+	ptr += sprintf(ptr, "    Access 2: %5s in thread %2d @ clock %3u",
 			race->isnewwrite ? "write" : "read",
 			id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
+	model->assert_bug(buf);
 }
 
 /** This function does race detection for a write on an expanded record. */
@@ -226,7 +234,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
 }
 
 /** This function does race detection on a read for an expanded record. */
-void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
+void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t * shadow, ClockVector *currClock) {
 	struct RaceRecord * record=(struct RaceRecord *) (*shadow);
 
 	/* Check for datarace against last write. */
@@ -284,7 +292,7 @@ void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, Cl
 }
 
 /** This function does race detection on a read. */
-void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
+void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock) {
 	uint64_t * shadow=lookupAddressEntry(location);
 	uint64_t shadowval=*shadow;