X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=cyclegraph.cc;h=51066c94601fef25bf99e021a91183b66719ad08;hb=24032577ab44f5adb4f072d022f70d0b0162ab90;hp=ead70ae6b38c2c687ab34c30db9659d57b68e110;hpb=c3ad6c109b0043a010838e77e2573aa820072820;p=model-checker.git diff --git a/cyclegraph.cc b/cyclegraph.cc index ead70ae..51066c9 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -15,7 +15,8 @@ CycleGraph::CycleGraph() : } /** CycleGraph destructor */ -CycleGraph::~CycleGraph() { +CycleGraph::~CycleGraph() +{ } /** @@ -23,10 +24,11 @@ CycleGraph::~CycleGraph() { * @param action The ModelAction to find a node for * @return The CycleNode paired with this action */ -CycleNode * CycleGraph::getNode(const ModelAction *action) { - CycleNode *node=actionToNode.get(action); - if (node==NULL) { - node=new CycleNode(action); +CycleNode * CycleGraph::getNode(const ModelAction *action) +{ + CycleNode *node = actionToNode.get(action); + if (node == NULL) { + node = new CycleNode(action); actionToNode.put(action, node); #if SUPPORT_MOD_ORDER_DUMP nodeList.push_back(node); @@ -41,12 +43,13 @@ CycleNode * CycleGraph::getNode(const ModelAction *action) { * @param to The edge points to this ModelAction * @param from The edge comes from this ModelAction */ -void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) { +void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) +{ ASSERT(from); ASSERT(to); - CycleNode *fromnode=getNode(from); - CycleNode *tonode=getNode(to); + CycleNode *fromnode = getNode(from); + CycleNode *tonode = getNode(to); if (!hasCycles) { // Reflexive edges are cycles @@ -54,26 +57,27 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) { } if (!hasCycles) { // Check for Cycles - hasCycles=checkReachable(tonode, fromnode); + hasCycles = checkReachable(tonode, fromnode); } if (fromnode->addEdge(tonode)) rollbackvector.push_back(fromnode); - CycleNode * rmwnode=fromnode->getRMW(); + 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()) { + /* + * 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()) { if (!hasCycles) { // Check for Cycles - hasCycles=checkReachable(tonode, rmwnode); + hasCycles = checkReachable(tonode, rmwnode); } if (rmwnode->addEdge(tonode)) @@ -86,16 +90,17 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) { * can occur in between the rmw and the from action. Only one RMW * action can read from a given write. */ -void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) { +void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) +{ ASSERT(from); ASSERT(rmw); - CycleNode *fromnode=getNode(from); - CycleNode *rmwnode=getNode(rmw); + CycleNode *fromnode = getNode(from); + CycleNode *rmwnode = getNode(rmw); /* Two RMW actions cannot read from the same write. */ if (fromnode->setRMW(rmwnode)) { - hasRMWViolation=true; + hasRMWViolation = true; } else { rmwrollbackvector.push_back(fromnode); } @@ -107,10 +112,9 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) { * (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]; - if (tonode!=rmwnode) { + for (unsigned int i = 0; i < fromnode->getNumEdges(); i++) { + CycleNode *tonode = fromnode->getEdge(i); + if (tonode != rmwnode) { if (rmwnode->addEdge(tonode)) rollbackvector.push_back(rmwnode); } @@ -124,34 +128,35 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) { if (!hasCycles) { // With promises we could be setting up a cycle here if we aren't // careful...avoid it.. - hasCycles=checkReachable(rmwnode, fromnode); + hasCycles = checkReachable(rmwnode, fromnode); } 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(); +void CycleGraph::dumpNodes(FILE *file) +{ + for (unsigned int i = 0; i < nodeList.size(); i++) { + CycleNode *cn = nodeList[i]; + 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) { + 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(); + for (unsigned int j = 0; j < cn->getNumEdges(); j++) { + CycleNode *dst = cn->getEdge(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) { +void CycleGraph::dumpGraphToFile(const char *filename) +{ char buffer[200]; sprintf(buffer, "%s.dot",filename); - FILE *file=fopen(buffer, "w"); + FILE *file = fopen(buffer, "w"); fprintf(file, "digraph %s {\n",filename); dumpNodes(file); fprintf(file,"}\n"); @@ -165,7 +170,8 @@ void CycleGraph::dumpGraphToFile(const char *filename) { * @param to The ModelAction to reach * @return True, @a from can reach @a to; otherwise, false */ -bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to) { +bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to) +{ CycleNode *fromnode = actionToNode.get(from); CycleNode *tonode = actionToNode.get(to); @@ -181,20 +187,21 @@ bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to) * @param to The CycleNode to reach * @return True, @a from can reach @a to; otherwise, false */ -bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) { +bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) +{ std::vector > queue; discovered->reset(); queue.push_back(from); discovered->put(from, from); - while(!queue.empty()) { - CycleNode * node=queue.back(); + while (!queue.empty()) { + CycleNode *node = queue.back(); queue.pop_back(); - if (node==to) + if (node == to) return true; - for(unsigned int i=0;igetEdges()->size();i++) { - CycleNode *next=(*node->getEdges())[i]; + for (unsigned int i = 0; i < node->getNumEdges(); i++) { + CycleNode *next = node->getEdge(i); if (!discovered->contains(next)) { discovered->put(next,next); queue.push_back(next); @@ -204,24 +211,24 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) { return false; } -bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) { +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(); + 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]; + for (unsigned int i = 0; i < node->getNumEdges(); i++) { + CycleNode *next = node->getEdge(i); if (!discovered->contains(next)) { discovered->put(next,next); queue.push_back(next); @@ -231,19 +238,21 @@ bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) { return false; } -void CycleGraph::startChanges() { - ASSERT(rollbackvector.size()==0); - ASSERT(rmwrollbackvector.size()==0); - ASSERT(oldCycles==hasCycles); - ASSERT(oldRMWViolation==hasRMWViolation); +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() { +void CycleGraph::commitChanges() +{ rollbackvector.resize(0); rmwrollbackvector.resize(0); - oldCycles=hasCycles; - oldRMWViolation=hasRMWViolation; + oldCycles = hasCycles; + oldRMWViolation = hasRMWViolation; } /** Rollback changes to the previous commit. */ @@ -281,25 +290,37 @@ CycleNode::CycleNode(const ModelAction *modelaction) : { } -/** @returns a vector of the edges from a CycleNode. */ -std::vector * CycleNode::getEdges() { - return &edges; +/** + * @param i The index of the edge to return + * @returns The a CycleNode edge indexed by i + */ +CycleNode * CycleNode::getEdge(unsigned int i) const +{ + return edges[i]; +} + +/** @returns The number of edges leaving this CycleNode */ +unsigned int CycleNode::getNumEdges() const +{ + return edges.size(); } /** * Adds an edge from this CycleNode to another CycleNode. * @param node The node to which we add a directed edge */ -bool CycleNode::addEdge(CycleNode *node) { - for(unsigned int i=0;i