From: Brian Norris <banorris@uci.edu>
Date: Thu, 6 Sep 2012 21:07:44 +0000 (-0700)
Subject: model: complete the Thread teardown during THREAD_FINISH
X-Git-Tag: pldi2013~235^2^2
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=33a0676006be6e35e0fa9e6bd907ca7bae5e53e2;p=model-checker.git

model: complete the Thread teardown during THREAD_FINISH
---

diff --git a/model.cc b/model.cc
index 0bb9617..56723c7 100644
--- a/model.cc
+++ b/model.cc
@@ -311,6 +311,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 			Thread *wake = th->pop_wait_list();
 			scheduler->wake(wake);
 		}
+		th->complete();
 	}
 
 	/* Deal with new thread */
@@ -978,11 +979,8 @@ bool ModelChecker::take_step() {
 			ASSERT(current_action);
 			nextThread = check_current_action(current_action);
 			current_action = NULL;
-			if (!curr->is_blocked())
+			if (!curr->is_blocked() && !curr->is_complete())
 				scheduler->add_thread(curr);
-		} else if (curr->get_state() == THREAD_RUNNING) {
-			/* Stopped while running; i.e., completed */
-			curr->complete();
 		} else {
 			ASSERT(false);
 		}