X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=threads.cc;h=dd2a59832027557b543d8fd606f842527b270f97;hb=e83585ce14ab6ae325c83d815dce8eb77b0e5897;hp=ca4b28b1bc850c9ea5bcab709e2d27a9e74e2581;hpb=af25bde59ce05189adee92825ecc03fbb83e675b;p=model-checker.git diff --git a/threads.cc b/threads.cc index ca4b28b..dd2a598 100644 --- a/threads.cc +++ b/threads.cc @@ -2,9 +2,11 @@ * @brief Thread functions. */ -#include "libthreads.h" +#include + +#include #include "common.h" -#include "threads.h" +#include "threads-model.h" /* global "model" object */ #include "model.h" @@ -112,6 +114,31 @@ void Thread::complete() } } +/** + * @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)); +} + /** * Construct a new thread. * @param t The thread identifier of the newly created thread. @@ -126,14 +153,15 @@ Thread::Thread(thrd_t *t, void (*func)(void *), void *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;