From 502c7029755b194e52526fe26c2e7327b5d64101 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 18 Sep 2012 16:42:09 -0700 Subject: [PATCH] model: add curr to action lists early The current action should be added to the ModelChecker lists early within check_current_action, so that we can have consistency throughout the function. We only allow an isolated piece of initialization (initialize_curr_action) to occur before this step. --- model.cc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/model.cc b/model.cc index ebadbb6..e41bc4e 100644 --- a/model.cc +++ b/model.cc @@ -400,6 +400,10 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) ModelAction *newcurr = initialize_curr_action(curr); + /* Add the action to lists before any other model-checking tasks */ + if (!second_part_of_rmw) + add_action_to_lists(newcurr); + /* Build may_read_from set for newly-created actions */ if (curr == newcurr && curr->is_read()) build_reads_from_past(curr); @@ -440,10 +444,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) break; } - /* Add current action to lists before work_queue loop */ - if (!second_part_of_rmw) - add_action_to_lists(curr); - work_queue_t work_queue(1, CheckCurrWorkEntry(curr)); while (!work_queue.empty()) { -- 2.34.1