X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=datarace.cc;h=270e52310730febec1e97956c787a06c7b670b7e;hb=d2cbbe4ce6d8f6e1aa23b8fe639ed58edf1789b7;hp=293743052858c8029fb685ff246ac071f38b821e;hpb=328a2c09c2ee06d0e1c49ccb84877fa17b436a01;p=model-checker.git

diff --git a/datarace.cc b/datarace.cc
index 2937430..270e523 100644
--- a/datarace.cc
+++ b/datarace.cc
@@ -1,9 +1,10 @@
 #include "datarace.h"
 #include "model.h"
-#include "threads.h"
+#include "threads-model.h"
 #include <stdio.h>
 #include <cstring>
 #include "mymemory.h"
+#include "clockvector.h"
 
 struct ShadowTable *root;
 std::vector<struct DataRace *> unrealizedraces;
@@ -119,11 +120,15 @@ bool checkDataRaces() {
 	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 clock %u, iswrite %u\n", race->newaction->get_tid(), race->newaction->get_seq_number() , race->isnewwrite);
+void printRace(struct DataRace *race)
+{
+	printf("Datarace detected @ address %p:\n", race->address);
+	printf("    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",
+			race->isnewwrite ? "write" : "read",
+			id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
 }
 
 /** This function does race detection for a write on an expanded record. */