From: Brian Norris Date: Thu, 28 Mar 2013 22:21:00 +0000 (-0700) Subject: nodestack: regroup some code X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=73ba97016012e678ba1ad7d45970265470501b61 nodestack: regroup some code To put "threads backtracking" code together --- diff --git a/nodestack.cc b/nodestack.cc index b9142435..2fa87841 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -190,87 +190,7 @@ void Node::print() const model_print(" rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty"); } -/*********************************** promise **********************************/ - -/** - * Sets a promise to explore meeting with the given node. - * @param i is the promise index. - */ -void Node::set_promise(unsigned int i) -{ - if (i >= resolve_promise.size()) - resolve_promise.resize(i + 1, false); - resolve_promise[i] = true; -} - -/** - * Looks up whether a given promise should be satisfied by this node. - * @param i The promise index. - * @return true if the promise should be satisfied by the given ModelAction. - */ -bool Node::get_promise(unsigned int i) const -{ - return (i < resolve_promise.size()) && (int)i == resolve_promise_idx; -} - -/** - * Increments to the next promise to resolve. - * @return true if we have a valid combination. - */ -bool Node::increment_promise() -{ - DBG(); - if (resolve_promise.empty()) - return false; - int prev_idx = resolve_promise_idx; - resolve_promise_idx++; - for ( ; resolve_promise_idx < (int)resolve_promise.size(); resolve_promise_idx++) - if (resolve_promise[resolve_promise_idx]) - return true; - resolve_promise_idx = prev_idx; - return false; -} - -/** - * Returns whether the promise set is empty. - * @return true if we have explored all promise combinations. - */ -bool Node::promise_empty() const -{ - for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++) - if (i >= 0 && resolve_promise[i]) - return false; - return true; -} - -/** @brief Clear any promise-resolution information for this Node */ -void Node::clear_promise_resolutions() -{ - resolve_promise.clear(); - resolve_promise_idx = -1; -} - -/******************************* end promise **********************************/ - -void Node::set_misc_max(int i) -{ - misc_max = i; -} - -int Node::get_misc() const -{ - return misc_index; -} - -bool Node::increment_misc() -{ - return (misc_index < misc_max) && ((++misc_index) < misc_max); -} - -bool Node::misc_empty() const -{ - return (misc_index + 1) >= misc_max; -} +/****************************** threads backtracking **************************/ /** * Checks if the Thread associated with this thread ID has been explored from @@ -294,6 +214,17 @@ bool Node::backtrack_empty() const return (numBacktracks == 0); } +void Node::explore(thread_id_t tid) +{ + int i = id_to_int(tid); + ASSERT(i < ((int)backtrack.size())); + if (backtrack[i]) { + backtrack[i] = false; + numBacktracks--; + } + explored_children[i] = true; +} + /** * Mark the appropriate backtracking information for exploring a thread choice. * @param act The ModelAction to explore @@ -354,6 +285,90 @@ void Node::clear_backtracking() numBacktracks = 0; } +/************************** end threads backtracking **************************/ + +/*********************************** promise **********************************/ + +/** + * Sets a promise to explore meeting with the given node. + * @param i is the promise index. + */ +void Node::set_promise(unsigned int i) +{ + if (i >= resolve_promise.size()) + resolve_promise.resize(i + 1, false); + resolve_promise[i] = true; +} + +/** + * Looks up whether a given promise should be satisfied by this node. + * @param i The promise index. + * @return true if the promise should be satisfied by the given ModelAction. + */ +bool Node::get_promise(unsigned int i) const +{ + return (i < resolve_promise.size()) && (int)i == resolve_promise_idx; +} + +/** + * Increments to the next promise to resolve. + * @return true if we have a valid combination. + */ +bool Node::increment_promise() +{ + DBG(); + if (resolve_promise.empty()) + return false; + int prev_idx = resolve_promise_idx; + resolve_promise_idx++; + for ( ; resolve_promise_idx < (int)resolve_promise.size(); resolve_promise_idx++) + if (resolve_promise[resolve_promise_idx]) + return true; + resolve_promise_idx = prev_idx; + return false; +} + +/** + * Returns whether the promise set is empty. + * @return true if we have explored all promise combinations. + */ +bool Node::promise_empty() const +{ + for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++) + if (i >= 0 && resolve_promise[i]) + return false; + return true; +} + +/** @brief Clear any promise-resolution information for this Node */ +void Node::clear_promise_resolutions() +{ + resolve_promise.clear(); + resolve_promise_idx = -1; +} + +/******************************* end promise **********************************/ + +void Node::set_misc_max(int i) +{ + misc_max = i; +} + +int Node::get_misc() const +{ + return misc_index; +} + +bool Node::increment_misc() +{ + return (misc_index < misc_max) && ((++misc_index) < misc_max); +} + +bool Node::misc_empty() const +{ + return (misc_index + 1) >= misc_max; +} + bool Node::is_enabled(Thread *t) const { int thread_id = id_to_int(t->get_id()); @@ -655,6 +670,8 @@ bool Node::increment_future_value() /************************** end future values *********************************/ +/*********************** breaking release sequences ***************************/ + /** * Add a write ModelAction to the set of writes that may break the release * sequence. This is used during replay exploration of pending release @@ -707,16 +724,7 @@ bool Node::relseq_break_empty() const return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size())); } -void Node::explore(thread_id_t tid) -{ - int i = id_to_int(tid); - ASSERT(i < ((int)backtrack.size())); - if (backtrack[i]) { - backtrack[i] = false; - numBacktracks--; - } - explored_children[i] = true; -} +/******************* end breaking release sequences ***************************/ NodeStack::NodeStack() : node_list(),