merge massive speedup with release sequence support...
authorBrian Demsky <bdemsky@uci.edu>
Mon, 8 Oct 2012 08:21:35 +0000 (01:21 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Mon, 8 Oct 2012 08:21:35 +0000 (01:21 -0700)
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

Conflicts:
schedule.cc
schedule.h

15 files changed:
action.cc
action.h
common.cc
model.cc
model.h
nodestack.cc
nodestack.h
schedule.cc
schedule.h
stacktrace.h [new file with mode: 0644]
test/double-relseq.c [new file with mode: 0644]
test/pending-release.c
test/releaseseq.c
threads.cc
threads.h

index 8dba82f..c1adc2e 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),
@@ -22,7 +35,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();
 }
 
@@ -52,6 +65,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;
@@ -307,6 +325,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 e05e094..b274989 100644 (file)
--- a/common.cc
+++ b/common.cc
@@ -4,12 +4,17 @@
 
 #include "common.h"
 #include "model.h"
+#include "stacktrace.h"
 
 #define MAX_TRACE_LEN 100
 
+#define CONFIG_STACKTRACE
 /** Print a backtrace of the current program state. */
 void print_trace(void)
 {
+#ifdef CONFIG_STACKTRACE
+       print_stacktrace(stdout);
+#else
        void *array[MAX_TRACE_LEN];
        char **strings;
        int size, i;
@@ -23,6 +28,7 @@ void print_trace(void)
                printf("\t%s\n", strings[i]);
 
        free(strings);
+#endif /* CONFIG_STACKTRACE */
 }
 
 void model_print_summary(void)
index 2c27567..4f2719f 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 */
@@ -166,6 +170,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 */
                        scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
@@ -249,7 +257,7 @@ bool ModelChecker::next_execution()
                num_feasible_executions++;
        }
 
-       DEBUG("Number of acquires waiting on pending release sequences: %lu\n",
+       DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
                        pending_rel_seqs->size());
 
        if (isfinalfeasible() || DBG_ENABLED())
@@ -582,6 +590,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
@@ -633,6 +711,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;
 }
@@ -721,6 +801,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)
@@ -781,7 +864,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;
@@ -1299,10 +1383,14 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
                bool future_ordered = false;
 
                ModelAction *last = get_last_action(int_to_id(i));
-               if (last && (rf->happens_before(last) ||
-                               get_thread(int_to_id(i))->is_complete()))
+               Thread *th = get_thread(int_to_id(i));
+               if ((last && rf->happens_before(last)) ||
+                               !scheduler->is_enabled(th) ||
+                               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 */
@@ -1691,6 +1779,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"
@@ -1894,7 +2005,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);
@@ -1917,6 +2028,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 d2baaf4..7bc3585 100644 (file)
--- a/model.h
+++ b/model.h
@@ -141,6 +141,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();
@@ -153,6 +154,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);
@@ -202,6 +204,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 76d167d..3db80e8 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 147b004..803d2b8 100644 (file)
@@ -92,6 +92,11 @@ public:
        bool promise_empty();
        enabled_type_t *get_enabled_array() {return enabled_array;}
 
+       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();
 
@@ -117,6 +122,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 c5e58fe..ea1d582 100644 (file)
@@ -9,7 +9,7 @@
 
 /** Constructor */
 Scheduler::Scheduler() :
-       is_enabled(NULL),
+       enabled(NULL),
        enabled_len(0),
        curr_thread_index(0),
        current(NULL)
@@ -21,25 +21,36 @@ void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) {
        if (threadid>=enabled_len) {
                enabled_type_t *new_enabled = (enabled_type_t *)snapshot_malloc(sizeof(enabled_type_t) * (threadid + 1));
                memset(&new_enabled[enabled_len], 0, (threadid+1-enabled_len)*sizeof(enabled_type_t));
-               if (is_enabled != NULL) {
-                       memcpy(new_enabled, is_enabled, enabled_len*sizeof(enabled_type_t));
-                       snapshot_free(is_enabled);
+               if (enabled != NULL) {
+                       memcpy(new_enabled, enabled, enabled_len*sizeof(enabled_type_t));
+                       snapshot_free(enabled);
                }
-               is_enabled=new_enabled;
+               enabled=new_enabled;
                enabled_len=threadid+1;
        }
-       is_enabled[threadid]=enabled_status;
+       enabled[threadid]=enabled_status;
+}
+
+/**
+ * @brief Check if a Thread is currently enabled
+ * @param t The Thread to check
+ * @return True if the Thread is currently enabled
+ */
+bool Scheduler::is_enabled(Thread *t) const
+{
+       int id = id_to_int(t->get_id());
+       return (id >= enabled_len) ? false : (enabled[id] != THREAD_DISABLED);
 }
 
 enabled_type_t Scheduler::get_enabled(Thread *t) {
-       return is_enabled[id_to_int(t->get_id())];
+       return enabled[id_to_int(t->get_id())];
 }
 
 void Scheduler::update_sleep_set(Node *n) {
        enabled_type_t *enabled_array=n->get_enabled_array();
        for(int i=0;i<enabled_len;i++) {
                if (enabled_array[i]==THREAD_SLEEP_SET) {
-                       is_enabled[i]=THREAD_SLEEP_SET;
+                       enabled[i]=THREAD_SLEEP_SET;
                }
        }
 }
@@ -71,6 +82,7 @@ void Scheduler::remove_sleep(Thread *t)
 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);
 }
 
@@ -102,6 +114,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);
 }
@@ -120,7 +133,7 @@ Thread * Scheduler::next_thread(Thread *t)
                int old_curr_thread = curr_thread_index;
                while(true) {
                        curr_thread_index = (curr_thread_index+1) % enabled_len;
-                       if (is_enabled[curr_thread_index]==THREAD_ENABLED) {
+                       if (enabled[curr_thread_index]==THREAD_ENABLED) {
                                t = model->get_thread(int_to_id(curr_thread_index));
                                break;
                        }
@@ -129,6 +142,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());
        }
@@ -143,6 +159,7 @@ Thread * Scheduler::next_thread(Thread *t)
  */
 Thread * Scheduler::get_current_thread() const
 {
+       ASSERT(!current || !current->is_model_thread());
        return current;
 }
 
index 3a54e8c..7267059 100644 (file)
@@ -30,15 +30,17 @@ public:
        Thread * next_thread(Thread *t);
        Thread * get_current_thread() const;
        void print() const;
-       enabled_type_t * get_enabled() { return is_enabled; };
+       enabled_type_t * get_enabled() { return enabled; };
        void remove_sleep(Thread *t);
        void add_sleep(Thread *t);
        enabled_type_t get_enabled(Thread *t);
        void update_sleep_set(Node *n);
+       bool is_enabled(Thread *t) const;
+
        SNAPSHOTALLOC
 private:
        /** The list of available Threads that are not currently running */
-       enabled_type_t * is_enabled;
+       enabled_type_t *enabled;
        int enabled_len;
        int curr_thread_index;
        void set_enabled(Thread *t, enabled_type_t enabled_status);
diff --git a/stacktrace.h b/stacktrace.h
new file mode 100644 (file)
index 0000000..01d31d2
--- /dev/null
@@ -0,0 +1,86 @@
+// stacktrace.h (c) 2008, Timo Bingmann from http://idlebox.net/
+// published under the WTFPL v2.0
+
+#ifndef __STACKTRACE_H__
+#define __STACKTRACE_H__
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <execinfo.h>
+#include <cxxabi.h>
+
+/** Print a demangled stack backtrace of the caller function to FILE* out. */
+static inline void print_stacktrace(FILE *out = stderr, unsigned int max_frames = 63)
+{
+       fprintf(out, "stack trace:\n");
+
+       // storage array for stack trace address data
+       void* addrlist[max_frames+1];
+
+       // retrieve current stack addresses
+       int addrlen = backtrace(addrlist, sizeof(addrlist) / sizeof(void*));
+
+       if (addrlen == 0) {
+               fprintf(out, "  <empty, possibly corrupt>\n");
+               return;
+       }
+
+       // resolve addresses into strings containing "filename(function+address)",
+       // this array must be free()-ed
+       char** symbollist = backtrace_symbols(addrlist, addrlen);
+
+       // allocate string which will be filled with the demangled function name
+       size_t funcnamesize = 256;
+       char* funcname = (char*)malloc(funcnamesize);
+
+       // iterate over the returned symbol lines. skip the first, it is the
+       // address of this function.
+       for (int i = 1; i < addrlen; i++) {
+               char *begin_name = 0, *begin_offset = 0, *end_offset = 0;
+
+               // find parentheses and +address offset surrounding the mangled name:
+               // ./module(function+0x15c) [0x8048a6d]
+               for (char *p = symbollist[i]; *p; ++p) {
+                       if (*p == '(')
+                               begin_name = p;
+                       else if (*p == '+')
+                               begin_offset = p;
+                       else if (*p == ')' && begin_offset) {
+                               end_offset = p;
+                               break;
+                       }
+               }
+
+               if (begin_name && begin_offset && end_offset && begin_name < begin_offset) {
+                       *begin_name++ = '\0';
+                       *begin_offset++ = '\0';
+                       *end_offset = '\0';
+
+                       // mangled name is now in [begin_name, begin_offset) and caller
+                       // offset in [begin_offset, end_offset). now apply
+                       // __cxa_demangle():
+
+                       int status;
+                       char* ret = abi::__cxa_demangle(begin_name,
+                                       funcname, &funcnamesize, &status);
+                       if (status == 0) {
+                               funcname = ret; // use possibly realloc()-ed string
+                               fprintf(out, "  %s : %s+%s\n",
+                                               symbollist[i], funcname, begin_offset);
+                       } else {
+                               // demangling failed. Output function name as a C function with
+                               // no arguments.
+                               fprintf(out, "  %s : %s()+%s\n",
+                                               symbollist[i], begin_name, begin_offset);
+                       }
+               } else {
+                       // couldn't parse the line? print the whole line.
+                       fprintf(out, "  %s\n", symbollist[i]);
+               }
+       }
+
+       free(funcname);
+       free(symbollist);
+}
+
+#endif // __STACKTRACE_H__
diff --git a/test/double-relseq.c b/test/double-relseq.c
new file mode 100644 (file)
index 0000000..5b220eb
--- /dev/null
@@ -0,0 +1,57 @@
+/*
+ * This test performs some relaxed, release, acquire opeations on a single
+ * atomic variable. It can give some rough idea of release sequence support but
+ * probably should be improved to give better information.
+ *
+ * This test tries to establish two release sequences, where we should always
+ * either establish both or establish neither. (Note that this is only true for
+ * a few executions of interest, where both load-acquire's read from the same
+ * write.)
+ */
+
+#include <stdio.h>
+
+#include "libthreads.h"
+#include "librace.h"
+#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);
+}
+
+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)
+{
+       atomic_store_explicit(&x, 2, memory_order_relaxed);
+}
+
+void user_main()
+{
+       thrd_t t1, t2, t3, t4;
+
+       atomic_init(&x, 0);
+
+       printf("Thread %d: creating 4 threads\n", thrd_current());
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&b, NULL);
+       thrd_create(&t3, (thrd_start_t)&b, NULL);
+       thrd_create(&t4, (thrd_start_t)&c, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+       thrd_join(t3);
+       thrd_join(t4);
+       printf("Thread %d is finished\n", thrd_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();