From 35c057636dd12235368cfb9644532c7561609624 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Fri, 2 Nov 2012 01:11:40 -0700 Subject: [PATCH] fix norris bugs --- model.cc | 4 ++++ nodestack.cc | 2 ++ nodestack.h | 2 +- 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/model.cc b/model.cc index 7181f86..2fa54d6 100644 --- a/model.cc +++ b/model.cc @@ -383,6 +383,10 @@ void ModelChecker::set_backtracking(ModelAction *act) for(int i = low_tid; i < high_tid; i++) { thread_id_t tid = int_to_id(i); + /* Make sure this thread can be enabled here. */ + if (i >= node->get_num_threads()) + break; + /* Don't backtrack into a point where the thread is disabled or sleeping. */ if (node->get_enabled_array()[i]!=THREAD_ENABLED) continue; diff --git a/nodestack.cc b/nodestack.cc index 06259b9..23e87ac 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -262,6 +262,7 @@ void Node::explore_child(ModelAction *act, enabled_type_t * is_enabled) bool Node::set_backtrack(thread_id_t id) { int i = id_to_int(id); + ASSERT(i<((int)backtrack.size())); if (backtrack[i]) return false; backtrack[i] = true; @@ -429,6 +430,7 @@ bool Node::relseq_break_empty() { void Node::explore(thread_id_t tid) { int i = id_to_int(tid); + ASSERT(i<((int)backtrack.size())); if (backtrack[i]) { backtrack[i] = false; numBacktracks--; diff --git a/nodestack.h b/nodestack.h index 1dfccfc..10331c2 100644 --- a/nodestack.h +++ b/nodestack.h @@ -53,7 +53,7 @@ struct fairness_info { */ class Node { public: - Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1, Node *prevfairness = NULL); + Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 2, Node *prevfairness = NULL); ~Node(); /* return true = thread choice has already been explored */ bool has_been_explored(thread_id_t tid); -- 2.34.1