X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=d6ebfe5abc9f4e60920f9b08bed0112746c3afce;hp=fc86d5c7e9955d3b5e4ccd17cc25ccc5e2e38fa6;hb=43144df37c0f1bb5b4efc4cf1bd2908b6cf440b9;hpb=4159ba45e83f6542e3a3320e83bca9fbaf2da3ea

diff --git a/model.cc b/model.cc
index fc86d5c7..d6ebfe5a 100644
--- a/model.cc
+++ b/model.cc
@@ -2289,15 +2289,20 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 				continue;
 
 			/* Don't consider more than one seq_cst write if we are a seq_cst read. */
-			if (!curr->is_seqcst() || (!act->is_seqcst() && (last_sc_write == NULL || !act->happens_before(last_sc_write))) || act == last_sc_write) {
-				if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) {
-					DEBUG("Adding action to may_read_from:\n");
-					if (DBG_ENABLED()) {
-						act->print();
-						curr->print();
-					}
-					curr->get_node()->add_read_from(act);
+			bool allow_read = true;
+
+			if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
+				allow_read = false;
+			else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
+				allow_read = false;
+
+			if (allow_read) {
+				DEBUG("Adding action to may_read_from:\n");
+				if (DBG_ENABLED()) {
+					act->print();
+					curr->print();
 				}
+				curr->get_node()->add_read_from(act);
 			}
 
 			/* Include at most one act per-thread that "happens before" curr */