From: Brian Norris <banorris@uci.edu>
Date: Thu, 13 Dec 2012 03:16:43 +0000 (-0800)
Subject: model: force first thread to run immediately
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1b561ab02787b79478b05189be3a4b342e5785f5;p=cdsspec-compiler.git

model: force first thread to run immediately

Forcing the first thread to run immediately yields us our first
ModelAction, so we won't have to special-case the case that
current_action == NULL.
---

diff --git a/model.cc b/model.cc
index 059a522..e6828c5 100644
--- a/model.cc
+++ b/model.cc
@@ -2781,9 +2781,13 @@ void ModelChecker::run()
 {
 	do {
 		thrd_t user_thread;
+		Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
 
-		/* Start user program */
-		add_thread(new Thread(&user_thread, &user_main_wrapper, NULL));
+		add_thread(t);
+
+		/* Run user thread up to its first action */
+		scheduler->next_thread(t);
+		Thread::swap(&system_context, t);
 
 		/* Wait for all threads to complete */
 		while (take_step());