From: Brian Demsky <bdemsky@uci.edu>
Date: Sat, 3 Nov 2012 00:35:42 +0000 (-0700)
Subject: changes to fix at least a bug
X-Git-Tag: pldi2013~20^2
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=d884d14a6288f1ee1809158e81ffb05bf83f483b

changes to fix at least a bug
---

diff --git a/model.cc b/model.cc
index 2fa54d6..7808b10 100644
--- a/model.cc
+++ b/model.cc
@@ -388,7 +388,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 			break;
 
 		/* Don't backtrack into a point where the thread is disabled or sleeping. */
-		if (node->get_enabled_array()[i]!=THREAD_ENABLED)
+		if (node->enabled_status(tid)!=THREAD_ENABLED)
 			continue;
 	
 		/* Check if this has been explored already */
@@ -2025,7 +2025,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
 	while(true) {
 		Node *prevnode=write->get_node()->get_parent();
-		bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
+		
+		bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
 		if (write->is_release()&&thread_sleep)
 			return true;
 		if (!write->is_rmw()) {
diff --git a/nodestack.cc b/nodestack.cc
index 23e87ac..d08fa5c 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -291,6 +291,14 @@ bool Node::is_enabled(Thread *t)
 	return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
 }
 
+enabled_type_t Node::enabled_status(thread_id_t tid) {
+	int thread_id=id_to_int(tid);
+	if (thread_id < num_threads)
+		return enabled_array[thread_id];
+	else
+		return THREAD_DISABLED;
+}
+
 bool Node::is_enabled(thread_id_t tid)
 {
 	int thread_id=id_to_int(tid);
diff --git a/nodestack.h b/nodestack.h
index 10331c2..648ef4d 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -66,6 +66,8 @@ public:
 	thread_id_t get_next_backtrack();
 	bool is_enabled(Thread *t);
 	bool is_enabled(thread_id_t tid);
+	enabled_type_t enabled_status(thread_id_t tid);
+
 	ModelAction * get_action() { return action; }
 	bool has_priority(thread_id_t tid);
 	int get_num_threads() {return num_threads;}
diff --git a/schedule.cc b/schedule.cc
index 14e6475..1cd5b0f 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -43,7 +43,9 @@ bool Scheduler::is_enabled(Thread *t) const
 }
 
 enabled_type_t Scheduler::get_enabled(Thread *t) {
-	return enabled[id_to_int(t->get_id())];
+	int id = id_to_int(t->get_id());
+	ASSERT(id<enabled_len);
+	return enabled[id];
 }
 
 void Scheduler::update_sleep_set(Node *n) {