X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=threads.cc;h=37b0f1a87ee6fb9ac975a84c8df9adf018d808c5;hb=c400af2b7dfb87ce64c86f2d2b6a37d02421b263;hp=a4ea252a2342e072385e10773a11008392eb1990;hpb=ee5a8df4c176af0f01dd2c47eecb092167f663f6;p=model-checker.git diff --git a/threads.cc b/threads.cc index a4ea252..37b0f1a 100644 --- a/threads.cc +++ b/threads.cc @@ -1,7 +1,4 @@ -#include - #include "libthreads.h" -#include "schedule.h" #include "common.h" #include "threads.h" @@ -12,12 +9,12 @@ static void * stack_allocate(size_t size) { - return userMalloc(size); + return malloc(size); } static void stack_free(void *stack) { - userFree(stack); + free(stack); } Thread * thread_current(void) @@ -25,6 +22,13 @@ Thread * thread_current(void) return model->scheduler->get_current_thread(); } +/* This method just gets around makecontext not being 64-bit clean */ + +void thread_startup() { + Thread * curr_thread = thread_current(); + curr_thread->start_routine(curr_thread->arg); +} + int Thread::create_context() { int ret; @@ -33,24 +37,25 @@ int Thread::create_context() if (ret) return ret; - /* start_routine == NULL means this is our initial context */ - if (!start_routine) - return 0; - /* Initialize new managed context */ stack = stack_allocate(STACK_SIZE); context.uc_stack.ss_sp = stack; context.uc_stack.ss_size = STACK_SIZE; context.uc_stack.ss_flags = 0; - context.uc_link = &model->system_thread->context; - makecontext(&context, start_routine, 1, arg); + context.uc_link = model->get_system_context(); + makecontext(&context, thread_startup, 0); return 0; } -int Thread::swap(Thread *t) +int Thread::swap(Thread *t, ucontext_t *ctxt) { - return swapcontext(&this->context, &t->context); + return swapcontext(&t->context, ctxt); +} + +int Thread::swap(ucontext_t *ctxt, Thread *t) +{ + return swapcontext(ctxt, &t->context); } void Thread::complete() @@ -63,7 +68,7 @@ void Thread::complete() } } -Thread::Thread(thrd_t *t, void (*func)(), void *a) { +Thread::Thread(thrd_t *t, void (*func)(void *), void *a) { int ret; user_thread = t; @@ -78,20 +83,7 @@ Thread::Thread(thrd_t *t, void (*func)(), void *a) { state = THREAD_CREATED; id = model->get_next_id(); *user_thread = id; -} - -Thread::Thread(thrd_t *t) { - /* system thread */ - user_thread = t; - 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); + parent = thread_current(); } Thread::~Thread() @@ -104,65 +96,3 @@ thread_id_t Thread::get_id() { return id; } - -/* - * Return 1 if found next thread, 0 otherwise - */ -static int thread_system_next(void) -{ - Thread *curr, *next; - - curr = thread_current(); - model->check_current_action(); - if (curr) { - if (curr->get_state() == THREAD_READY) - model->scheduler->add_thread(curr); - else if (curr->get_state() == THREAD_RUNNING) - /* Stopped while running; i.e., completed */ - curr->complete(); - else - DEBUG("ERROR: current thread in unexpected state??\n"); - } - next = model->scheduler->next_thread(); - if (next) - next->set_state(THREAD_RUNNING); - DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1); - if (!next) - return 1; - return model->system_thread->swap(next); -} - -static void thread_wait_finish(void) -{ - - DBG(); - - while (!thread_system_next()); -} - -/* - * Main system function - */ -int main() -{ - thrd_t user_thread, main_thread; - Thread *th; - - model = new ModelChecker(); - - th = new Thread(&main_thread); - - do { - /* Start user program */ - thrd_create(&user_thread, &user_main, NULL); - - /* Wait for all threads to complete */ - thread_wait_finish(); - } while (model->next_execution()); - - delete th; - delete model; - - DEBUG("Exiting\n"); - return 0; -}