From: Brian Demsky <bdemsky@uci.edu>
Date: Thu, 19 Jul 2012 21:15:27 +0000 (-0700)
Subject: Add RMW support to core.
X-Git-Tag: pldi2013~332
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=37c87f91496ff3e713003c21692c63b8e87d81fb

Add RMW support to core.

Eliminate annoying warning.
---

diff --git a/cyclegraph.cc b/cyclegraph.cc
index c526af0..6676f2f 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -30,6 +30,29 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
 	fromnode->addEdge(tonode);
 }
 
+void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
+	CycleNode *fromnode=getNode(from);
+	CycleNode *rmwnode=getNode(rmw);
+
+	/* Two RMW actions cannot read from the same write. */
+	if (fromnode->setRMW())
+		hasCycles=true;
+
+	/* 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<CycleNode *> * edges=fromnode->getEdges();
+	for(unsigned int i=0;edges->size();i++) {
+		CycleNode * tonode=(*edges)[i];
+		rmwnode->addEdge(tonode);
+	}
+	if (!hasCycles) {
+		hasCycles=checkReachable(rmwnode, fromnode);
+	}
+	fromnode->addEdge(rmwnode);
+}
+
+
 /** Checks whether the first CycleNode can reach the second one. */
 bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
 	std::vector<CycleNode *> queue;
@@ -73,3 +96,9 @@ std::vector<CycleNode *> * CycleNode::getEdges() {
 void CycleNode::addEdge(CycleNode * node) {
 	edges.push_back(node);
 }
+
+bool CycleNode::setRMW() {
+	bool oldhasRMW=hasRMW;
+	hasRMW=true;
+	return oldhasRMW;
+}
diff --git a/cyclegraph.h b/cyclegraph.h
index a98e68c..6901700 100644
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -15,6 +15,7 @@ class CycleGraph {
 	~CycleGraph();
 	void addEdge(const ModelAction *from, const ModelAction *to);
 	bool checkForCycles();
+	void addRMWEdge(const ModelAction *from, const ModelAction *to);
 
  private:
 	CycleNode * getNode(const ModelAction *);
@@ -28,10 +29,12 @@ class CycleNode {
 	CycleNode(const ModelAction *action);
 	void addEdge(CycleNode * node);
 	std::vector<CycleNode *> * getEdges();
+	bool setRMW();
 
  private:
 	const ModelAction *action;
 	std::vector<CycleNode *> edges;
+	bool hasRMW;
 };
 
 #endif
diff --git a/model.cc b/model.cc
index 3262f5e..9fc15cd 100644
--- a/model.cc
+++ b/model.cc
@@ -332,10 +332,9 @@ bool ModelChecker::isfeasible() {
 /** Process a RMW by converting previous read into a RMW. */
 void ModelChecker::process_rmw(ModelAction * act) {
 	int tid = id_to_int(act->get_tid());
-	std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
-	ASSERT(tid < (int) vec->size());
-	ModelAction *lastread=(*vec)[tid].back();
+	ModelAction *lastread=get_last_action(tid);
 	lastread->upgrade_rmw(act);
+	cyclegraph->addRMWEdge(lastread->get_reads_from(),lastread);
 }
 
 /**
diff --git a/snapshot-interface.cc b/snapshot-interface.cc
index 84749f1..84d9dbc 100644
--- a/snapshot-interface.cc
+++ b/snapshot-interface.cc
@@ -57,7 +57,7 @@ static void SnapshotGlobalSegments(){
 		if (buf[0]=='\n')
 			break;
 
-		sscanf(buf, "%22s %p-%p [%5dK] %c%c%c/%c%c%c SM=%3s %200s\n", &type, &begin, &end, &size, &r, &w, &x, &mr, &mw, &mx, smstr, regionname);
+		sscanf(buf, "%22s %p-%p [%5dK] %c%c%c/%c%c%c SM=%3s %200s\n", type, &begin, &end, &size, &r, &w, &x, &mr, &mw, &mx, smstr, regionname);
 
 		if (w == 'w' && (strstr(regionname, MYBINARYNAME) || strstr(regionname, MYLIBRARYNAME))) {
 			size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;