- if (readClock!=0) {
- record->capacity=INITCAPACITY;
- record->thread=(thread_id_t *) malloc(sizeof(thread_id_t)*record->capacity);
- record->readClock=(modelclock_t *) malloc(sizeof(modelclock_t)*record->capacity);
- record->numReads=1;
- record->thread[0]=readThread;
- record->readClock[0]=readClock;
+/** 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->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;