From: Brian Norris <banorris@uci.edu>
Date: Mon, 3 Dec 2012 21:05:55 +0000 (-0800)
Subject: model: refactor build_reads_from_past
X-Git-Tag: oopsla2013~485
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=43144df37c0f1bb5b4efc4cf1bd2908b6cf440b9;p=model-checker.git

model: refactor build_reads_from_past

Just rearrange the logic a little, to prepare for some other additions.
---

diff --git a/model.cc b/model.cc
index fc86d5c..d6ebfe5 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 */