model/schedule: comput "reduadant" measurement, print along with traces
authorBrian Norris <banorris@uci.edu>
Thu, 28 Feb 2013 20:23:51 +0000 (12:23 -0800)
committerBrian Norris <banorris@uci.edu>
Thu, 28 Feb 2013 20:23:51 +0000 (12:23 -0800)
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
schedule.cc
schedule.h

index 591d42a..fa4dcc6 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++;
                stats.num_buggy_executions++;
        else if (is_complete_execution())
                stats.num_complete++;
-       else
+       else if (scheduler->all_threads_sleeping())
                stats.num_redundant++;
                stats.num_redundant++;
+       else
+               ASSERT(false);
 }
 
 /** @brief Print execution stats */
 }
 
 /** @brief Print execution stats */
@@ -2792,9 +2794,11 @@ void ModelChecker::print_summary() const
 #endif
 
        model_print("Execution %d:", stats.num_total);
 #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");
                model_print("\n");
-       else
+       else
                print_infeasibility(" INFEASIBLE");
        print_list(action_trace);
        model_print("\n");
                print_infeasibility(" INFEASIBLE");
        print_list(action_trace);
        model_print("\n");
index 44def6d..a2eb4cf 100644 (file)
@@ -96,6 +96,23 @@ bool Scheduler::is_sleep_set(const Thread *t) const
        return get_enabled(t) == THREAD_SLEEP_SET;
 }
 
        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());
 enabled_type_t Scheduler::get_enabled(const Thread *t) const
 {
        int id = id_to_int(t->get_id());
index 0865310..c8555b6 100644 (file)
@@ -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 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
        void set_scheduler_thread(thread_id_t tid);
 
        SNAPSHOTALLOC