X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=cyclegraph.cc;h=26235d651e10ecb5e2178d281048ea6ce5007893;hb=57d7975634e97da2d32f95054dccf40ca871e558;hp=750086c5c1c37fa63ab18072a5a2a7d94b504879;hpb=9209688c955f7924af15da0c79c70948eb481b8c;p=model-checker.git diff --git a/cyclegraph.cc b/cyclegraph.cc index 750086c..26235d6 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -1,15 +1,26 @@ #include "cyclegraph.h" #include "action.h" +#include "common.h" /** Initializes a CycleGraph object. */ - -CycleGraph::CycleGraph() { - hasCycles=false; +CycleGraph::CycleGraph() : + hasCycles(false), + oldCycles(false), + hasRMWViolation(false), + oldRMWViolation(false) +{ } -/** Returns the CycleNode for a given ModelAction. */ +/** CycleGraph destructor */ +CycleGraph::~CycleGraph() { +} -CycleNode * CycleGraph::getNode(ModelAction * action) { +/** + * @brief Returns the CycleNode corresponding to a given ModelAction + * @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); @@ -18,20 +29,112 @@ CycleNode * CycleGraph::getNode(ModelAction * action) { return node; } -/** Adds an edge between two ModelActions. */ +/** + * Adds an edge between two ModelActions. The ModelAction @a to is ordered + * after the ModelAction @a from. + * @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) { + ASSERT(from); + ASSERT(to); -void CycleGraph::addEdge(ModelAction *from, ModelAction *to) { CycleNode *fromnode=getNode(from); CycleNode *tonode=getNode(to); + if (!hasCycles) { // Check for Cycles - hasCycles=checkReachable(fromnode, tonode); + hasCycles=checkReachable(tonode, fromnode); } + + rollbackvector.push_back(fromnode); fromnode->addEdge(tonode); + + 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 (!hasCycles) { + // Check for Cycles + hasCycles=checkReachable(tonode, rmwnode); + } + rollbackvector.push_back(rmwnode); + rmwnode->addEdge(tonode); + } +} + +/** Handles special case of a RMW action. The ModelAction rmw reads + * from the ModelAction from. The key differences are: (1) no write + * 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) { + ASSERT(from); + ASSERT(rmw); + + CycleNode *fromnode=getNode(from); + CycleNode *rmwnode=getNode(rmw); + + /* Two RMW actions cannot read from the same write. */ + if (fromnode->setRMW(rmwnode)) { + hasRMWViolation=true; + } else { + rmwrollbackvector.push_back(fromnode); + } + + /* Transfer all outgoing edges from the from node to the rmw node */ + /* 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]; + if (tonode!=rmwnode) { + rollbackvector.push_back(rmwnode); + rmwnode->addEdge(tonode); + } + } + rollbackvector.push_back(fromnode); + + if (!hasCycles) { + // With promises we could be setting up a cycle here if we aren't + // careful...avoid it.. + hasCycles=checkReachable(rmwnode, fromnode); + } + fromnode->addEdge(rmwnode); } -/** Checks whether the first CycleNode can reach the second one. */ +/** + * Checks whether one ModelAction can reach another. + * @param from The ModelAction from which to begin exploration + * @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) { + CycleNode *fromnode = actionToNode.get(from); + CycleNode *tonode = actionToNode.get(to); + if (!fromnode || !tonode) + return false; + + return checkReachable(fromnode, tonode); +} + +/** + * Checks whether one CycleNode can reach another. + * @param from The CycleNode from which to begin exploration + * @param to The CycleNode to reach + * @return True, @a from can reach @a to; otherwise, false + */ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) { std::vector queue; HashTable discovered; @@ -55,25 +158,83 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) { return false; } -/** Returns whether a CycleGraph contains cycles. */ -bool checkForCycles() { - return hasCycles; +void CycleGraph::startChanges() { + ASSERT(rollbackvector.size()==0); + ASSERT(rmwrollbackvector.size()==0); + ASSERT(oldCycles==hasCycles); + ASSERT(oldRMWViolation==hasRMWViolation); } -/** Constructor for a CycleNode. */ +/** Commit changes to the cyclegraph. */ +void CycleGraph::commitChanges() { + rollbackvector.resize(0); + rmwrollbackvector.resize(0); + oldCycles=hasCycles; + oldRMWViolation=hasRMWViolation; +} -CycleNode::CycleNode(ModelAction *modelaction) { - action=modelaction; +/** Rollback changes to the previous commit. */ +void CycleGraph::rollbackChanges() { + for (unsigned int i = 0; i < rollbackvector.size(); i++) { + rollbackvector[i]->popEdge(); + } + + for (unsigned int i = 0; i < rmwrollbackvector.size(); i++) { + rmwrollbackvector[i]->clearRMW(); + } + + hasCycles = oldCycles; + hasRMWViolation = oldRMWViolation; + rollbackvector.resize(0); + rmwrollbackvector.resize(0); } -/** Returns a vector of the edges from a CycleNode. */ +/** @returns whether a CycleGraph contains cycles. */ +bool CycleGraph::checkForCycles() { + return hasCycles; +} +bool CycleGraph::checkForRMWViolation() { + return hasRMWViolation; +} + +/** + * Constructor for a CycleNode. + * @param modelaction The ModelAction for this node + */ +CycleNode::CycleNode(const ModelAction *modelaction) : + action(modelaction), + hasRMW(NULL) +{ +} + +/** @returns a vector of the edges from a CycleNode. */ std::vector * CycleNode::getEdges() { return &edges; } -/** Adds an edge to a CycleNode. */ - -void CycleNode::addEdge(CycleNode * node) { +/** + * 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) { edges.push_back(node); } + +/** @returns the RMW CycleNode that reads from the current CycleNode */ +CycleNode * CycleNode::getRMW() { + return hasRMW; +} + +/** + * Set a RMW action node that reads from the current CycleNode. + * @param node The RMW that reads from the current node + * @return True, if this node already was read by another RMW; false otherwise + * @see CycleGraph::addRMWEdge + */ +bool CycleNode::setRMW(CycleNode *node) { + if (hasRMW!=NULL) + return true; + hasRMW=node; + return false; +}