X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=cyclegraph.cc;h=26ea215d434921f2b27fd69e07ef18d1e6029f54;hp=be7885c5c1d66a71837f16f07433a913b8c209c1;hb=d62cd6e5bbba2975923540d99bae0587fe03b791;hpb=875ebf8e11b4bdd702604785837b6b91b748900d diff --git a/cyclegraph.cc b/cyclegraph.cc index be7885c..26ea215 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -8,6 +8,7 @@ /** Initializes a CycleGraph object. */ CycleGraph::CycleGraph() : discovered(new HashTable(16)), + queue(new ModelVector()), hasCycles(false), oldCycles(false) { @@ -16,6 +17,7 @@ CycleGraph::CycleGraph() : /** CycleGraph destructor */ CycleGraph::~CycleGraph() { + delete queue; delete discovered; } @@ -113,17 +115,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 +146,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 +179,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); @@ -211,29 +198,33 @@ bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node, */ bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode) { - bool added; - - if (!hasCycles) - hasCycles = checkReachable(tonode, fromnode); - - if ((added = fromnode->addEdge(tonode))) + if (fromnode->addEdge(tonode)) { rollbackvector.push_back(fromnode); + if (!hasCycles) + hasCycles = checkReachable(tonode, fromnode); + } else + return false; /* No new edge */ /* - * If the fromnode has a rmwnode that is not the tonode, we should add - * an edge between its rmwnode and the tonode + * If the fromnode has a rmwnode that is not the tonode, we should + * follow its RMW chain to add an edge at the end, unless we encounter + * tonode along the way */ CycleNode *rmwnode = fromnode->getRMW(); - if (rmwnode && rmwnode != tonode) { - if (!hasCycles) - hasCycles = checkReachable(tonode, rmwnode); + if (rmwnode) { + while (rmwnode != tonode && rmwnode->getRMW()) + rmwnode = rmwnode->getRMW(); + + if (rmwnode != tonode) { + if (rmwnode->addEdge(tonode)) { + if (!hasCycles) + hasCycles = checkReachable(tonode, rmwnode); - if (rmwnode->addEdge(tonode)) { - rollbackvector.push_back(rmwnode); - added = true; + rollbackvector.push_back(rmwnode); + } } } - return added; + return true; } /** @@ -257,6 +248,9 @@ void CycleGraph::addRMWEdge(const T *from, const ModelAction *rmw) CycleNode *fromnode = getNode(from); CycleNode *rmwnode = getNode(rmw); + /* We assume that this RMW has no RMW reading from it yet */ + ASSERT(!rmwnode->getRMW()); + /* Two RMW actions cannot read from the same write. */ if (fromnode->setRMW(rmwnode)) hasCycles = true; @@ -401,22 +395,20 @@ void CycleGraph::dumpGraphToFile(const char *filename) const */ bool CycleGraph::checkReachable(const CycleNode *from, const CycleNode *to) const { - std::vector< const CycleNode *, ModelAlloc > queue; discovered->reset(); - - queue.push_back(from); + queue->clear(); + queue->push_back(from); discovered->put(from, from); - while (!queue.empty()) { - const CycleNode *node = queue.back(); - queue.pop_back(); + while (!queue->empty()) { + const CycleNode *node = queue->back(); + queue->pop_back(); if (node == to) return true; - for (unsigned int i = 0; i < node->getNumEdges(); i++) { CycleNode *next = node->getEdge(i); if (!discovered->contains(next)) { discovered->put(next, next); - queue.push_back(next); + queue->push_back(next); } } } @@ -440,26 +432,28 @@ bool CycleGraph::checkReachable(const T *from, const U *to) const return checkReachable(fromnode, tonode); } -/* Instantiate three forms of CycleGraph::checkReachable */ +/* Instantiate four forms of CycleGraph::checkReachable */ template bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to) const; template bool CycleGraph::checkReachable(const ModelAction *from, const Promise *to) const; template bool CycleGraph::checkReachable(const Promise *from, const ModelAction *to) const; +template bool CycleGraph::checkReachable(const Promise *from, + const Promise *to) const; /** @return True, if the promise has failed; false otherwise */ bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) const { - std::vector< CycleNode *, ModelAlloc > queue; discovered->reset(); + queue->clear(); CycleNode *from = actionToNode.get(fromact); - queue.push_back(from); + queue->push_back(from); discovered->put(from, from); - while (!queue.empty()) { - CycleNode *node = queue.back(); - queue.pop_back(); + while (!queue->empty()) { + const CycleNode *node = queue->back(); + queue->pop_back(); if (node->getPromise() == promise) return true; @@ -471,7 +465,7 @@ bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) cons CycleNode *next = node->getEdge(i); if (!discovered->contains(next)) { discovered->put(next, next); - queue.push_back(next); + queue->push_back(next); } } } @@ -567,7 +561,7 @@ unsigned int CycleNode::getNumBackEdges() const * @return True if the element was found; false otherwise */ template -static bool vector_remove_node(std::vector >& v, const T n) +static bool vector_remove_node(SnapVector& v, const T n) { for (unsigned int i = 0; i < v.size(); i++) { if (v[i] == n) {