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 d3ebf4d2e3fd99b0628d9577b95ff7e846b4867a..cb53e118b73231b643964edb2fe0a8782da984b7 100644 (file)
--- 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 66869ab12b2f2c0e17ba7b7c740e62391ba0b99a..131b06ca6fe1d190ed56f74577676cc81cc3b069 100644 (file)
--- 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 8a20c45cb2c03e53bdeaf53ee8e80a89b3882014..fc566d6dde8fd65561888899c3505babd79804b0 100644 (file)
--- 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
- * <ol><li>@b applicable: can be satisfied by this Node's ModelAction and</li>
- * <li>@b fulfilled: satisfied by this Node's ModelAction under the current
- * configuration.</li></ol>
- */
-
-#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<struct future_value> > future_values;
-       std::vector< promise_t, ModelAlloc<promise_t> > promises;
        int future_index;
 
+       std::vector< bool, ModelAlloc<bool> > resolve_promise;
+       int resolve_promise_idx;
+
        std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > relseq_break_writes;
        int relseq_break_index;