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 059a5228590f260813a50b28707d542cc20da4a3..e6828c57349f97d1e60875aef2c1ed03a1ad5012 100644 (file)
--- 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());