X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=cyclegraph.cc;h=2bac4de7cf0469c57818ceab835458a872bb7c29;hb=a1b119052d16810d6289855635c2b0e66a6b93b8;hp=c1fea4f3d0a96f14de433b6aac8b61e6f6479131;hpb=f7e1577b22ac26c12dc57a43de2761aa9249227c;p=model-checker.git diff --git a/cyclegraph.cc b/cyclegraph.cc index c1fea4f..2bac4de 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -1,10 +1,26 @@ #include "cyclegraph.h" +#include "action.h" +#include "common.h" -CycleGraph::CycleGraph() { - hasCycles=false; +/** Initializes a CycleGraph object. */ +CycleGraph::CycleGraph() : + hasCycles(false), + oldCycles(false), + hasRMWViolation(false), + oldRMWViolation(false) +{ } -CycleNode * CycleGraph::getNode(ModelAction * action) { +/** CycleGraph destructor */ +CycleGraph::~CycleGraph() { +} + +/** + * @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); @@ -13,28 +29,108 @@ CycleNode * CycleGraph::getNode(ModelAction * action) { return node; } -void CycleGraph::addEdge(ModelAction *from, ModelAction *to) { +/** + * 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); + 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 (rmwnode!=NULL&&rmwnode!=tonode) { + 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 cannot add a cycle because rmw should not have any + incoming edges yet.*/ + std::vector * edges=fromnode->getEdges(); + for(unsigned int i=0;isize();i++) { + CycleNode * tonode=(*edges)[i]; + rollbackvector.push_back(rmwnode); + rmwnode->addEdge(tonode); + } + rollbackvector.push_back(fromnode); + fromnode->addEdge(rmwnode); +} + +/** + * 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; - + std::vector queue; + HashTable discovered; + queue.push_back(from); discovered.put(from, from); while(!queue.empty()) { - class CycleNode * node=queue.back(); + CycleNode * node=queue.back(); queue.pop_back(); if (node==to) return true; - + for(unsigned int i=0;igetEdges()->size();i++) { CycleNode *next=(*node->getEdges())[i]; if (!discovered.contains(next)) { @@ -46,14 +142,83 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) { return false; } -CycleNode::CycleNode(ModelAction *modelaction) { - action=modelaction; +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() { + rollbackvector.resize(0); + rmwrollbackvector.resize(0); + oldCycles=hasCycles; + oldRMWViolation=hasRMWViolation; } -std::vector * CycleNode::getEdges() { +/** 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 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; } -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; +}