libthreads: utilize new model_checker framework

Just a simple drop-in of the current FCFS scheduler (with the ability to
generically switch out schedulers).

diff --git a/libthreads.c b/libthreads.c
index f355c9c303446fefa4e8ab206bcfab2c5d768f3e..3697c0851e035109ddd49329ea640f8a154b08ca 100644 (file)
--- a/libthreads.c
+++ b/libthreads.c
@@ -5,6 +5,9 @@
 #include "schedule.h"
 #include "common.h"
 
+/* global "model" struct */
+#include "model.h"
+
 #define STACK_SIZE (1024 * 1024)
 
 static struct thread *current, *main_thread;
@@ -60,8 +63,8 @@ int thread_yield(void)
 
        DBG();
        old = current;
-       schedule_add_thread(old);
-       next = schedule_choose_next();
+       model->scheduler->add_thread(old);
+       next = model->scheduler->next_thread();
        current = next;
        DEBUG("(%d, %d)\n", old->index, next->index);
        return thread_swap(old, next);
@@ -83,7 +86,7 @@ static void thread_wait_finish(void)
        do {
                if (current)
                        thread_dispose(current);
-               next = schedule_choose_next();
+               next = model->scheduler->next_thread();
                current = next;
        } while (next && !thread_swap(main_thread, next));
 }
@@ -107,7 +110,7 @@ int thread_create(struct thread *t, void (*start_routine), void *arg)
        if (ret)
                return ret;
 
-       schedule_add_thread(t);
+       model->scheduler->add_thread(t);
        return 0;
 }
 
@@ -126,6 +129,8 @@ int main()
 {
        struct thread user_thread;
 
+       model_checker_init();
+
        main_thread = malloc(sizeof(struct thread));
        create_initial_thread(main_thread);