Merge branch 'norris'
authorBrian Norris <banorris@uci.edu>
Mon, 8 Oct 2012 06:25:48 +0000 (23:25 -0700)
committerBrian Norris <banorris@uci.edu>
Mon, 8 Oct 2012 06:25:48 +0000 (23:25 -0700)
action.cc
action.h
model.cc
model.h
nodestack.cc
nodestack.h
schedule.cc
test/pending-release.c
test/releaseseq.c
threads.cc
threads.h

index b4f4e43..09352da 100644 (file)
--- a/action.cc
+++ b/action.cc
 
 #define ACTION_INITIAL_CLOCK 0
 
-ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value) :
+/**
+ * @brief Construct a new ModelAction
+ *
+ * @param type The type of action
+ * @param order The memory order of this action. A "don't care" for non-ATOMIC
+ * actions (e.g., THREAD_* or MODEL_* actions).
+ * @param loc The location that this action acts upon
+ * @param value (optional) A value associated with the action (e.g., the value
+ * read or written). Defaults to a given macro constant, for debugging purposes.
+ * @param thread (optional) The Thread in which this action occurred. If NULL
+ * (default), then a Thread is assigned according to the scheduler.
+ */
+ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
+               uint64_t value, Thread *thread) :
        type(type),
        order(order),
        location(loc),
@@ -20,7 +33,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint
        seq_number(ACTION_INITIAL_CLOCK),
        cv(NULL)
 {
-       Thread *t = thread_current();
+       Thread *t = thread ? thread : thread_current();
        this->tid = t->get_id();
 }
 
@@ -50,6 +63,11 @@ void ModelAction::set_seq_number(modelclock_t num)
        seq_number = num;
 }
 
+bool ModelAction::is_relseq_fixup() const
+{
+       return type == MODEL_FIXUP_RELSEQ;
+}
+
 bool ModelAction::is_mutex_op() const
 {
        return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;
@@ -305,6 +323,9 @@ void ModelAction::print() const
 {
        const char *type_str, *mo_str;
        switch (this->type) {
+       case MODEL_FIXUP_RELSEQ:
+               type_str = "relseq fixup";
+               break;
        case THREAD_CREATE:
                type_str = "thread create";
                break;
index 96ea6fa..65b060f 100644 (file)
--- a/action.h
+++ b/action.h
@@ -14,6 +14,7 @@
 #include "modeltypes.h"
 
 class ClockVector;
+class Thread;
 
 using std::memory_order;
 using std::memory_order_relaxed;
@@ -37,6 +38,8 @@ using std::memory_order_seq_cst;
 /** @brief Represents an action type, identifying one of several types of
  * ModelAction */
 typedef enum action_type {
+       MODEL_FIXUP_RELSEQ,   /**< Special ModelAction: finalize a release
+                              *   sequence */
        THREAD_CREATE,        /**< A thread creation action */
        THREAD_START,         /**< First action in each thread */
        THREAD_YIELD,         /**< A thread yield action */
@@ -64,7 +67,7 @@ class ClockVector;
  */
 class ModelAction {
 public:
-       ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE);
+       ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);
        ~ModelAction();
        void print() const;
 
@@ -82,6 +85,7 @@ public:
        void copy_from_new(ModelAction *newaction);
        void set_seq_number(modelclock_t num);
        void set_try_lock(bool obtainedlock);
+       bool is_relseq_fixup() const;
        bool is_mutex_op() const;
        bool is_lock() const;
        bool is_trylock() const;
index 6eaf656..8267377 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -47,6 +47,10 @@ ModelChecker::ModelChecker(struct model_params params) :
        priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
        /* First thread created will have id INITIAL_THREAD_ID */
        priv->next_thread_id = INITIAL_THREAD_ID;
+
+       /* Initialize a model-checker thread, for special ModelActions */
+       model_thread = new Thread(get_next_id());
+       thread_map->put(id_to_int(model_thread->get_id()), model_thread);
 }
 
 /** @brief Destructor */
@@ -163,6 +167,10 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
                        /* The next node will try to read from a different future value. */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
+               } else if (nextnode->increment_relseq_break()) {
+                       /* The next node will try to resolve a release sequence differently */
+                       tid = next->get_tid();
+                       node_stack->pop_restofstack(2);
                } else {
                        /* Make a different thread execute for next step */
                        Node *node = nextnode->get_parent();
@@ -540,6 +548,76 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
        return updated;
 }
 
+/**
+ * @brief Process the current action for release sequence fixup activity
+ *
+ * Performs model-checker release sequence fixups for the current action,
+ * forcing a single pending release sequence to break (with a given, potential
+ * "loose" write) or to complete (i.e., synchronize). If a pending release
+ * sequence forms a complete release sequence, then we must perform the fixup
+ * synchronization, mo_graph additions, etc.
+ *
+ * @param curr The current action; must be a release sequence fixup action
+ * @param work_queue The work queue to which to add work items as they are
+ * generated
+ */
+void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
+{
+       const ModelAction *write = curr->get_node()->get_relseq_break();
+       struct release_seq *sequence = pending_rel_seqs->back();
+       pending_rel_seqs->pop_back();
+       ASSERT(sequence);
+       ModelAction *acquire = sequence->acquire;
+       const ModelAction *rf = sequence->rf;
+       const ModelAction *release = sequence->release;
+       ASSERT(acquire);
+       ASSERT(release);
+       ASSERT(rf);
+       ASSERT(release->same_thread(rf));
+
+       if (write == NULL) {
+               /**
+                * @todo Forcing a synchronization requires that we set
+                * modification order constraints. For instance, we can't allow
+                * a fixup sequence in which two separate read-acquire
+                * operations read from the same sequence, where the first one
+                * synchronizes and the other doesn't. Essentially, we can't
+                * allow any writes to insert themselves between 'release' and
+                * 'rf'
+                */
+
+               /* Must synchronize */
+               if (!acquire->synchronize_with(release)) {
+                       set_bad_synchronization();
+                       return;
+               }
+               /* Re-check all pending release sequences */
+               work_queue->push_back(CheckRelSeqWorkEntry(NULL));
+               /* Re-check act for mo_graph edges */
+               work_queue->push_back(MOEdgeWorkEntry(acquire));
+
+               /* propagate synchronization to later actions */
+               action_list_t::reverse_iterator rit = action_trace->rbegin();
+               for (; (*rit) != acquire; rit++) {
+                       ModelAction *propagate = *rit;
+                       if (acquire->happens_before(propagate)) {
+                               propagate->synchronize_with(acquire);
+                               /* Re-check 'propagate' for mo_graph edges */
+                               work_queue->push_back(MOEdgeWorkEntry(propagate));
+                       }
+               }
+       } else {
+               /* Break release sequence with new edges:
+                *   release --mo--> write --mo--> rf */
+               mo_graph->addEdge(release, write);
+               mo_graph->addEdge(write, rf);
+       }
+
+       /* See if we have realized a data race */
+       if (checkDataRaces())
+               set_assert();
+}
+
 /**
  * Initialize the current action by performing one or more of the following
  * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
@@ -591,6 +669,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
                 */
                if (newcurr->is_write())
                        compute_promises(newcurr);
+               else if (newcurr->is_relseq_fixup())
+                       compute_relseq_breakwrites(newcurr);
        }
        return newcurr;
 }
@@ -678,6 +758,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                        if (act->is_mutex_op() && process_mutex(act))
                                update_all = true;
 
+                       if (act->is_relseq_fixup())
+                               process_relseq_fixup(curr, &work_queue);
+
                        if (update_all)
                                work_queue.push_back(CheckRelSeqWorkEntry(NULL));
                        else if (update)
@@ -740,7 +823,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) {
        if ((!parnode->backtrack_empty() ||
                         !currnode->read_from_empty() ||
                         !currnode->future_value_empty() ||
-                        !currnode->promise_empty())
+                        !currnode->promise_empty() ||
+                        !currnode->relseq_break_empty())
                        && (!priv->next_backtrack ||
                                        *curr > *priv->next_backtrack)) {
                priv->next_backtrack = curr;
@@ -1264,6 +1348,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
                                th->is_complete())
                        future_ordered = true;
 
+               ASSERT(!th->is_model_thread() || future_ordered);
+
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        const ModelAction *act = *rit;
                        /* Reach synchronization -> this thread is complete */
@@ -1652,6 +1738,29 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
        }
 }
 
+/**
+ * Compute the set of writes that may break the current pending release
+ * sequence. This information is extracted from previou release sequence
+ * calculations.
+ *
+ * @param curr The current ModelAction. Must be a release sequence fixup
+ * action.
+ */
+void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
+{
+       if (pending_rel_seqs->empty())
+               return;
+
+       struct release_seq *pending = pending_rel_seqs->back();
+       for (unsigned int i = 0; i < pending->writes.size(); i++) {
+               const ModelAction *write = pending->writes[i];
+               curr->get_node()->add_relseq_break(write);
+       }
+
+       /* NULL means don't break the sequence; just synchronize */
+       curr->get_node()->add_relseq_break(NULL);
+}
+
 /**
  * Build up an initial set of all past writes that this 'read' action may read
  * from. This set is determined by the clock vector's "happens before"
@@ -1855,7 +1964,7 @@ bool ModelChecker::take_step() {
        if (has_asserted())
                return false;
 
-       Thread *curr = thread_current();
+       Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
        if (curr) {
                if (curr->get_state() == THREAD_READY) {
                        ASSERT(priv->current_action);
@@ -1878,6 +1987,26 @@ bool ModelChecker::take_step() {
        DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
                        next ? id_to_int(next->get_id()) : -1);
 
+       /*
+        * Launch end-of-execution release sequence fixups only when there are:
+        *
+        * (1) no more user threads to run (or when execution replay chooses
+        *     the 'model_thread')
+        * (2) pending release sequences
+        * (3) pending assertions (i.e., data races)
+        * (4) no pending promises
+        */
+       if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
+                       isfinalfeasible() && !unrealizedraces.empty()) {
+               printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
+                               pending_rel_seqs->size());
+               ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
+                               std::memory_order_seq_cst, NULL, VALUE_NONE,
+                               model_thread);
+               set_current_action(fixup);
+               return true;
+       }
+
        /* next == NULL -> don't take any more steps */
        if (!next)
                return false;
diff --git a/model.h b/model.h
index d5dc422..68831b8 100644 (file)
--- a/model.h
+++ b/model.h
@@ -140,6 +140,7 @@ private:
        bool process_write(ModelAction *curr);
        bool process_mutex(ModelAction *curr);
        bool process_thread_action(ModelAction *curr);
+       void process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue);
        bool check_action_enabled(ModelAction *curr);
 
        bool take_step();
@@ -152,6 +153,7 @@ private:
        void reset_to_initial_state();
        bool resolve_promises(ModelAction *curr);
        void compute_promises(ModelAction *curr);
+       void compute_relseq_breakwrites(ModelAction *curr);
 
        void check_curr_backtracking(ModelAction * curr);
        void add_action_to_lists(ModelAction *act);
@@ -201,6 +203,10 @@ private:
         * together for efficiency and maintainability. */
        struct model_snapshot_members *priv;
 
+       /** A special model-checker Thread; used for associating with
+        *  model-checker-related ModelAcitons */
+       Thread *model_thread;
+
        /**
         * @brief The modification order graph
         *
index 4cf8950..72c8d5c 100644 (file)
@@ -32,7 +32,9 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
        may_read_from(),
        read_from_index(0),
        future_values(),
-       future_index(-1)
+       future_index(-1),
+       relseq_break_writes(),
+       relseq_break_index(0)
 {
        if (act) {
                act->set_node(this);
@@ -352,6 +354,58 @@ bool Node::increment_future_value() {
        return false;
 }
 
+/**
+ * Add a write ModelAction to the set of writes that may break the release
+ * sequence. This is used during replay exploration of pending release
+ * sequences. This Node must correspond to a release sequence fixup action.
+ *
+ * @param write The write that may break the release sequence. NULL means we
+ * allow the release sequence to synchronize.
+ */
+void Node::add_relseq_break(const ModelAction *write)
+{
+       relseq_break_writes.push_back(write);
+}
+
+/**
+ * Get the write that may break the current pending release sequence,
+ * according to the replay / divergence pattern.
+ *
+ * @return A write that may break the release sequence. If NULL, that means
+ * the release sequence should not be broken.
+ */
+const ModelAction * Node::get_relseq_break()
+{
+       if (relseq_break_index < (int)relseq_break_writes.size())
+               return relseq_break_writes[relseq_break_index];
+       else
+               return NULL;
+}
+
+/**
+ * Increments the index into the relseq_break_writes set to explore the next
+ * item.
+ * @return Returns false if we have explored all values.
+ */
+bool Node::increment_relseq_break()
+{
+       DBG();
+       promises.clear();
+       if (relseq_break_index < ((int)relseq_break_writes.size())) {
+               relseq_break_index++;
+               return (relseq_break_index < ((int)relseq_break_writes.size()));
+       }
+       return false;
+}
+
+/**
+ * @return True if all writes that may break the release sequence have been
+ * explored
+ */
+bool Node::relseq_break_empty() {
+       return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size()));
+}
+
 void Node::explore(thread_id_t tid)
 {
        int i = id_to_int(tid);
index 55deac5..cb281ca 100644 (file)
@@ -91,6 +91,11 @@ public:
        bool increment_promise();
        bool promise_empty();
 
+       void add_relseq_break(const ModelAction *write);
+       const ModelAction * get_relseq_break();
+       bool increment_relseq_break();
+       bool relseq_break_empty();
+
        void print();
        void print_may_read_from();
 
@@ -116,6 +121,9 @@ private:
        std::vector< struct future_value, ModelAlloc<struct future_value> > future_values;
        std::vector< promise_t, ModelAlloc<promise_t> > promises;
        int future_index;
+
+       std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > relseq_break_writes;
+       int relseq_break_index;
 };
 
 typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t;
index cca60eb..dd35237 100644 (file)
@@ -48,6 +48,7 @@ bool Scheduler::is_enabled(Thread *t) const
 void Scheduler::add_thread(Thread *t)
 {
        DEBUG("thread %d\n", id_to_int(t->get_id()));
+       ASSERT(!t->is_model_thread());
        set_enabled(t, THREAD_ENABLED);
 }
 
@@ -79,6 +80,7 @@ void Scheduler::sleep(Thread *t)
  */
 void Scheduler::wake(Thread *t)
 {
+       ASSERT(!t->is_model_thread());
        set_enabled(t, THREAD_DISABLED);
        t->set_state(THREAD_READY);
 }
@@ -106,6 +108,9 @@ Thread * Scheduler::next_thread(Thread *t)
                                return NULL;
                        }
                }
+       } else if (t->is_model_thread()) {
+               /* model-checker threads never run */
+               t = NULL;
        } else {
                curr_thread_index = id_to_int(t->get_id());
        }
@@ -120,6 +125,7 @@ Thread * Scheduler::next_thread(Thread *t)
  */
 Thread * Scheduler::get_current_thread() const
 {
+       ASSERT(!current || !current->is_model_thread());
        return current;
 }
 
index 37433b1..f3ae9f4 100644 (file)
 #include "stdatomic.h"
 
 atomic_int x;
+int var = 0;
 
 static void a(void *obj)
 {
+       store_32(&var, 1);
        atomic_store_explicit(&x, *((int *)obj), memory_order_release);
        atomic_store_explicit(&x, *((int *)obj) + 1, memory_order_relaxed);
 }
@@ -23,6 +25,7 @@ static void b2(void *obj)
 {
        int r = atomic_load_explicit(&x, memory_order_acquire);
        printf("r = %u\n", r);
+       store_32(&var, 3);
 }
 
 static void b1(void *obj)
@@ -31,6 +34,7 @@ static void b1(void *obj)
        int i = 7;
        int r = atomic_load_explicit(&x, memory_order_acquire);
        printf("r = %u\n", r);
+       store_32(&var, 2);
        thrd_create(&t3, (thrd_start_t)&a, &i);
        thrd_create(&t4, (thrd_start_t)&b2, NULL);
        thrd_join(t3);
index d3127f3..462a59f 100644 (file)
 #include "stdatomic.h"
 
 atomic_int x;
+int var = 0;
 
 static void a(void *obj)
 {
+       store_32(&var, 1);
        atomic_store_explicit(&x, 1, memory_order_release);
        atomic_store_explicit(&x, 42, memory_order_relaxed);
 }
@@ -22,6 +24,7 @@ static void b(void *obj)
 {
        int r = atomic_load_explicit(&x, memory_order_acquire);
        printf("r = %u\n", r);
+       printf("load %d\n", load_32(&var));
 }
 
 static void c(void *obj)
index ca4b28b..7f51515 100644 (file)
@@ -2,6 +2,8 @@
  *  @brief Thread functions.
  */
 
+#include <string.h>
+
 #include "libthreads.h"
 #include "common.h"
 #include "threads.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,7 +153,8 @@ 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;
 
index a379494..7f005c0 100644 (file)
--- a/threads.h
+++ b/threads.h
@@ -35,6 +35,7 @@ class ModelAction;
 /** @brief A Thread is created for each user-space thread */
 class Thread {
 public:
+       Thread(thread_id_t tid);
        Thread(thrd_t *t, void (*func)(void *), void *a);
        ~Thread();
        void complete();
@@ -101,6 +102,8 @@ public:
                return ret;
        }
 
+       bool is_model_thread() { return model_thread; }
+
        friend void thread_startup();
 
        SNAPSHOTALLOC
@@ -131,6 +134,9 @@ private:
         * @see Thread::get_return_value()
         */
        uint64_t last_action_val;
+
+       /** @brief Is this Thread a special model-checker thread? */
+       const bool model_thread;
 };
 
 Thread * thread_current();