X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=3262f5e55caf992397d9134f24f2bba325cc4e87;hb=805a3e1b51dacac117b394f1c1b0220e3ae9f5e4;hp=e9d1f1df069cb5f0f1b79c9683143b59c4b39ffe;hpb=e048b80fa298a5228d71466f4b84c1c64094f2f3;p=c11tester.git diff --git a/model.cc b/model.cc index e9d1f1df..3262f5e5 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 @@ -31,7 +32,8 @@ ModelChecker::ModelChecker() 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()) { } @@ -49,6 +51,7 @@ ModelChecker::~ModelChecker() delete thrd_last_action; delete node_stack; delete scheduler; + delete cyclegraph; } /** @@ -159,7 +162,10 @@ bool ModelChecker::next_execution() DBG(); num_executions++; - print_summary(); + + if (isfeasible() || DBG_ENABLED()) + print_summary(); + if ((diverge = model->get_next_backtrack()) == NULL) return false; @@ -229,6 +235,11 @@ void ModelChecker::set_backtracking(ModelAction *act) } } +/** + * Returns last backtracking point. The model checker will explore a different + * path for this point in the next execution. + * @return The ModelAction at which the next execution should diverge. + */ ModelAction * ModelChecker::get_next_backtrack() { ModelAction *next = next_backtrack; @@ -246,6 +257,15 @@ void ModelChecker::check_current_action(void) return; } + if (curr->is_rmw()) { + //We have a RMW action + process_rmw(curr); + //Force the current thread to continue since the RMW should be atomic + nextThread = thread_current()->get_id(); + delete curr; + return; + } + tmp = node_stack->explore_action(curr); if (tmp) { /* Discard duplicate ModelAction; use action from NodeStack */ @@ -268,6 +288,10 @@ void ModelChecker::check_current_action(void) th->set_creation(curr); } + /* Is there a better interface for setting the next thread rather + than this field/convoluted approach? Perhaps like just returning + it or something? */ + nextThread = get_next_replay_thread(); Node *currnode = curr->get_node(); @@ -279,8 +303,6 @@ void ModelChecker::check_current_action(void) set_backtracking(curr); - add_action_to_lists(curr); - /* Assign reads_from values */ /* TODO: perform release/acquire synchronization here; include * reads_from as ModelAction member? */ @@ -291,8 +313,99 @@ void ModelChecker::check_current_action(void) 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); +} + +/** @returns whether the current trace is feasible. */ +bool ModelChecker::isfeasible() { + return !cyclegraph->checkForCycles(); +} + +/** Process a RMW by converting previous read into a RMW. */ +void ModelChecker::process_rmw(ModelAction * act) { + int tid = id_to_int(act->get_tid()); + std::vector *vec = &(*obj_thrd_map)[act->get_location()]; + ASSERT(tid < (int) vec->size()); + ModelAction *lastread=(*vec)[tid].back(); + lastread->upgrade_rmw(act); +} + +/** + * Updates the cyclegraph with the constraints imposed from the current read. + * @param curr The current action. Must be a read. + * @param rf The action that curr reads from. Must be a write. + */ +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; + } + } + } +} + +/** + * Updates the cyclegraph with the constraints imposed from the current write. + * @param curr The current action. Must be a write. + */ +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; + } + } + } } /** @@ -352,6 +465,11 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid) return parent; } +/** + * Returns the clock vector for a given thread. + * @param tid The thread whose clock vector we want + * @return Desired clock vector + */ ClockVector * ModelChecker::get_cv(thread_id_t tid) { return get_parent_action(tid)->get_cv(); } @@ -449,6 +567,8 @@ void ModelChecker::print_summary(void) scheduler->print(); + if (!isfeasible()) + printf("INFEASIBLE EXECUTION!\n"); print_list(action_trace); printf("\n"); }