nodestack: rename 'read_from' to 'read_from_past'

One step of re-architecting the reads-from set in NodeStack (i.e.,
read from past + promised future values + future values).

diff --git a/model.cc b/model.cc
index 417cbc1cf05ee95dffb3bb37180f56fd9d0bcd9e..649f3d95a8bf555e4271cd260014be4daf78c876 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -259,7 +259,7 @@ 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()) {
+               } else if (nextnode->increment_read_from_past()) {
                        /* The next node will read from a different value. */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
@@ -851,7 +851,7 @@ bool ModelChecker::process_read(ModelAction *curr)
        uint64_t value = VALUE_NONE;
        bool updated = false;
        while (true) {
-               const ModelAction *reads_from = curr->get_node()->get_read_from();
+               const ModelAction *reads_from = curr->get_node()->get_read_from_past();
                if (reads_from != NULL) {
                        mo_graph->startChanges();
 
@@ -860,7 +860,7 @@ bool ModelChecker::process_read(ModelAction *curr)
                        check_recency(curr, reads_from);
                        bool r_status = r_modification_order(curr, reads_from);
 
-                       if (is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
+                       if (is_infeasible() && (curr->get_node()->increment_read_from_past() || curr->get_node()->increment_future_value())) {
                                mo_graph->rollbackChanges();
                                priv->too_many_reads = false;
                                continue;
@@ -1501,7 +1501,7 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr)
 
        if ((parnode && !parnode->backtrack_empty()) ||
                         !currnode->misc_empty() ||
-                        !currnode->read_from_empty() ||
+                        !currnode->read_from_past_empty() ||
                         !currnode->future_value_empty() ||
                         !currnode->promise_empty() ||
                         !currnode->relseq_break_empty()) {
@@ -1609,7 +1609,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 {
        if (params.maxreads != 0) {
-               if (curr->get_node()->get_read_from_size() <= 1)
+               if (curr->get_node()->get_read_from_past_size() <= 1)
                        return;
                //Must make sure that execution is currently feasible...  We could
                //accidentally clear by rolling back
@@ -1642,12 +1642,12 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 
                        if (act->get_reads_from() != rf)
                                return;
-                       if (act->get_node()->get_read_from_size() <= 1)
+                       if (act->get_node()->get_read_from_past_size() <= 1)
                                return;
                }
-               for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
+               for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
                        /* Get write */
-                       const ModelAction *write = curr->get_node()->get_read_from_at(i);
+                       const ModelAction *write = curr->get_node()->get_read_from_past(i);
 
                        /* Need a different write */
                        if (write == rf)
@@ -1665,8 +1665,8 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
                        for (int loop = count; loop > 0; loop--, rit++) {
                                ModelAction *act = *rit;
                                bool foundvalue = false;
-                               for (int j = 0; j < act->get_node()->get_read_from_size(); j++) {
-                                       if (act->get_node()->get_read_from_at(j) == write) {
+                               for (int j = 0; j < act->get_node()->get_read_from_past_size(); j++) {
+                                       if (act->get_node()->get_read_from_past(j) == write) {
                                                foundvalue = true;
                                                break;
                                        }
@@ -2631,7 +2631,7 @@ void ModelChecker::build_may_read_from(ModelAction *curr)
                                mo_graph->startChanges();
                                r_modification_order(curr, act);
                                if (!is_infeasible())
-                                       curr->get_node()->add_read_from(act);
+                                       curr->get_node()->add_read_from_past(act);
                                mo_graph->rollbackChanges();
                        }
 
@@ -2658,7 +2658,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_size() && curr->get_node()->future_value_empty()) {
+       if (!curr->get_node()->get_read_from_past_size() && curr->get_node()->future_value_empty()) {
                priv->no_valid_reads = true;
                set_assert();
        }
@@ -2666,9 +2666,9 @@ void ModelChecker::build_may_read_from(ModelAction *curr)
        if (DBG_ENABLED()) {
                model_print("Reached read action:\n");
                curr->print();
-               model_print("Printing may_read_from\n");
-               curr->get_node()->print_may_read_from();
-               model_print("End printing may_read_from\n");
+               model_print("Printing read_from_past\n");
+               curr->get_node()->print_read_from_past();
+               model_print("End printing read_from_past\n");
        }
 }
 

diff --git a/nodestack.cc b/nodestack.cc
index 9c0df20b5de89bd2876cde69ca281502506f4709..10115af6090f964793132e2656ecc9941f07cdc1 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -33,8 +33,8 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
        fairness(num_threads),
        numBacktracks(0),
        enabled_array(NULL),
-       may_read_from(),
-       read_from_index(0),
+       read_from_past(),
+       read_from_past_idx(0),
        future_values(),
        future_index(-1),
        relseq_break_writes(),
@@ -103,9 +103,9 @@ void Node::print() const
                model_print("[%#" PRIx64 "]", future_values[i].value);
        model_print("\n");
 
-       model_print("          read-from: %s", read_from_empty() ? "empty" : "non-empty ");
-       for (int i = read_from_index + 1; i < (int)may_read_from.size(); i++)
-               model_print("[%d]", may_read_from[i]->get_seq_number());
+       model_print("          read-from: %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("          promises: %s\n", promise_empty() ? "empty" : "non-empty");
@@ -113,11 +113,11 @@ void Node::print() const
        model_print("          rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
 }
 
-/** @brief Prints info about may_read_from set */
-void Node::print_may_read_from()
+/** @brief Prints info about read_from_past set */
+void Node::print_read_from_past()
 {
-       for (unsigned int i = 0; i < may_read_from.size(); i++)
-               may_read_from[i]->print();
+       for (unsigned int i = 0; i < read_from_past.size(); i++)
+               read_from_past[i]->print();
 }
 
 /**
@@ -292,9 +292,9 @@ bool Node::backtrack_empty() const
  * Checks whether the readsfrom set for this node is empty.
  * @return true if the readsfrom set is empty.
  */
-bool Node::read_from_empty() const
+bool Node::read_from_past_empty() const
 {
-       return ((read_from_index + 1) >= may_read_from.size());
+       return ((read_from_past_idx + 1) >= read_from_past.size());
 }
 
 /**
@@ -383,12 +383,12 @@ bool Node::has_priority(thread_id_t tid) const
 }
 
 /**
- * Add an action to the may_read_from set.
+ * Add an action to the read_from_past set.
  * @param act is the action to add
  */
-void Node::add_read_from(const ModelAction *act)
+void Node::add_read_from_past(const ModelAction *act)
 {
-       may_read_from.push_back(act);
+       read_from_past.push_back(act);
 }
 
 /**
@@ -402,25 +402,25 @@ struct future_value Node::get_future_value() const
        return future_values[future_index];
 }
 
-int Node::get_read_from_size() const
+int Node::get_read_from_past_size() const
 {
-       return may_read_from.size();
+       return read_from_past.size();
 }
 
-const ModelAction * Node::get_read_from_at(int i) const
+const ModelAction * Node::get_read_from_past(int i) const
 {
-       return may_read_from[i];
+       return read_from_past[i];
 }
 
 /**
- * Gets the next 'may_read_from' action from this Node. Only valid for a node
+ * Gets the next 'read_from_past' action from this Node. Only valid for a node
  * where this->action is a 'read'.
- * @return The first element in may_read_from
+ * @return The first element in read_from_past
  */
-const ModelAction * Node::get_read_from() const
+const ModelAction * Node::get_read_from_past() const
 {
-       if (read_from_index < may_read_from.size())
-               return may_read_from[read_from_index];
+       if (read_from_past_idx < read_from_past.size())
+               return read_from_past[read_from_past_idx];
        else
                return NULL;
 }
@@ -429,13 +429,13 @@ const ModelAction * Node::get_read_from() const
  * Increments the index into the readsfrom set to explore the next item.
  * @return Returns false if we have explored all items.
  */
-bool Node::increment_read_from()
+bool Node::increment_read_from_past()
 {
        DBG();
        promises.clear();
-       if (read_from_index < may_read_from.size()) {
-               read_from_index++;
-               return read_from_index < may_read_from.size();
+       if (read_from_past_idx < read_from_past.size()) {
+               read_from_past_idx++;
+               return read_from_past_idx < read_from_past.size();
        }
        return false;
 }

diff --git a/nodestack.h b/nodestack.h
index 941178d7be453267b7556a1226c4883a11128d9e..6200887a0e624c945fee33f09546ee87cd7109c1 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -77,12 +77,12 @@ public:
        bool increment_future_value();
        bool future_value_empty() const;
 
-       void add_read_from(const ModelAction *act);
-       const ModelAction * get_read_from() const;
-       bool increment_read_from();
-       bool read_from_empty() const;
-       int get_read_from_size() const;
-       const ModelAction * get_read_from_at(int i) const;
+       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;
 
        void set_promise(unsigned int i, bool is_rmw);
        bool get_promise(unsigned int i) const;
@@ -101,7 +101,7 @@ public:
        bool relseq_break_empty() const;
 
        void print() const;
-       void print_may_read_from();
+       void print_read_from_past();
 
        MEMALLOC
 private:
@@ -116,11 +116,12 @@ private:
        int numBacktracks;
        enabled_type_t *enabled_array;
 
-       /** The set of ModelActions that this the action at this Node may read
-        *  from. Only meaningful if this Node represents a 'read' action. */
-       std::vector< const ModelAction *, ModelAlloc< const ModelAction * > > may_read_from;
-
-       unsigned int read_from_index;
+       /**
+        * The set of past ModelActions that this the action at this Node may
+        * read from. Only meaningful if this Node represents a 'read' action.
+        */
+       std::vector< const ModelAction *, ModelAlloc< const ModelAction * > > read_from_past;
+       unsigned int read_from_past_idx;
 
        std::vector< struct future_value, ModelAlloc<struct future_value> > future_values;
        std::vector< promise_t, ModelAlloc<promise_t> > promises;