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).

diff --git a/nodestack.cc b/nodestack.cc
index d144a9d5ef921564a9212dd639929ac345f4773e..2e5a04c20cfaa5cf3dd6b73602302bf368c3c995 100644 (file)
--- 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 f6d3e4e36be07a0ffa0feec975181faacd283f4f..d7c13688e54898dc4fa09d0a532d8866622659a2 100644 (file)
--- 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;