race->isnewwrite=isnewwrite;
race->address=address;
unrealizedraces.push_back(race);
- checkDataRaces();
+
+ /* If the race is realized, bail out now. */
+ if (checkDataRaces()) {
+ model->set_assert();
+ model->switch_to_master(NULL);
+ }
}
/** 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) {
printf("Datarace detected\n");
printf("Location %p\n", race->address);
printf("Initial access: thread %u clock %u, iswrite %u\n",race->oldthread,race->oldclock, race->isoldwrite);
- printf("Second access: thread %u, iswrite %u\n", race->newaction->get_tid(), race->isnewwrite);
+ printf("Second access: thread %u clock %u, iswrite %u\n", race->newaction->get_tid(), race->newaction->get_seq_number() , race->isnewwrite);
}
/** This function does race detection for a write on an expanded record. */