From: Brian Norris <banorris@uci.edu>
Date: Fri, 7 Sep 2012 18:25:25 +0000 (-0700)
Subject: model: force THREAD_START to immediately follow THREAD_CREATE
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=8c83f796d2930427478e603d64e8410707011007;p=c11tester.git

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 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();
 }