X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=41e4421c52f3c8b8c932330523771c7a32622649;hp=27b6cd6a9df24856be3c9b2cc712eb2972ae98f3;hb=9e9096d119abfeed4753a5944b31916ae559e22e;hpb=ebab3e51073b1534ba5d9ce944568d933d16fb3d diff --git a/model.cc b/model.cc index 27b6cd6..41e4421 100644 --- a/model.cc +++ b/model.cc @@ -6,6 +6,7 @@ #include "schedule.h" #include "snapshot-interface.h" #include "common.h" +#include "clockvector.h" #define INITIAL_THREAD_ID 0 @@ -25,7 +26,7 @@ ModelChecker::ModelChecker() diverge(NULL), nextThread(THREAD_ID_T_NONE), action_trace(new action_list_t()), - thread_map(new std::map), + thread_map(new std::map), obj_thrd_map(new std::map >()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), @@ -36,7 +37,7 @@ ModelChecker::ModelChecker() /** @brief Destructor */ ModelChecker::~ModelChecker() { - std::map::iterator it; + std::map::iterator it; for (it = thread_map->begin(); it != thread_map->end(); it++) delete (*it).second; delete thread_map; @@ -77,7 +78,7 @@ int ModelChecker::get_num_threads() } /** @returns a sequence number for a new ModelAction */ -int ModelChecker::get_next_seq_num() +modelclock_t ModelChecker::get_next_seq_num() { return ++used_sequence_numbers; } @@ -123,7 +124,7 @@ thread_id_t ModelChecker::get_next_replay_thread() next = node_stack->get_next()->get_action(); if (next == diverge) { - Node *node = next->get_node(); + Node *node = next->get_node()->get_parent(); /* Reached divergence point */ DEBUG("*** Divergence point ***\n"); @@ -195,7 +196,7 @@ void ModelChecker::set_backtracking(ModelAction *act) if (prev == NULL) return; - node = prev->get_node(); + node = prev->get_node()->get_parent(); while (!node->is_enabled(t)) t = t->get_parent(); @@ -204,6 +205,7 @@ void ModelChecker::set_backtracking(ModelAction *act) if (node->has_been_explored(t->get_id())) return; + /* Cache the latest backtracking point */ if (!next_backtrack || *prev > *next_backtrack) next_backtrack = prev; @@ -230,14 +232,28 @@ void ModelChecker::check_current_action(void) Node *currnode; ModelAction *curr = this->current_action; + ModelAction *tmp; current_action = NULL; if (!curr) { DEBUG("trying to push NULL action...\n"); return; } - curr = node_stack->explore_action(curr); - curr->create_cv(get_parent_action(curr->get_tid())); + 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) { @@ -247,7 +263,7 @@ void ModelChecker::check_current_action(void) nextThread = get_next_replay_thread(); - currnode = curr->get_node(); + currnode = curr->get_node()->get_parent(); if (!currnode->backtrack_empty()) if (!next_backtrack || *curr > *next_backtrack) @@ -258,6 +274,13 @@ void ModelChecker::check_current_action(void) add_action_to_lists(curr); } +/** + * Performs various bookkeeping operations for the current ModelAction. For + * instance, adds action to the per-object, per-thread action vector and to the + * action trace list of all thread actions. + * + * @param act is the ModelAction to add. + */ void ModelChecker::add_action_to_lists(ModelAction *act) { action_trace->push_back(act); @@ -286,19 +309,69 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid) return parent; } -void ModelChecker::print_summary(void) +ClockVector * ModelChecker::get_cv(thread_id_t tid) { + return get_parent_action(tid)->get_cv(); +} + +/** + * 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) { - printf("\n"); - printf("Number of executions: %d\n", num_executions); - printf("Total nodes created: %d\n", node_stack->get_total_nodes()); + std::vector *thrd_lists = &(*obj_thrd_map)[curr->get_location()]; + unsigned int i; + + ASSERT(curr->is_read()); + + /* Track whether this object has been initialized */ + bool initialized = false; + + 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 per-thread that "happens before" curr */ + if (act->happens_before(curr)) { + initialized = true; + break; + } + } + } - scheduler->print(); + if (!initialized) { + /* TODO: need a more informative way of reporting errors */ + printf("ERROR: may read from uninitialized atomic\n"); + } - print_list(action_trace); - printf("\n"); + if (DBG_ENABLED() || !initialized) { + printf("Reached read action:\n"); + curr->print(); + printf("Printing may_read_from\n"); + curr->get_node()->print_may_read_from(); + printf("End printing may_read_from\n"); + } + + ASSERT(initialized); } -void ModelChecker::print_list(action_list_t *list) +static void print_list(action_list_t *list) { action_list_t::iterator it; @@ -311,6 +384,18 @@ void ModelChecker::print_list(action_list_t *list) printf("---------------------------------------------------------------------\n"); } +void ModelChecker::print_summary(void) +{ + printf("\n"); + printf("Number of executions: %d\n", num_executions); + printf("Total nodes created: %d\n", node_stack->get_total_nodes()); + + scheduler->print(); + + print_list(action_trace); + printf("\n"); +} + int ModelChecker::add_thread(Thread *t) { (*thread_map)[id_to_int(t->get_id())] = t;