X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=cyclegraph.cc;h=ead70ae6b38c2c687ab34c30db9659d57b68e110;hp=ecf8a781c2770ebd09766cff47030e3e094bd2d7;hb=4159ba45e83f6542e3a3320e83bca9fbaf2da3ea;hpb=202074f941d19cef894068e7f79d76b2df598f4b diff --git a/cyclegraph.cc b/cyclegraph.cc index ecf8a781..ead70ae6 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -1,9 +1,12 @@ #include "cyclegraph.h" #include "action.h" #include "common.h" +#include "promise.h" +#include "model.h" /** Initializes a CycleGraph object. */ CycleGraph::CycleGraph() : + discovered(new HashTable(16)), hasCycles(false), oldCycles(false), hasRMWViolation(false), @@ -45,6 +48,10 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) { CycleNode *fromnode=getNode(from); CycleNode *tonode=getNode(to); + if (!hasCycles) { + // Reflexive edges are cycles + hasCycles = (from == to); + } if (!hasCycles) { // Check for Cycles hasCycles=checkReachable(tonode, fromnode); @@ -110,22 +117,22 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) { } + if (!hasCycles) { + // Reflexive edges are cycles + hasCycles = (from == rmw); + } if (!hasCycles) { // With promises we could be setting up a cycle here if we aren't // careful...avoid it.. hasCycles=checkReachable(rmwnode, fromnode); } - if(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(); @@ -133,14 +140,22 @@ void CycleGraph::dumpGraphToFile(const char *filename) { 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]; + 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%u -> N%u;\n", action->get_seq_number(), dstaction->get_seq_number()); + } } - fprintf(file,"}\n"); - fclose(file); +} + +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 @@ -167,11 +182,11 @@ 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; + discovered->reset(); queue.push_back(from); - discovered.put(from, from); + discovered->put(from, from); while(!queue.empty()) { CycleNode * node=queue.back(); queue.pop_back(); @@ -180,8 +195,35 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) { for(unsigned int i=0;igetEdges()->size();i++) { CycleNode *next=(*node->getEdges())[i]; - if (!discovered.contains(next)) { - discovered.put(next,next); + if (!discovered->contains(next)) { + discovered->put(next,next); + queue.push_back(next); + } + } + } + return false; +} + +bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) { + std::vector > queue; + discovered->reset(); + CycleNode *from = actionToNode.get(fromact); + + + queue.push_back(from); + discovered->put(from, from); + while(!queue.empty()) { + CycleNode * node=queue.back(); + queue.pop_back(); + + if (promise->increment_threads(node->getAction()->get_tid())) { + return true; + } + + for(unsigned int i=0;igetEdges()->size();i++) { + CycleNode *next=(*node->getEdges())[i]; + if (!discovered->contains(next)) { + discovered->put(next,next); queue.push_back(next); } }