These public interfaces are no longer presentin ModelChecker.
#include "clockvector.h"
#include "config.h"
#include "action.h"
#include "clockvector.h"
#include "config.h"
#include "action.h"
static struct ShadowTable *root;
SnapVector<struct DataRace *> unrealizedraces;
static void *memory_base;
static 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()
/** This function initialized the data race detector. */
void initRaceDetector()
*/
bool 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++) {
bool race_asserted = false;
/* Prune the non-racing unrealized dataraces */
for (unsigned i = 0; i < unrealizedraces.size(); i++) {
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);
{
uint64_t *shadow = lookupAddressEntry(location);
uint64_t shadowval = *shadow;
{
uint64_t *shadow = lookupAddressEntry(location);
uint64_t shadowval = *shadow;
- ClockVector *currClock = model->get_cv(thread);
+ ClockVector *currClock = get_execution()->get_cv(thread);
/* Do full record */
if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
/* Do full record */
if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
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);
}
/* Check for datarace against last write. */
}
/* Check for datarace against last write. */
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);
}
/* Shorten vector when possible */
}
/* Shorten vector when possible */
{
uint64_t *shadow = lookupAddressEntry(location);
uint64_t shadowval = *shadow;
{
uint64_t *shadow = lookupAddressEntry(location);
uint64_t shadowval = *shadow;
- ClockVector *currClock = model->get_cv(thread);
+ ClockVector *currClock = get_execution()->get_cv(thread);
/* Do full record */
if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
/* Do full record */
if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
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);
}
modelclock_t readClock = READVECTOR(shadowval);
}
modelclock_t readClock = READVECTOR(shadowval);
void switch_from_master(Thread *thread);
uint64_t switch_to_master(ModelAction *act);
void switch_from_master(Thread *thread);
uint64_t switch_to_master(ModelAction *act);
- ClockVector * get_cv(thread_id_t tid) const;
- ModelAction * get_parent_action(thread_id_t tid) const;
void check_promises_thread_disabled();
void check_promises_thread_disabled();
- bool isfeasibleprefix() const;
bool assert_bug(const char *msg, ...);
void assert_user_bug(const char *msg);
bool assert_bug(const char *msg, ...);
void assert_user_bug(const char *msg);
#include <mutex>
#include "model.h"
#include <mutex>
#include "model.h"
#include "threads-model.h"
#include "clockvector.h"
#include "action.h"
#include "threads-model.h"
#include "clockvector.h"
#include "action.h"
state.locked = NULL;
thread_id_t tid = thread_current()->get_id();
state.alloc_tid = tid;
state.locked = NULL;
thread_id_t tid = thread_current()->get_id();
state.alloc_tid = tid;
- state.alloc_clock = model->get_cv(tid)->getClock(tid);
+ state.alloc_clock = model->get_execution()->get_cv(tid)->getClock(tid);