X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=cyclegraph.cc;h=20623347213d0958bfdff79d142595420461b015;hp=7e111b95a3a4bc43334d7037260fdc85ccbfc9c7;hb=7524803854c2de38c0311fe5037e3c17105ccfaa;hpb=e0f80c403452e544452f64687b3c489a869e4f77 diff --git a/cyclegraph.cc b/cyclegraph.cc index 7e111b9..2062334 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -8,6 +8,7 @@ /** Initializes a CycleGraph object. */ CycleGraph::CycleGraph() : discovered(new HashTable(16)), + queue(new model_vector< const CycleNode * >()), 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,45 +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())) { - 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 +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); @@ -212,11 +200,11 @@ bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode) { bool added; - if (!hasCycles) - hasCycles = checkReachable(tonode, fromnode); - - if ((added = fromnode->addEdge(tonode))) + if ((added = fromnode->addEdge(tonode))) { rollbackvector.push_back(fromnode); + if (!hasCycles) + hasCycles = checkReachable(tonode, fromnode); + } /* * If the fromnode has a rmwnode that is not the tonode, we should add @@ -224,10 +212,10 @@ bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode) */ CycleNode *rmwnode = fromnode->getRMW(); if (rmwnode && rmwnode != tonode) { - if (!hasCycles) - hasCycles = checkReachable(tonode, rmwnode); - if (rmwnode->addEdge(tonode)) { + if (!hasCycles) + hasCycles = checkReachable(tonode, rmwnode); + rollbackvector.push_back(rmwnode); added = true; } @@ -400,22 +388,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); } } } @@ -439,26 +425,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; @@ -470,7 +458,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); } } }