X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=datarace.cc;h=5856e770b326eece6dee601dbf346e32b140ed07;hb=2209d0061afe47ee786eafccc7aedc2e29be5748;hp=da9a3fc15c9716a5a0ec7320bf23bccfb5445ef1;hpb=bcb3a311780c22c8a344c1288f1dd883b7b1960a;p=model-checker.git

diff --git a/datarace.cc b/datarace.cc
index da9a3fc..5856e77 100644
--- a/datarace.cc
+++ b/datarace.cc
@@ -25,6 +25,21 @@ static uint64_t * lookupAddressEntry(void * address) {
 	return &basetable->array[((uintptr_t)address)&MASK16BIT];
 }
 
+/**
+ * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
+ * to check the potential for a data race.
+ * @param clock1 The current clock vector
+ * @param tid1 The current thread; paired with clock1
+ * @param clock2 The clock value for the potentially-racing action
+ * @param tid2 The thread ID for the potentially-racing action
+ * @return true if the current clock allows a race with the event at clock2/tid2
+ */
+static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
+                           modelclock_t clock2, thread_id_t tid2)
+{
+	return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
+}
+
 static void expandRecord(uint64_t * shadow) {
 	uint64_t shadowval=*shadow;
 
@@ -61,7 +76,10 @@ void fullRaceCheckWrite(thread_id_t thread, uint64_t * shadow, ClockVector *curr
 		modelclock_t readClock = record->readClock[i];
 		thread_id_t readThread = record->thread[i];
 
-		if (readThread != thread && readClock != 0 && currClock->getClock(readThread) <= readClock) {
+		/* Note that readClock can't actuall be zero here, so it could be
+			 optimized. */
+
+		if (clock_may_race(currClock, thread, readClock, readThread)) {
 			/* We have a datarace */
 			reportDataRace();
 		}
@@ -72,7 +90,7 @@ void fullRaceCheckWrite(thread_id_t thread, uint64_t * shadow, ClockVector *curr
 	modelclock_t writeClock = record->writeClock;
 	thread_id_t writeThread = record->writeThread;
 
-	if (writeThread != thread && writeClock != 0 && currClock->getClock(writeThread) <= writeClock) {
+	if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 		/* We have a datarace */
 		reportDataRace();
 	}
@@ -108,7 +126,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
 	modelclock_t readClock = READVECTOR(shadowval);
 	thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 
-	if (readThread != thread && readClock != 0 && currClock->getClock(readThread) <= readClock) {
+	if (clock_may_race(currClock, thread, readClock, readThread)) {
 		/* We have a datarace */
 		reportDataRace();
 	}
@@ -118,7 +136,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
 	modelclock_t writeClock = WRITEVECTOR(shadowval);
 	thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 
-	if (writeThread != thread && writeClock != 0 && currClock->getClock(writeThread) <= writeClock) {
+	if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 		/* We have a datarace */
 		reportDataRace();
 	}
@@ -133,7 +151,7 @@ void fullRaceCheckRead(thread_id_t thread, uint64_t * shadow, ClockVector *currC
 	modelclock_t writeClock = record->writeClock;
 	thread_id_t writeThread = record->writeThread;
 
-	if (writeThread != thread && writeClock != 0 && currClock->getClock(writeThread) <= writeClock) {
+	if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 		/* We have a datarace */
 		reportDataRace();
 	}
@@ -146,7 +164,13 @@ void fullRaceCheckRead(thread_id_t thread, uint64_t * shadow, ClockVector *currC
 		modelclock_t readClock = record->readClock[i];
 		thread_id_t readThread = record->thread[i];
 
-		if (readThread != thread && currClock->getClock(readThread) <= readClock) {
+		/*  Note that is not really a datarace check as reads cannott
+				actually race.  It is just determining that this read subsumes
+				another in the sense that either this read races or neither
+				read races. Note that readClock can't actually be zero, so it
+				could be optimized.  */
+
+		if (clock_may_race(currClock, thread, readClock, readThread) {
 			/* Still need this read in vector */
 			if (copytoindex!=i) {
 				record->readClock[copytoindex]=record->readClock[i];
@@ -201,7 +225,7 @@ void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
 	modelclock_t writeClock = WRITEVECTOR(shadowval);
 	thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 
-	if (writeThread != thread && writeClock != 0 && currClock->getClock(writeThread) <= writeClock) {
+	if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 		/* We have a datarace */
 		reportDataRace();
 	}
@@ -209,7 +233,7 @@ void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
 	modelclock_t readClock = READVECTOR(shadowval);
 	thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 
-	if (readThread != thread && readClock != 0 && currClock->getClock(readThread) <= readClock) {
+	if (clock_may_race(currClock, thread, readClock, readThread)) {
 		/* We don't subsume this read... Have to expand record. */
 		expandRecord(shadow);
 		fullRaceCheckRead(thread, shadow, currClock);