From: Brian Norris <banorris@uci.edu>
Date: Tue, 18 Sep 2012 23:26:52 +0000 (-0700)
Subject: model: pull "may_read_from set" calculation out of initialization
X-Git-Tag: pldi2013~177^2^2~6
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=31246eff241f4593a33501f8c33b6eadca1d7664;hp=ed5684e598c27e458bde4976848d48a0cd247dbb

model: pull "may_read_from set" calculation out of initialization

The build_reads_from_past calculation shouldn't be part of the action
initialization. It requires more information from the ModelChecker.

In the future, we will assume that all check_curren_action code (after
initialization) may include the current action in the model-checker lists. So
this also fixes up the build_reads_from_past code so that it skips the current
action.
---

diff --git a/model.cc b/model.cc
index 20d0880..a13ccb7 100644
--- a/model.cc
+++ b/model.cc
@@ -363,8 +363,6 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 		 * NodeStack
 		 */
 		curr->create_cv(get_parent_action(curr->get_tid()));
-		if (curr->is_read())
-			build_reads_from_past(curr);
 		if (curr->is_write())
 			compute_promises(curr);
 	}
@@ -389,7 +387,12 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 	bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
 
-	curr = initialize_curr_action(curr);
+	ModelAction *newcurr = initialize_curr_action(curr);
+
+	/* Build may_read_from set for newly-created actions */
+	if (curr == newcurr && curr->is_read())
+		build_reads_from_past(curr);
+	curr = newcurr;
 
 	/* Thread specific actions */
 	switch (curr->get_type()) {
@@ -1264,7 +1267,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 			ModelAction *act = *rit;
 
 			/* Only consider 'write' actions */
-			if (!act->is_write())
+			if (!act->is_write() || act == curr)
 				continue;
 
 			/* Don't consider more than one seq_cst write if we are a seq_cst read. */