From 9f343c92ce3e9ab184d3b45198aa8e547d5791c4 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Tue, 16 Apr 2013 12:27:06 -0700
Subject: [PATCH] nodestack: localize the model-checker parameters

---
 execution.h  |  2 ++
 nodestack.cc | 28 ++++++++++++++++++----------
 nodestack.h  |  8 +++++++-
 3 files changed, 27 insertions(+), 11 deletions(-)

diff --git a/execution.h b/execution.h
index 67e3fa4..8a2bcfa 100644
--- a/execution.h
+++ b/execution.h
@@ -66,6 +66,8 @@ public:
 			NodeStack *node_stack);
 	~ModelExecution();
 
+	const struct model_params * get_params() const { return params; }
+
 	Thread * take_step(ModelAction *curr);
 	void fixup_release_sequences();
 
diff --git a/nodestack.cc b/nodestack.cc
index 80bf5c4..e5f4687 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -6,10 +6,10 @@
 #include "nodestack.h"
 #include "action.h"
 #include "common.h"
-#include "model.h"
 #include "threads-model.h"
 #include "modeltypes.h"
 #include "execution.h"
+#include "params.h"
 
 /**
  * @brief Node constructor
@@ -19,15 +19,18 @@
  * as an empty stub, to represent the first thread "choice") and up to one
  * parent.
  *
+ * @param params The model-checker parameters
  * @param act The ModelAction to associate with this Node. May be NULL.
  * @param par The parent Node in the NodeStack. May be NULL if there is no
  * parent.
  * @param nthreads The number of threads which exist at this point in the
  * execution trace.
  */
-Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
+Node::Node(const struct model_params *params, ModelAction *act, Node *par,
+		int nthreads, Node *prevfairness) :
 	read_from_status(READ_FROM_PAST),
 	action(act),
+	params(params),
 	uninit_action(NULL),
 	parent(par),
 	num_threads(nthreads),
@@ -55,7 +58,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
 	int currtid = id_to_int(act->get_tid());
 	int prevtid = prevfairness ? id_to_int(prevfairness->action->get_tid()) : 0;
 
-	if (model->params.fairwindow != 0) {
+	if (get_params()->fairwindow != 0) {
 		for (int i = 0; i < num_threads; i++) {
 			ASSERT(i < ((int)fairness.size()));
 			struct fairness_info *fi = &fairness[i];
@@ -81,7 +84,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
 				 * conditions
 				 * If we meet the enabled count and have no
 				 * turns, give us priority */
-				if ((fi->enabled_count >= model->params.enabledcount) &&
+				if ((fi->enabled_count >= get_params()->enabledcount) &&
 						(fi->turns == 0))
 					fi->priority = true;
 			}
@@ -621,14 +624,14 @@ bool Node::add_future_value(struct future_value fv)
 		/* Future value hasn't been explored; update expiration */
 		future_values[idx].expiration = expiration;
 		return true;
-	} else if (idx >= 0 && expiration <= future_values[idx].expiration + model->params.expireslop) {
+	} else if (idx >= 0 && expiration <= future_values[idx].expiration + get_params()->expireslop) {
 		/* Future value has been explored and is within the "sloppy" window */
 		return false;
 	}
 
 	/* Limit the size of the future-values set */
-	if (model->params.maxfuturevalues > 0 &&
-			(int)future_values.size() >= model->params.maxfuturevalues)
+	if (get_params()->maxfuturevalues > 0 &&
+			(int)future_values.size() >= get_params()->maxfuturevalues)
 		return false;
 
 	future_values.push_back(fv);
@@ -771,6 +774,11 @@ void NodeStack::register_engine(const ModelExecution *exec)
 	this->execution = exec;
 }
 
+const struct model_params * NodeStack::get_params() const
+{
+	return execution->get_params();
+}
+
 void NodeStack::print() const
 {
 	model_print("............................................\n");
@@ -799,14 +807,14 @@ ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_ena
 	Node *prevfairness = NULL;
 	if (head) {
 		head->explore_child(act, is_enabled);
-		if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow)
-			prevfairness = node_list[head_idx - model->params.fairwindow];
+		if (get_params()->fairwindow != 0 && head_idx > (int)get_params()->fairwindow)
+			prevfairness = node_list[head_idx - get_params()->fairwindow];
 	}
 
 	int next_threads = execution->get_num_threads();
 	if (act->get_type() == THREAD_CREATE)
 		next_threads++;
-	node_list.push_back(new Node(act, head, next_threads, prevfairness));
+	node_list.push_back(new Node(get_params(), act, head, next_threads, prevfairness));
 	total_nodes++;
 	head_idx++;
 	return NULL;
diff --git a/nodestack.h b/nodestack.h
index 1a8bbbe..f26100b 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -54,7 +54,8 @@ typedef enum {
  */
 class Node {
 public:
-	Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness);
+	Node(const struct model_params *params, ModelAction *act, Node *par,
+			int nthreads, Node *prevfairness);
 	~Node();
 	/* return true = thread choice has already been explored */
 	bool has_been_explored(thread_id_t tid) const;
@@ -134,9 +135,12 @@ private:
 	bool future_value_empty() const;
 	bool increment_future_value();
 	read_from_type_t read_from_status;
+	const struct model_params * get_params() const { return params; }
 
 	ModelAction * const action;
 
+	const struct model_params * const params;
+
 	/** @brief ATOMIC_UNINIT action which was created at this Node */
 	ModelAction *uninit_action;
 
@@ -202,6 +206,8 @@ public:
 private:
 	node_list_t node_list;
 
+	const struct model_params * get_params() const;
+
 	/** @brief The model-checker execution object */
 	const ModelExecution *execution;
 
-- 
2.34.1