From: Brian Demsky Date: Fri, 7 Sep 2012 01:56:39 +0000 (-0700) Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=c5b57f3d98d1d14b4546995a0882753cf71a1c4b;hp=7c003db5218470054490a6777c97c6611b933a12 Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker check in my stuff... Conflicts: model.cc threads.h --- 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 0e2b818c..217d6421 100644 --- a/model.cc +++ b/model.cc @@ -9,6 +9,7 @@ #include "clockvector.h" #include "cyclegraph.h" #include "promise.h" +#include "datarace.h" #define INITIAL_THREAD_ID 0 @@ -36,7 +37,8 @@ ModelChecker::ModelChecker(struct model_params params) : node_stack(new NodeStack()), next_backtrack(NULL), mo_graph(new CycleGraph()), - failed_promise(false) + failed_promise(false), + asserted(false) { } @@ -77,6 +79,7 @@ void ModelChecker::reset_to_initial_state() nextThread = NULL; next_backtrack = NULL; failed_promise = false; + reset_asserted(); snapshotObject->backTrackBeforeStep(0); } @@ -299,6 +302,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 */ @@ -326,7 +342,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) } } else if (curr->is_write()) { if (w_modification_order(curr)) - updated = true;; + updated = true; if (resolve_promises(curr)) updated = true; } @@ -361,6 +377,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) * feasible trace. */ bool ModelChecker::isfeasibleprefix() { + return promises->size()==0; } /** @returns whether the current partial trace is feasible. */ @@ -693,6 +710,11 @@ bool ModelChecker::resolve_release_sequences(void *location) it++; } + // If we resolved promises or data races, see if we have realized a data race. + if (checkDataRaces()) { + model->set_assert(); + } + return updated; } @@ -784,6 +806,7 @@ bool ModelChecker::resolve_promises(ModelAction *write) } else promise_index++; } + return resolved; } @@ -947,10 +970,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) @@ -962,14 +982,6 @@ int ModelChecker::switch_to_master(ModelAction *act) return Thread::swap(old, &system_context); } -void ModelChecker::assert_thread() { - DBG(); - Thread *old = thread_current(); - set_current_action(NULL); - old->set_state(THREAD_ASSERTED); - return Thread::swap(old, &system_context); -} - /** * Takes the next step in the execution, if possible. * @return Returns true (success) if a step was taken and false otherwise. @@ -977,20 +989,17 @@ void ModelChecker::assert_thread() { bool ModelChecker::take_step() { Thread *curr, *next; + if (has_asserted()) + return false; + 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(); - } else if (curr->get_state()==THREAD_ASSERTED) { - /* Something bad happened. Stop taking steps. */ - return false; + 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 6872ffa1..248d948f 100644 --- a/threads.h +++ b/threads.h @@ -7,6 +7,7 @@ #include #include +#include #include "mymemory.h" #include "libthreads.h" @@ -21,13 +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_ASSERTED, + THREAD_BLOCKED, /** Thread has completed its execution */ THREAD_COMPLETED } thread_state; @@ -68,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 @@ -84,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()