From 8d8db345ee33c276ea7f6ee880035182448e7326 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 19 Jun 2012 16:33:52 -0700 Subject: [PATCH] nodestack: don't perform linear search to check if backtrack is empty Add a simple add/remove counter to record when threads are 'added' and 'removed' from the backtracking set. --- nodestack.cc | 16 +++++++++------- nodestack.h | 1 + 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/nodestack.cc b/nodestack.cc index c9878a3..65afd7c 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -8,7 +8,8 @@ Node::Node(ModelAction *act, int nthreads) : action(act), num_threads(nthreads), explored_children(num_threads), - backtrack(num_threads) + backtrack(num_threads), + numBacktracks(0) { } @@ -47,11 +48,7 @@ bool Node::has_been_explored(thread_id_t tid) */ bool Node::backtrack_empty() { - unsigned int i; - for (i = 0; i < backtrack.size(); i++) - if (backtrack[i] == true) - return false; - return true; + return numBacktracks == 0; } /** @@ -79,6 +76,7 @@ bool Node::set_backtrack(thread_id_t id) if (backtrack[i]) return false; backtrack[i] = true; + numBacktracks++; return true; } @@ -92,6 +90,7 @@ thread_id_t Node::get_next_backtrack() if (i >= backtrack.size()) return THREAD_ID_T_NONE; backtrack[i] = false; + numBacktracks--; return int_to_id(i); } @@ -103,7 +102,10 @@ bool Node::is_enabled(Thread *t) void Node::explore(thread_id_t tid) { int i = id_to_int(tid); - backtrack[i] = false; + if (backtrack[i]) { + backtrack[i] = false; + numBacktracks--; + } explored_children[i] = true; } diff --git a/nodestack.h b/nodestack.h index d3eab13..a73ce44 100644 --- a/nodestack.h +++ b/nodestack.h @@ -38,6 +38,7 @@ private: int num_threads; std::vector< bool, MyAlloc > explored_children; std::vector< bool, MyAlloc > backtrack; + int numBacktracks; }; typedef std::list > node_list_t; -- 2.34.1