changes

[c11tester.git] / nodestack.cc

diff --git a/nodestack.cc b/nodestack.cc
index 131452d8f8e220200b04c43be926232348afadbd..082835802629ac989c13e57ed4adbdd8de81eb48 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -24,7 +24,10 @@ Node::Node(ModelAction *act, Node *par, int nthreads)
        explored_children(num_threads),
        backtrack(num_threads),
        numBacktracks(0),
-       may_read_from()
+       may_read_from(),
+       read_from_index(0),
+       future_values(),
+       future_index(0)
 {
        if (act)
                act->set_node(this);
@@ -54,6 +57,20 @@ void Node::print_may_read_from()
                (*it)->print();
 }
 
+/**
+ * Adds a value from a weakly ordered future write to backtrack to.
+ * @param value is the value to backtrack to.
+ */
+
+bool Node::add_future_value(uint64_t value) {
+       for(int i=0;i<future_values.size();i++)
+               if (future_values[i]==value)
+                       return false;
+       future_values.push_back(value);
+       return true;
+}
+
+
 /**
  * Checks if the Thread associated with this thread ID has been explored from
  * this Node already.
@@ -73,11 +90,29 @@ bool Node::has_been_explored(thread_id_t tid)
  */
 bool Node::backtrack_empty()
 {
-       return numBacktracks == 0;
+       return (numBacktracks == 0);
+}
+
+
+/**
+ * Checks whether the readsfrom set for this node is empty.
+ * @return true if the readsfrom set is empty.
+ */
+bool Node::readsfrom_empty() {
+       return ((read_from_index+1)>=may_read_from.size());
+}
+
+/** 
+ * Checks whether the future_values set for this node is empty.
+ * @return true if the future_values set is empty.
+ */
+
+bool Node::futurevalues_empty() {
+       return ((future_index+1)>=future_values.size());
 }
 
 /**
- * Mark the appropriate backtracking infromation for exploring a thread choice.
+ * Mark the appropriate backtracking information for exploring a thread choice.
  * @param act The ModelAction to explore
  */
 void Node::explore_child(ModelAction *act)
@@ -104,11 +139,14 @@ bool Node::set_backtrack(thread_id_t id)
 
 thread_id_t Node::get_next_backtrack()
 {
-       /* TODO: find next backtrack */
+       /** @todo Find next backtrack */
        unsigned int i;
        for (i = 0; i < backtrack.size(); i++)
                if (backtrack[i] == true)
                        break;
+       /* Backtrack set was empty? */
+       ASSERT(i != backtrack.size());
+
        backtrack[i] = false;
        numBacktracks--;
        return int_to_id(i);
@@ -128,6 +166,17 @@ void Node::add_read_from(const ModelAction *act)
        may_read_from.push_back(act);
 }
 
+/**
+ * Gets the next 'future_value' value from this Node. Only valid for a node
+ * where this->action is a 'read'.
+ * @return The first element in future_values
+ */
+
+uint64_t Node::get_future_value() {
+       ASSERT(future_index<future_values.size());
+       return future_values[future_index];
+}
+
 /**
  * Gets the next 'may_read_from' action from this Node. Only valid for a node
  * where this->action is a 'read'.
@@ -135,13 +184,30 @@ void Node::add_read_from(const ModelAction *act)
  * may remove elements from may_read_from
  * @return The first element in may_read_from
  */
-const ModelAction * Node::get_next_read_from() {
-       const ModelAction *act;
-       ASSERT(!may_read_from.empty());
-       act = may_read_from.front();
-       /* TODO: perform reads_from replay properly */
-       /* may_read_from.pop_front(); */
-       return act;
+const ModelAction * Node::get_read_from() {
+       if (read_from_index<may_read_from.size())
+               return may_read_from[read_from_index];
+       else
+               return NULL;
+}
+
+/**
+ * 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() {
+       read_from_index++;
+       return (read_from_index<may_read_from.size());
+}
+
+/**
+ * Increments the index into the future_values set to explore the next item.
+ * @return Returns false if we have explored all values.
+ */
+
+bool Node::increment_future_values() {
+       future_index++;
+       return (future_index<future_values.size());
 }
 
 void Node::explore(thread_id_t tid)
@@ -195,17 +261,14 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
        DBG();
 
        ASSERT(!node_list.empty());
+       node_list_t::iterator it=iter;
+       it++;
 
-       if (get_head()->has_been_explored(act->get_tid())) {
+       if (it != node_list.end()) {
                iter++;
                return (*iter)->get_action();
        }
 
-       /* Diverging from previous execution; clear out remainder of list */
-       node_list_t::iterator it = iter;
-       it++;
-       clear_node_list(&node_list, it, node_list.end());
-
        /* Record action */
        get_head()->explore_child(act);
        node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
@@ -214,6 +277,23 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
        return NULL;
 }
 
+/**
+ * Empties the stack of all trailing nodes after a given position and calls the
+ * destructor for each. This function is provided an offset which determines
+ * how many nodes (relative to the current replay state) to save before popping
+ * the stack.
+ * @param numAhead gives the number of Nodes (including this Node) to skip over
+ * before removing nodes.
+ */
+void NodeStack::pop_restofstack(int numAhead)
+{
+       /* Diverging from previous execution; clear out remainder of list */
+       node_list_t::iterator it = iter;
+       while (numAhead--)
+               it++;
+       clear_node_list(&node_list, it, node_list.end());
+}
+
 Node * NodeStack::get_head()
 {
        if (node_list.empty())