X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=nodestack.cc;h=bacd067dcb4b8277408e2efd5685fc27bac8e2da;hp=dbc630739473bfa2fd0dbd44717ea2873c3c3bfd;hb=HEAD;hpb=90471233ff4dcca9a196152574dca4e7cf183698

diff --git a/nodestack.cc b/nodestack.cc
index dbc6307..bacd067 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -6,9 +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
@@ -18,15 +19,19 @@
  * 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),
 	explored_children(num_threads),
@@ -53,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];
@@ -79,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;
 			}
@@ -95,7 +100,8 @@ int Node::get_yield_data(int tid1, int tid2) const {
 }
 
 void Node::update_yield(Scheduler * scheduler) {
-	yield_data=(int *) model_calloc(1, sizeof(int)*num_threads*num_threads);
+	if (yield_data==NULL)
+		yield_data=(int *) model_calloc(1, sizeof(int)*num_threads*num_threads);
 	//handle base case
 	if (parent == NULL) {
 		for(int i = 0; i < num_threads*num_threads; i++) {
@@ -140,6 +146,8 @@ void Node::update_yield(Scheduler * scheduler) {
 Node::~Node()
 {
 	delete action;
+	if (uninit_action)
+		delete uninit_action;
 	if (enabled_array)
 		model_free(enabled_array);
 	if (yield_data)
@@ -186,87 +194,7 @@ void Node::print() const
 	model_print("          rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
 }
 
-/*********************************** promise **********************************/
-
-/**
- * Sets a promise to explore meeting with the given node.
- * @param i is the promise index.
- */
-void Node::set_promise(unsigned int i)
-{
-	if (i >= resolve_promise.size())
-		resolve_promise.resize(i + 1, false);
-	resolve_promise[i] = true;
-}
-
-/**
- * Looks up whether a given promise should be satisfied by this node.
- * @param i The promise index.
- * @return true if the promise should be satisfied by the given ModelAction.
- */
-bool Node::get_promise(unsigned int i) const
-{
-	return (i < resolve_promise.size()) && (int)i == resolve_promise_idx;
-}
-
-/**
- * Increments to the next promise to resolve.
- * @return true if we have a valid combination.
- */
-bool Node::increment_promise()
-{
-	DBG();
-	if (resolve_promise.empty())
-		return false;
-	int prev_idx = resolve_promise_idx;
-	resolve_promise_idx++;
-	for ( ; resolve_promise_idx < (int)resolve_promise.size(); resolve_promise_idx++)
-		if (resolve_promise[resolve_promise_idx])
-			return true;
-	resolve_promise_idx = prev_idx;
-	return false;
-}
-
-/**
- * Returns whether the promise set is empty.
- * @return true if we have explored all promise combinations.
- */
-bool Node::promise_empty() const
-{
-	for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++)
-		if (i >= 0 && resolve_promise[i])
-			return false;
-	return true;
-}
-
-/** @brief Clear any promise-resolution information for this Node */
-void Node::clear_promise_resolutions()
-{
-	resolve_promise.clear();
-	resolve_promise_idx = -1;
-}
-
-/******************************* end promise **********************************/
-
-void Node::set_misc_max(int i)
-{
-	misc_max = i;
-}
-
-int Node::get_misc() const
-{
-	return misc_index;
-}
-
-bool Node::increment_misc()
-{
-	return (misc_index < misc_max) && ((++misc_index) < misc_max);
-}
-
-bool Node::misc_empty() const
-{
-	return (misc_index + 1) >= misc_max;
-}
+/****************************** threads backtracking **************************/
 
 /**
  * Checks if the Thread associated with this thread ID has been explored from
@@ -290,6 +218,17 @@ bool Node::backtrack_empty() const
 	return (numBacktracks == 0);
 }
 
+void Node::explore(thread_id_t tid)
+{
+	int i = id_to_int(tid);
+	ASSERT(i < ((int)backtrack.size()));
+	if (backtrack[i]) {
+		backtrack[i] = false;
+		numBacktracks--;
+	}
+	explored_children[i] = true;
+}
+
 /**
  * Mark the appropriate backtracking information for exploring a thread choice.
  * @param act The ModelAction to explore
@@ -350,6 +289,90 @@ void Node::clear_backtracking()
 	numBacktracks = 0;
 }
 
+/************************** end threads backtracking **************************/
+
+/*********************************** promise **********************************/
+
+/**
+ * Sets a promise to explore meeting with the given node.
+ * @param i is the promise index.
+ */
+void Node::set_promise(unsigned int i)
+{
+	if (i >= resolve_promise.size())
+		resolve_promise.resize(i + 1, false);
+	resolve_promise[i] = true;
+}
+
+/**
+ * Looks up whether a given promise should be satisfied by this node.
+ * @param i The promise index.
+ * @return true if the promise should be satisfied by the given ModelAction.
+ */
+bool Node::get_promise(unsigned int i) const
+{
+	return (i < resolve_promise.size()) && (int)i == resolve_promise_idx;
+}
+
+/**
+ * Increments to the next promise to resolve.
+ * @return true if we have a valid combination.
+ */
+bool Node::increment_promise()
+{
+	DBG();
+	if (resolve_promise.empty())
+		return false;
+	int prev_idx = resolve_promise_idx;
+	resolve_promise_idx++;
+	for ( ; resolve_promise_idx < (int)resolve_promise.size(); resolve_promise_idx++)
+		if (resolve_promise[resolve_promise_idx])
+			return true;
+	resolve_promise_idx = prev_idx;
+	return false;
+}
+
+/**
+ * Returns whether the promise set is empty.
+ * @return true if we have explored all promise combinations.
+ */
+bool Node::promise_empty() const
+{
+	for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++)
+		if (i >= 0 && resolve_promise[i])
+			return false;
+	return true;
+}
+
+/** @brief Clear any promise-resolution information for this Node */
+void Node::clear_promise_resolutions()
+{
+	resolve_promise.clear();
+	resolve_promise_idx = -1;
+}
+
+/******************************* end promise **********************************/
+
+void Node::set_misc_max(int i)
+{
+	misc_max = i;
+}
+
+int Node::get_misc() const
+{
+	return misc_index;
+}
+
+bool Node::increment_misc()
+{
+	return (misc_index < misc_max) && ((++misc_index) < misc_max);
+}
+
+bool Node::misc_empty() const
+{
+	return (misc_index + 1) >= misc_max;
+}
+
 bool Node::is_enabled(Thread *t) const
 {
 	int thread_id = id_to_int(t->get_id());
@@ -601,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);
@@ -651,6 +674,8 @@ bool Node::increment_future_value()
 
 /************************** end future values *********************************/
 
+/*********************** breaking release sequences ***************************/
+
 /**
  * Add a write ModelAction to the set of writes that may break the release
  * sequence. This is used during replay exploration of pending release
@@ -703,15 +728,27 @@ bool Node::relseq_break_empty() const
 	return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size()));
 }
 
-void Node::explore(thread_id_t tid)
+/******************* end breaking release sequences ***************************/
+
+/**
+ * Increments some behavior's index, if a new behavior is available
+ * @return True if there is a new behavior available; otherwise false
+ */
+bool Node::increment_behaviors()
 {
-	int i = id_to_int(tid);
-	ASSERT(i < ((int)backtrack.size()));
-	if (backtrack[i]) {
-		backtrack[i] = false;
-		numBacktracks--;
-	}
-	explored_children[i] = true;
+	/* satisfy a different misc_index values */
+	if (increment_misc())
+		return true;
+	/* satisfy a different set of promises */
+	if (increment_promise())
+		return true;
+	/* read from a different value */
+	if (increment_read_from())
+		return true;
+	/* resolve a release sequence differently */
+	if (increment_relseq_break())
+		return true;
+	return false;
 }
 
 NodeStack::NodeStack() :
@@ -728,6 +765,20 @@ NodeStack::~NodeStack()
 		delete node_list[i];
 }
 
+/**
+ * @brief Register the model-checker object with this NodeStack
+ * @param exec The execution structure for the ModelChecker
+ */
+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");
@@ -756,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 = model->get_num_threads();
+	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;
@@ -787,6 +838,16 @@ void NodeStack::pop_restofstack(int numAhead)
 	node_list.back()->clear_backtracking();
 }
 
+/** Reset the node stack. */
+void NodeStack::full_reset() 
+{
+	for (unsigned int i = 0; i < node_list.size(); i++)
+		delete node_list[i];
+	node_list.clear();
+	reset_execution();
+	total_nodes = 1;
+}
+
 Node * NodeStack::get_head() const
 {
 	if (node_list.empty() || head_idx < 0)