action: add THREAD_FINISH action

[model-checker.git] / threads.cc

diff --git a/threads.cc b/threads.cc
index 9b7954d9386b6f5390ed42a32b43a53f5f5f1ca7..b3a1d5599fb541d340184e0e2ba0f7589c0ec5ae 100644 (file)
--- 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));
 }
 
 /**