}
/**
- * 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.
+ * Check if a Thread has entered a circular wait 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
+bool ModelChecker::is_circular_wait(const Thread *t) const
{
for (Thread *waiting = t->waiting_on() ; waiting != NULL; waiting = waiting->waiting_on())
if (waiting == t)
print_infeasibility(" INFEASIBLE");
print_list(action_trace);
model_print("\n");
+ if (!promises->empty()) {
+ model_print("Pending promises:\n");
+ for (unsigned int i = 0; i < promises->size(); i++) {
+ model_print(" [P%u] ", i);
+ (*promises)[i]->print();
+ }
+ model_print("\n");
+ }
}
/**
Thread *thr = get_thread(tid);
if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
switch_from_master(thr);
- if (check_deadlock(thr))
+ if (is_circular_wait(thr))
assert_bug("Deadlock detected");
}
}