From dae59b7e635c23bc78f27177f64e184d7642ef59 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 11 Sep 2012 11:19:50 -0700 Subject: [PATCH] model: refactor "get next thread" code get_next_replay_thread() might as well handle all the Thread decisions for the model-checker. Refactor, and rename to get_next_thread(). --- model.cc | 32 +++++++++++++++++++------------- model.h | 2 +- 2 files changed, 20 insertions(+), 14 deletions(-) diff --git a/model.cc b/model.cc index c8af6cc..90c7ad9 100644 --- a/model.cc +++ b/model.cc @@ -98,16 +98,29 @@ modelclock_t ModelChecker::get_next_seq_num() } /** - * Choose the next thread in the replay sequence. + * @brief Choose the next thread to execute. * - * If the replay sequence has reached the 'diverge' point, returns a thread - * from the backtracking set. Otherwise, simply returns the next thread in the - * sequence that is being replayed. + * This function chooses the next thread that should execute. It can force the + * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be + * followed by a THREAD_START, or it can enforce execution replay/backtracking. + * The model-checker may have no preference regarding the next thread (i.e., + * when exploring a new execution ordering), in which case this will return + * NULL. + * @param curr The current ModelAction. This action might guide the choice of + * next thread. + * @return The next thread to run. If the model-checker has no preference, NULL. */ -Thread * ModelChecker::get_next_replay_thread() +Thread * ModelChecker::get_next_thread(ModelAction *curr) { thread_id_t tid; + /* Do not split atomic actions. */ + if (curr->is_rmwr()) + return thread_current(); + /* The THREAD_CREATE action points to the created Thread */ + else if (curr->get_type() == THREAD_CREATE) + return (Thread *)curr->get_location(); + /* Have we completed exploring the preselected path? */ if (diverge == NULL) return NULL; @@ -362,14 +375,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) set_backtracking(curr); - /* Do not split atomic actions. */ - if (curr->is_rmwr()) - return thread_current(); - /* The THREAD_CREATE action points to the created Thread */ - else if (curr->get_type() == THREAD_CREATE) - return (Thread *)curr->get_location(); - else - return get_next_replay_thread(); + return get_next_thread(curr); } /** @returns whether the current partial trace must be a prefix of a diff --git a/model.h b/model.h index b2f7897..1b6bb10 100644 --- a/model.h +++ b/model.h @@ -105,7 +105,7 @@ private: ModelAction * get_last_conflict(ModelAction *act); void set_backtracking(ModelAction *act); - Thread * get_next_replay_thread(); + Thread * get_next_thread(ModelAction *curr); ModelAction * get_next_backtrack(); void reset_to_initial_state(); bool resolve_promises(ModelAction *curr); -- 2.34.1