From d884d14a6288f1ee1809158e81ffb05bf83f483b Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Fri, 2 Nov 2012 17:35:42 -0700 Subject: [PATCH] changes to fix at least a bug --- model.cc | 5 +++-- nodestack.cc | 8 ++++++++ nodestack.h | 2 ++ schedule.cc | 4 +++- 4 files changed, 16 insertions(+), 3 deletions(-) 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