From a23393a8fa54e0318f3958838acbdec6d5d3d82a Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 14 May 2012 13:26:03 -0700 Subject: [PATCH] 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. --- action.h | 4 --- model.cc | 84 ++++++++++++++++++++++++++++---------------------------- model.h | 13 ++++----- 3 files changed, 48 insertions(+), 53 deletions(-) diff --git a/action.h b/action.h index cfe1f34..b30b650 100644 --- 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 c19c37f..e5af1a6 100644 --- 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 8651a4f..e8a8c5e 100644 --- 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 thread_map; - class TreeNode *rootNode, *currentNode; - std::list backtrack_list; + class NodeStack *node_stack; + ModelAction *next_backtrack; }; extern ModelChecker *model; -- 2.34.1