From: Brian Norris <banorris@uci.edu>
Date: Fri, 1 Mar 2013 23:01:47 +0000 (-0800)
Subject: model: fix ASSERT()
X-Git-Tag: oopsla2013~192
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=22efc98d95682e33aa85fd85f5e79d887875734b

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
---

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 */