From 2eb6b99ea42e152d878a8c4805f3cf119f316c3e Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 4 Sep 2012 12:45:49 -0700 Subject: [PATCH] model/schedule: revise 'nextThread' data flow The ModelChecker::nextThread field was being abused a little in my aging design. It really should be either a private field (not accessed even via accessors) or else just a return value / function parameter. This commit makes a change so that nextThread is a Thread pointer and is directly supplied to the Scheduler. If it is NULL, then the Scheduler is allowed to pick its own Thread to run. --- model.cc | 36 ++++++++---------------------------- model.h | 6 ++---- schedule.cc | 10 ++++++---- schedule.h | 2 +- 4 files changed, 17 insertions(+), 37 deletions(-) diff --git a/model.cc b/model.cc index 6ded3f5..c306f0e 100644 --- a/model.cc +++ b/model.cc @@ -25,7 +25,7 @@ ModelChecker::ModelChecker(struct model_params params) : params(params), current_action(NULL), diverge(NULL), - nextThread(THREAD_ID_T_NONE), + nextThread(NULL), action_trace(new action_list_t()), thread_map(new HashTable()), obj_map(new HashTable()), @@ -74,7 +74,7 @@ void ModelChecker::reset_to_initial_state() current_action = NULL; next_thread_id = INITIAL_THREAD_ID; used_sequence_numbers = 0; - nextThread = 0; + nextThread = NULL; next_backtrack = NULL; failed_promise = false; snapshotObject->backTrackBeforeStep(0); @@ -98,27 +98,6 @@ modelclock_t ModelChecker::get_next_seq_num() return ++used_sequence_numbers; } -/** - * Performs the "scheduling" for the model-checker. That is, it checks if the - * model-checker has selected a "next thread to run" and returns it, if - * available. This function should be called from the Scheduler routine, where - * the Scheduler falls back to a default scheduling routine if needed. - * - * @return The next thread chosen by the model-checker. If the model-checker - * makes no selection, retuns NULL. - */ -Thread * ModelChecker::schedule_next_thread() -{ - Thread *t; - if (nextThread == THREAD_ID_T_NONE) - return NULL; - t = thread_map->get(id_to_int(nextThread)); - - ASSERT(t != NULL); - - return t; -} - /** * Choose the next thread in the replay sequence. * @@ -126,13 +105,13 @@ Thread * ModelChecker::schedule_next_thread() * from the backtracking set. Otherwise, simply returns the next thread in the * sequence that is being replayed. */ -thread_id_t ModelChecker::get_next_replay_thread() +Thread * ModelChecker::get_next_replay_thread() { thread_id_t tid; /* Have we completed exploring the preselected path? */ if (diverge == NULL) - return THREAD_ID_T_NONE; + return NULL; /* Else, we are trying to replay an execution */ ModelAction *next = node_stack->get_next()->get_action(); @@ -164,7 +143,8 @@ thread_id_t ModelChecker::get_next_replay_thread() tid = next->get_tid(); } DEBUG("*** ModelChecker chose next thread = %d ***\n", tid); - return tid; + ASSERT(tid != THREAD_ID_T_NONE); + return thread_map->get(id_to_int(tid)); } /** @@ -358,7 +338,7 @@ void ModelChecker::check_current_action(void) /* Do not split atomic actions. */ if (curr->is_rmwr()) - nextThread = thread_current()->get_id(); + nextThread = thread_current(); else nextThread = get_next_replay_thread(); @@ -991,7 +971,7 @@ bool ModelChecker::take_step() { ASSERT(false); } } - next = scheduler->next_thread(); + next = scheduler->next_thread(nextThread); /* Infeasible -> don't take any more steps */ if (!isfeasible()) diff --git a/model.h b/model.h index 970881c..bc827fa 100644 --- a/model.h +++ b/model.h @@ -42,8 +42,6 @@ public: /** Prints an execution summary with trace information. */ void print_summary(); - Thread * schedule_next_thread(); - void add_thread(Thread *t); void remove_thread(Thread *t); Thread * get_thread(thread_id_t tid) { return thread_map->get(id_to_int(tid)); } @@ -90,7 +88,7 @@ private: ModelAction * get_last_conflict(ModelAction *act); void set_backtracking(ModelAction *act); - thread_id_t get_next_replay_thread(); + Thread * get_next_replay_thread(); ModelAction * get_next_backtrack(); void reset_to_initial_state(); bool resolve_promises(ModelAction *curr); @@ -111,7 +109,7 @@ private: ModelAction *current_action; ModelAction *diverge; - thread_id_t nextThread; + Thread *nextThread; ucontext_t system_context; action_list_t *action_trace; diff --git a/schedule.cc b/schedule.cc index 69e3d88..d96172e 100644 --- a/schedule.cc +++ b/schedule.cc @@ -32,13 +32,15 @@ void Scheduler::remove_thread(Thread *t) } /** - * Remove one Thread from the scheduler. This implementation performs FIFO. + * Remove one Thread from the scheduler. This implementation defaults to FIFO, + * if a thread is not already provided. + * + * @param t Thread to run, if chosen by an external entity (e.g., + * ModelChecker). May be NULL to indicate no external choice. * @return The next Thread to run */ -Thread * Scheduler::next_thread() +Thread * Scheduler::next_thread(Thread *t) { - Thread *t = model->schedule_next_thread(); - if (t != NULL) { current = t; readyList.remove(t); diff --git a/schedule.h b/schedule.h index c8153b3..c3d029f 100644 --- a/schedule.h +++ b/schedule.h @@ -18,7 +18,7 @@ public: Scheduler(); void add_thread(Thread *t); void remove_thread(Thread *t); - Thread * next_thread(); + Thread * next_thread(Thread *t); Thread * get_current_thread() const; void print() const; -- 2.34.1