projects
/
c11tester.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
[c11tester.git]
/
cyclegraph.cc
diff --git
a/cyclegraph.cc
b/cyclegraph.cc
index 8d37dea8b9fc6ea6770528e57238df13d2b5a323..26ea215d434921f2b27fd69e07ef18d1e6029f54 100644
(file)
--- a/
cyclegraph.cc
+++ b/
cyclegraph.cc
@@
-198,29
+198,33
@@
bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node)
*/
bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode)
{
*/
bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode)
{
- bool added;
-
- if ((added = fromnode->addEdge(tonode))) {
+ if (fromnode->addEdge(tonode)) {
rollbackvector.push_back(fromnode);
if (!hasCycles)
hasCycles = checkReachable(tonode, fromnode);
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();
*/
CycleNode *rmwnode = fromnode->getRMW();
- if (rmwnode && rmwnode != tonode) {
- if (rmwnode->addEdge(tonode)) {
- if (!hasCycles)
- hasCycles = checkReachable(tonode, rmwnode);
+ if (rmwnode) {
+ while (rmwnode != tonode && rmwnode->getRMW())
+ rmwnode = rmwnode->getRMW();
- rollbackvector.push_back(rmwnode);
- added = true;
+ if (rmwnode != tonode) {
+ if (rmwnode->addEdge(tonode)) {
+ if (!hasCycles)
+ hasCycles = checkReachable(tonode, rmwnode);
+
+ rollbackvector.push_back(rmwnode);
+ }
}
}
}
}
- return
added
;
+ return
true
;
}
/**
}
/**
@@
-244,6
+248,9
@@
void CycleGraph::addRMWEdge(const T *from, const ModelAction *rmw)
CycleNode *fromnode = getNode(from);
CycleNode *rmwnode = getNode(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;
/* Two RMW actions cannot read from the same write. */
if (fromnode->setRMW(rmwnode))
hasCycles = true;