dataraces: don't print an uninformative "Data race" bug msg

Now that checkDataRaces() handles all bug reporting and assertions on
its own, we don't need an additional bug report message printed by the
caller. In some cases, this means the caller doesn't have any action to
take. In one case (a race immediately-realized from a user thread), we
still need to "bail out" to the model-checker.

diff --git a/datarace.cc b/datarace.cc
index 8d913c708e80677a4817ae297a5aa66153ff544e..bdfade358e60595d1157e94cd2fcd0b5a18d0b86 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -103,7 +103,7 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
 
        /* If the race is realized, bail out now. */
        if (checkDataRaces())
-               model->assert_bug("Data race", true);
+               model->switch_to_master(NULL);
 }
 
 /**

diff --git a/model.cc b/model.cc
index ab16bf82528ea5ebf30766970b37faca5a6ada1f..33e8805078b546ac8d1b4f87dab3ea31e9be2651 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -446,8 +446,8 @@ bool ModelChecker::next_execution()
                if (is_deadlocked())
                        assert_bug("Deadlock detected");
 
-               print_bugs();
                checkDataRaces();
+               print_bugs();
                printf("\n");
                print_stats();
                print_summary();
@@ -917,8 +917,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
        }
 
        /* See if we have realized a data race */
-       if (checkDataRaces())
-               assert_bug("Data race");
+       checkDataRaces();
 }
 
 /**
@@ -1849,8 +1848,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
        }
 
        // If we resolved promises or data races, see if we have realized a data race.
-       if (checkDataRaces())
-               assert_bug("Data race");
+       checkDataRaces();
 
        return updated;
 }