From 1b561ab02787b79478b05189be3a4b342e5785f5 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 12 Dec 2012 19:16:43 -0800 Subject: [PATCH] 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. --- model.cc | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) 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()); -- 2.34.1