changes

[model-checker.git] / datarace.cc

diff --git a/datarace.cc b/datarace.cc
index 12a2e6bb1d60aa84a94d0e970617e703c324ecc3..5856e770b326eece6dee601dbf346e32b140ed07 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -21,10 +21,25 @@ static uint64_t * lookupAddressEntry(void * address) {
        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]=calloc(sizeof(struct ShadowBaseTable),1));
-       }       
+       }
        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;
 
@@ -60,23 +75,26 @@ void fullRaceCheckWrite(thread_id_t thread, uint64_t * shadow, ClockVector *curr
        for(int i=0;i<record->numReads;i++) {
                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();
                }
        }
-       
+
        /* Check for datarace against last write. */
-       
+
        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();
        }
-       
+
        record->numReads=0;
        record->writeThread=thread;
        modelclock_t ourClock = currClock->getClock(thread);
@@ -95,20 +113,20 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
 
        int threadid = id_to_int(thread);
        modelclock_t ourClock = currClock->getClock(thread);
-       
+
        /* Thread ID is too large or clock is too large. */
        if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
                expandRecord(shadow);
                fullRaceCheckWrite(thread, shadow, currClock);
                return;
        }
-       
+
        /* Check for datarace against last read. */
 
        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();
        }
@@ -117,8 +135,8 @@ 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();
        }
@@ -129,11 +147,11 @@ void fullRaceCheckRead(thread_id_t thread, uint64_t * shadow, ClockVector *currC
        struct RaceRecord * record=(struct RaceRecord *) (*shadow);
 
        /* Check for datarace against last write. */
-       
+
        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();
        }
@@ -145,8 +163,14 @@ void fullRaceCheckRead(thread_id_t thread, uint64_t * shadow, ClockVector *currC
        for(int i=0;i<record->numReads;i++) {
                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];
@@ -155,7 +179,7 @@ void fullRaceCheckRead(thread_id_t thread, uint64_t * shadow, ClockVector *currC
                        copytoindex++;
                }
        }
-       
+
        if (copytoindex>=record->capacity) {
                int newCapacity=record->capacity*2;
                thread_id_t *newthread=(thread_id_t *) malloc(sizeof(thread_id_t)*newCapacity);
@@ -170,7 +194,7 @@ void fullRaceCheckRead(thread_id_t thread, uint64_t * shadow, ClockVector *currC
        }
 
        modelclock_t ourClock = currClock->getClock(thread);
-       
+
        record->thread[copytoindex]=thread;
        record->readClock[copytoindex]=ourClock;
        record->numReads=copytoindex+1;
@@ -188,7 +212,7 @@ void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
 
        int threadid = id_to_int(thread);
        modelclock_t ourClock = currClock->getClock(thread);
-       
+
        /* Thread ID is too large or clock is too large. */
        if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
                expandRecord(shadow);
@@ -200,21 +224,21 @@ 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();
        }
-       
+
        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);
                return;
        }
-               
+
        *shadow = ENCODEOP(writeThread, writeClock, threadid, ourClock);
 }