X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=0e24f1b0eaa91679726a8e805c6056acf89f824a;hp=93e06d0262de2b4c4d93bf8c9207f018b710cb3e;hb=187f2106785fe1ea4d34b0aee54d68468630675e;hpb=6cb1abb7f1f69690ecf78a293744204980912a7d diff --git a/model.cc b/model.cc index 93e06d02..0e24f1b0 100644 --- a/model.cc +++ b/model.cc @@ -7,6 +7,7 @@ #include "snapshot-interface.h" #include "common.h" #include "clockvector.h" +#include "cyclegraph.h" #define INITIAL_THREAD_ID 0 @@ -26,27 +27,31 @@ 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_map(new std::map()), obj_thrd_map(new std::map >()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), - next_backtrack(NULL) + next_backtrack(NULL), + cyclegraph(new CycleGraph()) { } /** @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; delete obj_thrd_map; + delete obj_map; delete action_trace; delete thrd_last_action; delete node_stack; delete scheduler; + delete cyclegraph; } /** @@ -78,7 +83,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; } @@ -124,11 +129,19 @@ thread_id_t ModelChecker::get_next_replay_thread() next = node_stack->get_next()->get_action(); if (next == diverge) { - Node *node = next->get_node(); - + Node *nextnode = next->get_node(); /* Reached divergence point */ + if (nextnode->increment_read_from()) { + /* The next node will read from a different value */ + tid = next->get_tid(); + node_stack->pop_restofstack(2); + } else { + /* Make a different thread execute for next step */ + Node *node = nextnode->get_parent(); + tid = node->get_next_backtrack(); + node_stack->pop_restofstack(1); + } DEBUG("*** Divergence point ***\n"); - tid = node->get_next_backtrack(); diverge = NULL; } else { tid = next->get_tid(); @@ -167,18 +180,17 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) action_type type = act->get_type(); switch (type) { - case THREAD_CREATE: - case THREAD_YIELD: - case THREAD_JOIN: - return NULL; case ATOMIC_READ: case ATOMIC_WRITE: - default: + case ATOMIC_RMW: break; + default: + return NULL; } /* linear search: from most recent to oldest */ + action_list_t *list = &(*obj_map)[act->get_location()]; action_list_t::reverse_iterator rit; - for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) { + for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; if (act->is_synchronizing(prev)) return prev; @@ -196,7 +208,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(); @@ -205,6 +217,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; @@ -228,8 +241,6 @@ ModelAction * ModelChecker::get_next_backtrack() void ModelChecker::check_current_action(void) { - Node *currnode; - ModelAction *curr = this->current_action; ModelAction *tmp; current_action = NULL; @@ -262,17 +273,101 @@ void ModelChecker::check_current_action(void) nextThread = get_next_replay_thread(); - currnode = curr->get_node(); + Node *currnode = curr->get_node(); + Node *parnode = currnode->get_parent(); - if (!currnode->backtrack_empty()) + if (!parnode->backtrack_empty()||!currnode->readsfrom_empty()) if (!next_backtrack || *curr > *next_backtrack) next_backtrack = curr; set_backtracking(curr); + /* Assign reads_from values */ + /* TODO: perform release/acquire synchronization here; include + * reads_from as ModelAction member? */ + Thread *th = get_thread(curr->get_tid()); + uint64_t value = VALUE_NONE; + if (curr->is_read()) { + const ModelAction *reads_from = curr->get_node()->get_read_from(); + value = reads_from->get_value(); + /* Assign reads_from, perform release/acquire synchronization */ + curr->read_from(reads_from); + r_modification_order(curr,reads_from); + } else if (curr->is_write()) { + w_modification_order(curr); + } + + th->set_return_value(value); + + /* Add action to list last. */ add_action_to_lists(curr); } +bool ModelChecker::isfeasible() { + return !cyclegraph->checkForCycles(); +} + +void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) { + std::vector *thrd_lists = &(*obj_thrd_map)[curr->get_location()]; + unsigned int i; + ASSERT(curr->is_read()); + + /* Iterate over all threads */ + for (i = 0; i < thrd_lists->size(); i++) { + /* Iterate over actions in thread, starting from most recent */ + action_list_t *list = &(*thrd_lists)[i]; + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *act = *rit; + + /* Include at most one act per-thread that "happens before" curr */ + if (act->happens_before(curr)) { + if (act->is_read()) { + const ModelAction * prevreadfrom=act->get_reads_from(); + if (rf!=prevreadfrom) + cyclegraph->addEdge(rf, prevreadfrom); + } else if (rf!=act) { + cyclegraph->addEdge(rf, act); + } + break; + } + } + } +} + +void ModelChecker::w_modification_order(ModelAction * curr) { + std::vector *thrd_lists = &(*obj_thrd_map)[curr->get_location()]; + unsigned int i; + ASSERT(curr->is_write()); + + if (curr->is_seqcst()) { + /* We have to at least see the last sequentially consistent write, + so we are initialized. */ + ModelAction * last_seq_cst=get_last_seq_cst(curr->get_location()); + if (last_seq_cst!=NULL) + cyclegraph->addEdge(curr, last_seq_cst); + } + + /* Iterate over all threads */ + for (i = 0; i < thrd_lists->size(); i++) { + /* Iterate over actions in thread, starting from most recent */ + action_list_t *list = &(*thrd_lists)[i]; + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *act = *rit; + + /* Include at most one act per-thread that "happens before" curr */ + if (act->happens_before(curr)) { + if (act->is_read()) { + cyclegraph->addEdge(curr, act->get_reads_from()); + } else + cyclegraph->addEdge(curr, act); + break; + } + } + } +} + /** * Performs various bookkeeping operations for the current ModelAction. For * instance, adds action to the per-object, per-thread action vector and to the @@ -282,14 +377,19 @@ void ModelChecker::check_current_action(void) */ void ModelChecker::add_action_to_lists(ModelAction *act) { + int tid = id_to_int(act->get_tid()); action_trace->push_back(act); + (*obj_map)[act->get_location()].push_back(act); + std::vector *vec = &(*obj_thrd_map)[act->get_location()]; - if (id_to_int(act->get_tid()) >= (int)vec->size()) + if (tid >= (int)vec->size()) vec->resize(next_thread_id); - (*vec)[id_to_int(act->get_tid())].push_back(act); + (*vec)[tid].push_back(act); - (*thrd_last_action)[id_to_int(act->get_tid())] = act; + if ((int)thrd_last_action->size() <= tid) + thrd_last_action->resize(get_num_threads()); + (*thrd_last_action)[tid] = act; } ModelAction * ModelChecker::get_last_action(thread_id_t tid) @@ -300,6 +400,23 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) return (*thrd_last_action)[id_to_int(tid)]; } +/** + * Gets the last memory_order_seq_cst action (in the total global sequence) + * performed on a particular object (i.e., memory location). + * @param location The object location to check + * @return The last seq_cst action performed + */ +ModelAction * ModelChecker::get_last_seq_cst(const void *location) +{ + action_list_t *list = &(*obj_map)[location]; + /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */ + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) + if ((*rit)->is_write() && (*rit)->is_seqcst()) + return *rit; + return NULL; +} + ModelAction * ModelChecker::get_parent_action(thread_id_t tid) { ModelAction *parent = get_last_action(tid); @@ -308,6 +425,10 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid) return parent; } +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" @@ -319,10 +440,24 @@ 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()); + ModelAction *last_seq_cst = NULL; + + /* Track whether this object has been initialized */ + bool initialized = false; + + if (curr->is_seqcst()) { + last_seq_cst = get_last_seq_cst(curr->get_location()); + /* We have to at least see the last sequentially consistent write, + so we are initialized. */ + if (last_seq_cst != NULL) + initialized = true; + } + + /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { + /* Iterate over actions in thread, starting from most recent */ action_list_t *list = &(*thrd_lists)[i]; action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { @@ -332,18 +467,38 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) if (!act->is_write()) continue; - DEBUG("Adding action to may_read_from:\n"); - if (DBG_ENABLED()) { - act->print(); - curr->print(); + /* Don't consider more than one seq_cst write if we are a seq_cst read. */ + if (!act->is_seqcst() || !curr->is_seqcst() || act == last_seq_cst) { + DEBUG("Adding action to may_read_from:\n"); + if (DBG_ENABLED()) { + act->print(); + curr->print(); + } + curr->get_node()->add_read_from(act); } - curr->get_node()->add_read_from(act); - /* Include at most one act that "happens before" curr */ - if (act->happens_before(curr)) + /* Include at most one act per-thread that "happens before" curr */ + if (act->happens_before(curr)) { + initialized = true; break; + } } } + + if (!initialized) { + /* TODO: need a more informative way of reporting errors */ + printf("ERROR: may read from uninitialized atomic\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); } static void print_list(action_list_t *list) @@ -361,10 +516,18 @@ static void print_list(action_list_t *list) void ModelChecker::print_summary(void) { + if (!isfeasible()) { + if (DBG_ENABLED()) + printf("INFEASIBLE EXECUTION!\n"); + else + return; + } + 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); @@ -383,6 +546,17 @@ void ModelChecker::remove_thread(Thread *t) scheduler->remove_thread(t); } +/** + * Switch from a user-context to the "master thread" context (a.k.a. system + * context). This switch is made with the intention of exploring a particular + * model-checking action (described by a ModelAction object). Must be called + * from a user-thread context. + * @param act The current action that will be explored. May be NULL, although + * there is little reason to switch to the model-checker without an action to + * explore (note: act == NULL is sometimes used as a hack to allow a thread to + * yield control without performing any progress; see thrd_join()). + * @return Return status from the 'swap' call (i.e., success/fail, 0/-1) + */ int ModelChecker::switch_to_master(ModelAction *act) { Thread *old;