X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=cyclegraph.cc;h=ead70ae6b38c2c687ab34c30db9659d57b68e110;hb=7966c737f2a88e5e1a56817eb9f6fdaead3eca92;hp=aa3d24548a554ab039074282f5bab3246e3d3ccd;hpb=e00292b5adf2b85eb1c6e2399159b5c28fde48eb;p=c11tester.git diff --git a/cyclegraph.cc b/cyclegraph.cc index aa3d2454..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), @@ -41,11 +44,14 @@ 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); + if (!hasCycles) { + // Reflexive edges are cycles + hasCycles = (from == to); + } if (!hasCycles) { // Check for Cycles hasCycles=checkReachable(tonode, fromnode); @@ -83,7 +89,6 @@ 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); @@ -112,18 +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::dumpNodes(FILE *file) { - for(unsigned int i=0;i * edges=cn->getEdges(); const ModelAction *action=cn->getAction(); @@ -131,22 +140,22 @@ void CycleGraph::dumpNodes(FILE *file) { 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()); + } } } 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); + sprintf(buffer, "%s.dot",filename); + FILE *file=fopen(buffer, "w"); + fprintf(file, "digraph %s {\n",filename); dumpNodes(file); - fprintf(file,"}\n"); - fclose(file); + fprintf(file,"}\n"); + fclose(file); } #endif @@ -174,10 +183,10 @@ bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to) */ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) { std::vector > queue; - HashTable discovered; + discovered->reset(); queue.push_back(from); - discovered.put(from, from); + discovered->put(from, from); while(!queue.empty()) { CycleNode * node=queue.back(); queue.pop_back(); @@ -186,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); } }