X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=44c7e353d79b5f8cd87de1f50763c1b705b6224e;hb=1f89a2b5691c26417c93d283e73e181bc6cea1a5;hp=d8699b0ebfe850b3a0a8d3d277f3ca914db0b59f;hpb=bbf356ecc0554af1ecff878e305055ac1673d75e;p=c11tester.git diff --git a/model.cc b/model.cc index d8699b0e..44c7e353 100644 --- a/model.cc +++ b/model.cc @@ -15,14 +15,14 @@ ModelChecker *model; /** @brief Constructor */ -ModelChecker::ModelChecker() - : +ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ 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), + params(params), current_action(NULL), diverge(NULL), nextThread(THREAD_ID_T_NONE), @@ -42,9 +42,8 @@ ModelChecker::ModelChecker() /** @brief Destructor */ ModelChecker::~ModelChecker() { - /* std::map::iterator it; - for (it = thread_map->begin(); it != thread_map->end(); it++) - delete (*it).second;*/ + for (int i = 0; i < get_num_threads(); i++) + delete thread_map->get(i); delete thread_map; delete obj_thrd_map; @@ -133,7 +132,7 @@ thread_id_t ModelChecker::get_next_replay_thread() if (next == diverge) { Node *nextnode = next->get_node(); /* Reached divergence point */ - if (nextnode->increment_promises()) { + if (nextnode->increment_promise()) { /* The next node will try to satisfy a different set of promises. */ tid = next->get_tid(); node_stack->pop_restofstack(2); @@ -141,7 +140,7 @@ thread_id_t ModelChecker::get_next_replay_thread() /* The next node will read from a different value. */ tid = next->get_tid(); node_stack->pop_restofstack(2); - } else if (nextnode->increment_future_values()) { + } else if (nextnode->increment_future_value()) { /* The next node will try to read from a different future value. */ tid = next->get_tid(); node_stack->pop_restofstack(2); @@ -173,7 +172,7 @@ bool ModelChecker::next_execution() num_executions++; - if (isfeasible() || DBG_ENABLED()) + if (isfinalfeasible() || DBG_ENABLED()) print_summary(); if ((diverge = model->get_next_backtrack()) == NULL) @@ -267,11 +266,11 @@ void ModelChecker::check_current_action(void) return; } - if (curr->is_rmwc()||curr->is_rmw()) { - ModelAction *tmp=process_rmw(curr); + if (curr->is_rmwc() || curr->is_rmw()) { + ModelAction *tmp = process_rmw(curr); already_added = true; delete curr; - curr=tmp; + curr = tmp; } else { ModelAction * tmp = node_stack->explore_action(curr); if (tmp) { @@ -279,6 +278,11 @@ void ModelChecker::check_current_action(void) /* First restore type and order in case of RMW operation */ if (curr->is_rmwr()) tmp->copy_typeandorder(curr); + + /* If we have diverged, we need to reset the clock vector. */ + if (diverge == NULL) + tmp->create_cv(get_parent_action(tmp->get_tid())); + delete curr; curr = tmp; } else { @@ -302,16 +306,15 @@ void ModelChecker::check_current_action(void) } /* Deal with new thread */ - if (curr->get_type() == THREAD_START) { + if (curr->get_type() == THREAD_START) check_promises(NULL, curr->get_cv()); - } /* Assign reads_from values */ 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(); - if (reads_from!=NULL) { + if (reads_from != NULL) { value = reads_from->get_value(); /* Assign reads_from, perform release/acquire synchronization */ curr->read_from(reads_from); @@ -320,7 +323,7 @@ void ModelChecker::check_current_action(void) /* Read from future value */ value = curr->get_node()->get_future_value(); curr->read_from(NULL); - Promise * valuepromise=new Promise(curr, value); + Promise * valuepromise = new Promise(curr, value); promises->push_back(valuepromise); } } else if (curr->is_write()) { @@ -334,36 +337,41 @@ void ModelChecker::check_current_action(void) if (!already_added) add_action_to_lists(curr); - /* Is there a better interface for setting the next thread rather + /** @todo Is there a better interface for setting the next thread rather than this field/convoluted approach? Perhaps like just returning it or something? */ /* Do not split atomic actions. */ - if (curr->is_rmwr()) { + if (curr->is_rmwr()) nextThread = thread_current()->get_id(); - } else { + else nextThread = get_next_replay_thread(); - } Node *currnode = curr->get_node(); Node *parnode = currnode->get_parent(); - if (!parnode->backtrack_empty()||!currnode->readsfrom_empty()||!currnode->futurevalues_empty()||!currnode->promises_empty()) + if (!parnode->backtrack_empty() || !currnode->read_from_empty() || + !currnode->future_value_empty() || !currnode->promise_empty()) if (!next_backtrack || *curr > *next_backtrack) next_backtrack = curr; - + set_backtracking(curr); } -/** @returns whether the current trace is feasible. */ +/** @returns whether the current partial trace is feasible. */ bool ModelChecker::isfeasible() { return !cyclegraph->checkForCycles() && !failed_promise; } +/** Returns whether the current completed trace is feasible. */ +bool ModelChecker::isfinalfeasible() { + return isfeasible() && promises->size() == 0; +} + /** Close out a RMWR by converting previous RMWR into a RMW or READ. */ ModelAction * ModelChecker::process_rmw(ModelAction * act) { int tid = id_to_int(act->get_tid()); - ModelAction *lastread=get_last_action(tid); + ModelAction *lastread = get_last_action(tid); lastread->process_rmw(act); if (act->is_rmw()) cyclegraph->addRMWEdge(lastread, lastread->get_reads_from()); @@ -391,10 +399,10 @@ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *r /* 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) + const ModelAction * prevreadfrom = act->get_reads_from(); + if (prevreadfrom != NULL && rf != prevreadfrom) cyclegraph->addEdge(rf, prevreadfrom); - } else if (rf!=act) { + } else if (rf != act) { cyclegraph->addEdge(rf, act); } break; @@ -403,6 +411,43 @@ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *r } } +/** Updates the cyclegraph with the constraints imposed from the + * current read. */ +void ModelChecker::post_r_modification_order(ModelAction * curr, const ModelAction *rf) { + std::vector *thrd_lists = obj_thrd_map->ensureptr(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; + ModelAction *lastact = NULL; + + /* Find last action that happens after curr */ + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *act = *rit; + if (curr->happens_before(act)) { + lastact = act; + } else + break; + } + + /* Include at most one act per-thread that "happens before" curr */ + if (lastact != NULL) { + if (lastact->is_read()) { + const ModelAction * postreadfrom = lastact->get_reads_from(); + if (postreadfrom != NULL&&rf != postreadfrom) + cyclegraph->addEdge(postreadfrom, rf); + } else if (rf != lastact) { + cyclegraph->addEdge(lastact, rf); + } + break; + } + } +} + /** * Updates the cyclegraph with the constraints imposed from the current write. * @param curr The current action. Must be a write. @@ -415,8 +460,8 @@ void ModelChecker::w_modification_order(ModelAction * curr) { 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) + ModelAction * last_seq_cst = get_last_seq_cst(curr->get_location()); + if (last_seq_cst != NULL) cyclegraph->addEdge(curr, last_seq_cst); } @@ -430,26 +475,24 @@ void ModelChecker::w_modification_order(ModelAction * curr) { /* Include at most one act per-thread that "happens before" curr */ if (act->happens_before(curr)) { - if (act->is_read()) { + if (act->is_read()) cyclegraph->addEdge(curr, act->get_reads_from()); - } else + else cyclegraph->addEdge(curr, act); break; - } else { - if (act->is_read()&&!act->is_synchronizing(curr)&&!act->same_thread(curr)) { - /* We have an action that: - (1) did not happen before us - (2) is a read and we are a write - (3) cannot synchronize with us - (4) is in a different thread - => - that read could potentially read from our write. - */ - - if (act->get_node()->add_future_value(curr->get_value())&& - (!next_backtrack || *act > * next_backtrack)) - next_backtrack = act; - } + } else if (act->is_read() && !act->is_synchronizing(curr) && + !act->same_thread(curr)) { + /* We have an action that: + (1) did not happen before us + (2) is a read and we are a write + (3) cannot synchronize with us + (4) is in a different thread + => + that read could potentially read from our write. + */ + if (act->get_node()->add_future_value(curr->get_value()) && + (!next_backtrack || *act > *next_backtrack)) + next_backtrack = act; } } } @@ -522,28 +565,34 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) { } -/** Resolve promises. */ +/** Resolve the given promises. */ void ModelChecker::resolve_promises(ModelAction *write) { - for(unsigned int i=0;isize();i++) { - Promise * promise=(*promises)[i]; + for (unsigned int i = 0, promise_index = 0;promise_indexsize(); i++) { + Promise * promise = (*promises)[promise_index]; if (write->get_node()->get_promise(i)) { - ModelAction * read=promise->get_action(); + ModelAction * read = promise->get_action(); read->read_from(write); r_modification_order(read, write); - } + post_r_modification_order(read, write); + promises->erase(promises->begin()+promise_index); + } else + promise_index++; } } +/** Compute the set of promises that could potentially be satisfied by + * this action. */ + void ModelChecker::compute_promises(ModelAction *curr) { - for(unsigned int i=0;isize();i++) { - Promise * promise=(*promises)[i]; - const ModelAction * act=promise->get_action(); + for (unsigned int i = 0;isize();i++) { + Promise * promise = (*promises)[i]; + const ModelAction * act = promise->get_action(); if (!act->happens_before(curr)&& act->is_read()&& !act->is_synchronizing(curr)&& !act->same_thread(curr)&& - promise->get_value()==curr->get_value()) { + promise->get_value() == curr->get_value()) { curr->get_node()->set_promise(i); } } @@ -552,14 +601,14 @@ void ModelChecker::compute_promises(ModelAction *curr) { /** Checks promises in response to change in ClockVector Threads. */ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector * merge_cv) { - for(unsigned int i=0;isize();i++) { - Promise * promise=(*promises)[i]; - const ModelAction * act=promise->get_action(); - if ((old_cv==NULL||!old_cv->synchronized_since(act))&& + for (unsigned int i = 0;isize();i++) { + Promise * promise = (*promises)[i]; + const ModelAction * act = promise->get_action(); + if ((old_cv == NULL||!old_cv->synchronized_since(act))&& merge_cv->synchronized_since(act)) { //This thread is no longer able to send values back to satisfy the promise - int num_synchronized_threads=promise->increment_threads(); - if (num_synchronized_threads==model->get_num_threads()) { + int num_synchronized_threads = promise->increment_threads(); + if (num_synchronized_threads == model->get_num_threads()) { //Promise has failed failed_promise = true; return; @@ -601,7 +650,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) 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; @@ -653,7 +702,7 @@ static void print_list(action_list_t *list) printf("---------------------------------------------------------------------\n"); } -void ModelChecker::print_summary(void) +void ModelChecker::print_summary() { printf("\n"); printf("Number of executions: %d\n", num_executions); @@ -661,17 +710,21 @@ void ModelChecker::print_summary(void) scheduler->print(); - if (!isfeasible()) + if (!isfinalfeasible()) printf("INFEASIBLE EXECUTION!\n"); print_list(action_trace); printf("\n"); } -int ModelChecker::add_thread(Thread *t) +/** + * Add a Thread to the system for the first time. Should only be called once + * per thread. + * @param t The Thread to add + */ +void ModelChecker::add_thread(Thread *t) { thread_map->put(id_to_int(t->get_id()), t); scheduler->add_thread(t); - return 0; } void ModelChecker::remove_thread(Thread *t) @@ -696,5 +749,48 @@ int ModelChecker::switch_to_master(ModelAction *act) Thread * old = thread_current(); set_current_action(act); old->set_state(THREAD_READY); - return Thread::swap(old, get_system_context()); + return Thread::swap(old, &system_context); +} + +/** + * Takes the next step in the execution, if possible. + * @return Returns true (success) if a step was taken and false otherwise. + */ +bool ModelChecker::take_step() { + Thread *curr, *next; + + curr = thread_current(); + if (curr) { + if (curr->get_state() == THREAD_READY) { + check_current_action(); + scheduler->add_thread(curr); + } else if (curr->get_state() == THREAD_RUNNING) { + /* Stopped while running; i.e., completed */ + curr->complete(); + } else { + ASSERT(false); + } + } + next = scheduler->next_thread(); + + /* Infeasible -> don't take any more steps */ + if (!isfeasible()) + return false; + + if (next) + next->set_state(THREAD_RUNNING); + DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1); + + /* next == NULL -> don't take any more steps */ + if (!next) + return false; + /* Return false only if swap fails with an error */ + return (Thread::swap(&system_context, next) == 0); +} + +/** Runs the current execution until threre are no more steps to take. */ +void ModelChecker::finish_execution() { + DBG(); + + while (take_step()); }