X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=3e54a001a4541b8d5acada69e76c189ff5e82b36;hp=6f144abab044d5d6a23880a9744e2b95ee5b3f24;hb=50b95c3747f4fe79b2ab1a1a6fc303224e16e418;hpb=7c6c6a9bd044f8986ec17641cb8ea5f4e1aae345;ds=sidebyside

diff --git a/model.cc b/model.cc
index 6f144ab..3e54a00 100644
--- a/model.cc
+++ b/model.cc
@@ -100,16 +100,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;
@@ -339,28 +352,37 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		}
 	}
 
-	/* Assign 'creation' parent */
-	if (curr->get_type() == THREAD_CREATE) {
+	/* Thread specific actions */
+	switch(curr->get_type()) {
+	case THREAD_CREATE: {
 		Thread *th = (Thread *)curr->get_location();
 		th->set_creation(curr);
-	} else if (curr->get_type() == THREAD_JOIN) {
+		break;
+	}
+	case THREAD_JOIN: {
 		Thread *wait, *join;
 		wait = get_thread(curr->get_tid());
 		join = (Thread *)curr->get_location();
 		if (!join->is_complete())
 			scheduler->wait(wait, join);
-	} else if (curr->get_type() == THREAD_FINISH) {
+		break;
+	}
+	case THREAD_FINISH: {
 		Thread *th = get_thread(curr->get_tid());
 		while (!th->wait_list_empty()) {
 			Thread *wake = th->pop_wait_list();
 			scheduler->wake(wake);
 		}
 		th->complete();
+		break;
 	}
-
-	/* Deal with new thread */
-	if (curr->get_type() == THREAD_START)
+	case THREAD_START: {
 		check_promises(NULL, curr->get_cv());
+		break;
+	}
+	default:
+		break;
+	}
 
 	Thread *th = get_thread(curr->get_tid());
 
@@ -399,14 +421,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