From 656bbd79e7e4c9f0e713a553753d7e8b472c8cf8 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Tue, 11 Sep 2012 11:43:18 -0700
Subject: [PATCH] model: handle RMW, unresolved reads in w_modification_order
 checks

---
 model.cc | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

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) &&
-- 
2.34.1