From: Derek Yeh <djyeh@plrg-1.ics.uci.edu>
Date: Fri, 31 Jul 2020 01:19:58 +0000 (-0700)
Subject: fix edge case
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=64383895f2f6937f62ebb8dd52e2db0932ca5278

fix edge case
---

diff --git a/model.cc b/model.cc
index 53bb7b0d..2f744eee 100644
--- a/model.cc
+++ b/model.cc
@@ -351,9 +351,9 @@ void ModelChecker::continueExecution(Thread *old)
 		checkfree += params.checkthreshold;
 		execution->collectActions();
 	}
+	thread_chosen = false;
 	curr_thread_num = 1;
-	thread_id_t tid = int_to_id(1);
-	Thread *thr = get_thread(tid);
+	Thread *thr = getNextThread();
 	scheduler->set_current_thread(thr);
 	if (Thread::swap(old, thr) < 0) {
 		perror("swap threads");
@@ -361,6 +361,20 @@ void ModelChecker::continueExecution(Thread *old)
 	}
 }
 
+Thread* ModelChecker::getNextThread()
+{
+	Thread *thr = NULL;
+	for (unsigned int i = curr_thread_num; i < get_num_threads(); i++) {
+		thread_id_t tid = int_to_id(i);
+		thr = get_thread(tid);
+		if (!thr->is_complete() && !thr->get_pending()) {
+			curr_thread_num = i;
+			break;
+		}
+	}
+	return thr;
+}
+
 void ModelChecker::finishExecution(Thread *old) 
 {
 	scheduler->set_current_thread(NULL);
@@ -399,18 +413,11 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
 
 	old->set_pending(act);
 
-	Thread *next = NULL;
 	curr_thread_num++;
-	while (curr_thread_num < get_num_threads()) {
-		thread_id_t tid = int_to_id(curr_thread_num);
-		next = get_thread(tid);
-		if (!next->is_complete() && !next->get_pending())
-			break;
-		curr_thread_num++;
-	}
+	Thread* next = getNextThread();
 
 	if (old->is_waiting_on(old))
-		assert_bug("Deadlock detected (thread %u)", curr_thread_num);
+		assert_bug("Deadlock detected (thread %u)", curr_thread_num-1);
 
 	ModelAction *act2 = old->get_pending();
 		
diff --git a/model.h b/model.h
index dc36eb63..cabd9904 100644
--- a/model.h
+++ b/model.h
@@ -58,6 +58,7 @@ public:
 	void continueExecution(Thread *old);
 	void finishExecution(Thread *old);
 	void consumeAction();
+	Thread * getNextThread();
 
 	void assert_bug(const char *msg, ...);