#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()
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)
* @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;
}
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())
*/
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;
*/
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",
- race->isoldwrite ? "write" : "read",
- id_to_int(race->oldthread), race->oldclock);
- ptr += sprintf(ptr, " Access 2: %5s in thread %2d @ clock %3u",
- race->isnewwrite ? "write" : "read",
- id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
- model->assert_bug(buf);
+ 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()
+ );
}
/** This function does race detection for a write on an expanded record. */
/* 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 */
- reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
+ reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
}
}
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;
}
/** 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)) {
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. */
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);
}
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 */
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 */
}
/** 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)) {
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);
*shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
}
+
+bool haveUnrealizedRaces()
+{
+ return !unrealizedraces->empty();
+}
projects / c11tester.git / blobdiff