+/** 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, 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\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 clock %u, iswrite %u\n", race->newaction->get_tid(), race->newaction->get_seq_number() , race->isnewwrite);