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.

diff --git a/model.cc b/model.cc
index 591d42a1ab3dbbc9aae2b8ea152e252c58379fd5..fa4dcc6fd3976281633317152bd4450d636fcc0c 100644 (file)
--- 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 44def6d67583e1282605de06fbb72dfe4fc3ab6b..a2eb4cf7254834fecac49905838d53b647b95de5 100644 (file)
--- 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 0865310a27ed4509b3646e003aa015eeb141f00a..c8555b6916d9f9badc8f69d14618ec73de8ffeae 100644 (file)
--- 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