#include "mymemory.h"
#include "clockvector.h"
#include "config.h"
+#include "action.h"
+#include "execution.h"
-struct ShadowTable *root;
-std::vector<struct DataRace *> unrealizedraces;
-void *memory_base;
-void *memory_top;
+static struct ShadowTable *root;
+SnapVector<struct 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()
*/
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++) {
*/
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. */
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 */
}
/** 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);