From ecf16617a0c289981925fcd2437595f3a2fce8fe Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 16 Nov 2012 14:44:32 -0800 Subject: [PATCH] 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. --- datarace.cc | 2 +- model.cc | 8 +++----- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/datarace.cc b/datarace.cc index 8d913c7..bdfade3 100644 --- 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 ab16bf8..33e8805 100644 --- 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; } -- 2.34.1