Merge branch 'brian'

diff --git a/Makefile b/Makefile
index ddc89cb2440926aaf0551084fe89c88a3e2bbdfa..6ef1e94de3cc5e879d402dfe424b5b21c79b8120 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -50,8 +50,8 @@ mymemory.o: mymemory.h snapshotimp.h snapshot.h mymemory.cc
 snapshot.o: mymemory.h snapshot.h snapshotimp.h snapshot.cc
        $(CXX) -fPIC -c snapshot.cc $(CPPFLAGS)
 
-$(MODEL_O): $(MODEL_CC) $(MODEL_H)
-       $(CXX) -fPIC -c $(MODEL_CC) $(CPPFLAGS)
+%.o: %.cc $(MODEL_H)
+       $(CXX) -fPIC -c $< $(CPPFLAGS)
 
 clean:
        rm -f $(BIN) *.o *.so

diff --git a/action.cc b/action.cc
index 9f95727c8dcb63b27dfffc9782ab376a644d852b..6627714e1089b2ad16c85cc7ef4abe43d77b6f95 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -144,7 +144,7 @@ bool ModelAction::happens_before(ModelAction *act)
        return act->cv->synchronized_since(this);
 }
 
-void ModelAction::print(void)
+void ModelAction::print(void) const
 {
        const char *type_str;
        switch (this->type) {

diff --git a/action.h b/action.h
index ae4afb29d27f928cbe63a34d79629a6d6310b28b..e342e63271d223417e55393d4d8bc941b1d2a0ba 100644 (file)
--- a/action.h
+++ b/action.h
@@ -31,18 +31,20 @@ class ClockVector;
  */
 class ModelAction {
 public:
-       ModelAction(action_type_t type, memory_order order, void *loc, int value);
+       ModelAction(action_type_t type, memory_order order, void *loc, int value = VALUE_NONE);
        ~ModelAction();
-       void print(void);
+       void print(void) const;
 
        thread_id_t get_tid() const { return tid; }
        action_type get_type() const { return type; }
        memory_order get_mo() const { return order; }
        void * get_location() const { return location; }
        int get_seq_number() const { return seq_number; }
+       int get_value() const { return value; }
 
        Node * get_node() const { return node; }
        void set_node(Node *n) { node = n; }
+       void set_value(int val) { value = val; }
 
        bool is_read() const;
        bool is_write() const;

diff --git a/model.cc b/model.cc
index 19d273de50bf67aa60cf6835845b21ac347fc7be..f12e4d27db44af7b3593067c806c539ce930ced9 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -124,7 +124,7 @@ thread_id_t ModelChecker::get_next_replay_thread()
        next = node_stack->get_next()->get_action();
 
        if (next == diverge) {
-               Node *node = next->get_node();
+               Node *node = next->get_node()->get_parent();
 
                /* Reached divergence point */
                DEBUG("*** Divergence point ***\n");
@@ -196,7 +196,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
        if (prev == NULL)
                return;
 
-       node = prev->get_node();
+       node = prev->get_node()->get_parent();
 
        while (!node->is_enabled(t))
                t = t->get_parent();
@@ -205,6 +205,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
        if (node->has_been_explored(t->get_id()))
                return;
 
+       /* Cache the latest backtracking point */
        if (!next_backtrack || *prev > *next_backtrack)
                next_backtrack = prev;
 
@@ -262,7 +263,7 @@ void ModelChecker::check_current_action(void)
 
        nextThread = get_next_replay_thread();
 
-       currnode = curr->get_node();
+       currnode = curr->get_node()->get_parent();
 
        if (!currnode->backtrack_empty())
                if (!next_backtrack || *curr > *next_backtrack)
@@ -273,12 +274,13 @@ void ModelChecker::check_current_action(void)
        add_action_to_lists(curr);
 }
 
-
 /**
- * Adds an action to the per-object, per-thread action vector.
+ * Performs various bookkeeping operations for the current ModelAction. For
+ * instance, adds action to the per-object, per-thread action vector and to the
+ * action trace list of all thread actions.
+ *
  * @param act is the ModelAction to add.
  */
-
 void ModelChecker::add_action_to_lists(ModelAction *act)
 {
        action_trace->push_back(act);
@@ -345,19 +347,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
        }
 }
 
-void ModelChecker::print_summary(void)
-{
-       printf("\n");
-       printf("Number of executions: %d\n", num_executions);
-       printf("Total nodes created: %d\n", node_stack->get_total_nodes());
-
-       scheduler->print();
-
-       print_list(action_trace);
-       printf("\n");
-}
-
-void ModelChecker::print_list(action_list_t *list)
+static void print_list(action_list_t *list)
 {
        action_list_t::iterator it;
 
@@ -370,6 +360,18 @@ void ModelChecker::print_list(action_list_t *list)
        printf("---------------------------------------------------------------------\n");
 }
 
+void ModelChecker::print_summary(void)
+{
+       printf("\n");
+       printf("Number of executions: %d\n", num_executions);
+       printf("Total nodes created: %d\n", node_stack->get_total_nodes());
+
+       scheduler->print();
+
+       print_list(action_trace);
+       printf("\n");
+}
+
 int ModelChecker::add_thread(Thread *t)
 {
        (*thread_map)[id_to_int(t->get_id())] = t;

diff --git a/model.h b/model.h
index ab961f840b03613492a4da2b8585453bbe6b2847..4635644b6b40b6bf1cfda8d08fc587b3a0fe67bb 100644 (file)
--- a/model.h
+++ b/model.h
@@ -80,8 +80,6 @@ private:
        ModelAction * get_parent_action(thread_id_t tid);
        void build_reads_from_past(ModelAction *curr);
 
-       void print_list(action_list_t *list);
-
        ModelAction *current_action;
        ModelAction *diverge;
        thread_id_t nextThread;

diff --git a/nodestack.cc b/nodestack.cc
index 87b3ee531fbe2d10a7b52f229f23e7ea90196e9d..d3b7c104316161d0268c8ae1b2db7a116fbbac74 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -3,15 +3,31 @@
 #include "common.h"
 #include "model.h"
 
-/** @brief Node constructor */
-Node::Node(ModelAction *act, int nthreads)
+/**
+ * @brief Node constructor
+ *
+ * Constructs a single Node for use in a NodeStack. Each Node is associated
+ * with exactly one ModelAction (exception: the first Node should be created
+ * as an empty stub, to represent the first thread "choice") and up to one
+ * parent.
+ *
+ * @param act The ModelAction to associate with this Node. May be NULL.
+ * @param par The parent Node in the NodeStack. May be NULL if there is no
+ * parent.
+ * @param nthreads The number of threads which exist at this point in the
+ * execution trace.
+ */
+Node::Node(ModelAction *act, Node *par, int nthreads)
        : action(act),
+       parent(par),
        num_threads(nthreads),
        explored_children(num_threads),
        backtrack(num_threads),
        numBacktracks(0),
        may_read_from()
 {
+       if (act)
+               act->set_node(this);
 }
 
 /** @brief Node desctructor */
@@ -53,14 +69,11 @@ bool Node::backtrack_empty()
 }
 
 /**
- * Explore a child Node using a given ModelAction. This updates both the
- * Node-internal and the ModelAction data to associate the ModelAction with
- * this Node.
- * @param act is the ModelAction to explore
+ * Mark the appropriate backtracking infromation for exploring a thread choice.
+ * @param act The ModelAction to explore
  */
 void Node::explore_child(ModelAction *act)
 {
-       act->set_node(this);
        explore(act->get_tid());
 }
 
@@ -173,7 +186,7 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
 
        /* Record action */
        get_head()->explore_child(act);
-       node_list.push_back(new Node(act, model->get_num_threads()));
+       node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
        total_nodes++;
        iter++;
        return NULL;

diff --git a/nodestack.h b/nodestack.h
index 74ac245f3b3b00331a3328482d7c21c47bdc7cdb..37f9261149bc49a9d0a99182e21102be39e1161a 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -16,9 +16,18 @@ class ModelAction;
 
 typedef std::set< ModelAction *, std::less< ModelAction *>, MyAlloc< ModelAction * > > action_set_t;
 
+/**
+ * @brief A single node in a NodeStack
+ *
+ * Represents a single node in the NodeStack. Each Node is associated with up
+ * to one action and up to one parent node. A node holds information
+ * regarding the last action performed (the "associated action"), the thread
+ * choices that have been explored (explored_children) and should be explored
+ * (backtrack), and the actions that the last action may read from.
+ */
 class Node {
 public:
-       Node(ModelAction *act = NULL, int nthreads = 1);
+       Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1);
        ~Node();
        /* return true = thread choice has already been explored */
        bool has_been_explored(thread_id_t tid);
@@ -31,6 +40,10 @@ public:
        bool is_enabled(Thread *t);
        ModelAction * get_action() { return action; }
 
+       /** @return the parent Node to this Node; that is, the action that
+        * occurred previously in the stack. */
+       Node * get_parent() const { return parent; }
+
        void add_read_from(ModelAction *act);
 
        void print();
@@ -40,6 +53,7 @@ private:
        void explore(thread_id_t tid);
 
        ModelAction *action;
+       Node *parent;
        int num_threads;
        std::vector< bool, MyAlloc<bool> > explored_children;
        std::vector< bool, MyAlloc<bool> > backtrack;
@@ -52,6 +66,14 @@ private:
 
 typedef std::list<class Node *, MyAlloc< class Node * > > node_list_t;
 
+/**
+ * @brief A stack of nodes
+ *
+ * Holds a Node linked-list that can be used for holding backtracking,
+ * may-read-from, and replay information. It is used primarily as a
+ * stack-like structure, in that backtracking points and replay nodes are
+ * only removed from the top (most recent).
+ */
 class NodeStack {
 public:
        NodeStack();