Merge branch 'norris'
authorBrian Norris <banorris@uci.edu>
Thu, 16 Aug 2012 17:40:59 +0000 (10:40 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 16 Aug 2012 17:41:30 +0000 (10:41 -0700)
action.cc
action.h
libthreads.cc
main.cc
model.cc
model.h
schedule.cc
schedule.h
threads.cc

index a88cc45..5c036ef 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -161,23 +161,22 @@ void ModelAction::create_cv(const ModelAction *parent)
                cv = new ClockVector(NULL, this);
 }
 
-
 /** Update the model action's read_from action */
 void ModelAction::read_from(const ModelAction *act)
 {
        ASSERT(cv);
        if (act!=NULL && act->is_release() && this->is_acquire()) {
-               synchronized(act);
-               cv->merge(act->cv);
+               synchronize_with(act);
        }
        reads_from = act;
 }
 
-
-/** Synchronize the current thread with the thread corresponding to
- *  the ModelAction parameter. */
-
-void ModelAction::synchronized(const ModelAction *act) {
+/**
+ * Synchronize the current thread with the thread corresponding to the
+ * ModelAction parameter.
+ * @param act The ModelAction to synchronize with
+ */
+void ModelAction::synchronize_with(const ModelAction *act) {
        model->check_promises(cv, act->cv);
        cv->merge(act->cv);
 }
index 7c45707..ffe60dc 100644 (file)
--- a/action.h
+++ b/action.h
@@ -81,8 +81,6 @@ public:
        void create_cv(const ModelAction *parent = NULL);
        ClockVector * get_cv() const { return cv; }
        void read_from(const ModelAction *act);
-       void synchronized(const ModelAction *act);
-
 
        bool happens_before(const ModelAction *act) const;
 
@@ -98,6 +96,7 @@ public:
 
        MEMALLOC
 private:
+       void synchronize_with(const ModelAction *act);
 
        /** Type of action (read, write, thread create, thread yield, thread join) */
        action_type type;
index 2898258..98df424 100644 (file)
 int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg)
 {
        Thread *thread;
-       int ret;
        DBG();
        thread = new Thread(t, start_routine, arg);
-       ret = model->add_thread(thread);
+       model->add_thread(thread);
        DEBUG("create thread %d\n", id_to_int(thrd_to_id(*t)));
        /* seq_cst is just a 'don't care' parameter */
        model->switch_to_master(new ModelAction(THREAD_CREATE, std::memory_order_seq_cst, thread, VALUE_NONE));
-       return ret;
+       return 0;
 }
 
 int thrd_join(thrd_t t)
diff --git a/main.cc b/main.cc
index 9a6c2d8..75efafe 100644 (file)
--- a/main.cc
+++ b/main.cc
 #include "model.h"
 #include "snapshot-interface.h"
 
-/**
- * The thread_system_next function takes the next step in the execution, if
- * possible.
- * @return Returns 0 (success) if there is another step and non-zero otherwise.
- */
-static int thread_system_next(void) {
-       Thread *curr, *next;
-
-       curr = thread_current();
-       if (curr) {
-               if (curr->get_state() == THREAD_READY) {
-                       model->check_current_action();
-                       model->scheduler->add_thread(curr);
-               } else if (curr->get_state() == THREAD_RUNNING) {
-                       /* Stopped while running; i.e., completed */
-                       curr->complete();
-               } else {
-                       ASSERT(false);
-               }
-       }
-       next = model->scheduler->next_thread();
-
-       /* Infeasible -> don't take any more steps */
-       if (!model->isfeasible())
-               return 1;
-
-       if (next)
-               next->set_state(THREAD_RUNNING);
-       DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
-
-       /* next == NULL -> don't take any more steps */
-       if (!next)
-               return 1;
-       /* Return non-zero only if swap fails with an error */
-       return Thread::swap(model->get_system_context(), next);
-}
-
-/** The thread_wait_finish method runs the current execution until we
- *  have no more steps to take.
- */
-static void thread_wait_finish(void) {
-       DBG();
-
-       while (!thread_system_next());
-}
-
 static void parse_options(struct model_params *params, int argc, char **argv) {
 }
 
@@ -67,7 +21,6 @@ char **main_argv;
 /** The real_main function contains the main model checking loop. */
 static void real_main() {
        thrd_t user_thread;
-       ucontext_t main_context;
        struct model_params params;
 
        parse_options(&params, main_argc, main_argv);
@@ -80,18 +33,13 @@ static void real_main() {
 
        model = new ModelChecker(params);
 
-       if (getcontext(&main_context))
-               return;
-
-       model->set_system_context(&main_context);
-
        snapshotObject->snapshotStep(0);
        do {
                /* Start user program */
                model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL));
 
                /* Wait for all threads to complete */
-               thread_wait_finish();
+               model->finish_execution();
        } while (model->next_execution());
 
        delete model;
index 7c6684f..25f85d0 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -716,11 +716,15 @@ void ModelChecker::print_summary()
        printf("\n");
 }
 
-int ModelChecker::add_thread(Thread *t)
+/**
+ * Add a Thread to the system for the first time. Should only be called once
+ * per thread.
+ * @param t The Thread to add
+ */
+void ModelChecker::add_thread(Thread *t)
 {
        thread_map->put(id_to_int(t->get_id()), t);
        scheduler->add_thread(t);
-       return 0;
 }
 
 void ModelChecker::remove_thread(Thread *t)
@@ -745,5 +749,48 @@ int ModelChecker::switch_to_master(ModelAction *act)
        Thread * old = thread_current();
        set_current_action(act);
        old->set_state(THREAD_READY);
-       return Thread::swap(old, get_system_context());
+       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.
+ */
+bool ModelChecker::take_step() {
+       Thread *curr, *next;
+
+       curr = thread_current();
+       if (curr) {
+               if (curr->get_state() == THREAD_READY) {
+                       check_current_action();
+                       scheduler->add_thread(curr);
+               } else if (curr->get_state() == THREAD_RUNNING) {
+                       /* Stopped while running; i.e., completed */
+                       curr->complete();
+               } else {
+                       ASSERT(false);
+               }
+       }
+       next = scheduler->next_thread();
+
+       /* Infeasible -> don't take any more steps */
+       if (!isfeasible())
+               return false;
+
+       if (next)
+               next->set_state(THREAD_RUNNING);
+       DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
+
+       /* next == NULL -> don't take any more steps */
+       if (!next)
+               return false;
+       /* Return false only if swap fails with an error */
+       return (Thread::swap(&system_context, next) == 0);
+}
+
+/** Runs the current execution until threre are no more steps to take. */
+void ModelChecker::finish_execution() {
+       DBG();
+
+       while (take_step());
 }
diff --git a/model.h b/model.h
index dc6ef6a..6d3827c 100644 (file)
--- a/model.h
+++ b/model.h
@@ -36,26 +36,15 @@ public:
        ModelChecker(struct model_params params);
        ~ModelChecker();
 
-       /** The scheduler to use: tracks the running/ready Threads */
-       Scheduler *scheduler;
-
-       /** Stores the context for the main model-checking system thread (call
-        * once)
-        * @param ctxt The system context structure
-        */
-       void set_system_context(ucontext_t *ctxt) { system_context = ctxt; }
-
        /** @returns the context for the main model-checking system thread */
-       ucontext_t * get_system_context(void) { return system_context; }
-
-       void check_current_action(void);
+       ucontext_t * get_system_context() { return &system_context; }
 
        /** Prints an execution summary with trace information. */
        void print_summary();
 
        Thread * schedule_next_thread();
 
-       int add_thread(Thread *t);
+       void add_thread(Thread *t);
        void remove_thread(Thread *t);
        Thread * get_thread(thread_id_t tid) { return thread_map->get(id_to_int(tid)); }
 
@@ -63,6 +52,9 @@ public:
        int get_num_threads();
        modelclock_t get_next_seq_num();
 
+       /** @return The currently executing Thread. */
+       Thread * get_current_thread() { return scheduler->get_current_thread(); }
+
        int switch_to_master(ModelAction *act);
        ClockVector * get_cv(thread_id_t tid);
        bool next_execution();
@@ -70,8 +62,13 @@ public:
        bool isfinalfeasible();
        void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
 
+       void finish_execution();
+
        MEMALLOC
 private:
+       /** The scheduler to use: tracks the running/ready Threads */
+       Scheduler *scheduler;
+
        int next_thread_id;
        modelclock_t used_sequence_numbers;
        int num_executions;
@@ -85,6 +82,9 @@ private:
         * @param act The ModelAction created by the user-thread action
         */
        void set_current_action(ModelAction *act) { current_action = act; }
+       void check_current_action();
+
+       bool take_step();
 
        ModelAction * get_last_conflict(ModelAction *act);
        void set_backtracking(ModelAction *act);
@@ -108,7 +108,7 @@ private:
        ModelAction *diverge;
        thread_id_t nextThread;
 
-       ucontext_t *system_context;
+       ucontext_t system_context;
        action_list_t *action_trace;
        HashTable<int, Thread *, int> *thread_map;
 
index 1791605..69e3d88 100644 (file)
@@ -3,17 +3,26 @@
 #include "common.h"
 #include "model.h"
 
+/** Constructor */
 Scheduler::Scheduler() :
        current(NULL)
 {
 }
 
+/**
+ * Add a Thread to the scheduler's ready list.
+ * @param t The Thread to add
+ */
 void Scheduler::add_thread(Thread *t)
 {
        DEBUG("thread %d\n", t->get_id());
        readyList.push_back(t);
 }
 
+/**
+ * Remove a given Thread from the scheduler.
+ * @param t The Thread to remove
+ */
 void Scheduler::remove_thread(Thread *t)
 {
        if (current == t)
@@ -22,7 +31,11 @@ void Scheduler::remove_thread(Thread *t)
                readyList.remove(t);
 }
 
-Thread * Scheduler::next_thread(void)
+/**
+ * Remove one Thread from the scheduler. This implementation performs FIFO.
+ * @return The next Thread to run
+ */
+Thread * Scheduler::next_thread()
 {
        Thread *t = model->schedule_next_thread();
 
@@ -42,12 +55,19 @@ Thread * Scheduler::next_thread(void)
        return t;
 }
 
-Thread * Scheduler::get_current_thread(void)
+/**
+ * @return The currently-running Thread
+ */
+Thread * Scheduler::get_current_thread() const
 {
        return current;
 }
 
-void Scheduler::print()
+/**
+ * Print debugging information about the current state of the scheduler. Only
+ * prints something if debugging is enabled.
+ */
+void Scheduler::print() const
 {
        if (current)
                DEBUG("Current thread: %d\n", current->get_id());
@@ -55,7 +75,7 @@ void Scheduler::print()
                DEBUG("No current thread\n");
        DEBUG("Num. threads in ready list: %zu\n", readyList.size());
 
-       std::list<Thread *, MyAlloc< Thread * > >::iterator it;
+       std::list<Thread *, MyAlloc< Thread * > >::const_iterator it;
        for (it = readyList.begin(); it != readyList.end(); it++)
                DEBUG("In ready list: thread %d\n", (*it)->get_id());
 }
index cba4b11..c8153b3 100644 (file)
@@ -18,13 +18,16 @@ public:
        Scheduler();
        void add_thread(Thread *t);
        void remove_thread(Thread *t);
-       Thread * next_thread(void);
-       Thread * get_current_thread(void);
-       void print();
+       Thread * next_thread();
+       Thread * get_current_thread() const;
+       void print() const;
 
        SNAPSHOTALLOC
 private:
+       /** The list of available Threads that are not currently running */
        std::list<Thread *> readyList;
+
+       /** The currently-running Thread */
        Thread *current;
 };
 
index 2697579..9b7954d 100644 (file)
@@ -22,11 +22,10 @@ static void stack_free(void *stack)
 }
 
 /** Return the currently executing thread. */
-
 Thread * thread_current(void)
 {
        ASSERT(model);
-       return model->scheduler->get_current_thread();
+       return model->get_current_thread();
 }
 
 /**
@@ -47,11 +46,11 @@ void thread_startup()
        curr_thread->start_routine(curr_thread->arg);
 }
 
-/** Create a thread context for a new thread so we can use
- *  setcontext/getcontext/swapcontext to swap it out.
- *  @return 0 on success.
+/**
+ * Create a thread context for a new thread so we can use
+ * setcontext/getcontext/swapcontext to swap it out.
+ * @return 0 on success; otherwise, non-zero error condition
  */
-
 int Thread::create_context()
 {
        int ret;
@@ -74,8 +73,9 @@ int Thread::create_context()
 /**
  * Swaps the current context to another thread of execution. This form switches
  * from a user Thread to a system context.
- * @param t Thread representing the current context
- * @param ctxt Context to switch to
+ * @param t Thread representing the currently-running thread. The current
+ * context is saved here.
+ * @param ctxt Context to which we will swap. Must hold a valid system context.
  * @return Does not return, unless we return to Thread t's context. See
  * swapcontext(3) (returns 0 for success, -1 for failure).
  */
@@ -87,9 +87,9 @@ int Thread::swap(Thread *t, ucontext_t *ctxt)
 /**
  * Swaps the current context to another thread of execution. This form switches
  * from a system context to a user Thread.
- * @param t Thread representing the current context
- * @param ctxt Context to switch to
- * @return Does not return, unless we return to Thread t's context. See
+ * @param ctxt System context variable to which to save the current context.
+ * @param t Thread to which we will swap. Must hold a valid user context.
+ * @return Does not return, unless we return to the system context (ctxt). See
  * swapcontext(3) (returns 0 for success, -1 for failure).
  */
 int Thread::swap(ucontext_t *ctxt, Thread *t)
@@ -109,12 +109,12 @@ void Thread::complete()
        }
 }
 
-/** Create a new thread.
- *  Takes the following parameters:
- *  @param t The thread identifier of the newly created thread.
- *  @param func  The function that the thread will call.
- *  @param a The parameter to pass to this function. */
-
+/**
+ * Construct a new thread.
+ * @param t The thread identifier of the newly created thread.
+ * @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) :
        start_routine(func),
        arg(a),
@@ -134,14 +134,14 @@ Thread::Thread(thrd_t *t, void (*func)(void *), void *a) :
        parent = thread_current();
 }
 
+/** Destructor */
 Thread::~Thread()
 {
        complete();
        model->remove_thread(this);
 }
 
-/** Return the thread_id_t corresponding to this Thread object. */
-
+/** @return The thread_id_t corresponding to this Thread object. */
 thread_id_t Thread::get_id()
 {
        return id;