From: Brian Norris <banorris@uci.edu>
Date: Tue, 11 Sep 2012 18:43:18 +0000 (-0700)
Subject: model: handle RMW, unresolved reads in w_modification_order checks
X-Git-Tag: pldi2013~223^2~1
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=656bbd79e7e4c9f0e713a553753d7e8b472c8cf8;p=model-checker.git

model: handle RMW, unresolved reads in w_modification_order checks
---

diff --git a/model.cc b/model.cc
index 2be1c82..567cbd7 100644
--- a/model.cc
+++ b/model.cc
@@ -620,10 +620,16 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 
 			/* Include at most one act per-thread that "happens before" curr */
 			if (act->happens_before(curr)) {
-				if (act->is_read())
-					mo_graph->addEdge(act->get_reads_from(), curr);
-				else
+				/*
+				 * Note: if act is RMW, just add edge:
+				 *   act --mo--> curr
+				 * The following edge should be handled elsewhere:
+				 *   readfrom(act) --mo--> act
+				 */
+				if (act->is_write())
 					mo_graph->addEdge(act, curr);
+				else if (act->is_read() && act->get_reads_from() != NULL)
+					mo_graph->addEdge(act->get_reads_from(), curr);
 				added = true;
 				break;
 			} else if (act->is_read() && !act->is_synchronizing(curr) &&