mutex: fix indentation

[model-checker.git] / cyclegraph.cc

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 49ff00249fe9c49dbe9a1cda9fdad32af78c0f70..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,45 +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())) {
-               hasCycles = true;
+       if (!promise->is_compatible(w_node->getAction()) ||
+                       !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 */
@@ -185,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);
@@ -320,7 +306,7 @@ static void print_node(FILE *file, const CycleNode *node, int label)
        if (node->is_promise()) {
                const Promise *promise = node->getPromise();
                int idx = model->get_promise_number(promise);
-               fprintf(file, "P%d", idx);
+               fprintf(file, "P%u", idx);
                if (label) {
                        int first = 1;
                        fprintf(file, " [label=\"P%d, T", idx);
@@ -350,6 +336,23 @@ static void print_edge(FILE *file, const CycleNode *from, const CycleNode *to, c
        fprintf(file, ";\n");
 }
 
+void CycleGraph::dot_print_node(FILE *file, const ModelAction *act)
+{
+       print_node(file, getNode(act), 1);
+}
+
+template <typename T, typename U>
+void CycleGraph::dot_print_edge(FILE *file, const T *from, const U *to, const char *prop)
+{
+       CycleNode *fromnode = getNode(from);
+       CycleNode *tonode = getNode(to);
+
+       print_edge(file, fromnode, tonode, prop);
+}
+/* Instantiate two forms of CycleGraph::dot_print_edge */
+template void CycleGraph::dot_print_edge(FILE *file, const Promise *from, const ModelAction *to, const char *prop);
+template void CycleGraph::dot_print_edge(FILE *file, const ModelAction *from, const ModelAction *to, const char *prop);
+
 void CycleGraph::dumpNodes(FILE *file) const
 {
        for (unsigned int i = 0; i < nodeList.size(); i++) {