From c6fb6d40ad44767d31cb682d3d4e32c7bbb4b6d3 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Tue, 18 Sep 2012 17:15:01 -0700 Subject: [PATCH] ichange --- model.cc | 2 ++ schedule.cc | 5 +++++ 2 files changed, 7 insertions(+) diff --git a/model.cc b/model.cc index 72919c6d..7c0575fe 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 b19a5d30..5c93381b 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; -- 2.34.1