From 2d9c8d86e9a5050786c5f83ab6f18cd583984279 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 12 Dec 2012 19:57:44 -0800 Subject: [PATCH] nodestack: don't create empty base node We don't actually need an empty base node, since the first thread will never be backtracked. But it does mean that we no longer assume that every newly-constructed Node has a parent. Note that this changes the number of executions performed for some programs. Even though the model-checker should be deterministic, this is not a bug, AFAICT. The discrepancy seems to come from a change in scheduling, where the scheduler order may differ after reaching a divergence point. This is caused by the fairness support which is hacked into Node creation, so threads may gain priority sooner in the presence of a useless Node. In fact, before this change, (almost?) every execution caused a thread (typically thread 1) to gain priority due to fairness. Now, we reach this condition much more occasionally. I made measurements of the scheduling decisions based on priority for the execution of: # ./run.sh test/linuxrwlocks.o -f 10 -m 2 Previously, threads gained priority 10042 times in 7906 executions (9947 of those were for thread 1, when it would shortly become disabled). Now, threads gain priority 68 times in 8396 executions (thread 1 never gains priority). --- nodestack.cc | 23 ++++++++++++----------- nodestack.h | 4 ++-- 2 files changed, 14 insertions(+), 13 deletions(-) diff --git a/nodestack.cc b/nodestack.cc index d144a9d..2e5a04c 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -51,7 +51,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) if (prevfi) { *fi = *prevfi; } - if (parent->is_enabled(int_to_id(i))) { + if (parent && parent->is_enabled(int_to_id(i))) { fi->enabled_count++; } if (i == currtid) { @@ -501,8 +501,8 @@ void Node::explore(thread_id_t tid) } NodeStack::NodeStack() : - node_list(1, new Node()), - head_idx(0), + node_list(), + head_idx(-1), total_nodes(0) { total_nodes++; @@ -532,19 +532,20 @@ ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_ena { DBG(); - ASSERT(!node_list.empty()); - if ((head_idx + 1) < (int)node_list.size()) { head_idx++; return node_list[head_idx]->get_action(); } /* Record action */ - get_head()->explore_child(act, is_enabled); + Node *head = get_head(); Node *prevfairness = NULL; - if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow) - prevfairness = node_list[head_idx - model->params.fairwindow]; - node_list.push_back(new Node(act, get_head(), model->get_num_threads(), prevfairness)); + if (head) { + head->explore_child(act, is_enabled); + if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow) + prevfairness = node_list[head_idx - model->params.fairwindow]; + } + node_list.push_back(new Node(act, head, model->get_num_threads(), prevfairness)); total_nodes++; head_idx++; return NULL; @@ -569,7 +570,7 @@ void NodeStack::pop_restofstack(int numAhead) Node * NodeStack::get_head() const { - if (node_list.empty()) + if (node_list.empty() || head_idx < 0) return NULL; return node_list[head_idx]; } @@ -590,5 +591,5 @@ Node * NodeStack::get_next() const void NodeStack::reset_execution() { - head_idx = 0; + head_idx = -1; } diff --git a/nodestack.h b/nodestack.h index f6d3e4e..d7c1368 100644 --- a/nodestack.h +++ b/nodestack.h @@ -56,7 +56,7 @@ struct fairness_info { */ class Node { public: - Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 2, Node *prevfairness = NULL); + Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness); ~Node(); /* return true = thread choice has already been explored */ bool has_been_explored(thread_id_t tid) const; @@ -171,7 +171,7 @@ private: * @brief the index position of the current head Node * * This index is relative to node_list. The index should point to the - * current head Node. + * current head Node. It is negative when the list is empty. */ int head_idx; -- 2.34.1