Merge branch 'new_fuzzer' into branch-weiyu

[c11tester.git] / datarace.cc

diff --git a/datarace.cc b/datarace.cc
index af70041b231fbccbba9f109a8c4b282267e4a022..9ba59399f2a07c52cf62136a897e59cd55717739 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -8,9 +8,10 @@
 #include "config.h"
 #include "action.h"
 #include "execution.h"
+#include "stl-model.h"
 
 static struct ShadowTable *root;
-SnapVector<struct DataRace *> unrealizedraces;
+static SnapVector<DataRace *> *unrealizedraces;
 static void *memory_base;
 static void *memory_top;
 
@@ -25,6 +26,7 @@ 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;
+       unrealizedraces = new SnapVector<DataRace *>();
 }
 
 void * table_calloc(size_t size)
@@ -67,7 +69,7 @@ static uint64_t * lookupAddressEntry(const void *address)
  * @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)
+                                                                                                        modelclock_t clock2, thread_id_t tid2)
 {
        return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
 }
@@ -110,7 +112,7 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
        race->newaction = newaction;
        race->isnewwrite = isnewwrite;
        race->address = address;
-       unrealizedraces.push_back(race);
+       unrealizedraces->push_back(race);
 
        /* If the race is realized, bail out now. */
        if (checkDataRaces())
@@ -131,15 +133,15 @@ bool checkDataRaces()
        if (get_execution()->isfeasibleprefix()) {
                bool race_asserted = false;
                /* Prune the non-racing unrealized dataraces */
-               for (unsigned 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)) {
                                assert_race(race);
                                race_asserted = true;
                        }
                        snapshot_free(race);
                }
-               unrealizedraces.clear();
+               unrealizedraces->clear();
                return race_asserted;
        }
        return false;
@@ -156,16 +158,16 @@ bool checkDataRaces()
 void assert_race(struct DataRace *race)
 {
        model->assert_bug(
-                       "Data race detected @ address %p:\n"
-                       "    Access 1: %5s in thread %2d @ clock %3u\n"
-                       "    Access 2: %5s in thread %2d @ clock %3u",
-                       race->address,
-                       race->isoldwrite ? "write" : "read",
-                       id_to_int(race->oldthread),
-                       race->oldclock,
-                       race->isnewwrite ? "write" : "read",
-                       id_to_int(race->newaction->get_tid()),
-                       race->newaction->get_seq_number()
+               "Data race detected @ address %p:\n"
+               "    Access 1: %5s in thread %2d @ clock %3u\n"
+               "    Access 2: %5s in thread %2d @ clock %3u",
+               race->address,
+               race->isoldwrite ? "write" : "read",
+               id_to_int(race->oldthread),
+               race->oldclock,
+               race->isnewwrite ? "write" : "read",
+               id_to_int(race->newaction->get_tid()),
+               race->newaction->get_seq_number()
                );
 }
 
@@ -176,12 +178,12 @@ void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl
 
        /* Check for datarace against last read. */
 
-       for (int i = 0; i < record->numReads; i++) {
+       for (int i = 0;i < record->numReads;i++) {
                modelclock_t readClock = record->readClock[i];
                thread_id_t readThread = record->thread[i];
 
                /* Note that readClock can't actuall be zero here, so it could be
-                        optimized. */
+                        optimized. */
 
                if (clock_may_race(currClock, thread, readClock, readThread)) {
                        /* We have a datarace */
@@ -269,15 +271,15 @@ void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shado
 
        int copytoindex = 0;
 
-       for (int i = 0; i < record->numReads; i++) {
+       for (int i = 0;i < record->numReads;i++) {
                modelclock_t readClock = record->readClock[i];
                thread_id_t readThread = record->thread[i];
 
                /*  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.  */
+                               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 */
@@ -354,3 +356,8 @@ void raceCheckRead(thread_id_t thread, const void *location)
 
        *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
 }
+
+bool haveUnrealizedRaces()
+{
+       return !unrealizedraces->empty();
+}