X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=19d273de50bf67aa60cf6835845b21ac347fc7be;hb=f3ef22bef8d339c7d45b7d7232cdcf183a0b7776;hp=914ae3daccefa90aa0c24be3cff1d712c1e5b5a7;hpb=6c25cb78e05b059e0b57a6cf9cfd5637c58d936b;p=c11tester.git diff --git a/model.cc b/model.cc index 914ae3da..19d273de 100644 --- a/model.cc +++ b/model.cc @@ -1,78 +1,135 @@ #include #include "model.h" +#include "action.h" +#include "nodestack.h" #include "schedule.h" +#include "snapshot-interface.h" #include "common.h" +#include "clockvector.h" + +#define INITIAL_THREAD_ID 0 ModelChecker *model; +/** @brief Constructor */ ModelChecker::ModelChecker() -{ - /* First thread created (system_thread) will have id 1 */ - this->used_thread_id = 0; + : /* Initialize default scheduler */ - this->scheduler = new Scheduler(); - - num_executions = 0; - this->current_action = NULL; - this->exploring = NULL; - this->nextThread = THREAD_ID_T_NONE; - - rootNode = new TreeNode(NULL); - currentNode = rootNode; - action_trace = new action_list_t(); + scheduler(new Scheduler()), + /* First thread created will have id INITIAL_THREAD_ID */ + next_thread_id(INITIAL_THREAD_ID), + used_sequence_numbers(0), + + num_executions(0), + current_action(NULL), + diverge(NULL), + nextThread(THREAD_ID_T_NONE), + action_trace(new action_list_t()), + 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) +{ } +/** @brief Destructor */ ModelChecker::~ModelChecker() { + std::map::iterator it; + for (it = thread_map->begin(); it != thread_map->end(); it++) + delete (*it).second; + delete thread_map; + + delete obj_thrd_map; delete action_trace; - delete this->scheduler; - delete rootNode; + delete thrd_last_action; + delete node_stack; + delete scheduler; } -void ModelChecker::assign_id(Thread *t) +/** + * Restores user program to initial state and resets all model-checker data + * structures. + */ +void ModelChecker::reset_to_initial_state() { - t->set_id(++used_thread_id); + DEBUG("+++ Resetting to initial state +++\n"); + node_stack->reset_execution(); + current_action = NULL; + next_thread_id = INITIAL_THREAD_ID; + used_sequence_numbers = 0; + nextThread = 0; + next_backtrack = NULL; + snapshotObject->backTrackBeforeStep(0); } -void ModelChecker::add_system_thread(Thread *t) +/** @returns a thread ID for a new Thread */ +thread_id_t ModelChecker::get_next_id() { - this->system_thread = t; + return next_thread_id++; } -Thread *ModelChecker::schedule_next_thread() +/** @returns the number of user threads created during this execution */ +int ModelChecker::get_num_threads() +{ + return next_thread_id; +} + +/** @returns a sequence number for a new ModelAction */ +int ModelChecker::get_next_seq_num() +{ + return ++used_sequence_numbers; +} + +/** + * Performs the "scheduling" for the model-checker. That is, it checks if the + * model-checker has selected a "next thread to run" and returns it, if + * available. This function should be called from the Scheduler routine, where + * the Scheduler falls back to a default scheduling routine if needed. + * + * @return The next thread chosen by the model-checker. If the model-checker + * makes no selection, retuns NULL. + */ +Thread * ModelChecker::schedule_next_thread() { Thread *t; if (nextThread == THREAD_ID_T_NONE) return NULL; - t = thread_map[nextThread]; - if (t == NULL) - DEBUG("*** error: thread not in thread_map: id = %d\n", nextThread); + t = (*thread_map)[id_to_int(nextThread)]; + + ASSERT(t != NULL); + return t; } -/* - * get_next_replay_thread() - Choose the next thread in the replay sequence +/** + * Choose the next thread in the replay sequence. * - * If we've reached the 'diverge' point, then we pick a thread from the - * backtracking set. - * Otherwise, we simply return the next thread in the sequence. + * If the replay sequence has reached the 'diverge' point, returns a thread + * from the backtracking set. Otherwise, simply returns the next thread in the + * sequence that is being replayed. */ 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_node(); + 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(); } @@ -80,30 +137,34 @@ thread_id_t ModelChecker::get_next_replay_thread() return tid; } -thread_id_t ModelChecker::advance_backtracking_state() +/** + * Queries the model-checker for more executions to explore and, if one + * exists, resets the model-checker state to execute a new execution. + * + * @return If there are more executions to explore, return true. Otherwise, + * return false. + */ +bool ModelChecker::next_execution() { - /* Have we completed exploring the preselected path? */ - if (exploring == NULL) - return THREAD_ID_T_NONE; + DBG(); - /* Else, we are trying to replay an execution */ - exploring->advance_state(); - if (exploring->get_state() == NULL) - DEBUG("*** error: reached end of backtrack trace\n"); + num_executions++; + print_summary(); + if ((diverge = model->get_next_backtrack()) == NULL) + return false; - return get_next_replay_thread(); -} + if (DBG_ENABLED()) { + printf("Next execution will diverge at:\n"); + diverge->print(); + } -bool ModelChecker::next_execution() -{ - return false; + model->reset_to_initial_state(); + return true; } -ModelAction *ModelChecker::get_last_conflict(ModelAction *act) +ModelAction * ModelChecker::get_last_conflict(ModelAction *act) { - void *loc = act->get_location(); action_type type = act->get_type(); - thread_id_t id = act->get_tid(); switch (type) { case THREAD_CREATE: @@ -119,14 +180,8 @@ ModelAction *ModelChecker::get_last_conflict(ModelAction *act) action_list_t::reverse_iterator rit; for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) { ModelAction *prev = *rit; - if (prev->get_location() != loc) - continue; - if (type == ATOMIC_READ && prev->get_type() != ATOMIC_WRITE) - continue; - /* Conflict from the same thread is not really a conflict */ - if (id == prev->get_tid()) - return NULL; - return prev; + if (act->is_synchronizing(prev)) + return prev; } return NULL; } @@ -134,7 +189,8 @@ 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) @@ -142,52 +198,173 @@ void ModelChecker::set_backtracking(ModelAction *act) node = prev->get_node(); + while (!node->is_enabled(t)) + t = t->get_parent(); + /* Check if this has been explored already */ - if (node->hasBeenExplored(act->get_tid())) + 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(act->get_tid()) != 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(); + } +} - printf("Setting backtrack: conflict = %d, instead tid = %d\n", - prev->get_tid(), act->get_tid()); - prev->print(); - act->print(); - - Backtrack *back = new Backtrack(prev, action_trace); - backtrack_list.push_back(back); +ModelAction * ModelChecker::get_next_backtrack() +{ + 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; + ModelAction *tmp; + current_action = NULL; + if (!curr) { DEBUG("trying to push NULL action...\n"); return; } - nextThread = advance_backtracking_state(); - next->set_node(currentNode); - set_backtracking(next); - currentNode = currentNode->exploreChild(next->get_tid()); - this->action_trace->push_back(next); + + tmp = node_stack->explore_action(curr); + if (tmp) { + /* Discard duplicate ModelAction; use action from NodeStack */ + delete curr; + curr = tmp; + } else { + /* + * Perform one-time actions when pushing new ModelAction onto + * NodeStack + */ + curr->create_cv(get_parent_action(curr->get_tid())); + /* Build may_read_from set */ + if (curr->is_read()) + build_reads_from_past(curr); + } + + /* Assign 'creation' parent */ + if (curr->get_type() == THREAD_CREATE) { + Thread *th = (Thread *)curr->get_location(); + th->set_creation(curr); + } + + 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::print_trace(void) + +/** + * Adds an action to the per-object, per-thread action vector. + * @param act is the ModelAction to add. + */ + +void ModelChecker::add_action_to_lists(ModelAction *act) { - action_list_t::iterator it; + 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)]; +} + +ModelAction * ModelChecker::get_parent_action(thread_id_t tid) +{ + ModelAction *parent = get_last_action(tid); + if (!parent) + parent = get_thread(tid)->get_creation(); + return parent; +} + +/** + * Build up an initial set of all past writes that this 'read' action may read + * from. This set is determined by the clock vector's "happens before" + * relationship. + * @param curr is the current ModelAction that we are exploring; it must be a + * 'read' operation. + */ +void ModelChecker::build_reads_from_past(ModelAction *curr) +{ + std::vector *thrd_lists = &(*obj_thrd_map)[curr->get_location()]; + unsigned int i; + + ASSERT(curr->is_read()); + + for (i = 0; i < thrd_lists->size(); i++) { + action_list_t *list = &(*thrd_lists)[i]; + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *act = *rit; + + /* Only consider 'write' actions */ + if (!act->is_write()) + continue; + + DEBUG("Adding action to may_read_from:\n"); + if (DBG_ENABLED()) { + act->print(); + curr->print(); + } + curr->get_node()->add_read_from(act); + + /* Include at most one act that "happens before" curr */ + if (act->happens_before(curr)) + break; + } + } +} + +void ModelChecker::print_summary(void) +{ 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", node_stack->get_total_nodes()); scheduler->print(); - printf("\nTrace:\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"); @@ -195,56 +372,23 @@ void ModelChecker::print_trace(void) int ModelChecker::add_thread(Thread *t) { - thread_map[t->get_id()] = t; + (*thread_map)[id_to_int(t->get_id())] = t; + scheduler->add_thread(t); return 0; } +void ModelChecker::remove_thread(Thread *t) +{ + scheduler->remove_thread(t); +} + int ModelChecker::switch_to_master(ModelAction *act) { - Thread *old, *next; + Thread *old; DBG(); old = thread_current(); set_current_action(act); old->set_state(THREAD_READY); - next = system_thread; - return old->swap(next); -} - -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; -} - -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("Thread: %d\tAction: %s\tMO: %d\tLoc: %#014zx\tValue: %d\n", tid, type_str, order, (size_t)location, value); + return Thread::swap(old, get_system_context()); }