From: Brian Norris <banorris@uci.edu>
Date: Sat, 6 Oct 2012 02:18:13 +0000 (-0700)
Subject: model: add special model-checker Thread to ModelChecker
X-Git-Tag: pldi2013~97^2~1^2~6
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=495dd308fe91920ea85719d8380d9cf28ee85274

model: add special model-checker Thread to ModelChecker

Note the change in take_step(), so that we base the "current thread" off
of the provided ModelAction, rather than thread_current() (i.e., the
Scheduler). This is because the Scheduler will never run the
model-checker thread.
---

diff --git a/model.cc b/model.cc
index c5e41ab..c1818ad 100644
--- a/model.cc
+++ b/model.cc
@@ -47,6 +47,10 @@ ModelChecker::ModelChecker(struct model_params params) :
 	priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
 	/* First thread created will have id INITIAL_THREAD_ID */
 	priv->next_thread_id = INITIAL_THREAD_ID;
+
+	/* Initialize a model-checker thread, for special ModelActions */
+	model_thread = new Thread(get_next_id());
+	thread_map->put(id_to_int(model_thread->get_id()), model_thread);
 }
 
 /** @brief Destructor */
@@ -1944,7 +1948,7 @@ bool ModelChecker::take_step() {
 	if (has_asserted())
 		return false;
 
-	Thread *curr = thread_current();
+	Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
 	if (curr) {
 		if (curr->get_state() == THREAD_READY) {
 			ASSERT(priv->current_action);
diff --git a/model.h b/model.h
index 4032ef1..68831b8 100644
--- a/model.h
+++ b/model.h
@@ -203,6 +203,10 @@ private:
 	 * together for efficiency and maintainability. */
 	struct model_snapshot_members *priv;
 
+	/** A special model-checker Thread; used for associating with
+	 *  model-checker-related ModelAcitons */
+	Thread *model_thread;
+
 	/**
 	 * @brief The modification order graph
 	 *