projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
datarace: don't export unrealized race vector
[model-checker.git]
/
datarace.cc
diff --git
a/datarace.cc
b/datarace.cc
index 5f007f36522754960db4c4588c80ee75c2a49ad5..41bfbe0eaa5679d77faa111502833205c936e540 100644
(file)
--- a/
datarace.cc
+++ b/
datarace.cc
@@
-7,12
+7,18
@@
#include "clockvector.h"
#include "config.h"
#include "action.h"
#include "clockvector.h"
#include "config.h"
#include "action.h"
+#include "execution.h"
+#include "stl-model.h"
static struct ShadowTable *root;
static struct ShadowTable *root;
-
SnapVector<struct
DataRace *> unrealizedraces;
+
static SnapVector<
DataRace *> unrealizedraces;
static void *memory_base;
static void *memory_top;
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()
@@
-123,7
+129,7
@@
static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
*/
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++) {
@@
-180,7
+186,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 */
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);
}
}
}
}
@@
-191,7
+197,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 */
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;
}
record->numReads = 0;
@@
-201,10
+207,11
@@
void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl
}
/** This function does race detection on a write. */
}
/** 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;
{
uint64_t *shadow = lookupAddressEntry(location);
uint64_t shadowval = *shadow;
+ ClockVector *currClock = get_execution()->get_cv(thread);
/* Do full record */
if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
/* Do full record */
if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
@@
-229,7
+236,7
@@
void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
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. */
@@
-239,7
+246,7
@@
void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
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);
}
@@
-256,7
+263,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 */
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 */
@@
-304,10
+311,11
@@
void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shado
}
/** This function does race detection on a read. */
}
/** 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;
{
uint64_t *shadow = lookupAddressEntry(location);
uint64_t shadowval = *shadow;
+ ClockVector *currClock = get_execution()->get_cv(thread);
/* Do full record */
if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
/* Do full record */
if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
@@
-332,7
+340,7
@@
void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currCl
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);
@@
-347,3
+355,8
@@
void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currCl
*shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
}
*shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
}
+
+bool haveUnrealizedRaces()
+{
+ return !unrealizedraces.empty();
+}