From: Brian Norris <banorris@uci.edu> Date: Fri, 16 Nov 2012 22:38:26 +0000 (-0800) Subject: datarace: redirect "Data race @ ..." messages to model-checker bug list X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=122aad1259a2df612ad39c640551be8da9cb26b9;p=cdsspec-compiler.git datarace: redirect "Data race @ ..." messages to model-checker bug list Data race information was previously printed in multiple ways: through the datarace.cc printRace() method and through the model-checker assert_bug() method. Start unifying that. Other notes: - Data race objects probably should be freed (even though they are snapshotted). I fix this. - Races could be printed more than once previously, since the unrealizedraces vector was never cleared of realized races. Now, we clear this vector every time we process it (in a feasible execution), either stashing a bug message or dropping the race entirely. --- diff --git a/datarace.cc b/datarace.cc index 448929b..8d913c7 100644 --- a/datarace.cc +++ b/datarace.cc @@ -106,43 +106,53 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is model->assert_bug("Data race", true); } -/** This function goes through the list of unrealized data races, - * removes the impossible ones, and print the realized ones. */ - +/** + * @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 */ - unsigned int i,newloc=0; - for(i=0;i<unrealizedraces.size();i++) { - struct DataRace * race=unrealizedraces[i]; + 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)) { - unrealizedraces[newloc++]=race; + assert_race(race); + race_asserted = true; } + snapshot_free(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; - } + unrealizedraces.clear(); + return race_asserted; } return false; } -void printRace(struct DataRace *race) +/** + * @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) { - printf("Data race detected @ address %p:\n", race->address); - printf(" Access 1: %5s in thread %2d @ clock %3u\n", + 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); - printf(" Access 2: %5s in thread %2d @ clock %3u\n", + 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); } /** This function does race detection for a write on an expanded record. */ diff --git a/datarace.h b/datarace.h index 2fb1a7f..d1f91b2 100644 --- a/datarace.h +++ b/datarace.h @@ -45,7 +45,7 @@ void initRaceDetector(); void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock); void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock); bool checkDataRaces(); -void printRace(struct DataRace *race); +void assert_race(struct DataRace *race); extern std::vector<struct DataRace *> unrealizedraces;