From 8c83f796d2930427478e603d64e8410707011007 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 7 Sep 2012 11:25:25 -0700 Subject: [PATCH] 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. --- model.cc | 3 +++ 1 file changed, 3 insertions(+) diff --git a/model.cc b/model.cc index e71947dd..811cf825 100644 --- 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(); } -- 2.34.1