From: Brian Norris Date: Wed, 27 Feb 2013 02:42:51 +0000 (-0800) Subject: nodestack: rewrite promise-resolution "counting" X-Git-Tag: oopsla2013~206 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=e356dc963edf27f8a97b1ae3d39e276723aa5968 nodestack: rewrite promise-resolution "counting" We don't need to perform a full check of all possible combinations of Promises to resolve; we only perform 0 or 1 resolution. --- diff --git a/model.cc b/model.cc index d3ebf4d..cb53e11 100644 --- a/model.cc +++ b/model.cc @@ -2500,7 +2500,7 @@ void ModelChecker::compute_promises(ModelAction *curr) !act->could_synchronize_with(curr) && promise->is_compatible(curr) && promise->get_value() == curr->get_value()) { - curr->get_node()->set_promise(i, act->is_rmw()); + curr->get_node()->set_promise(i); } } } diff --git a/nodestack.cc b/nodestack.cc index 66869ab..131b06c 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -40,6 +40,8 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) : read_from_promise_idx(-1), future_values(), future_index(-1), + resolve_promise(), + resolve_promise_idx(-1), relseq_break_writes(), relseq_break_index(0), misc_index(0), @@ -122,61 +124,44 @@ 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, bool is_rmw) -{ - if (i >= promises.size()) - promises.resize(i + 1, PROMISE_IGNORE); - if (promises[i] == PROMISE_IGNORE) { - promises[i] = PROMISE_UNFULFILLED; - if (is_rmw) - promises[i] |= PROMISE_RMW; - } +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 model action. + * @return true if the promise should be satisfied by the given ModelAction. */ bool Node::get_promise(unsigned int i) const { - return (i < promises.size()) && ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED); + return (i < resolve_promise.size()) && (int)i == resolve_promise_idx; } /** - * Increments to the next combination of promises. + * Increments to the next promise to resolve. * @return true if we have a valid combination. */ bool Node::increment_promise() { DBG(); - unsigned int rmw_count = 0; - for (unsigned int i = 0; i < promises.size(); i++) { - if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED)) - rmw_count++; - } - - for (unsigned int i = 0; i < promises.size(); i++) { - if ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED) { - if ((rmw_count > 0) && (promises[i] & PROMISE_RMW)) { - //sending our value to two rmws... not going to work..try next combination - continue; - } - promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_FULFILLED; - while (i > 0) { - i--; - if ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED) - promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_UNFULFILLED; - } + 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; - } else if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED)) { - rmw_count--; - } - } + resolve_promise_idx = prev_idx; return false; } @@ -186,18 +171,21 @@ bool Node::increment_promise() */ bool Node::promise_empty() const { - bool fulfilledrmw = false; - for (int i = promises.size() - 1; i >= 0; i--) { - if (promises[i] == PROMISE_UNFULFILLED) + for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++) + if (i >= 0 && resolve_promise[i]) return false; - if (!fulfilledrmw && ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED)) - return false; - if (promises[i] == (PROMISE_FULFILLED | PROMISE_RMW)) - fulfilledrmw = true; - } 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; @@ -345,7 +333,7 @@ read_from_type_t Node::get_read_from_status() */ bool Node::increment_read_from() { - promises.clear(); + clear_promise_resolutions(); if (increment_read_from_past()) { read_from_status = READ_FROM_PAST; return true; @@ -614,7 +602,6 @@ const ModelAction * Node::get_relseq_break() const bool Node::increment_relseq_break() { DBG(); - promises.clear(); if (relseq_break_index < ((int)relseq_break_writes.size())) { relseq_break_index++; return (relseq_break_index < ((int)relseq_break_writes.size())); diff --git a/nodestack.h b/nodestack.h index 8a20c45..fc566d6 100644 --- a/nodestack.h +++ b/nodestack.h @@ -16,22 +16,6 @@ class ModelAction; class Thread; -/** - * A flag used for the promise counting/combination problem within a node, - * denoting whether a particular Promise is - *
  1. @b applicable: can be satisfied by this Node's ModelAction and
    2. - *
  2. @b fulfilled: satisfied by this Node's ModelAction under the current - * configuration.
- */ - -#define PROMISE_IGNORE 0 /**< This promise is inapplicable; ignore it */ -#define PROMISE_UNFULFILLED 1 /**< This promise is applicable but unfulfilled */ -#define PROMISE_FULFILLED 2 /**< This promise is applicable and fulfilled */ -#define PROMISE_MASK 0xf -#define PROMISE_RMW 0x10 - -typedef int promise_t; - struct fairness_info { unsigned int enabled_count; unsigned int turns; @@ -96,10 +80,12 @@ public: bool add_future_value(struct future_value fv); struct future_value get_future_value() const; - void set_promise(unsigned int i, bool is_rmw); + void set_promise(unsigned int i); bool get_promise(unsigned int i) const; bool increment_promise(); bool promise_empty() const; + void clear_promise_resolutions(); + enabled_type_t *get_enabled_array() {return enabled_array;} void set_misc_max(int i); @@ -146,9 +132,11 @@ private: int read_from_promise_idx; std::vector< struct future_value, ModelAlloc > future_values; - std::vector< promise_t, ModelAlloc > promises; int future_index; + std::vector< bool, ModelAlloc > resolve_promise; + int resolve_promise_idx; + std::vector< const ModelAction *, ModelAlloc > relseq_break_writes; int relseq_break_index;