changes to fix at least a bug

diff --git a/model.cc b/model.cc
index 2fa54d6e9ba1e76be577ec0625f6138ee7d1c5d4..7808b104969f72fd9f9b62fe25a8574fffdac9b5 100644 (file)
--- 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 23e87ac690a79c334da6a9f8ed85a269ce073116..d08fa5c733e126f1faa710bfb613bb1df6ecccff 100644 (file)
--- 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 10331c2ef59ccb00046ad62c3e40439543a1288d..648ef4dfc318afc38a4e98b1e31bf4a1bcc944eb 100644 (file)
--- 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 14e6475af1a781803647f7d3bd6fa56887ccf6d4..1cd5b0f1a9f3db7410965a8afad7e67f27a360d3 100644 (file)
--- 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) {