Add basic reads from support

Now we need to use the cyclegraph to eliminate bad executions...

diff --git a/model.cc b/model.cc
index a22e17e1f46fd20c780136f6f232399170111356..e9d1f1df069cb5f0f1b79c9683143b59c4b39ffe 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -126,13 +126,20 @@ thread_id_t ModelChecker::get_next_replay_thread()
        next = node_stack->get_next()->get_action();
 
        if (next == diverge) {
-               Node *node = next->get_node()->get_parent();
-
+               Node *nextnode = next->get_node();
                /* Reached divergence point */
+               if (nextnode->increment_read_from()) {
+                       /* The next node will read from a different value */
+                       tid = next->get_tid();
+                       node_stack->pop_restofstack(2);
+               } else {
+                       /* Make a different thread execute for next step */
+                       Node *node = nextnode->get_parent();
+                       tid = node->get_next_backtrack();
+                       node_stack->pop_restofstack(1);
+               }
                DEBUG("*** Divergence point ***\n");
-               tid = node->get_next_backtrack();
                diverge = NULL;
-               node_stack->pop_restofstack();
        } else {
                tid = next->get_tid();
        }
@@ -231,8 +238,6 @@ ModelAction * ModelChecker::get_next_backtrack()
 
 void ModelChecker::check_current_action(void)
 {
-       Node *currnode;
-
        ModelAction *curr = this->current_action;
        ModelAction *tmp;
        current_action = NULL;
@@ -265,9 +270,10 @@ void ModelChecker::check_current_action(void)
 
        nextThread = get_next_replay_thread();
 
-       currnode = curr->get_node()->get_parent();
+       Node *currnode = curr->get_node();
+       Node *parnode = currnode->get_parent();
 
-       if (!currnode->backtrack_empty())
+       if (!parnode->backtrack_empty()||!currnode->readsfrom_empty())
                if (!next_backtrack || *curr > *next_backtrack)
                        next_backtrack = curr;
 
@@ -281,7 +287,7 @@ void ModelChecker::check_current_action(void)
        Thread *th = get_thread(curr->get_tid());
        uint64_t value = VALUE_NONE;
        if (curr->is_read()) {
-               const ModelAction *reads_from = curr->get_node()->get_next_read_from();
+               const ModelAction *reads_from = curr->get_node()->get_read_from();
                value = reads_from->get_value();
                /* Assign reads_from, perform release/acquire synchronization */
                curr->read_from(reads_from);
@@ -361,7 +367,6 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 {
        std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
        unsigned int i;
-
        ASSERT(curr->is_read());
 
        ModelAction *last_seq_cst = NULL;
@@ -389,8 +394,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                        if (!act->is_write())
                                continue;
 
-                       /* Don't consider more than one seq_cst write */
-                       if (!act->is_seqcst() || act == last_seq_cst) {
+                       /* Don't consider more than one seq_cst write if we are a seq_cst read. */
+                       if (!act->is_seqcst() || !curr->is_seqcst() || act == last_seq_cst) {
                                DEBUG("Adding action to may_read_from:\n");
                                if (DBG_ENABLED()) {
                                        act->print();

diff --git a/nodestack.cc b/nodestack.cc
index 725bc5399f0fb84322b9ad90c161c8a386123fd4..5a65821188fa0698de88a3c03684abea0f12adc8 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -24,7 +24,8 @@ 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)
 {
        if (act)
                act->set_node(this);
@@ -73,7 +74,11 @@ bool Node::has_been_explored(thread_id_t tid)
  */
 bool Node::backtrack_empty()
 {
-       return numBacktracks == 0;
+       return (numBacktracks == 0);
+}
+
+bool Node::readsfrom_empty() {
+       return ((read_from_index+1)>=may_read_from.size());
 }
 
 /**
@@ -138,13 +143,14 @@ 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() {
+       ASSERT(read_from_index<may_read_from.size());
+       return may_read_from[read_from_index];
+}
+
+bool Node::increment_read_from() {
+       read_from_index++;
+       return (read_from_index<may_read_from.size());
 }
 
 void Node::explore(thread_id_t tid)
@@ -215,11 +221,12 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
 }
 
 
-void NodeStack::pop_restofstack()
+void NodeStack::pop_restofstack(int numAhead)
 {
        /* Diverging from previous execution; clear out remainder of list */
        node_list_t::iterator it = iter;
-       it++;
+       while (numAhead--)
+               it++;
        clear_node_list(&node_list, it, node_list.end());
 }
 

diff --git a/nodestack.h b/nodestack.h
index ad63d4dfc999f3ee5beec28c258c9facf5c8d9b0..6f7807f66f97626cb96b816bd9c7c86fd4d07dbe 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -13,7 +13,7 @@
 
 class ModelAction;
 
-typedef std::list< const ModelAction *, MyAlloc< const ModelAction * > > readfrom_set_t;
+typedef std::vector< const ModelAction *, MyAlloc< const ModelAction * > > readfrom_set_t;
 
 /**
  * @brief A single node in a NodeStack
@@ -32,6 +32,7 @@ public:
        bool has_been_explored(thread_id_t tid);
        /* return true = backtrack set is empty */
        bool backtrack_empty();
+       bool readsfrom_empty();
        void explore_child(ModelAction *act);
        /* return false = thread was already in backtrack */
        bool set_backtrack(thread_id_t id);
@@ -44,7 +45,8 @@ public:
        Node * get_parent() const { return parent; }
 
        void add_read_from(const ModelAction *act);
-       const ModelAction * get_next_read_from();
+       const ModelAction * get_read_from();
+       bool increment_read_from();
 
        void print();
        void print_may_read_from();
@@ -63,6 +65,7 @@ private:
        /** The set of ModelActions that this the action at this Node may read
         *  from. Only meaningful if this Node represents a 'read' action. */
        readfrom_set_t may_read_from;
+       unsigned int read_from_index;
 };
 
 typedef std::list< Node *, MyAlloc< Node * > > node_list_t;
@@ -83,7 +86,7 @@ public:
        Node * get_head();
        Node * get_next();
        void reset_execution();
-       void pop_restofstack();
+       void pop_restofstack(int numAhead);
        int get_total_nodes() { return total_nodes; }
 
        void print();