Merge branch 'norris'
authorBrian Norris <banorris@uci.edu>
Thu, 6 Sep 2012 23:16:51 +0000 (16:16 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 6 Sep 2012 23:16:55 +0000 (16:16 -0700)
Fixes up some THREAD_JOIN behavior, cleaning up a little bit of general model-checker structure.

action.cc
action.h
libthreads.cc
model.cc
schedule.cc
schedule.h
snapshot-interface.cc
threads.cc
threads.h

index 692d14c..205bedb 100644 (file)
--- 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;
index 6559928..3e590aa 100644 (file)
--- 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 */
index 98df424..4d6a024 100644 (file)
@@ -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;
 }
 
index ec953ef..56723c7 100644 (file)
--- 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);
                }
index d96172e..be4a92f 100644 (file)
@@ -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.
index c3d029f..664b2d2 100644 (file)
@@ -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;
index 072c1f9..d93e5c2 100644 (file)
@@ -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);
index 9b7954d..7fa4507 100644 (file)
@@ -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;
index e7cd792..248d948 100644 (file)
--- a/threads.h
+++ b/threads.h
@@ -7,6 +7,7 @@
 
 #include <ucontext.h>
 #include <stdint.h>
+#include <vector>
 
 #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<Thread *> wait_list;
+
        /**
         * The value returned by the last action in this thread
         * @see Thread::set_return_value()