From: Brian Norris <banorris@uci.edu>
Date: Thu, 6 Sep 2012 20:54:06 +0000 (-0700)
Subject: model: hook up THREAD_JOIN and THREAD_FINISH actions
X-Git-Tag: pldi2013~235^2^2~3
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=1ca0878f2578b5a928be493f80c72e159cb27f55

model: hook up THREAD_JOIN and THREAD_FINISH actions
---

diff --git a/model.cc b/model.cc
index ec953ef..d171ad0 100644
--- a/model.cc
+++ b/model.cc
@@ -299,6 +299,18 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 	if (curr->get_type() == THREAD_CREATE) {
 		Thread *th = (Thread *)curr->get_location();
 		th->set_creation(curr);
+	} else if (curr->get_type() == THREAD_JOIN) {
+		Thread *wait, *join;
+		wait = get_thread(curr->get_tid());
+		join = (Thread *)curr->get_location();
+		if (!join->is_complete())
+			scheduler->wait(wait, join);
+	} else if (curr->get_type() == THREAD_FINISH) {
+		Thread *th = get_thread(curr->get_tid());
+		while (!th->wait_list_empty()) {
+			Thread *wake = th->pop_wait_list();
+			scheduler->wake(wake);
+		}
 	}
 
 	/* Deal with new thread */
@@ -970,7 +982,8 @@ bool ModelChecker::take_step() {
 				nextThread = check_current_action(current_action);
 				current_action = NULL;
 			}
-			scheduler->add_thread(curr);
+			if (!curr->is_blocked())
+				scheduler->add_thread(curr);
 		} else if (curr->get_state() == THREAD_RUNNING) {
 			/* Stopped while running; i.e., completed */
 			curr->complete();