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.

diff --git a/model.cc b/model.cc
index 6ded3f5d0ee1edeeb5f7b5e711a8f91396fd9523..c306f0e70869de9362ea83af601f6d94bda30ef9 100644 (file)
--- 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<int, Thread *, int>()),
        obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
@@ -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 970881cd24b3a707eb575a11522ebb6809a71a74..bc827fa378e6bc260d30f49def8c67420e589d58 100644 (file)
--- 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 69e3d88803bcc06d15ee2fed115330b1397662f5..d96172e010d445a2b06eff5b392b89161126f12e 100644 (file)
--- 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 c8153b31821d554940d9faa5d4f1b83dd912f58c..c3d029fb2ed4b77246889ad8f7a070b7893a080a 100644 (file)
--- 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;