model: pull "may_read_from set" calculation out of initialization
authorBrian Norris <banorris@uci.edu>
Tue, 18 Sep 2012 23:26:52 +0000 (16:26 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 18 Sep 2012 23:45:55 +0000 (16:45 -0700)
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.

model.cc

index 20d0880..a13ccb7 100644 (file)
--- 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. */