X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=threads.cc;h=cbedbb18bae1d73db1c46a531b4141886875b6be;hp=7fa4507ee94397e7e092730567901de94cf07a46;hb=0997f5bf1b28a79066ed4abfed57f14419ee44d3;hpb=c5b57f3d98d1d14b4546995a0882753cf71a1c4b diff --git a/threads.cc b/threads.cc index 7fa4507..cbedbb1 100644 --- a/threads.cc +++ b/threads.cc @@ -2,9 +2,12 @@ * @brief Thread functions. */ -#include "libthreads.h" +#include + +#include #include "common.h" -#include "threads.h" +#include "threads-model.h" +#include "action.h" /* global "model" object */ #include "model.h" @@ -12,16 +15,22 @@ /** Allocate a stack for a new thread. */ static void * stack_allocate(size_t size) { - return malloc(size); + return snapshot_malloc(size); } /** Free a stack for a terminated thread. */ static void stack_free(void *stack) { - free(stack); + snapshot_free(stack); } -/** Return the currently executing thread. */ +/** + * @brief Get the current Thread + * + * Must be called from a user context + * + * @return The currently executing thread + */ Thread * thread_current(void) { ASSERT(model); @@ -32,8 +41,6 @@ Thread * thread_current(void) * Provides a startup wrapper for each thread, allowing some initial * model-checking data to be recorded. This method also gets around makecontext * not being 64-bit clean - * @todo We should make the START event always immediately follow the - * CREATE event, so we don't get redundant traces... */ void thread_startup() { @@ -84,6 +91,7 @@ int Thread::create_context() */ int Thread::swap(Thread *t, ucontext_t *ctxt) { + t->set_state(THREAD_READY); return swapcontext(&t->context, ctxt); } @@ -97,6 +105,7 @@ int Thread::swap(Thread *t, ucontext_t *ctxt) */ int Thread::swap(ucontext_t *ctxt, Thread *t) { + t->set_state(THREAD_RUNNING); return swapcontext(ctxt, &t->context); } @@ -104,12 +113,36 @@ int Thread::swap(ucontext_t *ctxt, Thread *t) /** Terminate a thread and free its stack. */ void Thread::complete() { - if (!is_complete()) { - DEBUG("completed thread %d\n", get_id()); - state = THREAD_COMPLETED; - if (stack) - stack_free(stack); - } + ASSERT(!is_complete()); + DEBUG("completed thread %d\n", id_to_int(get_id())); + state = THREAD_COMPLETED; + if (stack) + stack_free(stack); +} + +/** + * @brief Construct a new model-checker Thread + * + * A model-checker Thread is used for accounting purposes only. It will never + * have its own stack, and it should never be inserted into the Scheduler. + * + * @param tid The thread ID to assign + */ +Thread::Thread(thread_id_t tid) : + parent(NULL), + creation(NULL), + pending(NULL), + start_routine(NULL), + arg(NULL), + stack(NULL), + user_thread(NULL), + id(tid), + state(THREAD_READY), /* Thread is always ready? */ + wait_list(), + last_action_val(0), + model_thread(true) +{ + memset(&context, 0, sizeof(context)); } /** @@ -118,35 +151,49 @@ void Thread::complete() * @param func The function that the thread will call. * @param a The parameter to pass to this function. */ -Thread::Thread(thrd_t *t, void (*func)(void *), void *a) : +Thread::Thread(thrd_t *t, void (*func)(void *), void *a, Thread * parent_thrd) : + creation(NULL), + pending(NULL), start_routine(func), arg(a), user_thread(t), state(THREAD_CREATED), wait_list(), - last_action_val(VALUE_NONE) + last_action_val(VALUE_NONE), + model_thread(false) { int ret; /* Initialize state */ ret = create_context(); if (ret) - printf("Error in create_context\n"); + model_print("Error in create_context\n"); id = model->get_next_id(); - *user_thread = id; - parent = thread_current(); + user_thread->priv = this; + parent = parent_thrd ? parent_thrd : thread_current(); } /** Destructor */ Thread::~Thread() { - complete(); + if (!is_complete()) + complete(); model->remove_thread(this); } /** @return The thread_id_t corresponding to this Thread object. */ -thread_id_t Thread::get_id() +thread_id_t Thread::get_id() const { return id; } + +/** + * Set a thread's THREAD_* state (@see thread_state) + * @param s The state to enter + */ +void Thread::set_state(thread_state s) +{ + ASSERT(s == THREAD_COMPLETED || state != THREAD_COMPLETED); + state = s; +}