threads: prepare system to loop over many executions

[model-checker.git] / threads.cc

diff --git a/threads.cc b/threads.cc
index 38a0dce8775a4f3490f50163477582b43db6de76..830ea1a484159c9df61b641994781d30f97cb989 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -3,7 +3,7 @@
 #include "libthreads.h"
 #include "schedule.h"
 #include "common.h"
-#include "threads_internal.h"
+#include "threads.h"
 
 /* global "model" object */
 #include "model.h"
@@ -60,17 +60,6 @@ void Thread::dispose()
        stack_free(stack);
 }
 
-int Thread::switch_to_master(ModelAction *act)
-{
-       Thread *next;
-
-       DBG();
-       model->set_current_action(act);
-       state = THREAD_READY;
-       next = model->system_thread;
-       return swap(next);
-}
-
 Thread::Thread(thrd_t *t, void (*func)(), void *a) {
        int ret;
 
@@ -149,13 +138,16 @@ int main()
 
        th = new Thread(&main_thread);
 
-       /* Start user program */
-       thrd_create(&user_thread, &user_main, NULL);
+       do {
+               /* Start user program */
+               thrd_create(&user_thread, &user_main, NULL);
+
+               /* Wait for all threads to complete */
+               thread_wait_finish();
 
-       /* Wait for all threads to complete */
-       thread_wait_finish();
+               model->print_trace();
+       } while (model->next_execution());
 
-       model->print_trace();
        delete th;
        delete model;