From: Brian Norris Date: Thu, 6 Sep 2012 23:16:51 +0000 (-0700) Subject: Merge branch 'norris' X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=0accacf66b9f7bb4479205a0840f208dd8da6960;hp=620c53f1b91d3f9b51424ff57c652d247f6fbaac Merge branch 'norris' Fixes up some THREAD_JOIN behavior, cleaning up a little bit of general model-checker structure. --- diff --git a/action.cc b/action.cc index 692d14cf..205bedbf 100644 --- a/action.cc +++ b/action.cc @@ -218,6 +218,9 @@ void ModelAction::print(void) const case THREAD_JOIN: type_str = "thread join"; break; + case THREAD_FINISH: + type_str = "thread finish"; + break; case ATOMIC_READ: type_str = "atomic read"; break; diff --git a/action.h b/action.h index 6559928b..3e590aae 100644 --- a/action.h +++ b/action.h @@ -32,6 +32,7 @@ typedef enum action_type { THREAD_START, /**< First action in each thread */ THREAD_YIELD, /**< A thread yield action */ THREAD_JOIN, /**< A thread join action */ + THREAD_FINISH, /**< A thread completion action */ ATOMIC_READ, /**< An atomic read action */ ATOMIC_WRITE, /**< An atomic write action */ ATOMIC_RMWR, /**< The read part of an atomic RMW action */ diff --git a/libthreads.cc b/libthreads.cc index 98df4248..4d6a0243 100644 --- a/libthreads.cc +++ b/libthreads.cc @@ -23,8 +23,7 @@ int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg) int thrd_join(thrd_t t) { Thread *th = model->get_thread(thrd_to_id(t)); - while (th->get_state() != THREAD_COMPLETED) - model->switch_to_master(NULL); + model->switch_to_master(new ModelAction(THREAD_JOIN, std::memory_order_seq_cst, th, thrd_to_id(t))); return 0; } diff --git a/model.cc b/model.cc index ec953ef1..56723c7d 100644 --- a/model.cc +++ b/model.cc @@ -299,6 +299,19 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (curr->get_type() == THREAD_CREATE) { Thread *th = (Thread *)curr->get_location(); th->set_creation(curr); + } else if (curr->get_type() == THREAD_JOIN) { + Thread *wait, *join; + wait = get_thread(curr->get_tid()); + join = (Thread *)curr->get_location(); + if (!join->is_complete()) + scheduler->wait(wait, join); + } else if (curr->get_type() == THREAD_FINISH) { + Thread *th = get_thread(curr->get_tid()); + while (!th->wait_list_empty()) { + Thread *wake = th->pop_wait_list(); + scheduler->wake(wake); + } + th->complete(); } /* Deal with new thread */ @@ -941,10 +954,7 @@ void ModelChecker::remove_thread(Thread *t) * context). This switch is made with the intention of exploring a particular * model-checking action (described by a ModelAction object). Must be called * from a user-thread context. - * @param act The current action that will be explored. May be NULL, although - * there is little reason to switch to the model-checker without an action to - * explore (note: act == NULL is sometimes used as a hack to allow a thread to - * yield control without performing any progress; see thrd_join()). + * @param act The current action that will be explored. Must not be NULL. * @return Return status from the 'swap' call (i.e., success/fail, 0/-1) */ int ModelChecker::switch_to_master(ModelAction *act) @@ -966,14 +976,11 @@ bool ModelChecker::take_step() { curr = thread_current(); if (curr) { if (curr->get_state() == THREAD_READY) { - if (current_action) { - nextThread = check_current_action(current_action); - current_action = NULL; - } - scheduler->add_thread(curr); - } else if (curr->get_state() == THREAD_RUNNING) { - /* Stopped while running; i.e., completed */ - curr->complete(); + ASSERT(current_action); + nextThread = check_current_action(current_action); + current_action = NULL; + if (!curr->is_blocked() && !curr->is_complete()) + scheduler->add_thread(curr); } else { ASSERT(false); } diff --git a/schedule.cc b/schedule.cc index d96172e0..be4a92f7 100644 --- a/schedule.cc +++ b/schedule.cc @@ -31,6 +31,30 @@ void Scheduler::remove_thread(Thread *t) readyList.remove(t); } +/** + * Force one Thread to wait on another Thread. The "join" Thread should + * eventually wake up the waiting Thread via Scheduler::wake. + * @param wait The Thread that should wait + * @param join The Thread on which we are waiting. + */ +void Scheduler::wait(Thread *wait, Thread *join) +{ + ASSERT(!join->is_complete()); + remove_thread(wait); + join->push_wait_list(wait); + wait->set_state(THREAD_BLOCKED); +} + +/** + * Wake a Thread up that was previously waiting (see Scheduler::wait) + * @param t The Thread to wake up + */ +void Scheduler::wake(Thread *t) +{ + add_thread(t); + t->set_state(THREAD_READY); +} + /** * Remove one Thread from the scheduler. This implementation defaults to FIFO, * if a thread is not already provided. diff --git a/schedule.h b/schedule.h index c3d029fb..664b2d24 100644 --- a/schedule.h +++ b/schedule.h @@ -18,6 +18,8 @@ public: Scheduler(); void add_thread(Thread *t); void remove_thread(Thread *t); + void wait(Thread *wait, Thread *join); + void wake(Thread *t); Thread * next_thread(Thread *t); Thread * get_current_thread() const; void print() const; diff --git a/snapshot-interface.cc b/snapshot-interface.cc index 072c1f95..d93e5c20 100644 --- a/snapshot-interface.cc +++ b/snapshot-interface.cc @@ -93,7 +93,7 @@ static void SnapshotGlobalSegments(){ size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE; if (len != 0) addMemoryRegionToSnapShot(begin, len); - DEBUG("%45s: %18p - %18p\t%c%c%c%c\n", regionname, begin, end, r, w, x, p); + DEBUG("%55s: %18p - %18p\t%c%c%c%c\n", regionname, begin, end, r, w, x, p); } } fclose(map); diff --git a/threads.cc b/threads.cc index 9b7954d9..7fa4507e 100644 --- a/threads.cc +++ b/threads.cc @@ -44,6 +44,9 @@ void thread_startup() /* Call the actual thread function */ curr_thread->start_routine(curr_thread->arg); + + /* Finish thread properly */ + model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, curr_thread)); } /** @@ -101,7 +104,7 @@ int Thread::swap(ucontext_t *ctxt, Thread *t) /** Terminate a thread and free its stack. */ void Thread::complete() { - if (state != THREAD_COMPLETED) { + if (!is_complete()) { DEBUG("completed thread %d\n", get_id()); state = THREAD_COMPLETED; if (stack) @@ -120,6 +123,7 @@ Thread::Thread(thrd_t *t, void (*func)(void *), void *a) : arg(a), user_thread(t), state(THREAD_CREATED), + wait_list(), last_action_val(VALUE_NONE) { int ret; diff --git a/threads.h b/threads.h index e7cd792a..248d948f 100644 --- a/threads.h +++ b/threads.h @@ -7,6 +7,7 @@ #include #include +#include #include "mymemory.h" #include "libthreads.h" @@ -21,12 +22,13 @@ typedef enum thread_state { THREAD_CREATED, /** Thread is running */ THREAD_RUNNING, + /** Thread is not currently running but is ready to run */ + THREAD_READY, /** - * Thread has yielded to the model-checker but is ready to run. Used - * during an action that caused a context switch to the model-checking - * context. + * Thread is waiting on another action (e.g., thread completion, lock + * release, etc.) */ - THREAD_READY, + THREAD_BLOCKED, /** Thread has completed its execution */ THREAD_COMPLETED } thread_state; @@ -67,6 +69,31 @@ public: */ uint64_t get_return_value() { return last_action_val; } + /** @return True if this thread is finished executing */ + bool is_complete() { return state == THREAD_COMPLETED; } + + /** @return True if this thread is blocked */ + bool is_blocked() { return state == THREAD_BLOCKED; } + + /** @return True if no threads are waiting on this Thread */ + bool wait_list_empty() { return wait_list.empty(); } + + /** + * Add a thread to the waiting list for this thread. + * @param t The Thread to add + */ + void push_wait_list(Thread *t) { wait_list.push_back(t); } + + /** + * Remove one Thread from the waiting list + * @return The Thread that was removed from the waiting list + */ + Thread * pop_wait_list() { + Thread *ret = wait_list.front(); + wait_list.pop_back(); + return ret; + } + friend void thread_startup(); SNAPSHOTALLOC @@ -83,6 +110,13 @@ private: thread_id_t id; thread_state state; + /** + * A list of Threads waiting on this Thread. Particularly, this list is + * used for thread joins, where another Thread waits for this Thread to + * complete + */ + std::vector wait_list; + /** * The value returned by the last action in this thread * @see Thread::set_return_value()