Optimize RaceCheckRead

[c11tester.git] / datarace.cc

diff --git a/datarace.cc b/datarace.cc
index be0fc3b6a3fee6803f95d5f6127706cdabb24c27..8af2b1e64713f1c7d3436079428482b5e7e775f5 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -66,12 +66,12 @@ bool hasNonAtomicStore(const void *address) {
        uint64_t shadowval = *shadow;
        if (ISSHORTRECORD(shadowval)) {
                //Do we have a non atomic write with a non-zero clock
-               return ((WRITEVECTOR(shadowval) != 0) && !(ATOMICMASK & shadowval));
+               return !(ATOMICMASK & shadowval);
        } else {
                if (shadowval == 0)
-                       return false;
+                       return true;
                struct RaceRecord *record = (struct RaceRecord *)shadowval;
-               return !record->isAtomic && record->writeClock != 0;
+               return !record->isAtomic;
        }
 }
 
@@ -81,8 +81,10 @@ void setAtomicStoreFlag(const void *address) {
        if (ISSHORTRECORD(shadowval)) {
                *shadow = shadowval | ATOMICMASK;
        } else {
-               if (shadowval == 0)
+               if (shadowval == 0) {
+                       *shadow = ATOMICMASK | ENCODEOP(0, 0, 0, 0);
                        return;
+               }
                struct RaceRecord *record = (struct RaceRecord *)shadowval;
                record->isAtomic = 1;
        }
@@ -91,7 +93,7 @@ void setAtomicStoreFlag(const void *address) {
 void getStoreThreadAndClock(const void *address, thread_id_t * thread, modelclock_t * clock) {
        uint64_t * shadow = lookupAddressEntry(address);
        uint64_t shadowval = *shadow;
-       if (ISSHORTRECORD(shadowval)) {
+       if (ISSHORTRECORD(shadowval) || shadowval == 0) {
                //Do we have a non atomic write with a non-zero clock
                *thread = WRTHREADID(shadowval);
                *clock = WRITEVECTOR(shadowval);
@@ -676,7 +678,7 @@ void atomraceCheckRead(thread_id_t thread, const void *location)
                goto Exit;
        }
 
-       if (shadowval && ATOMICMASK)
+       if (shadowval & ATOMICMASK)
                return;
 
        {
@@ -701,3 +703,75 @@ Exit:
                else model_free(race);
        }
 }
+
+void raceCheckReadOpt(thread_id_t thread, const void * addr, int bytes)
+{
+       const ModelExecution * execution = get_execution();
+       ClockVector *currClock = execution->get_cv(thread);
+       if (currClock == NULL)
+               return;
+
+       int threadid = id_to_int(thread);
+       modelclock_t ourClock = currClock->getClock(thread);
+       bool should_expand = threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR;
+
+       bool hasRace = false;
+
+       for (int i = 0; i < bytes; i++) {
+               const void * location = (void *)(((uintptr_t)addr) + i);
+               uint64_t *shadow = lookupAddressEntry(location);
+               uint64_t shadowval = *shadow;
+
+               struct DataRace * race = NULL;
+
+               /* Do full record */
+               if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
+                       race = fullRaceCheckRead(thread, location, shadow, currClock);
+                       goto Exit;
+               }
+
+               {
+                       /* Thread ID is too large or clock is too large. */
+                       if (should_expand) {
+                               expandRecord(shadow);
+                               race = fullRaceCheckRead(thread, location, shadow, currClock);
+                               goto Exit;
+                       }
+
+                       /* Check for datarace against last write. */
+
+                       modelclock_t writeClock = WRITEVECTOR(shadowval);
+                       thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
+
+                       // If there is already has a race, skip check
+                       if (!hasRace && clock_may_race(currClock, thread, writeClock, writeThread)) {
+                               /* We have a datarace */
+                               race = reportDataRace(writeThread, writeClock, true, execution->get_parent_action(thread), false, location);
+                       }
+
+                       modelclock_t readClock = READVECTOR(shadowval);
+                       thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
+
+                       if (clock_may_race(currClock, thread, readClock, readThread)) {
+                               /* We don't subsume this read... Have to expand record. */
+                               expandRecord(shadow);
+                               struct RaceRecord *record = (struct RaceRecord *) (*shadow);
+                               record->thread[1] = thread;
+                               record->readClock[1] = ourClock;
+                               record->numReads++;
+
+                               goto Exit;
+                       }
+
+                       *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock) | (shadowval & ATOMICMASK);
+               }
+Exit:
+               if (race) {
+                       hasRace = true;
+                       race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
+                       if (raceset->add(race))
+                               assert_race(race);
+                       else model_free(race);
+               }
+       }
+}