model/schedule: revise 'nextThread' data flow
authorBrian Norris <banorris@uci.edu>
Tue, 4 Sep 2012 19:45:49 +0000 (12:45 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 4 Sep 2012 19:49:01 +0000 (12:49 -0700)
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
model.h
schedule.cc
schedule.h

index 6ded3f5..c306f0e 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 970881c..bc827fa 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;
index 69e3d88..d96172e 100644 (file)
@@ -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);
index c8153b3..c3d029f 100644 (file)
@@ -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;