From 2daff868a7ef4f6235c2776b746cec9947a87b13 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 28 Feb 2013 12:23:51 -0800
Subject: [PATCH 1/1] model/schedule: comput "reduadant" measurement, print
 along with traces

This will help debuggability. For instance, it will be more obvious that
right now, the 'deadlock.c' test is completing executions as "redundant"
when in fact they should be deadlocks.
---
 model.cc    | 10 +++++++---
 schedule.cc | 17 +++++++++++++++++
 schedule.h  |  1 +
 3 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/model.cc b/model.cc
index 591d42a..fa4dcc6 100644
--- a/model.cc
+++ b/model.cc
@@ -483,8 +483,10 @@ void ModelChecker::record_stats()
 		stats.num_buggy_executions++;
 	else if (is_complete_execution())
 		stats.num_complete++;
-	else
+	else if (scheduler->all_threads_sleeping())
 		stats.num_redundant++;
+	else
+		ASSERT(false);
 }
 
 /** @brief Print execution stats */
@@ -2792,9 +2794,11 @@ void ModelChecker::print_summary() const
 #endif
 
 	model_print("Execution %d:", stats.num_total);
-	if (isfeasibleprefix())
+	if (isfeasibleprefix()) {
+		if (scheduler->all_threads_sleeping())
+			model_print(" SLEEP-SET REDUNDANT");
 		model_print("\n");
-	else
+	} else
 		print_infeasibility(" INFEASIBLE");
 	print_list(action_trace);
 	model_print("\n");
diff --git a/schedule.cc b/schedule.cc
index 44def6d..a2eb4cf 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -96,6 +96,23 @@ bool Scheduler::is_sleep_set(const Thread *t) const
 	return get_enabled(t) == THREAD_SLEEP_SET;
 }
 
+/**
+ * @brief Check if execution is stuck with no enabled threads and some sleeping
+ * thread
+ * @return True if no threads are enabled an some thread is in the sleep set;
+ * false otherwise
+ */
+bool Scheduler::all_threads_sleeping() const
+{
+	bool sleeping = false;
+	for (int i = 0; i < enabled_len; i++)
+		if (enabled[i] == THREAD_ENABLED)
+			return false;
+		else if (enabled[i] == THREAD_SLEEP_SET)
+			sleeping = true;
+	return sleeping;
+}
+
 enabled_type_t Scheduler::get_enabled(const Thread *t) const
 {
 	int id = id_to_int(t->get_id());
diff --git a/schedule.h b/schedule.h
index 0865310..c8555b6 100644
--- a/schedule.h
+++ b/schedule.h
@@ -39,6 +39,7 @@ public:
 	bool is_enabled(const Thread *t) const;
 	bool is_enabled(thread_id_t tid) const;
 	bool is_sleep_set(const Thread *t) const;
+	bool all_threads_sleeping() const;
 	void set_scheduler_thread(thread_id_t tid);
 
 	SNAPSHOTALLOC
-- 
2.34.1