model: fix ASSERT()
authorBrian Norris <banorris@uci.edu>
Fri, 1 Mar 2013 23:01:47 +0000 (15:01 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 1 Mar 2013 23:01:47 +0000 (15:01 -0800)
Apparently this ASSERT() is still not good. ASSERT() was triggered, for
example, with:

  $ ./run.sh test/linuxrwlocks.o -f 4 -m 1

model.cc

index 7048096..9135e5c 100644 (file)
--- 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 */