a bug fix

[c11tester.git] / datarace.cc

diff --git a/datarace.cc b/datarace.cc
index 5ab52fc49eefa87ea1d2ad4e3c8c1a4b607f15f5..1cc407bb991889545210f54ec313ae84c49cf412 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -82,14 +82,19 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
        race->isnewwrite=isnewwrite;
        race->address=address;
        unrealizedraces.push_back(race);
-       checkDataRaces();
+
+       /* 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. */
 
-void checkDataRaces() {
-       if (true) {
+bool checkDataRaces() {
+       if (model->isfeasibleprefix()) {
                /* Prune the non-racing unrealized dataraces */
                unsigned int i,newloc=0;
                for(i=0;i<unrealizedraces.size();i++) {
@@ -100,18 +105,24 @@ void checkDataRaces() {
                }
                if (newloc!=i)
                        unrealizedraces.resize(newloc);
-               for(i=0;i<unrealizedraces.size();i++) {
-                       struct DataRace * race=unrealizedraces[i];
-                       printRace(race);
+
+               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, iswrite %u\n", race->newaction->get_tid(), race->isnewwrite);
+       printf("Second access: thread %u clock %u, iswrite %u\n", race->newaction->get_tid(), race->newaction->get_seq_number() , race->isnewwrite);
 }
 
 /** This function does race detection for a write on an expanded record. */