From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 19 Sep 2012 00:15:01 +0000 (-0700)
Subject: ichange
X-Git-Tag: pldi2013~185
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=c6fb6d40ad44767d31cb682d3d4e32c7bbb4b6d3

ichange
---

diff --git a/model.cc b/model.cc
index 72919c6..7c0575f 100644
--- a/model.cc
+++ b/model.cc
@@ -381,6 +381,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 			if (diverge == NULL)
 				tmp->create_cv(get_parent_action(tmp->get_tid()));
 			
+			ASSERT(curr->get_location()==tmp->get_location());
+
 			delete curr;
 			curr = tmp;
 		} else {
diff --git a/schedule.cc b/schedule.cc
index b19a5d3..5c93381 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -77,6 +77,7 @@ void Scheduler::wake(Thread *t)
  */
 Thread * Scheduler::next_thread(Thread *t)
 {
+	printf("%p\n",t);
 	if ( t == NULL ) {
 		int old_curr_thread = curr_thread_index;
 		while(true) {
@@ -90,7 +91,11 @@ Thread * Scheduler::next_thread(Thread *t)
 				return NULL;
 			}
 		}
+	} else {
+		curr_thread_index = id_to_int(t->get_id());
 	}
+	printf("index=%u enabled=%u\n", curr_thread_index, is_enabled[curr_thread_index]);
+
 	current = t;
 	print();
 	return t;