check in my stuff...
Conflicts:
model.cc
threads.h
race->isnewwrite=isnewwrite;
race->address=address;
unrealizedraces.push_back(race);
- checkDataRaces();
+
+ /* If the race is realized, bail out now. */
+ if (checkDataRaces()) {
+ model->assert_thread();
+ }
}
/** This function goes through the list of unrealized data races,
* removes the impossible ones, and print the realized ones. */
-void checkDataRaces() {
- if (true) {
+bool checkDataRaces() {
+ if (model->isfeasibleprefix()) {
/* Prune the non-racing unrealized dataraces */
unsigned int i,newloc=0;
for(i=0;i<unrealizedraces.size();i++) {
}
if (newloc!=i)
unrealizedraces.resize(newloc);
- for(i=0;i<unrealizedraces.size();i++) {
- struct DataRace * race=unrealizedraces[i];
- printRace(race);
+
+ if (unrealizedraces.size()!=0) {
+ /* We have an actual realized race. */
+ for(i=0;i<unrealizedraces.size();i++) {
+ struct DataRace * race=unrealizedraces[i];
+ printRace(race);
+ }
+ return true;
}
}
+ return false;
}
void printRace(struct DataRace * race) {
void initRaceDetector();
void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock);
void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock);
-void checkDataRaces();
+bool checkDataRaces();
void printRace(struct DataRace *race);
extern std::vector<struct DataRace *> unrealizedraces;
#include "clockvector.h"
#include "cyclegraph.h"
#include "promise.h"
+#include "datarace.h"
#define INITIAL_THREAD_ID 0
node_stack(new NodeStack()),
next_backtrack(NULL),
mo_graph(new CycleGraph()),
- failed_promise(false)
+ failed_promise(false),
+ asserted(false)
{
}
nextThread = NULL;
next_backtrack = NULL;
failed_promise = false;
+ reset_asserted();
snapshotObject->backTrackBeforeStep(0);
}
}
} else if (curr->is_write()) {
if (w_modification_order(curr))
- updated = true;;
+ updated = true;
if (resolve_promises(curr))
updated = true;
}
return get_next_replay_thread();
}
+/** @returns whether the current partial trace must be a prefix of a
+ * feasible trace. */
+
+bool ModelChecker::isfeasibleprefix() {
+ return promises->size()==0;
+}
+
/** @returns whether the current partial trace is feasible. */
bool ModelChecker::isfeasible() {
return !mo_graph->checkForCycles() && !failed_promise;
it++;
}
+ // If we resolved promises or data races, see if we have realized a data race.
+ if (checkDataRaces()) {
+ model->set_assert();
+ }
+
return updated;
}
} else
promise_index++;
}
+
return resolved;
}
bool ModelChecker::take_step() {
Thread *curr, *next;
+ if (has_asserted())
+ return false;
+
curr = thread_current();
if (curr) {
if (curr->get_state() == THREAD_READY) {
/** @return The currently executing Thread. */
Thread * get_current_thread() { return scheduler->get_current_thread(); }
+ void assert_thread();
int switch_to_master(ModelAction *act);
ClockVector * get_cv(thread_id_t tid);
ModelAction * get_parent_action(thread_id_t tid);
std::vector<const ModelAction *> *release_heads);
void finish_execution();
+ bool isfeasibleprefix();
MEMALLOC
private: