From: Brian Demsky <bdemsky@uci.edu>
Date: Sun, 9 Sep 2012 02:37:11 +0000 (-0700)
Subject: cyclegraph: support rolling back changes
X-Git-Tag: pldi2013~223^2~6
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=8574719911b1f66fbcbaedef47eebb84b860d526;hp=307520433027a3e7440d1b3e34c52e1adbf2b05a

cyclegraph: support rolling back changes
---

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 3168923..967b076 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -3,7 +3,8 @@
 
 /** Initializes a CycleGraph object. */
 CycleGraph::CycleGraph() :
-	hasCycles(false)
+	hasCycles(false),
+	oldCycles(false)
 {
 }
 
@@ -39,6 +40,8 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
 		// Check for Cycles
 		hasCycles=checkReachable(tonode, fromnode);
 	}
+
+	rollbackvector.push_back(fromnode);
 	fromnode->addEdge(tonode);
 
 	CycleNode * rmwnode=fromnode->getRMW();
@@ -51,6 +54,7 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
 			// Check for Cycles
 			hasCycles=checkReachable(tonode, rmwnode);
 		}
+		rollbackvector.push_back(rmwnode);
 		rmwnode->addEdge(tonode);
 	}
 }
@@ -67,6 +71,8 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
 	/* Two RMW actions cannot read from the same write. */
 	if (fromnode->setRMW(rmwnode)) {
 		hasCycles=true;
+	} else {
+		rmwrollbackvector.push_back(fromnode);
 	}
 
 	/* Transfer all outgoing edges from the from node to the rmw node */
@@ -75,9 +81,10 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
 	std::vector<CycleNode *> * edges=fromnode->getEdges();
 	for(unsigned int i=0;i<edges->size();i++) {
 		CycleNode * tonode=(*edges)[i];
+		rollbackvector.push_back(rmwnode);
 		rmwnode->addEdge(tonode);
 	}
-
+	rollbackvector.push_back(fromnode);
 	fromnode->addEdge(rmwnode);
 }
 
@@ -126,6 +133,28 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
 	return false;
 }
 
+/** Commit changes to the cyclegraph. */
+void CycleGraph::commitChanges() {
+	rollbackvector.resize(0);
+	rmwrollbackvector.resize(0);
+	oldCycles=hasCycles;
+}
+
+/** 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;
+	rollbackvector.resize(0);
+	rmwrollbackvector.resize(0);
+}
+
 /** @returns whether a CycleGraph contains cycles. */
 bool CycleGraph::checkForCycles() {
 	return hasCycles;
@@ -166,7 +195,8 @@ CycleNode * CycleNode::getRMW() {
  * @see CycleGraph::addRMWEdge
  */
 bool CycleNode::setRMW(CycleNode *node) {
-	CycleNode * oldhasRMW=hasRMW;
+	if (hasRMW!=NULL)
+		return true;
 	hasRMW=node;
-	return (oldhasRMW!=NULL);
+	return false;
 }
diff --git a/cyclegraph.h b/cyclegraph.h
index 2e523d7..0bb01c4 100644
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -22,6 +22,8 @@ class CycleGraph {
 	void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
 
 	bool checkReachable(const ModelAction *from, const ModelAction *to);
+	void commitChanges();
+	void rollbackChanges();
 
  private:
 	CycleNode * getNode(const ModelAction *);
@@ -33,6 +35,11 @@ class CycleGraph {
 
 	/** @brief A flag: true if this graph contains cycles */
 	bool hasCycles;
+
+	bool oldCycles;
+
+	std::vector<CycleNode *> rollbackvector;
+	std::vector<CycleNode *> rmwrollbackvector;
 };
 
 /** @brief A node within a CycleGraph; corresponds to one ModelAction */
@@ -43,6 +50,12 @@ class CycleNode {
 	std::vector<CycleNode *> * getEdges();
 	bool setRMW(CycleNode *);
 	CycleNode* getRMW();
+	void popEdge() {
+		edges.pop_back();
+	};
+	void clearRMW() {
+		hasRMW=NULL;
+	}
 
  private:
 	/** @brief The ModelAction that this node represents */