From: Brian Norris <banorris@uci.edu>
Date: Thu, 6 Sep 2012 20:07:26 +0000 (-0700)
Subject: action: add THREAD_FINISH action
X-Git-Tag: pldi2013~235^2^2~9
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;ds=sidebyside;h=f472540b6ab3b65c91221f6f0790d8327333a5c2;p=model-checker.git

action: add THREAD_FINISH action

For cleanly finalizing a thread.
---

diff --git a/action.cc b/action.cc
index 692d14c..205bedb 100644
--- a/action.cc
+++ b/action.cc
@@ -218,6 +218,9 @@ void ModelAction::print(void) const
 	case THREAD_JOIN:
 		type_str = "thread join";
 		break;
+	case THREAD_FINISH:
+		type_str = "thread finish";
+		break;
 	case ATOMIC_READ:
 		type_str = "atomic read";
 		break;
diff --git a/action.h b/action.h
index 6559928..3e590aa 100644
--- a/action.h
+++ b/action.h
@@ -32,6 +32,7 @@ typedef enum action_type {
 	THREAD_START,         /**< First action in each thread */
 	THREAD_YIELD,         /**< A thread yield action */
 	THREAD_JOIN,          /**< A thread join action */
+	THREAD_FINISH,        /**< A thread completion action */
 	ATOMIC_READ,          /**< An atomic read action */
 	ATOMIC_WRITE,         /**< An atomic write action */
 	ATOMIC_RMWR,          /**< The read part of an atomic RMW action */
diff --git a/threads.cc b/threads.cc
index 9b7954d..b3a1d55 100644
--- a/threads.cc
+++ b/threads.cc
@@ -44,6 +44,9 @@ void thread_startup()
 
 	/* Call the actual thread function */
 	curr_thread->start_routine(curr_thread->arg);
+
+	/* Finish thread properly */
+	model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, curr_thread));
 }
 
 /**