From 3cf4799ac961046bb2464ae1b6ee72f064d94716 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 6 Nov 2012 19:18:34 -0800 Subject: [PATCH] model: add deadlock detection This is only a simple end-of-execution deadlock detection. If we have a true deadlock, and no other threads are spinning, then our execution will exit --- we can recognize this state. For more complicated deadlocks involving other spinning threads, we need to perform some sort of depth-first-search cycle detection. --- model.cc | 22 ++++++++++++++++++++++ model.h | 1 + 2 files changed, 23 insertions(+) diff --git a/model.cc b/model.cc index ff1fdf9..94620ea 100644 --- a/model.cc +++ b/model.cc @@ -244,6 +244,26 @@ void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { } } +/** + * Check if we are in a deadlock. Should only be called at the end of an + * execution, although it should not give false positives in the middle of an + * execution (there should be some ENABLED thread). + * + * @return True if program is in a deadlock; false otherwise + */ +bool ModelChecker::is_deadlocked() const +{ + bool blocking_threads = false; + for (unsigned int i = 0; i < get_num_threads(); i++) { + Thread *t = get_thread(int_to_id(i)); + if (scheduler->is_enabled(t) != THREAD_DISABLED) + return false; + else if (!t->is_model_thread() && t->get_pending()) + blocking_threads = true; + } + return blocking_threads; +} + /** * Queries the model-checker for more executions to explore and, if one * exists, resets the model-checker state to execute a new execution. @@ -257,6 +277,8 @@ bool ModelChecker::next_execution() num_executions++; + if (is_deadlocked()) + printf("ERROR: DEADLOCK\n"); if (isfinalfeasible()) { printf("Earliest divergence point since last feasible execution:\n"); if (earliest_diverge) diff --git a/model.h b/model.h index 3ef6ee3..6d702b0 100644 --- a/model.h +++ b/model.h @@ -115,6 +115,7 @@ public: void finish_execution(); bool isfeasibleprefix(); void set_assert() {asserted=true;} + bool is_deadlocked() const; /** @brief Alert the model-checker that an incorrectly-ordered * synchronization was made */ -- 2.34.1