X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=datarace.cc;h=bdfade358e60595d1157e94cd2fcd0b5a18d0b86;hb=84d0cd2f078f4cb15c318a0fef2515feab570375;hp=e6bbe05c29ddb2dd83e454751cab04ff8d201233;hpb=fe5cffdbd16698d2508cdb472212189ab12bde4f;p=model-checker.git

diff --git a/datarace.cc b/datarace.cc
index e6bbe05..bdfade3 100644
--- a/datarace.cc
+++ b/datarace.cc
@@ -5,13 +5,29 @@
 #include <cstring>
 #include "mymemory.h"
 #include "clockvector.h"
+#include "config.h"
 
 struct ShadowTable *root;
 std::vector<struct DataRace *> unrealizedraces;
+void *memory_base;
+void *memory_top;
+
 
 /** This function initialized the data race detector. */
 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;
+}
+
+void * table_calloc(size_t size) {
+	if ((((char *)memory_base)+size)>memory_top) {
+		return snapshot_calloc(size, 1);
+	} else {
+		void *tmp=memory_base;
+		memory_base=((char *)memory_base)+size;
+		return tmp;
+	}
 }
 
 /** This function looks up the entry in the shadow table corresponding to a
@@ -21,13 +37,13 @@ static uint64_t * lookupAddressEntry(const void * address) {
 #if BIT48
 	currtable=(struct ShadowTable *) currtable->array[(((uintptr_t)address)>>32)&MASK16BIT];
 	if (currtable==NULL) {
-		currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address)>>32)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowTable), 1));
+		currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address)>>32)&MASK16BIT] = table_calloc(sizeof(struct ShadowTable)));
 	}
 #endif
 
 	struct ShadowBaseTable * basetable=(struct ShadowBaseTable *) currtable->array[(((uintptr_t)address)>>16)&MASK16BIT];
 	if (basetable==NULL) {
-		basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address)>>16)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowBaseTable), 1));
+		basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address)>>16)&MASK16BIT] = table_calloc(sizeof(struct ShadowBaseTable)));
 	}
 	return &basetable->array[((uintptr_t)address)&MASK16BIT];
 }
@@ -86,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;
-			}
-		}
-		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);
+				assert_race(race);
+				race_asserted = true;
 			}
-			return true;
+			snapshot_free(race);
 		}
+		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. */