+/** This function is called when we detect a data race.*/
+static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address) {
+ struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
+ race->oldthread=oldthread;
+ race->oldclock=oldclock;
+ race->isoldwrite=isoldwrite;
+ race->newaction=newaction;
+ race->isnewwrite=isnewwrite;
+ race->address=address;
+ unrealizedraces.push_back(race);
+
+ /* 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. */
+
+bool checkDataRaces() {
+ if (model->isfeasibleprefix()) {
+ /* Prune the non-racing unrealized dataraces */
+ unsigned int i,newloc=0;
+ for(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)) {
+ unrealizedraces[newloc++]=race;
+ }
+ }
+ if (newloc!=i)
+ unrealizedraces.resize(newloc);
+
+ 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 @ address %p:\n", race->address);
+ printf(" Access 1: %5s in thread %2d @ clock %3u\n",
+ race->isoldwrite ? "write" : "read",
+ id_to_int(race->oldthread), race->oldclock);
+ printf(" Access 2: %5s in thread %2d @ clock %3u\n",
+ race->isnewwrite ? "write" : "read",
+ id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());