CycleNode *fromnode = getNode(from);
CycleNode *tonode = getNode(to);
+ addEdge(fromnode, tonode);
+}
+
+/**
+ * Adds an edge between two CycleNodes.
+ * @param fromnode The edge comes from this CycleNode
+ * @param tonode The edge points to this CycleNode
+ */
+void CycleGraph::addEdge(CycleNode *fromnode, CycleNode *tonode)
+{
if (!hasCycles)
- hasCycles = edgeCreatesCycle(fromnode, tonode);
+ hasCycles = checkReachable(tonode, fromnode);
if (fromnode->addEdge(tonode))
rollbackvector.push_back(fromnode);
-
- CycleNode *rmwnode = fromnode->getRMW();
-
/*
* If the fromnode has a rmwnode that is not the tonode, we should add
* an edge between its rmwnode and the tonode
- *
- * If tonode is also a rmw, don't do this check as the execution is
- * doomed and we'll catch the problem elsewhere, but we want to allow
- * for the possibility of sending to's write value to rmwnode
*/
- if (rmwnode != NULL && !to->is_rmw()) {
+ CycleNode *rmwnode = fromnode->getRMW();
+ if (rmwnode && rmwnode != tonode) {
if (!hasCycles)
- hasCycles = edgeCreatesCycle(rmwnode, tonode);
+ hasCycles = checkReachable(tonode, rmwnode);
if (rmwnode->addEdge(tonode))
rollbackvector.push_back(rmwnode);
}
}
- if (!hasCycles)
- hasCycles = edgeCreatesCycle(fromnode, rmwnode);
-
- if (fromnode->addEdge(rmwnode))
- rollbackvector.push_back(fromnode);
+ addEdge(fromnode, rmwnode);
}
#if SUPPORT_MOD_ORDER_DUMP
}
#endif
-/**
- * Checks whether the addition of an edge between these two nodes would create
- * a cycle in the graph.
- * @param from The CycleNode from which the edge would start
- * @param to The CycleNode to which the edge would point
- * @return True if this edge would create a cycle; false otherwise
- */
-bool CycleGraph::edgeCreatesCycle(const CycleNode *from, const CycleNode *to) const
-{
- return (from == to) || checkReachable(to, from);
-}
-
/**
* Checks whether one ModelAction can reach another.
* @param from The ModelAction from which to begin exploration
CycleNode *node = queue.back();
queue.pop_back();
- if (promise->increment_threads(node->getAction()->get_tid())) {
+ if (promise->eliminate_thread(node->getAction()->get_tid())) {
return true;
}
/**
* Adds an edge from this CycleNode to another CycleNode.
* @param node The node to which we add a directed edge
+ * @return True if this edge is a new edge; false otherwise
*/
bool CycleNode::addEdge(CycleNode *node)
{