From: Brian Norris <banorris@uci.edu>
Date: Sat, 3 Nov 2012 22:31:02 +0000 (-0700)
Subject: Merge remote-tracking branch 'origin/master' into pldi13
X-Git-Tag: pldi2013~17
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=4ee9f33221f490599093e74b527ba7e401133f96;hp=ff6281947505d1b5bf6491dbfeaa27d5d41ab964;p=model-checker.git

Merge remote-tracking branch 'origin/master' into pldi13
---

diff --git a/model.cc b/model.cc
index 1e730d7..da982d0 100644
--- a/model.cc
+++ b/model.cc
@@ -1388,7 +1388,6 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
 {
 	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
 	unsigned int i;
-
 	/* Iterate over all threads */
 	for (i = 0; i < thrd_lists->size(); i++) {
 		const ModelAction *write_after_read = NULL;
@@ -1403,7 +1402,7 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
 				break;
 			else if (act->is_write())
 				write_after_read = act;
-			else if (act->is_read()&&act->get_reads_from()!=NULL) {
+			else if (act->is_read()&&act->get_reads_from()!=NULL&&act!=reader) {
 				write_after_read = act->get_reads_from();
 			}
 		}
@@ -1411,7 +1410,6 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
 		if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
 			return false;
 	}
-
 	return true;
 }