From a26fa96048fab9b13239e49e37ed8cf8c39583c9 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Sat, 2 Mar 2013 23:53:58 -0800 Subject: [PATCH] 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. --- model.cc | 18 ++++++++++++++++++ model.h | 1 + 2 files changed, 19 insertions(+) diff --git a/model.cc b/model.cc index 276d18e..7a5edc7 100644 --- 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 d8c1be4..0cbff4c 100644 --- 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; -- 2.34.1