+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->switch_to_master(NULL);
+}
+
+/**
+ * @brief Check and report data races
+ *
+ * If the trace is feasible (a feasible prefix), clear out the list of
+ * unrealized data races, asserting any realized ones as execution bugs so that
+ * the model-checker will end the execution.
+ *
+ * @return True if any data races were realized
+ */
+bool checkDataRaces()
+{
+ if (model->isfeasibleprefix()) {
+ bool race_asserted = false;
+ /* Prune the non-racing unrealized dataraces */
+ for (unsigned 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)) {
+ assert_race(race);
+ race_asserted = true;
+ }
+ snapshot_free(race);
+ }
+ unrealizedraces.clear();
+ return race_asserted;
+ }
+ return false;
+}
+
+/**
+ * @brief Assert a data race
+ *
+ * Asserts a data race which is currently realized, causing the execution to
+ * end and stashing a message in the model-checker's bug list
+ *
+ * @param race The race to report
+ */
+void assert_race(struct DataRace *race)
+{
+ char buf[200];
+ char *ptr = buf;
+ ptr += sprintf(ptr, "Data race detected @ address %p:\n", race->address);
+ ptr += sprintf(ptr, " Access 1: %5s in thread %2d @ clock %3u\n",
+ race->isoldwrite ? "write" : "read",
+ id_to_int(race->oldthread), race->oldclock);
+ ptr += sprintf(ptr, " Access 2: %5s in thread %2d @ clock %3u",
+ race->isnewwrite ? "write" : "read",
+ id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
+ model->assert_bug(buf);