From 31246eff241f4593a33501f8c33b6eadca1d7664 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 18 Sep 2012 16:26:52 -0700 Subject: [PATCH] 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. --- model.cc | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) 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. */ -- 2.34.1