From 626e8f932c7cb841ef6ba75c86fe7be2aaa9f869 Mon Sep 17 00:00:00 2001 From: Derek Yeh Date: Mon, 27 Jul 2020 22:52:49 -0700 Subject: [PATCH] fix bugs --- model.cc | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/model.cc b/model.cc index 2aacaa2d..5decd2be 100644 --- a/model.cc +++ b/model.cc @@ -440,6 +440,9 @@ uint64_t ModelChecker::switch_thread(ModelAction *act) exit(EXIT_FAILURE); } } else { + if (old->is_waiting_on(old)) + assert_bug("Deadlock detected (thread %u)", curr_thread_num); + if (execution->has_asserted()) finishExecution(old); if (!chosen_thread) @@ -450,7 +453,11 @@ uint64_t ModelChecker::switch_thread(ModelAction *act) chosen_thread->set_wakeup_state(false); chosen_thread->set_pending(NULL); chosen_thread = NULL; - continueExecution(old); // Allow this thread to stash the next pending action + // Allow this thread to stash the next pending action + if (should_terminate_execution()) + finishExecution(old); + else + continueExecution(old); } else { /* Consume the next action for a Thread */ consumeAction(); -- 2.34.1