From 87d1cbc6f5149794253614a9f4b435ccd339e04e Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Tue, 17 Jul 2012 16:02:27 -0700 Subject: [PATCH] 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. --- model.cc | 1 + nodestack.cc | 19 +++++++++++++------ nodestack.h | 2 +- 3 files changed, 15 insertions(+), 7 deletions(-) diff --git a/model.cc b/model.cc index 0c5733b..a22e17e 100644 --- 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 aa3a6c9..725bc53 100644 --- 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 11cbdfa..ad63d4d 100644 --- 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(); -- 2.34.1