From: Brian Norris <banorris@uci.edu>
Date: Fri, 25 Jan 2013 21:35:38 +0000 (-0800)
Subject: cyclegraph: RMW atomicity violation must flag a cycle
X-Git-Tag: oopsla2013~318
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=72524dae1144e6fe437c8317f8f718e534ccfe0f;p=model-checker.git

cyclegraph: RMW atomicity violation must flag a cycle

Because we've removed some of the special-casing for RMW atomicity
violations, we don't need the separate 'hasRMWViolation' condition;
instead, we should explicitly flag atomicity violations as a cycle.
Previously, there was a subtle bug related to this issue, where cycles
were flagged only as RMW violations and did not show up to the
model-checker at the appropriate points.
---

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 3214363..7632b0c 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -8,9 +8,7 @@
 CycleGraph::CycleGraph() :
 	discovered(new HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free>(16)),
 	hasCycles(false),
-	oldCycles(false),
-	hasRMWViolation(false),
-	oldRMWViolation(false)
+	oldCycles(false)
 {
 }
 
@@ -113,11 +111,10 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
 	CycleNode *rmwnode = getNode(rmw);
 
 	/* Two RMW actions cannot read from the same write. */
-	if (fromnode->setRMW(rmwnode)) {
-		hasRMWViolation = true;
-	} else {
+	if (fromnode->setRMW(rmwnode))
+		hasCycles = 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:
@@ -246,7 +243,6 @@ void CycleGraph::startChanges()
 	ASSERT(rollbackvector.size() == 0);
 	ASSERT(rmwrollbackvector.size() == 0);
 	ASSERT(oldCycles == hasCycles);
-	ASSERT(oldRMWViolation == hasRMWViolation);
 }
 
 /** Commit changes to the cyclegraph. */
@@ -255,7 +251,6 @@ void CycleGraph::commitChanges()
 	rollbackvector.resize(0);
 	rmwrollbackvector.resize(0);
 	oldCycles = hasCycles;
-	oldRMWViolation = hasRMWViolation;
 }
 
 /** Rollback changes to the previous commit. */
@@ -270,7 +265,6 @@ void CycleGraph::rollbackChanges()
 	}
 
 	hasCycles = oldCycles;
-	hasRMWViolation = oldRMWViolation;
 	rollbackvector.resize(0);
 	rmwrollbackvector.resize(0);
 }
@@ -281,11 +275,6 @@ bool CycleGraph::checkForCycles() const
 	return hasCycles;
 }
 
-bool CycleGraph::checkForRMWViolation() const
-{
-	return hasRMWViolation;
-}
-
 /**
  * @brief Constructor for a CycleNode
  * @param act The ModelAction for this node
diff --git a/cyclegraph.h b/cyclegraph.h
index 8668077..5f6974b 100644
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -26,7 +26,6 @@ class CycleGraph {
 	~CycleGraph();
 	void addEdge(const ModelAction *from, const ModelAction *to);
 	bool checkForCycles() const;
-	bool checkForRMWViolation() const;
 	void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
 	bool checkPromise(const ModelAction *from, Promise *p) const;
 	bool checkReachable(const ModelAction *from, const ModelAction *to) const;
@@ -57,9 +56,6 @@ class CycleGraph {
 	bool hasCycles;
 	bool oldCycles;
 
-	bool hasRMWViolation;
-	bool oldRMWViolation;
-
 	std::vector< CycleNode *, SnapshotAlloc<CycleNode *> > rollbackvector;
 	std::vector< CycleNode *, SnapshotAlloc<CycleNode *> > rmwrollbackvector;
 };
diff --git a/model.cc b/model.cc
index 9e611fa..1ecc48e 100644
--- a/model.cc
+++ b/model.cc
@@ -1372,8 +1372,6 @@ void ModelChecker::print_infeasibility(const char *prefix) const
 {
 	char buf[100];
 	char *ptr = buf;
-	if (mo_graph->checkForRMWViolation())
-		ptr += sprintf(ptr, "[RMW atomicity]");
 	if (mo_graph->checkForCycles())
 		ptr += sprintf(ptr, "[mo cycle]");
 	if (priv->failed_promise)
@@ -1407,8 +1405,7 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
  */
 bool ModelChecker::is_infeasible() const
 {
-	return mo_graph->checkForRMWViolation() ||
-		mo_graph->checkForCycles() ||
+	return mo_graph->checkForCycles() ||
 		priv->failed_promise ||
 		priv->too_many_reads ||
 		priv->bad_synchronization ||