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.

diff --git a/model.cc b/model.cc
index ebadbb6c8a86482a97999871bba1f0dae6da6a61..e41bc4e926f39c42487fd833bfd7e6c57d8a0baf 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -400,6 +400,10 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
        ModelAction *newcurr = initialize_curr_action(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);
        /* 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;
        }
 
                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()) {
        work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
 
        while (!work_queue.empty()) {