model: complete the Thread teardown during THREAD_FINISH

diff --git a/model.cc b/model.cc
index 0bb96175eff46b3cfc00b8d926b13055ff8e9c9a..56723c7d5660077c3b1e27d484976d5092388bd7 100644 (file)
--- 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);
                }
                        Thread *wake = th->pop_wait_list();
                        scheduler->wake(wake);
                }

+               th->complete();

        }
 
        /* Deal with new thread */
        }
 
        /* Deal with new thread */


@@ -978,11 +979,8 @@ bool ModelChecker::take_step() {
                        ASSERT(current_action);
                        nextThread = check_current_action(current_action);
                        current_action = NULL;
                        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);
                                scheduler->add_thread(curr);

-               } else if (curr->get_state() == THREAD_RUNNING) {
-                       /* Stopped while running; i.e., completed */
-                       curr->complete();

                } else {
                        ASSERT(false);
                }
                } else {
                        ASSERT(false);
                }