model: move init code to ModelChecker::initialize_curr_action

Refactoring

diff --git a/model.cc b/model.cc
index e1e80fab33be61f3f58600db19787b3118f28146..f2d4eb193c0a0c428870cf24535da6cc0b3df9fd 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -333,24 +333,8 @@ bool ModelChecker::process_write(ModelAction *curr)
        return updated_mod_order || updated_promises;
 }
 
        return updated_mod_order || updated_promises;
 }
 

-/**
- * This is the heart of the model checker routine. It performs model-checking
- * actions corresponding to a given "current action." Among other processes, it
- * calculates reads-from relationships, updates synchronization clock vectors,
- * forms a memory_order constraints graph, and handles replay/backtrack
- * execution when running permutations of previously-observed executions.
- *
- * @param curr The current action to process
- * @return The next Thread that must be executed. May be NULL if ModelChecker
- * makes no choice (e.g., according to replay execution, combining RMW actions,
- * etc.)
- */
-Thread * ModelChecker::check_current_action(ModelAction *curr)
+ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)

 {
 {

-       ASSERT(curr);
-
-       bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
-

        if (curr->is_rmwc() || curr->is_rmw()) {
                ModelAction *tmp = process_rmw(curr);
                delete curr;
        if (curr->is_rmwc() || curr->is_rmw()) {
                ModelAction *tmp = process_rmw(curr);
                delete curr;


@@ -383,6 +367,28 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                                compute_promises(curr);
                }
        }
                                compute_promises(curr);
                }
        }

+       return curr;
+}
+
+/**
+ * This is the heart of the model checker routine. It performs model-checking
+ * actions corresponding to a given "current action." Among other processes, it
+ * calculates reads-from relationships, updates synchronization clock vectors,
+ * forms a memory_order constraints graph, and handles replay/backtrack
+ * execution when running permutations of previously-observed executions.
+ *
+ * @param curr The current action to process
+ * @return The next Thread that must be executed. May be NULL if ModelChecker
+ * makes no choice (e.g., according to replay execution, combining RMW actions,
+ * etc.)
+ */
+Thread * ModelChecker::check_current_action(ModelAction *curr)
+{
+       ASSERT(curr);
+
+       bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
+
+       curr = initialize_curr_action(curr);

 
        /* Thread specific actions */
        switch (curr->get_type()) {
 
        /* Thread specific actions */
        switch (curr->get_type()) {

diff --git a/model.h b/model.h
index 030d7ddf67723aa1878364e4a7f84c8898136f81..b8a485931882f119ff5b70140c63f213fb79658f 100644 (file)
--- a/model.h
+++ b/model.h
@@ -112,6 +112,7 @@ private:
         */
        void set_current_action(ModelAction *act) { priv->current_action = act; }
        Thread * check_current_action(ModelAction *curr);
         */
        void set_current_action(ModelAction *act) { priv->current_action = act; }
        Thread * check_current_action(ModelAction *curr);

+       ModelAction * initialize_curr_action(ModelAction *curr);

        bool process_read(ModelAction *curr, bool second_part_of_rmw);
        bool process_write(ModelAction *curr);
 
        bool process_read(ModelAction *curr, bool second_part_of_rmw);
        bool process_write(ModelAction *curr);