X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=53411c64199529dcea4e463d1bb058f2ea6898ab;hb=d6132c396ec2037c65e1b72382679a8e98781e29;hp=c3452b07e5e7c502384ddfd2c8a0c981be2bf620;hpb=3e0ad5e987371d52c9377a12cff4c4dec2b6fd81;p=model-checker.git diff --git a/model.cc b/model.cc index c3452b0..53411c6 100644 --- a/model.cc +++ b/model.cc @@ -8,30 +8,64 @@ #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() { - /* First thread created will have id (INITIAL_THREAD_ID + 1) */ - this->used_thread_id = INITIAL_THREAD_ID; + /* First thread created will have id INITIAL_THREAD_ID */ + next_thread_id = INITIAL_THREAD_ID; used_sequence_numbers = 0; /* Initialize default scheduler */ - this->scheduler = new Scheduler(); + scheduler = new Scheduler(); num_executions = 0; - this->current_action = NULL; - this->exploring = NULL; - this->nextThread = THREAD_ID_T_NONE; + current_action = NULL; + exploring = NULL; + nextThread = THREAD_ID_T_NONE; - rootNode = new TreeNode(NULL); + rootNode = new TreeNode(); currentNode = rootNode; action_trace = new action_list_t(); } ModelChecker::~ModelChecker() { - delete action_trace; - delete this->scheduler; + std::map::iterator it; + for (it = thread_map.begin(); it != thread_map.end(); it++) + delete (*it).second; + thread_map.clear(); + + free_action_list(action_trace); + + delete scheduler; delete rootNode; } @@ -45,14 +79,14 @@ void ModelChecker::reset_to_initial_state() action_trace = new action_list_t(); currentNode = rootNode; current_action = NULL; - used_thread_id = INITIAL_THREAD_ID; + next_thread_id = INITIAL_THREAD_ID; used_sequence_numbers = 0; /* scheduler reset ? */ } thread_id_t ModelChecker::get_next_id() { - return ++used_thread_id; + return next_thread_id++; } int ModelChecker::get_next_seq_num() @@ -66,8 +100,9 @@ Thread * ModelChecker::schedule_next_thread() if (nextThread == THREAD_ID_T_NONE) return NULL; t = thread_map[id_to_int(nextThread)]; - if (t == NULL) - DEBUG("*** error: thread not in thread_map: id = %d\n", nextThread); + + ASSERT(t != NULL); + return t; } @@ -86,7 +121,7 @@ thread_id_t ModelChecker::get_next_replay_thread() next = exploring->get_state(); if (next == exploring->get_diverge()) { - TreeNode *node = next->get_node(); + TreeNode *node = next->get_treenode(); /* Reached divergence point; discard our current 'exploring' */ DEBUG("*** Discard 'Backtrack' object ***\n"); @@ -108,18 +143,27 @@ thread_id_t ModelChecker::advance_backtracking_state() /* Else, we are trying to replay an execution */ exploring->advance_state(); - if (exploring->get_state() == NULL) - DEBUG("*** error: reached end of backtrack trace\n"); + + 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) return false; + + if (DBG_ENABLED()) { + printf("Next execution will diverge at:\n"); + exploring->get_diverge()->print(); + print_list(exploring->get_trace()); + } + model->reset_to_initial_state(); nextThread = get_next_replay_thread(); return true; @@ -153,22 +197,26 @@ void ModelChecker::set_backtracking(ModelAction *act) { ModelAction *prev; TreeNode *node; + Thread *t = get_thread(act->get_tid()); prev = get_last_conflict(act); if (prev == NULL) return; - node = prev->get_node(); + node = prev->get_treenode(); + + while (t && !node->is_enabled(t)) + t = t->get_parent(); /* Check if this has been explored already */ - if (node->hasBeenExplored(act->get_tid())) + if (node->hasBeenExplored(t->get_id())) return; /* If this is a new backtracking point, mark the tree */ - if (node->setBacktrack(act->get_tid()) != 0) + if (node->setBacktrack(t->get_id()) != 0) return; DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n", - prev->get_tid(), act->get_tid()); + prev->get_tid(), t->get_id()); if (DBG_ENABLED()) { prev->print(); act->print(); @@ -200,25 +248,31 @@ void ModelChecker::check_current_action(void) nextThread = advance_backtracking_state(); next->set_node(currentNode); set_backtracking(next); - currentNode = currentNode->exploreChild(next->get_tid()); + currentNode = currentNode->explore_child(next); this->action_trace->push_back(next); } void ModelChecker::print_summary(void) { - action_list_t::iterator it; - printf("\n"); - printf("---------------------------------------------------------------------\n"); printf("Number of executions: %d\n", num_executions); - printf("Total nodes created: %d\n\n", TreeNode::getTotalNodes()); + printf("Total nodes created: %d\n", TreeNode::getTotalNodes()); scheduler->print(); - printf("Trace:\n\n"); + print_list(action_trace); + printf("\n"); + +} + +void ModelChecker::print_list(action_list_t *list) +{ + action_list_t::iterator it; + + printf("---------------------------------------------------------------------\n"); + printf("Trace:\n"); - for (it = action_trace->begin(); it != action_trace->end(); it++) { - DBG(); + for (it = list->begin(); it != list->end(); it++) { (*it)->print(); } printf("---------------------------------------------------------------------\n"); @@ -246,99 +300,3 @@ int ModelChecker::switch_to_master(ModelAction *act) old->set_state(THREAD_READY); return Thread::swap(old, get_system_context()); } - -ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value) -{ - Thread *t = thread_current(); - ModelAction *act = this; - - act->type = type; - act->order = order; - act->location = loc; - act->tid = t->get_id(); - act->value = value; - act->seq_number = model->get_next_seq_num(); -} - -bool ModelAction::is_read() -{ - return type == ATOMIC_READ; -} - -bool ModelAction::is_write() -{ - return type == ATOMIC_WRITE; -} - -bool ModelAction::is_acquire() -{ - switch (order) { - case memory_order_acquire: - case memory_order_acq_rel: - case memory_order_seq_cst: - return true; - default: - return false; - } -} - -bool ModelAction::is_release() -{ - switch (order) { - case memory_order_release: - case memory_order_acq_rel: - case memory_order_seq_cst: - return true; - default: - return false; - } -} - -bool ModelAction::same_var(ModelAction *act) -{ - return location == act->location; -} - -bool ModelAction::same_thread(ModelAction *act) -{ - return tid == act->tid; -} - -bool ModelAction::is_dependent(ModelAction *act) -{ - if (!is_read() && !is_write()) - return false; - if (!act->is_read() && !act->is_write()) - return false; - if (same_var(act) && !same_thread(act) && - (is_write() || act->is_write())) - return true; - return false; -} - -void ModelAction::print(void) -{ - const char *type_str; - switch (this->type) { - case THREAD_CREATE: - type_str = "thread create"; - break; - case THREAD_YIELD: - type_str = "thread yield"; - break; - case THREAD_JOIN: - type_str = "thread join"; - break; - case ATOMIC_READ: - type_str = "atomic read"; - break; - case ATOMIC_WRITE: - type_str = "atomic write"; - break; - default: - type_str = "unknown type"; - } - - printf("(%4d) Thread: %d\tAction: %s\tMO: %d\tLoc: %14p\tValue: %d\n", - seq_number, id_to_int(tid), type_str, order, location, value); -}