Make stack popping explicit.

The current check will break in subtle ways as soon as we start to
add reads_from support as the thread selection is no longer the
only backtracking choice.

diff --git a/model.cc b/model.cc
index 0c5733b543cf84899a582cdabfd6eecb1fba8b90..a22e17e1f46fd20c780136f6f232399170111356 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -132,6 +132,7 @@ thread_id_t ModelChecker::get_next_replay_thread()
                DEBUG("*** Divergence point ***\n");
                tid = node->get_next_backtrack();
                diverge = NULL;
+               node_stack->pop_restofstack();
        } else {
                tid = next->get_tid();
        }

diff --git a/nodestack.cc b/nodestack.cc
index aa3a6c97d4520f1f9faee2ae7592dbaf218da490..725bc5399f0fb84322b9ad90c161c8a386123fd4 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -198,17 +198,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()));
@@ -217,6 +214,16 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
        return NULL;
 }
 
+
+void NodeStack::pop_restofstack()
+{
+       /* 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());
+}
+
+
 Node * NodeStack::get_head()
 {
        if (node_list.empty())

diff --git a/nodestack.h b/nodestack.h
index 11cbdfa801d772d70e210668db374fd71f718b71..ad63d4dfc999f3ee5beec28c258c9facf5c8d9b0 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -83,7 +83,7 @@ public:
        Node * get_head();
        Node * get_next();
        void reset_execution();
-
+       void pop_restofstack();
        int get_total_nodes() { return total_nodes; }
 
        void print();