cyclegraph: simplify resolvePromise / mergeNodes

We only ever will merge a single Promise node with a single ModelAction
node. Any other nodes will just create cycles or unresolveable promises.
So we can simplify much of the logic and avoid passing around a vector
of Promises.

diff --git a/cyclegraph.cc b/cyclegraph.cc
index be7885c5c1d66a71837f16f07433a913b8c209c1..f8cbdda81054a3992aa0f507c1b1bb8499887c5e 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -113,17 +113,22 @@ CycleNode * CycleGraph::getNode(const Promise *promise)
 }
 
 /**
- * @return false if the resolution results in a cycle; true otherwise
+ * Resolve/satisfy a Promise with a particular store ModelAction, taking care
+ * of the CycleGraph cleanups, including merging any necessary CycleNodes.
+ *
+ * @param promise The Promise to resolve
+ * @param writer The store that will resolve this Promise
+ * @return false if the resolution results in a cycle (or fails in some other
+ * way); true otherwise
  */
-bool CycleGraph::resolvePromise(const Promise *promise, ModelAction *writer,
-               promise_list_t *mustResolve)
+bool CycleGraph::resolvePromise(const Promise *promise, ModelAction *writer)
 {
        CycleNode *promise_node = promiseToNode.get(promise);
        CycleNode *w_node = actionToNode.get(writer);
        ASSERT(promise_node);
 
        if (w_node)
-               return mergeNodes(w_node, promise_node, mustResolve);
+               return mergeNodes(w_node, promise_node);
        /* No existing write-node; just convert the promise-node */
        promise_node->resolvePromise(writer);
        erasePromiseNode(promise_node->getPromise());
@@ -139,46 +144,32 @@ bool CycleGraph::resolvePromise(const Promise *promise, ModelAction *writer,
  * @param w_node The write ModelAction node with which to merge
  * @param p_node The Promise node to merge. Will be destroyed after this
  * function.
- * @param mustMerge Return (pass-by-reference) any additional Promises that
- * must also be merged with w_node
  *
- * @return false if the merge results in a cycle; true otherwise
+ * @return false if the merge cannot succeed; true otherwise
  */
-bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node,
-               promise_list_t *mustMerge)
+bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node)
 {
        ASSERT(!w_node->is_promise());
        ASSERT(p_node->is_promise());
 
        const Promise *promise = p_node->getPromise();
        if (!promise->is_compatible(w_node->getAction()) ||
-                       !promise->same_value(w_node->getAction())) {
-               hasCycles = true;
+                       !promise->same_value(w_node->getAction()))
                return false;
-       }
 
        /* Transfer the RMW */
        CycleNode *promise_rmw = p_node->getRMW();
-       if (promise_rmw && promise_rmw != w_node->getRMW() && w_node->setRMW(promise_rmw)) {
-               hasCycles = true;
+       if (promise_rmw && promise_rmw != w_node->getRMW() && w_node->setRMW(promise_rmw))
                return false;
-       }
 
        /* Transfer back edges to w_node */
        while (p_node->getNumBackEdges() > 0) {
                CycleNode *back = p_node->removeBackEdge();
                if (back == w_node)
                        continue;
-               if (back->is_promise()) {
-                       if (checkReachable(w_node, back)) {
-                               /* Edge would create cycle; merge instead */
-                               mustMerge->push_back(back->getPromise());
-                               if (!mergeNodes(w_node, back, mustMerge))
-                                       return false;
-                       } else
-                               back->addEdge(w_node);
-               } else
-                       addNodeEdge(back, w_node);
+               addNodeEdge(back, w_node);
+               if (hasCycles)
+                       return false;
        }
 
        /* Transfer forward edges to w_node */
@@ -186,15 +177,9 @@ bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node,
                CycleNode *forward = p_node->removeEdge();
                if (forward == w_node)
                        continue;
-               if (forward->is_promise()) {
-                       if (checkReachable(forward, w_node)) {
-                               mustMerge->push_back(forward->getPromise());
-                               if (!mergeNodes(w_node, forward, mustMerge))
-                                       return false;
-                       } else
-                               w_node->addEdge(forward);
-               } else
-                       addNodeEdge(w_node, forward);
+               addNodeEdge(w_node, forward);
+               if (hasCycles)
+                       return false;
        }
 
        erasePromiseNode(promise);

diff --git a/cyclegraph.h b/cyclegraph.h
index a2cb93d7ca702217be5af879cbf0c2ba34f9a67e..3f1c9330b4b14631fe70959a0827e70a8d2139bd 100644 (file)
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -53,8 +53,7 @@ class CycleGraph {
        void dot_print_edge(FILE *file, const T *from, const U *to, const char *prop);
 #endif
 
-       bool resolvePromise(const Promise *promise, ModelAction *writer,
-                       promise_list_t *mustResolve);
+       bool resolvePromise(const Promise *promise, ModelAction *writer);
 
        SNAPSHOTALLOC
  private:
@@ -66,8 +65,7 @@ class CycleGraph {
        CycleNode * getNode(const Promise *promise);
        CycleNode * getNode_noCreate(const ModelAction *act) const;
        CycleNode * getNode_noCreate(const Promise *promise) const;
-       bool mergeNodes(CycleNode *node1, CycleNode *node2,
-                       promise_list_t *mustMerge);
+       bool mergeNodes(CycleNode *node1, CycleNode *node2);
 
        HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> *discovered;
 

diff --git a/model.cc b/model.cc
index 63ff36386a1db6425ce124700d6c776349779cc0..e016ae49bc9cb212638cbff3ae59ea22b7faa8f6 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2511,7 +2511,6 @@ int ModelChecker::get_promise_to_resolve(const ModelAction *curr) const
 bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
 {
        std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
-       promise_list_t mustResolve;
        Promise *promise = (*promises)[promise_idx];
 
        for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
@@ -2521,15 +2520,10 @@ bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
        }
        /* Make sure the promise's value matches the write's value */
        ASSERT(promise->is_compatible(write) && promise->same_value(write));
-       mo_graph->resolvePromise(promise, write, &mustResolve);
+       if (!mo_graph->resolvePromise(promise, write))
+               priv->failed_promise = true;
 
        promises->erase(promises->begin() + promise_idx);
-
-       /** @todo simplify the 'mustResolve' stuff */
-       ASSERT(mustResolve.size() <= 1);
-
-       if (!mustResolve.empty() && mustResolve[0] != promise)
-               priv->failed_promise = true;
        delete promise;
 
        //Check whether reading these writes has made threads unable to