From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 2 Nov 2012 08:11:40 +0000 (-0700)
Subject: fix norris bugs
X-Git-Tag: pldi2013~23
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=35c057636dd12235368cfb9644532c7561609624

fix norris bugs
---

diff --git a/model.cc b/model.cc
index 7181f86..2fa54d6 100644
--- a/model.cc
+++ b/model.cc
@@ -383,6 +383,10 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	for(int i = low_tid; i < high_tid; i++) {
 		thread_id_t tid = int_to_id(i);
 
+		/* Make sure this thread can be enabled here. */
+		if (i >= node->get_num_threads())
+			break;
+
 		/* Don't backtrack into a point where the thread is disabled or sleeping. */
 		if (node->get_enabled_array()[i]!=THREAD_ENABLED)
 			continue;
diff --git a/nodestack.cc b/nodestack.cc
index 06259b9..23e87ac 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -262,6 +262,7 @@ void Node::explore_child(ModelAction *act, enabled_type_t * is_enabled)
 bool Node::set_backtrack(thread_id_t id)
 {
 	int i = id_to_int(id);
+	ASSERT(i<((int)backtrack.size()));
 	if (backtrack[i])
 		return false;
 	backtrack[i] = true;
@@ -429,6 +430,7 @@ bool Node::relseq_break_empty() {
 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--;
diff --git a/nodestack.h b/nodestack.h
index 1dfccfc..10331c2 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -53,7 +53,7 @@ struct fairness_info {
  */
 class Node {
 public:
-	Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1, Node *prevfairness = NULL);
+	Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 2, Node *prevfairness = NULL);
 	~Node();
 	/* return true = thread choice has already been explored */
 	bool has_been_explored(thread_id_t tid);