README: extra "from"

[cdsspec-compiler.git] / datarace.cc

diff --git a/datarace.cc b/datarace.cc
index c70d41897f4fd5c4ff9c68f3daf96d4ed6240ba6..653039b3307e3ebfb195e2dc99efda36ae123a7c 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -6,12 +6,19 @@
 #include "mymemory.h"
 #include "clockvector.h"
 #include "config.h"
+#include "action.h"
+#include "execution.h"
+#include "stl-model.h"
 
-struct ShadowTable *root;
-std::vector<struct DataRace *> unrealizedraces;
-void *memory_base;
-void *memory_top;
+static struct ShadowTable *root;
+static SnapVector<DataRace *> *unrealizedraces;
+static void *memory_base;
+static void *memory_top;
 
+static const ModelExecution * get_execution()
+{
+       return model->get_execution();
+}
 
 /** This function initialized the data race detector. */
 void initRaceDetector()
@@ -19,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)
@@ -104,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())
@@ -122,18 +130,18 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
  */
 bool checkDataRaces()
 {
-       if (model->isfeasibleprefix()) {
+       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;
@@ -149,16 +157,18 @@ bool checkDataRaces()
  */
 void assert_race(struct DataRace *race)
 {
-       char buf[200];
-       char *ptr = buf;
-       ptr += sprintf(ptr, "Data race detected @ address %p:\n", race->address);
-       ptr += sprintf(ptr, "    Access 1: %5s in thread %2d @ clock %3u\n",
+       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);
-       ptr += sprintf(ptr, "    Access 2: %5s in thread %2d @ clock %3u",
+                       id_to_int(race->oldthread),
+                       race->oldclock,
                        race->isnewwrite ? "write" : "read",
-                       id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
-       model->assert_bug(buf);
+                       id_to_int(race->newaction->get_tid()),
+                       race->newaction->get_seq_number()
+               );
 }
 
 /** This function does race detection for a write on an expanded record. */
@@ -177,7 +187,7 @@ void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl
 
                if (clock_may_race(currClock, thread, readClock, readThread)) {
                        /* We have a datarace */
-                       reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
+                       reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
                }
        }
 
@@ -188,7 +198,7 @@ void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl
 
        if (clock_may_race(currClock, thread, writeClock, writeThread)) {
                /* We have a datarace */
-               reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
+               reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
        }
 
        record->numReads = 0;
@@ -198,10 +208,11 @@ void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl
 }
 
 /** This function does race detection on a write. */
-void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
+void raceCheckWrite(thread_id_t thread, void *location)
 {
        uint64_t *shadow = lookupAddressEntry(location);
        uint64_t shadowval = *shadow;
+       ClockVector *currClock = get_execution()->get_cv(thread);
 
        /* Do full record */
        if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
@@ -226,7 +237,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
 
        if (clock_may_race(currClock, thread, readClock, readThread)) {
                /* We have a datarace */
-               reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
+               reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
        }
 
        /* Check for datarace against last write. */
@@ -236,7 +247,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
 
        if (clock_may_race(currClock, thread, writeClock, writeThread)) {
                /* We have a datarace */
-               reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
+               reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
        }
        *shadow = ENCODEOP(0, 0, threadid, ourClock);
 }
@@ -253,7 +264,7 @@ void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shado
 
        if (clock_may_race(currClock, thread, writeClock, writeThread)) {
                /* We have a datarace */
-               reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
+               reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
        }
 
        /* Shorten vector when possible */
@@ -301,10 +312,11 @@ void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shado
 }
 
 /** This function does race detection on a read. */
-void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock)
+void raceCheckRead(thread_id_t thread, const void *location)
 {
        uint64_t *shadow = lookupAddressEntry(location);
        uint64_t shadowval = *shadow;
+       ClockVector *currClock = get_execution()->get_cv(thread);
 
        /* Do full record */
        if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
@@ -329,7 +341,7 @@ void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currCl
 
        if (clock_may_race(currClock, thread, writeClock, writeThread)) {
                /* We have a datarace */
-               reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
+               reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
        }
 
        modelclock_t readClock = READVECTOR(shadowval);
@@ -344,3 +356,8 @@ void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currCl
 
        *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
 }
+
+bool haveUnrealizedRaces()
+{
+       return !unrealizedraces->empty();
+}