common: introduce userMalloc() and userFree()

[model-checker.git] / threads.cc

diff --git a/threads.cc b/threads.cc
index 397c7894b70291b10016d1d3774ea74f7c840c73..a4ea252a2342e072385e10773a11008392eb1990 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -3,24 +3,24 @@
 #include "libthreads.h"
 #include "schedule.h"
 #include "common.h"
-#include "threads_internal.h"
+#include "threads.h"
 
 /* global "model" object */
 #include "model.h"
 
 #define STACK_SIZE (1024 * 1024)
 
-static void *stack_allocate(size_t size)
+static void * stack_allocate(size_t size)
 {
-       return malloc(size);
+       return userMalloc(size);
 }
 
 static void stack_free(void *stack)
 {
-       free(stack);
+       userFree(stack);
 }
 
-Thread *thread_current(void)
+Thread * thread_current(void)
 {
        return model->scheduler->get_current_thread();
 }
@@ -53,11 +53,14 @@ int Thread::swap(Thread *t)
        return swapcontext(&this->context, &t->context);
 }
 
-void Thread::dispose()
+void Thread::complete()
 {
-       DEBUG("completed thread %d\n", thread_current()->get_id());
-       state = THREAD_COMPLETED;
-       stack_free(stack);
+       if (state != THREAD_COMPLETED) {
+               DEBUG("completed thread %d\n", get_id());
+               state = THREAD_COMPLETED;
+               if (stack)
+                       stack_free(stack);
+       }
 }
 
 Thread::Thread(thrd_t *t, void (*func)(), void *a) {
@@ -73,22 +76,33 @@ Thread::Thread(thrd_t *t, void (*func)(), void *a) {
                printf("Error in create_context\n");
 
        state = THREAD_CREATED;
-       model->assign_id(this);
-       model->scheduler->add_thread(this);
+       id = model->get_next_id();
+       *user_thread = id;
 }
 
 Thread::Thread(thrd_t *t) {
        /* system thread */
        user_thread = t;
-       state = THREAD_CREATED;
-       model->assign_id(this);
+       start_routine = NULL;
+       arg = NULL;
+
        create_context();
+       stack = NULL;
+       state = THREAD_CREATED;
+       id = model->get_next_id();
+       *user_thread = id;
        model->add_system_thread(this);
 }
 
+Thread::~Thread()
+{
+       complete();
+       model->remove_thread(this);
+}
+
 thread_id_t Thread::get_id()
 {
-       return thrd_to_id(*user_thread);
+       return id;
 }
 
 /*
@@ -105,7 +119,7 @@ static int thread_system_next(void)
                        model->scheduler->add_thread(curr);
                else if (curr->get_state() == THREAD_RUNNING)
                        /* Stopped while running; i.e., completed */
-                       curr->dispose();
+                       curr->complete();
                else
                        DEBUG("ERROR: current thread in unexpected state??\n");
        }
@@ -138,13 +152,14 @@ 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();
+       } while (model->next_execution());
 
-       model->print_trace();
        delete th;
        delete model;