model: replace TreeNode with NodeStack

Big structural change to the model-checker internal data structure. It's now
tested to work, and hopefully it's still easy enough to understand.

Note that also, we remove the backtrack_list, since this type of structure
depended on keeping around "action lists" of each trace. Instead, I can free up
those lists at the end of each execution, preventing leaks and limiting memory
usage.

diff --git a/action.h b/action.h
index cfe1f34eece13b4600f6de66393a872c7540e33a..b30b650008194239c363d9948e8db6d882cc1a9b 100644 (file)
--- a/action.h
+++ b/action.h
@@ -17,7 +17,6 @@ typedef enum action_type {
 } action_type_t;
 
 /* Forward declaration */
-class TreeNode;
 class Node;
 
 class ModelAction {
@@ -31,8 +30,6 @@ public:
        void * get_location() { return location; }
        int get_seq_number() const { return seq_number; }
 
-       TreeNode * get_treenode() { return treenode; }
-       void set_node(TreeNode *n) { treenode = n; }
        Node * get_node() { return node; }
        void set_node(Node *n) { node = n; }
 
@@ -56,7 +53,6 @@ private:
        void *location;
        thread_id_t tid;
        int value;
-       TreeNode *treenode;
        Node *node;
        int seq_number;
 };

diff --git a/model.cc b/model.cc
index c19c37f0cdc778684d6796842043a7b71afee440..e5af1a6f328e729ffe7885071a42c1a70dc4581a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2,7 +2,7 @@
 
 #include "model.h"
 #include "action.h"
-#include "tree.h"
+#include "nodestack.h"
 #include "schedule.h"
 #include "common.h"
 
@@ -48,11 +48,11 @@ ModelChecker::ModelChecker()
 
        num_executions(0),
        current_action(NULL),
-       exploring(NULL),
+       diverge(NULL),
        nextThread(THREAD_ID_T_NONE),
        action_trace(new action_list_t()),
-       rootNode(new TreeNode()),
-       currentNode(rootNode)
+       node_stack(new NodeStack()),
+       next_backtrack(NULL)
 {
 }
 
@@ -63,10 +63,10 @@ ModelChecker::~ModelChecker()
                delete (*it).second;
        thread_map.clear();
 
-       free_action_list(action_trace);
+       delete action_trace;
 
+       delete node_stack;
        delete scheduler;
-       delete rootNode;
 }
 
 void ModelChecker::reset_to_initial_state()
@@ -76,12 +76,14 @@ void ModelChecker::reset_to_initial_state()
        for (it = thread_map.begin(); it != thread_map.end(); it++)
                delete (*it).second;
        thread_map.clear();
+       delete action_trace;
        action_trace = new action_list_t();
-       currentNode = rootNode;
+       node_stack->reset_execution();
        current_action = NULL;
        next_thread_id = INITIAL_THREAD_ID;
        used_sequence_numbers = 0;
        nextThread = 0;
+       next_backtrack = NULL;
        /* scheduler reset ? */
 }
 
@@ -120,24 +122,19 @@ thread_id_t ModelChecker::get_next_replay_thread()
        thread_id_t tid;
 
        /* Have we completed exploring the preselected path? */
-       if (exploring == NULL)
+       if (diverge == NULL)
                return THREAD_ID_T_NONE;
 
        /* Else, we are trying to replay an execution */
-       exploring->advance_state();
+       next = node_stack->get_next()->get_action();
 
-       ASSERT(exploring->get_state() != NULL);
+       if (next == diverge) {
+               Node *node = next->get_node();
 
-       next = exploring->get_state();
-
-       if (next == exploring->get_diverge()) {
-               TreeNode *node = next->get_treenode();
-
-               /* Reached divergence point; discard our current 'exploring' */
-               DEBUG("*** Discard 'Backtrack' object ***\n");
-               tid = node->getNextBacktrack();
-               delete exploring;
-               exploring = NULL;
+               /* Reached divergence point */
+               DEBUG("*** Divergence point ***\n");
+               tid = node->get_next_backtrack();
+               diverge = NULL;
        } else {
                tid = next->get_tid();
        }
@@ -151,13 +148,12 @@ bool ModelChecker::next_execution()
 
        num_executions++;
        print_summary();
-       if ((exploring = model->get_next_backtrack()) == NULL)
+       if ((diverge = model->get_next_backtrack()) == NULL)
                return false;
 
        if (DBG_ENABLED()) {
                printf("Next execution will diverge at:\n");
-               exploring->get_diverge()->print();
-               print_list(exploring->get_trace());
+               diverge->print();
        }
 
        model->reset_to_initial_state();
@@ -191,48 +187,47 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 void ModelChecker::set_backtracking(ModelAction *act)
 {
        ModelAction *prev;
-       TreeNode *node;
+       Node *node;
        Thread *t = get_thread(act->get_tid());
 
        prev = get_last_conflict(act);
        if (prev == NULL)
                return;
 
-       node = prev->get_treenode();
+       node = prev->get_node();
 
-       while (t && !node->is_enabled(t))
+       while (!node->is_enabled(t))
                t = t->get_parent();
 
        /* Check if this has been explored already */
-       if (node->hasBeenExplored(t->get_id()))
+       if (node->has_been_explored(t->get_id()))
                return;
+
+       if (!next_backtrack || *prev > *next_backtrack)
+               next_backtrack = prev;
+
        /* If this is a new backtracking point, mark the tree */
-       if (node->setBacktrack(t->get_id()) != 0)
+       if (!node->set_backtrack(t->get_id()))
                return;
-
        DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
                        prev->get_tid(), t->get_id());
        if (DBG_ENABLED()) {
                prev->print();
                act->print();
        }
-
-       Backtrack *back = new Backtrack(prev, action_trace);
-       backtrack_list.push_back(back);
 }
 
-Backtrack * ModelChecker::get_next_backtrack()
+ModelAction * ModelChecker::get_next_backtrack()
 {
-       Backtrack *next;
-       if (backtrack_list.empty())
-               return NULL;
-       next = backtrack_list.back();
-       backtrack_list.pop_back();
+       ModelAction *next = next_backtrack;
+       next_backtrack = NULL;
        return next;
 }
 
 void ModelChecker::check_current_action(void)
 {
+       Node *currnode;
+
        ModelAction *curr = this->current_action;
        current_action = NULL;
        if (!curr) {
@@ -240,10 +235,16 @@ void ModelChecker::check_current_action(void)
                return;
        }
 
+       curr = node_stack->explore_action(curr);
        nextThread = get_next_replay_thread();
-       curr->set_node(currentNode);
+
+       currnode = curr->get_node();
+
+       if (!currnode->backtrack_empty())
+               if (!next_backtrack || *curr > *next_backtrack)
+                       next_backtrack = curr;
+
        set_backtracking(curr);
-       currentNode = currentNode->explore_child(curr);
        this->action_trace->push_back(curr);
 }
 
@@ -251,13 +252,12 @@ void ModelChecker::print_summary(void)
 {
        printf("\n");
        printf("Number of executions: %d\n", num_executions);
-       printf("Total nodes created: %d\n", TreeNode::getTotalNodes());
+       printf("Total nodes created: %d\n", Node::get_total_nodes());
 
        scheduler->print();
 
        print_list(action_trace);
        printf("\n");
-
 }
 
 void ModelChecker::print_list(action_list_t *list)

diff --git a/model.h b/model.h
index 8651a4f9ffe166125571920414dff6999a009798..e8a8c5eb9e868dc2d4dca77e647d2d97484fed50 100644 (file)
--- a/model.h
+++ b/model.h
@@ -13,8 +13,7 @@
 #include "action.h"
 
 /* Forward declaration */
-class TreeNode;
-class Backtrack;
+class NodeStack;
 
 class ModelChecker {
 public:
@@ -48,20 +47,20 @@ private:
        ModelAction * get_last_conflict(ModelAction *act);
        void set_backtracking(ModelAction *act);
        thread_id_t get_next_replay_thread();
-       Backtrack * get_next_backtrack();
+       ModelAction * get_next_backtrack();
        void reset_to_initial_state();
 
        void print_list(action_list_t *list);
 
-       class ModelAction *current_action;
-       Backtrack *exploring;
+       ModelAction *current_action;
+       ModelAction *diverge;
        thread_id_t nextThread;
 
        ucontext_t *system_context;
        action_list_t *action_trace;
        std::map<int, class Thread *> thread_map;
-       class TreeNode *rootNode, *currentNode;
-       std::list<class Backtrack *> backtrack_list;
+       class NodeStack *node_stack;
+       ModelAction *next_backtrack;
 };
 
 extern ModelChecker *model;