From: Derek Yeh <djyeh@plrg-1.ics.uci.edu>
Date: Tue, 28 Jul 2020 05:52:49 +0000 (-0700)
Subject: fix bugs
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=626e8f932c7cb841ef6ba75c86fe7be2aaa9f869

fix bugs
---

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();