From: Brian Norris <banorris@uci.edu>
Date: Fri, 13 Jul 2012 00:50:14 +0000 (-0700)
Subject: model: only include the most recent seq_cst write in may_read_from
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=64a8c6d165d850f2069026bd77a750708a01896e;p=cdsspec-compiler.git

model: only include the most recent seq_cst write in may_read_from
---

diff --git a/model.cc b/model.cc
index 8e6e1b8..4cfc0ef 100644
--- a/model.cc
+++ b/model.cc
@@ -363,6 +363,11 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
 	ASSERT(curr->is_read());
 
+	ModelAction *last_seq_cst = NULL;
+
+	if (curr->is_seqcst())
+		last_seq_cst = get_last_seq_cst(curr->get_location());
+
 	/* Track whether this object has been initialized */
 	bool initialized = false;
 
@@ -376,12 +381,15 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 			if (!act->is_write())
 				continue;
 
-			DEBUG("Adding action to may_read_from:\n");
-			if (DBG_ENABLED()) {
-				act->print();
-				curr->print();
+			/* Don't consider more than one seq_cst write */
+			if (!act->is_seqcst() || act == last_seq_cst) {
+				DEBUG("Adding action to may_read_from:\n");
+				if (DBG_ENABLED()) {
+					act->print();
+					curr->print();
+				}
+				curr->get_node()->add_read_from(act);
 			}
-			curr->get_node()->add_read_from(act);
 
 			/* Include at most one act per-thread that "happens before" curr */
 			if (act->happens_before(curr)) {