model: force THREAD_START to immediately follow THREAD_CREATE

Note that on the current userprog.c test case, this change causes more
infeasible executions to appear. This is somewhat unexpected but probably just
a result of sub-optimal scheduling.

diff --git a/model.cc b/model.cc
index e71947ddd5540f6e2db045deac77644e6a09a862..811cf8251ed4252179fefbceb8f4c5a9c5e2b8dd 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -370,6 +370,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        /* Do not split atomic actions. */
        if (curr->is_rmwr())
                return thread_current();
        /* Do not split atomic actions. */
        if (curr->is_rmwr())
                return thread_current();

+       /* The THREAD_CREATE action points to the created Thread */
+       else if (curr->get_type() == THREAD_CREATE)
+               return (Thread *)curr->get_location();

        else
                return get_next_replay_thread();
 }
        else
                return get_next_replay_thread();
 }