From: Brian Norris Date: Sat, 2 Mar 2013 22:17:19 +0000 (-0800) Subject: cyclegraph: simplify resolvePromise / mergeNodes X-Git-Tag: oopsla2013~177 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=438b20cfc07029629c03b4f219c190cbdb5b9d1b 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 be7885c..f8cbdda 100644 --- 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 a2cb93d..3f1c933 100644 --- 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 *discovered; diff --git a/model.cc b/model.cc index 63ff363..e016ae4 100644 --- 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 > 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