X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=142ae3efdfab1bf0812350a5fc89d37ea45c21b9;hb=c3ec6bb763ab72e04596bbdfb534578aab545d8f;hp=142e862c0cbfd898a01d638eb9b4dbec9976bc68;hpb=2f3e4e24140493a96a7ece89429d294546a9e0c0;p=model-checker.git diff --git a/model.cc b/model.cc index 142e862..142ae3e 100644 --- a/model.cc +++ b/model.cc @@ -2,42 +2,15 @@ #include "model.h" #include "action.h" -#include "tree.h" +#include "nodestack.h" #include "schedule.h" +#include "snapshot-interface.h" #include "common.h" #define INITIAL_THREAD_ID 0 -class Backtrack { -public: - Backtrack(ModelAction *d, action_list_t *t) { - diverge = d; - actionTrace = t; - iter = actionTrace->begin(); - } - ModelAction * get_diverge() { return diverge; } - action_list_t * get_trace() { return actionTrace; } - void advance_state() { iter++; } - ModelAction * get_state() { - return iter == actionTrace->end() ? NULL : *iter; - } -private: - ModelAction *diverge; - action_list_t *actionTrace; - /* points to position in actionTrace as we replay */ - action_list_t::iterator iter; -}; - ModelChecker *model; -void free_action_list(action_list_t *list) -{ - action_list_t::iterator it; - for (it = list->begin(); it != list->end(); it++) - delete (*it); - delete list; -} - ModelChecker::ModelChecker() : /* Initialize default scheduler */ @@ -48,40 +21,41 @@ 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) + thread_map(new std::map), + obj_thrd_map(new std::map >()), + thrd_last_action(new std::vector(1)), + node_stack(new NodeStack()), + next_backtrack(NULL) { } ModelChecker::~ModelChecker() { std::map::iterator it; - for (it = thread_map.begin(); it != thread_map.end(); it++) + for (it = thread_map->begin(); it != thread_map->end(); it++) delete (*it).second; - thread_map.clear(); - - free_action_list(action_trace); + delete thread_map; + delete obj_thrd_map; + delete action_trace; + delete thrd_last_action; + delete node_stack; delete scheduler; - delete rootNode; } void ModelChecker::reset_to_initial_state() { DEBUG("+++ Resetting to initial state +++\n"); - std::map::iterator it; - for (it = thread_map.begin(); it != thread_map.end(); it++) - delete (*it).second; - thread_map.clear(); - 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; - /* scheduler reset ? */ + nextThread = 0; + next_backtrack = NULL; + snapshotObject->backTrackBeforeStep(0); } thread_id_t ModelChecker::get_next_id() @@ -89,6 +63,11 @@ thread_id_t ModelChecker::get_next_id() return next_thread_id++; } +int ModelChecker::get_num_threads() +{ + return next_thread_id; +} + int ModelChecker::get_next_seq_num() { return ++used_sequence_numbers; @@ -99,7 +78,7 @@ Thread * ModelChecker::schedule_next_thread() Thread *t; if (nextThread == THREAD_ID_T_NONE) return NULL; - t = thread_map[id_to_int(nextThread)]; + t = (*thread_map)[id_to_int(nextThread)]; ASSERT(t != NULL); @@ -118,16 +97,20 @@ thread_id_t ModelChecker::get_next_replay_thread() ModelAction *next; thread_id_t tid; - next = exploring->get_state(); + /* Have we completed exploring the preselected path? */ + if (diverge == NULL) + return THREAD_ID_T_NONE; + + /* Else, we are trying to replay an execution */ + next = node_stack->get_next()->get_action(); - if (next == exploring->get_diverge()) { - TreeNode *node = next->get_treenode(); + if (next == diverge) { + Node *node = next->get_node(); - /* 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(); } @@ -135,37 +118,21 @@ thread_id_t ModelChecker::get_next_replay_thread() return tid; } -thread_id_t ModelChecker::advance_backtracking_state() -{ - /* Have we completed exploring the preselected path? */ - if (exploring == NULL) - return THREAD_ID_T_NONE; - - /* Else, we are trying to replay an execution */ - exploring->advance_state(); - - ASSERT(exploring->get_state() != NULL); - - return get_next_replay_thread(); -} - bool ModelChecker::next_execution() { DBG(); 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(); - nextThread = get_next_replay_thread(); return true; } @@ -196,73 +163,99 @@ 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) { - ModelAction *next = this->current_action; + Node *currnode; - if (!next) { + ModelAction *curr = this->current_action; + current_action = NULL; + if (!curr) { DEBUG("trying to push NULL action...\n"); return; } - current_action = NULL; - nextThread = advance_backtracking_state(); - next->set_node(currentNode); - set_backtracking(next); - currentNode = currentNode->explore_child(next); - this->action_trace->push_back(next); + + /* TODO: if get_last_action() is NULL, sync with parent thread */ + curr = node_stack->explore_action(curr, get_last_action(curr->get_tid())); + nextThread = get_next_replay_thread(); + + currnode = curr->get_node(); + + if (!currnode->backtrack_empty()) + if (!next_backtrack || *curr > *next_backtrack) + next_backtrack = curr; + + set_backtracking(curr); + + add_action_to_lists(curr); +} + +void ModelChecker::add_action_to_lists(ModelAction *act) +{ + action_trace->push_back(act); + + std::vector *vec = &(*obj_thrd_map)[act->get_location()]; + if (id_to_int(act->get_tid()) >= (int)vec->size()) + vec->resize(next_thread_id); + (*vec)[id_to_int(act->get_tid())].push_back(act); + + (*thrd_last_action)[id_to_int(act->get_tid())] = act; +} + +ModelAction * ModelChecker::get_last_action(thread_id_t tid) +{ + int nthreads = get_num_threads(); + if ((int)thrd_last_action->size() < nthreads) + thrd_last_action->resize(nthreads); + return (*thrd_last_action)[id_to_int(tid)]; } 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) @@ -280,7 +273,7 @@ void ModelChecker::print_list(action_list_t *list) int ModelChecker::add_thread(Thread *t) { - thread_map[id_to_int(t->get_id())] = t; + (*thread_map)[id_to_int(t->get_id())] = t; scheduler->add_thread(t); return 0; }