model: add improved (?) deadlock detection

This proactively detects cyclic waits in threads, using join or lock
information. It does not account for wait yet, but that is covered by
is_deadlocked(), at least in some cases.

diff --git a/model.cc b/model.cc
index 276d18e49a53758b79ef0955325f11f62c0da211..7a5edc7a1b8666ff8be384edd4e06f0e3ccc3f5e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -400,6 +400,22 @@ bool ModelChecker::is_deadlocked() const
        return blocking_threads;
 }
 
+/**
+ * Check if a Thread has entered a deadlock situation. This will not check
+ * other threads for potential deadlock situations, and may miss deadlocks
+ * involving WAIT.
+ *
+ * @param t The thread which may have entered a deadlock
+ * @return True if this Thread entered a deadlock; false otherwise
+ */
+bool ModelChecker::check_deadlock(const Thread *t) const
+{
+       for (Thread *waiting = t->waiting_on() ; waiting != NULL; waiting = waiting->waiting_on())
+               if (waiting == t)
+                       return true;
+       return false;
+}
+
 /**
  * Check if this is a complete execution. That is, have all thread completed
  * execution (rather than exiting because sleep sets have forced a redundant
@@ -3036,6 +3052,8 @@ void ModelChecker::run()
                                Thread *thr = get_thread(tid);
                                if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
                                        switch_from_master(thr);
+                                       if (check_deadlock(thr))
+                                               assert_bug("Deadlock detected");
                                }
                        }
 

diff --git a/model.h b/model.h
index d8c1be495075f2e276c770acab49cd7bbe29ea89..0cbff4ce36bad6148bb22a6d6d40a5bf4cf7a1a1 100644 (file)
--- a/model.h
+++ b/model.h
@@ -276,6 +276,7 @@ private:
        bool is_feasible_prefix_ignore_relseq() const;
        bool is_infeasible() const;
        bool is_deadlocked() const;
+       bool check_deadlock(const Thread *t) const;
        bool is_complete_execution() const;
        bool have_bug_reports() const;
        void print_bugs() const;