From: Brian Norris <banorris@uci.edu>
Date: Tue, 4 Sep 2012 19:45:49 +0000 (-0700)
Subject: model/schedule: revise 'nextThread' data flow
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=2eb6b99ea42e152d878a8c4805f3cf119f316c3e;p=cdsspec-compiler.git

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 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<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
--- 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;