X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=cyclegraph.cc;h=321ebe9e2f242babe1adad4e233dd7fe51427e71;hb=f94de5b6daa067501562ed3047bfb6b4939f9435;hp=967b0763abbdcdba0ec35cdd2608cb0fa94caa13;hpb=8574719911b1f66fbcbaedef47eebb84b860d526;p=c11tester.git diff --git a/cyclegraph.cc b/cyclegraph.cc index 967b0763..321ebe9e 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -1,10 +1,13 @@ #include "cyclegraph.h" #include "action.h" +#include "common.h" /** Initializes a CycleGraph object. */ CycleGraph::CycleGraph() : hasCycles(false), - oldCycles(false) + oldCycles(false), + hasRMWViolation(false), + oldRMWViolation(false) { } @@ -22,6 +25,9 @@ CycleNode * CycleGraph::getNode(const ModelAction *action) { if (node==NULL) { node=new CycleNode(action); actionToNode.put(action, node); +#if SUPPORT_MOD_ORDER_DUMP + nodeList.push_back(node); +#endif } return node; } @@ -33,6 +39,10 @@ CycleNode * CycleGraph::getNode(const ModelAction *action) { * @param from The edge comes from this ModelAction */ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) { + ASSERT(from); + ASSERT(to); + ASSERT(from != to); + CycleNode *fromnode=getNode(from); CycleNode *tonode=getNode(to); @@ -41,21 +51,27 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) { hasCycles=checkReachable(tonode, fromnode); } - rollbackvector.push_back(fromnode); - fromnode->addEdge(tonode); + 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 (rmwnode!=NULL&&rmwnode!=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()) { if (!hasCycles) { // Check for Cycles hasCycles=checkReachable(tonode, rmwnode); } - rollbackvector.push_back(rmwnode); - rmwnode->addEdge(tonode); + + if (rmwnode->addEdge(tonode)) + rollbackvector.push_back(rmwnode); } } @@ -65,29 +81,75 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) { * action can read from a given write. */ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) { + ASSERT(from); + ASSERT(rmw); + ASSERT(from != rmw); + CycleNode *fromnode=getNode(from); CycleNode *rmwnode=getNode(rmw); /* Two RMW actions cannot read from the same write. */ if (fromnode->setRMW(rmwnode)) { - hasCycles=true; + hasRMWViolation=true; } else { rmwrollbackvector.push_back(fromnode); } /* Transfer all outgoing edges from the from node to the rmw node */ - /* This process cannot add a cycle because rmw should not have any - incoming edges yet.*/ + /* This process should not add a cycle because either: + * (1) The rmw should not have any incoming edges yet if it is the + * new node or + * (2) the fromnode is the new node and therefore it should not + * have any outgoing edges. + */ std::vector * edges=fromnode->getEdges(); for(unsigned int i=0;isize();i++) { CycleNode * tonode=(*edges)[i]; - rollbackvector.push_back(rmwnode); - rmwnode->addEdge(tonode); + if (tonode!=rmwnode) { + if (rmwnode->addEdge(tonode)) + rollbackvector.push_back(rmwnode); + } + } + + + if (!hasCycles) { + // With promises we could be setting up a cycle here if we aren't + // careful...avoid it.. + hasCycles=checkReachable(rmwnode, fromnode); } - rollbackvector.push_back(fromnode); - fromnode->addEdge(rmwnode); + if(fromnode->addEdge(rmwnode)) + rollbackvector.push_back(fromnode); } +#if SUPPORT_MOD_ORDER_DUMP +void CycleGraph::dumpNodes(FILE *file) { + for(unsigned int i=0;i * edges=cn->getEdges(); + const ModelAction *action=cn->getAction(); + fprintf(file, "N%u [label=\"%u, T%u\"];\n",action->get_seq_number(),action->get_seq_number(), action->get_tid()); + if (cn->getRMW()!=NULL) { + fprintf(file, "N%u -> N%u[style=dotted];\n", action->get_seq_number(), cn->getRMW()->getAction()->get_seq_number()); + } + for(unsigned int j=0;jsize();j++) { + CycleNode *dst=(*edges)[j]; + const ModelAction *dstaction=dst->getAction(); + fprintf(file, "N%u -> N%u;\n", action->get_seq_number(), dstaction->get_seq_number()); + } + } +} + +void CycleGraph::dumpGraphToFile(const char *filename) { + char buffer[200]; + sprintf(buffer, "%s.dot",filename); + FILE *file=fopen(buffer, "w"); + fprintf(file, "digraph %s {\n",filename); + dumpNodes(file); + fprintf(file,"}\n"); + fclose(file); +} +#endif + /** * Checks whether one ModelAction can reach another. * @param from The ModelAction from which to begin exploration @@ -111,8 +173,8 @@ bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to) * @return True, @a from can reach @a to; otherwise, false */ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) { - std::vector queue; - HashTable discovered; + std::vector > queue; + HashTable discovered; queue.push_back(from); discovered.put(from, from); @@ -133,11 +195,19 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) { return false; } +void CycleGraph::startChanges() { + ASSERT(rollbackvector.size()==0); + ASSERT(rmwrollbackvector.size()==0); + ASSERT(oldCycles==hasCycles); + ASSERT(oldRMWViolation==hasRMWViolation); +} + /** Commit changes to the cyclegraph. */ void CycleGraph::commitChanges() { rollbackvector.resize(0); rmwrollbackvector.resize(0); oldCycles=hasCycles; + oldRMWViolation=hasRMWViolation; } /** Rollback changes to the previous commit. */ @@ -151,6 +221,7 @@ void CycleGraph::rollbackChanges() { } hasCycles = oldCycles; + hasRMWViolation = oldRMWViolation; rollbackvector.resize(0); rmwrollbackvector.resize(0); } @@ -160,6 +231,10 @@ bool CycleGraph::checkForCycles() { return hasCycles; } +bool CycleGraph::checkForRMWViolation() { + return hasRMWViolation; +} + /** * Constructor for a CycleNode. * @param modelaction The ModelAction for this node @@ -179,8 +254,12 @@ std::vector * CycleNode::getEdges() { * Adds an edge from this CycleNode to another CycleNode. * @param node The node to which we add a directed edge */ -void CycleNode::addEdge(CycleNode *node) { +bool CycleNode::addEdge(CycleNode *node) { + for(unsigned int i=0;i