model: force THREAD_START to immediately follow THREAD_CREATE
authorBrian Norris <banorris@uci.edu>
Fri, 7 Sep 2012 18:25:25 +0000 (11:25 -0700)
committerBrian Norris <banorris@uci.edu>
Fri, 7 Sep 2012 18:29:16 +0000 (11:29 -0700)
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.

model.cc

index e71947d..811cf82 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();
+       /* 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();
 }