nodestack: bugfix - rewrite 'may-read-from' and 'future values' as the same set
authorBrian Norris <banorris@uci.edu>
Thu, 28 Feb 2013 02:48:46 +0000 (18:48 -0800)
committerBrian Norris <banorris@uci.edu>
Thu, 28 Feb 2013 03:06:58 +0000 (19:06 -0800)
There were some subtle bugs that appeared because of the difficulty in
iterating over two separate sets that represent the "read from" set for
a particular read. Now, we expose an interface where there's just a
single pair of functions 'increment_read_from()' and
'read_from_empty()', for iterating over this set, along with a
flag-check 'get_read_from_status()', so that we know where to grab
values from (get_read_from_past() or get_future_value()).

This also does a lot of code moving and documentation in nodestack.cc,
for better readability and organization.

model.cc
nodestack.cc
nodestack.h

index 73bafc0..ced3431 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -259,14 +259,10 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
                        /* The next node will try to satisfy a different set of promises. */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
-               } else if (nextnode->increment_read_from_past()) {
+               } else if (nextnode->increment_read_from()) {
                        /* The next node will read from a different value. */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
-               } else if (nextnode->increment_future_value()) {
-                       /* 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();
@@ -852,16 +848,17 @@ bool ModelChecker::process_read(ModelAction *curr)
        uint64_t value = VALUE_NONE;
        bool updated = false;
        while (true) {
-               const ModelAction *rf = node->get_read_from_past();
-               if (rf != NULL) {
-                       mo_graph->startChanges();
+               switch (node->get_read_from_status()) {
+               case READ_FROM_PAST: {
+                       const ModelAction *rf = node->get_read_from_past();
+                       ASSERT(rf);
 
+                       mo_graph->startChanges();
                        value = rf->get_value();
-
                        check_recency(curr, rf);
                        bool r_status = r_modification_order(curr, rf);
 
-                       if (is_infeasible() && (node->increment_read_from_past() || node->increment_future_value())) {
+                       if (is_infeasible() && node->increment_read_from()) {
                                mo_graph->rollbackChanges();
                                priv->too_many_reads = false;
                                continue;
@@ -872,7 +869,9 @@ bool ModelChecker::process_read(ModelAction *curr)
                        mo_check_promises(curr, true);
 
                        updated |= r_status;
-               } else {
+                       break;
+               }
+               case READ_FROM_FUTURE: {
                        /* Read from future value */
                        struct future_value fv = node->get_future_value();
                        Promise *promise = new Promise(curr, fv);
@@ -882,6 +881,10 @@ bool ModelChecker::process_read(ModelAction *curr)
                        mo_graph->startChanges();
                        updated = r_modification_order(curr, promise);
                        mo_graph->commitChanges();
+                       break;
+               }
+               default:
+                       ASSERT(false);
                }
                get_thread(curr)->set_return_value(value);
                return updated;
@@ -1502,8 +1505,7 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr)
 
        if ((parnode && !parnode->backtrack_empty()) ||
                         !currnode->misc_empty() ||
-                        !currnode->read_from_past_empty() ||
-                        !currnode->future_value_empty() ||
+                        !currnode->read_from_empty() ||
                         !currnode->promise_empty() ||
                         !currnode->relseq_break_empty()) {
                set_latest_backtrack(curr);
@@ -2659,7 +2661,7 @@ void ModelChecker::build_may_read_from(ModelAction *curr)
        }
 
        /* We may find no valid may-read-from only if the execution is doomed */
-       if (!curr->get_node()->get_read_from_past_size() && curr->get_node()->future_value_empty()) {
+       if (!curr->get_node()->read_from_size()) {
                priv->no_valid_reads = true;
                set_assert();
        }
index 10115af..730c702 100644 (file)
@@ -24,8 +24,9 @@
  * @param nthreads The number of threads which exist at this point in the
  * execution trace.
  */
-Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
-       : action(act),
+Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
+       read_from_status(READ_FROM_PAST),
+       action(act),
        parent(par),
        num_threads(nthreads),
        explored_children(num_threads),
@@ -98,28 +99,22 @@ void Node::print() const
                if (backtrack[i] == true)
                        model_print("[%d]", i);
        model_print("\n");
-       model_print("          future values: %s", future_value_empty() ? "empty" : "non-empty ");
-       for (int i = future_index + 1; i < (int)future_values.size(); i++)
-               model_print("[%#" PRIx64 "]", future_values[i].value);
-       model_print("\n");
 
-       model_print("          read-from: %s", read_from_past_empty() ? "empty" : "non-empty ");
+       model_print("          read from past: %s", read_from_past_empty() ? "empty" : "non-empty ");
        for (int i = read_from_past_idx + 1; i < (int)read_from_past.size(); i++)
                model_print("[%d]", read_from_past[i]->get_seq_number());
        model_print("\n");
 
+       model_print("          future values: %s", future_value_empty() ? "empty" : "non-empty ");
+       for (int i = future_index + 1; i < (int)future_values.size(); i++)
+               model_print("[%#" PRIx64 "]", future_values[i].value);
+       model_print("\n");
+
        model_print("          promises: %s\n", promise_empty() ? "empty" : "non-empty");
        model_print("          misc: %s\n", misc_empty() ? "empty" : "non-empty");
        model_print("          rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
 }
 
-/** @brief Prints info about read_from_past set */
-void Node::print_read_from_past()
-{
-       for (unsigned int i = 0; i < read_from_past.size(); i++)
-               read_from_past[i]->print();
-}
-
 /**
  * Sets a promise to explore meeting with the given node.
  * @param i is the promise index.
@@ -216,56 +211,6 @@ bool Node::misc_empty() const
        return (misc_index + 1) >= misc_max;
 }
 
-/**
- * Adds a value from a weakly ordered future write to backtrack to. This
- * operation may "fail" if the future value has already been run (within some
- * sloppiness window of this expiration), or if the futurevalues set has
- * reached its maximum.
- * @see model_params.maxfuturevalues
- *
- * @param value is the value to backtrack to.
- * @return True if the future value was successully added; false otherwise
- */
-bool Node::add_future_value(struct future_value fv)
-{
-       uint64_t value = fv.value;
-       modelclock_t expiration = fv.expiration;
-       thread_id_t tid = fv.tid;
-       int idx = -1; /* Highest index where value is found */
-       for (unsigned int i = 0; i < future_values.size(); i++) {
-               if (future_values[i].value == value && future_values[i].tid == tid) {
-                       if (expiration <= future_values[i].expiration)
-                               return false;
-                       idx = i;
-               }
-       }
-       if (idx > future_index) {
-               /* Future value hasn't been explored; update expiration */
-               future_values[idx].expiration = expiration;
-               return true;
-       } else if (idx >= 0 && expiration <= future_values[idx].expiration + model->params.expireslop) {
-               /* Future value has been explored and is within the "sloppy" window */
-               return false;
-       }
-
-       /* Limit the size of the future-values set */
-       if (model->params.maxfuturevalues > 0 &&
-                       (int)future_values.size() >= model->params.maxfuturevalues)
-               return false;
-
-       future_values.push_back(fv);
-       return true;
-}
-
-/**
- * Checks whether the future_values set for this node is empty.
- * @return true if the future_values set is empty.
- */
-bool Node::future_value_empty() const
-{
-       return ((future_index + 1) >= ((int)future_values.size()));
-}
-
 /**
  * Checks if the Thread associated with this thread ID has been explored from
  * this Node already.
@@ -288,15 +233,6 @@ bool Node::backtrack_empty() const
        return (numBacktracks == 0);
 }
 
-/**
- * Checks whether the readsfrom set for this node is empty.
- * @return true if the readsfrom set is empty.
- */
-bool Node::read_from_past_empty() const
-{
-       return ((read_from_past_idx + 1) >= read_from_past.size());
-}
-
 /**
  * Mark the appropriate backtracking information for exploring a thread choice.
  * @param act The ModelAction to explore
@@ -382,34 +318,74 @@ bool Node::has_priority(thread_id_t tid) const
        return fairness[id_to_int(tid)].priority;
 }
 
+/*********************************** read from ********************************/
+
 /**
- * Add an action to the read_from_past set.
- * @param act is the action to add
+ * Get the current state of the may-read-from set iteration
+ * @return The read-from type we should currently be checking (past or future)
  */
-void Node::add_read_from_past(const ModelAction *act)
+read_from_type_t Node::get_read_from_status()
 {
-       read_from_past.push_back(act);
+       if (read_from_status == READ_FROM_PAST && read_from_past.empty())
+               increment_read_from();
+       return read_from_status;
 }
 
 /**
- * Gets the next 'future_value' from this Node. Only valid for a node where
- * this->action is a 'read'.
- * @return The first element in future_values
+ * Iterate one step in the may-read-from iteration. This includes a step in
+ * reading from the either the past or the future.
+ * @return True if there is a new read-from to explore; false otherwise
  */
-struct future_value Node::get_future_value() const
+bool Node::increment_read_from()
 {
-       ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
-       return future_values[future_index];
+       promises.clear();
+       if (increment_read_from_past()) {
+              read_from_status = READ_FROM_PAST;
+              return true;
+       } else if (increment_future_value()) {
+               read_from_status = READ_FROM_FUTURE;
+               return true;
+       }
+       read_from_status = READ_FROM_NONE;
+       return false;
 }
 
-int Node::get_read_from_past_size() const
+/**
+ * @return True if there are any new read-froms to explore
+ */
+bool Node::read_from_empty() const
 {
-       return read_from_past.size();
+       return read_from_past_empty() && future_value_empty();
 }
 
-const ModelAction * Node::get_read_from_past(int i) const
+/**
+ * Get the total size of the may-read-from set, including both past and future
+ * values
+ * @return The size of may-read-from
+ */
+unsigned int Node::read_from_size() const
 {
-       return read_from_past[i];
+       return read_from_past.size() + future_values.size();
+}
+
+/******************************* end read from ********************************/
+
+/****************************** read from past ********************************/
+
+/** @brief Prints info about read_from_past set */
+void Node::print_read_from_past()
+{
+       for (unsigned int i = 0; i < read_from_past.size(); i++)
+               read_from_past[i]->print();
+}
+
+/**
+ * Add an action to the read_from_past set.
+ * @param act is the action to add
+ */
+void Node::add_read_from_past(const ModelAction *act)
+{
+       read_from_past.push_back(act);
 }
 
 /**
@@ -425,6 +401,25 @@ const ModelAction * Node::get_read_from_past() const
                return NULL;
 }
 
+const ModelAction * Node::get_read_from_past(int i) const
+{
+       return read_from_past[i];
+}
+
+int Node::get_read_from_past_size() const
+{
+       return read_from_past.size();
+}
+
+/**
+ * Checks whether the readsfrom set for this node is empty.
+ * @return true if the readsfrom set is empty.
+ */
+bool Node::read_from_past_empty() const
+{
+       return ((read_from_past_idx + 1) >= read_from_past.size());
+}
+
 /**
  * Increments the index into the readsfrom set to explore the next item.
  * @return Returns false if we have explored all items.
@@ -432,7 +427,6 @@ const ModelAction * Node::get_read_from_past() const
 bool Node::increment_read_from_past()
 {
        DBG();
-       promises.clear();
        if (read_from_past_idx < read_from_past.size()) {
                read_from_past_idx++;
                return read_from_past_idx < read_from_past.size();
@@ -440,6 +434,71 @@ bool Node::increment_read_from_past()
        return false;
 }
 
+/************************** end read from past ********************************/
+
+/****************************** future values *********************************/
+
+/**
+ * Adds a value from a weakly ordered future write to backtrack to. This
+ * operation may "fail" if the future value has already been run (within some
+ * sloppiness window of this expiration), or if the futurevalues set has
+ * reached its maximum.
+ * @see model_params.maxfuturevalues
+ *
+ * @param value is the value to backtrack to.
+ * @return True if the future value was successully added; false otherwise
+ */
+bool Node::add_future_value(struct future_value fv)
+{
+       uint64_t value = fv.value;
+       modelclock_t expiration = fv.expiration;
+       thread_id_t tid = fv.tid;
+       int idx = -1; /* Highest index where value is found */
+       for (unsigned int i = 0; i < future_values.size(); i++) {
+               if (future_values[i].value == value && future_values[i].tid == tid) {
+                       if (expiration <= future_values[i].expiration)
+                               return false;
+                       idx = i;
+               }
+       }
+       if (idx > future_index) {
+               /* Future value hasn't been explored; update expiration */
+               future_values[idx].expiration = expiration;
+               return true;
+       } else if (idx >= 0 && expiration <= future_values[idx].expiration + model->params.expireslop) {
+               /* Future value has been explored and is within the "sloppy" window */
+               return false;
+       }
+
+       /* Limit the size of the future-values set */
+       if (model->params.maxfuturevalues > 0 &&
+                       (int)future_values.size() >= model->params.maxfuturevalues)
+               return false;
+
+       future_values.push_back(fv);
+       return true;
+}
+
+/**
+ * Gets the next 'future_value' from this Node. Only valid for a node where
+ * this->action is a 'read'.
+ * @return The first element in future_values
+ */
+struct future_value Node::get_future_value() const
+{
+       ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
+       return future_values[future_index];
+}
+
+/**
+ * Checks whether the future_values set for this node is empty.
+ * @return true if the future_values set is empty.
+ */
+bool Node::future_value_empty() const
+{
+       return ((future_index + 1) >= ((int)future_values.size()));
+}
+
 /**
  * Increments the index into the future_values set to explore the next item.
  * @return Returns false if we have explored all values.
@@ -447,7 +506,6 @@ bool Node::increment_read_from_past()
 bool Node::increment_future_value()
 {
        DBG();
-       promises.clear();
        if (future_index < ((int)future_values.size())) {
                future_index++;
                return (future_index < ((int)future_values.size()));
@@ -455,6 +513,8 @@ bool Node::increment_future_value()
        return false;
 }
 
+/************************** end future values *********************************/
+
 /**
  * Add a write ModelAction to the set of writes that may break the release
  * sequence. This is used during replay exploration of pending release
index 6200887..a857084 100644 (file)
@@ -38,6 +38,12 @@ struct fairness_info {
        bool priority;
 };
 
+typedef enum {
+       READ_FROM_PAST,
+       READ_FROM_FUTURE,
+       READ_FROM_NONE,
+} read_from_type_t;
+
 /**
  * @brief A single node in a NodeStack
  *
@@ -72,17 +78,19 @@ public:
         * occurred previously in the stack. */
        Node * get_parent() const { return parent; }
 
-       bool add_future_value(struct future_value fv);
-       struct future_value get_future_value() const;
-       bool increment_future_value();
-       bool future_value_empty() const;
+       read_from_type_t get_read_from_status();
+       bool increment_read_from();
+       bool read_from_empty() const;
+       unsigned int read_from_size() const;
 
+       void print_read_from_past();
        void add_read_from_past(const ModelAction *act);
        const ModelAction * get_read_from_past() const;
-       bool increment_read_from_past();
-       bool read_from_past_empty() const;
-       int get_read_from_past_size() const;
        const ModelAction * get_read_from_past(int i) const;
+       int get_read_from_past_size() const;
+
+       bool add_future_value(struct future_value fv);
+       struct future_value get_future_value() const;
 
        void set_promise(unsigned int i, bool is_rmw);
        bool get_promise(unsigned int i) const;
@@ -101,12 +109,17 @@ public:
        bool relseq_break_empty() const;
 
        void print() const;
-       void print_read_from_past();
 
        MEMALLOC
 private:
        void explore(thread_id_t tid);
 
+       bool read_from_past_empty() const;
+       bool increment_read_from_past();
+       bool future_value_empty() const;
+       bool increment_future_value();
+       read_from_type_t read_from_status;
+
        ModelAction * const action;
        Node * const parent;
        const int num_threads;