From 22efc98d95682e33aa85fd85f5e79d887875734b Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 1 Mar 2013 15:01:47 -0800 Subject: [PATCH] model: fix ASSERT() Apparently this ASSERT() is still not good. ASSERT() was triggered, for example, with: $ ./run.sh test/linuxrwlocks.o -f 4 -m 1 --- model.cc | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/model.cc b/model.cc index 7048096..9135e5c 100644 --- a/model.cc +++ b/model.cc @@ -483,10 +483,16 @@ void ModelChecker::record_stats() stats.num_buggy_executions++; else if (is_complete_execution()) stats.num_complete++; - else if (scheduler->all_threads_sleeping()) + else { stats.num_redundant++; - else - ASSERT(false); + + /** + * @todo We can violate this ASSERT() when fairness/sleep sets + * conflict to cause an execution to terminate, e.g. with: + * Scheduler: [0: disabled][1: disabled][2: sleep][3: current, enabled] + */ + //ASSERT(scheduler->all_threads_sleeping()); + } } /** @brief Print execution stats */ -- 2.34.1