X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=cyclegraph.cc;h=2bfe76ac424c274bf8152638543ad7dd6bc1d31f;hb=05f82cd6ab941db2d63ca83e778a430752de1900;hp=f519dac93b39975742887746f79a194e63dd12fe;hpb=a0562e0739fd643fdb2108f784f4722482ea5a4f;p=c11tester.git diff --git a/cyclegraph.cc b/cyclegraph.cc index f519dac9..2bfe76ac 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -5,7 +5,9 @@ /** Initializes a CycleGraph object. */ CycleGraph::CycleGraph() : hasCycles(false), - oldCycles(false) + oldCycles(false), + hasRMWViolation(false), + oldRMWViolation(false) { } @@ -23,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; } @@ -36,6 +41,7 @@ CycleNode * CycleGraph::getNode(const ModelAction *action) { void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) { ASSERT(from); ASSERT(to); + ASSERT(from != to); CycleNode *fromnode=getNode(from); CycleNode *tonode=getNode(to); @@ -45,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); } } @@ -71,30 +83,69 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) { 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::dumpGraphToFile(const char *filename) { + char buffer[200]; + sprintf(buffer, "%s.dot",filename); + FILE *file=fopen(buffer, "w"); + fprintf(file, "digraph %s {\n",filename); + 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()); + } + } + fprintf(file,"}\n"); + fclose(file); +} +#endif + /** * Checks whether one ModelAction can reach another. * @param from The ModelAction from which to begin exploration @@ -118,8 +169,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); @@ -144,6 +195,7 @@ void CycleGraph::startChanges() { ASSERT(rollbackvector.size()==0); ASSERT(rmwrollbackvector.size()==0); ASSERT(oldCycles==hasCycles); + ASSERT(oldRMWViolation==hasRMWViolation); } /** Commit changes to the cyclegraph. */ @@ -151,6 +203,7 @@ void CycleGraph::commitChanges() { rollbackvector.resize(0); rmwrollbackvector.resize(0); oldCycles=hasCycles; + oldRMWViolation=hasRMWViolation; } /** Rollback changes to the previous commit. */ @@ -164,6 +217,7 @@ void CycleGraph::rollbackChanges() { } hasCycles = oldCycles; + hasRMWViolation = oldRMWViolation; rollbackvector.resize(0); rmwrollbackvector.resize(0); } @@ -173,6 +227,10 @@ bool CycleGraph::checkForCycles() { return hasCycles; } +bool CycleGraph::checkForRMWViolation() { + return hasRMWViolation; +} + /** * Constructor for a CycleNode. * @param modelaction The ModelAction for this node @@ -192,8 +250,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