-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;
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;
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;
- 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);
}
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);
}
- 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,
- 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,
- 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()
+ );
if (clock_may_race(currClock, thread, readClock, readThread)) {
/* We have a datarace */
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 */
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);
if (clock_may_race(currClock, thread, readClock, readThread)) {
/* We have a datarace */
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 */
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);
}
}
*shadow = ENCODEOP(0, 0, threadid, ourClock);
}
if (clock_may_race(currClock, thread, writeClock, writeThread)) {
/* We have a datarace */
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);
if (clock_may_race(currClock, thread, writeClock, writeThread)) {
/* We have a datarace */
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);
*shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
}
*shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
}