X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=b456c246468cd7d5674e65bfe42ff2cd4a348462;hb=b118d83f84a47a6ac778ed8ea43030d477b0bc9c;hp=e18fda15248399cda859339296447ca2b35bd9f5;hpb=84e24d516d4e9dbd30f1fff7e9a185d1540d20eb;p=model-checker.git diff --git a/model.cc b/model.cc index e18fda1..b456c24 100644 --- a/model.cc +++ b/model.cc @@ -8,41 +8,42 @@ #include "common.h" #include "clockvector.h" #include "cyclegraph.h" +#include "promise.h" #define INITIAL_THREAD_ID 0 ModelChecker *model; /** @brief Constructor */ -ModelChecker::ModelChecker() - : +ModelChecker::ModelChecker() : /* 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), current_action(NULL), diverge(NULL), nextThread(THREAD_ID_T_NONE), action_trace(new action_list_t()), - thread_map(new std::map), - obj_map(new std::map()), - obj_thrd_map(new std::map >()), + thread_map(new HashTable()), + obj_map(new HashTable()), + obj_thrd_map(new HashTable, uintptr_t, 4 >()), + promises(new std::vector()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), next_backtrack(NULL), - cyclegraph(new CycleGraph()) + cyclegraph(new CycleGraph()), + failed_promise(false) { } /** @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 (*it).second;*/ delete thread_map; delete obj_thrd_map; @@ -67,6 +68,7 @@ void ModelChecker::reset_to_initial_state() used_sequence_numbers = 0; nextThread = 0; next_backtrack = NULL; + failed_promise = false; snapshotObject->backTrackBeforeStep(0); } @@ -102,7 +104,7 @@ Thread * ModelChecker::schedule_next_thread() Thread *t; if (nextThread == THREAD_ID_T_NONE) return NULL; - t = (*thread_map)[id_to_int(nextThread)]; + t = thread_map->get(id_to_int(nextThread)); ASSERT(t != NULL); @@ -130,8 +132,16 @@ thread_id_t ModelChecker::get_next_replay_thread() if (next == diverge) { Node *nextnode = next->get_node(); /* Reached divergence point */ - if (nextnode->increment_read_from()) { - /* The next node will read from a different value */ + 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); + } else if (nextnode->increment_read_from()) { + /* The next node will read from a different value. */ + tid = next->get_tid(); + node_stack->pop_restofstack(2); + } 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); } else { @@ -162,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) @@ -190,7 +200,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) return NULL; } /* linear search: from most recent to oldest */ - action_list_t *list = &(*obj_map)[act->get_location()]; + action_list_t *list = obj_map->ensureptr(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -268,6 +278,12 @@ 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 { @@ -279,6 +295,8 @@ void ModelChecker::check_current_action(void) /* Build may_read_from set */ if (curr->is_read()) build_reads_from_past(curr); + if (curr->is_write()) + compute_promises(curr); } } @@ -288,17 +306,31 @@ void ModelChecker::check_current_action(void) th->set_creation(curr); } + /* Deal with new thread */ + 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(); - value = reads_from->get_value(); - /* Assign reads_from, perform release/acquire synchronization */ - curr->read_from(reads_from); - r_modification_order(curr,reads_from); + if (reads_from!=NULL) { + value = reads_from->get_value(); + /* Assign reads_from, perform release/acquire synchronization */ + curr->read_from(reads_from); + r_modification_order(curr,reads_from); + } else { + /* Read from future value */ + value = curr->get_node()->get_future_value(); + curr->read_from(NULL); + Promise * valuepromise=new Promise(curr, value); + promises->push_back(valuepromise); + } } else if (curr->is_write()) { w_modification_order(curr); + resolve_promises(curr); } th->set_return_value(value); @@ -321,16 +353,21 @@ void ModelChecker::check_current_action(void) Node *currnode = curr->get_node(); Node *parnode = currnode->get_parent(); - if (!parnode->backtrack_empty()||!currnode->readsfrom_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(); + 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. */ @@ -349,7 +386,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction * act) { * @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()]; + std::vector *thrd_lists = obj_thrd_map->ensureptr(curr->get_location()); unsigned int i; ASSERT(curr->is_read()); @@ -365,7 +402,7 @@ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *r if (act->happens_before(curr)) { if (act->is_read()) { const ModelAction * prevreadfrom=act->get_reads_from(); - if (rf!=prevreadfrom) + if (prevreadfrom!=NULL&&rf!=prevreadfrom) cyclegraph->addEdge(rf, prevreadfrom); } else if (rf!=act) { cyclegraph->addEdge(rf, act); @@ -376,12 +413,49 @@ 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. */ void ModelChecker::w_modification_order(ModelAction * curr) { - std::vector *thrd_lists = &(*obj_thrd_map)[curr->get_location()]; + std::vector *thrd_lists = obj_thrd_map->ensureptr(curr->get_location()); unsigned int i; ASSERT(curr->is_write()); @@ -408,6 +482,20 @@ void ModelChecker::w_modification_order(ModelAction * curr) { } 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; + } } } } @@ -425,9 +513,9 @@ 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); + obj_map->ensureptr(act->get_location())->push_back(act); - std::vector *vec = &(*obj_thrd_map)[act->get_location()]; + std::vector *vec = obj_thrd_map->ensureptr(act->get_location()); if (tid >= (int)vec->size()) vec->resize(next_thread_id); (*vec)[tid].push_back(act); @@ -453,7 +541,7 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) */ ModelAction * ModelChecker::get_last_seq_cst(const void *location) { - action_list_t *list = &(*obj_map)[location]; + action_list_t *list = obj_map->ensureptr(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++) @@ -479,6 +567,59 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) { return get_parent_action(tid)->get_cv(); } + +/** Resolve the given promises. */ + +void ModelChecker::resolve_promises(ModelAction *write) { + 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(); + 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(); + if (!act->happens_before(curr)&& + act->is_read()&& + !act->is_synchronizing(curr)&& + !act->same_thread(curr)&& + promise->get_value()==curr->get_value()) { + curr->get_node()->set_promise(i); + } + } +} + +/** 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))&& + 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()) { + //Promise has failed + failed_promise = true; + return; + } + } + } +} + /** * 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" @@ -488,7 +629,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) { */ void ModelChecker::build_reads_from_past(ModelAction *curr) { - std::vector *thrd_lists = &(*obj_thrd_map)[curr->get_location()]; + std::vector *thrd_lists = obj_thrd_map->ensureptr(curr->get_location()); unsigned int i; ASSERT(curr->is_read()); @@ -536,7 +677,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) } if (!initialized) { - /* TODO: need a more informative way of reporting errors */ + /** @todo Need a more informative way of reporting errors. */ printf("ERROR: may read from uninitialized atomic\n"); } @@ -572,7 +713,7 @@ void ModelChecker::print_summary(void) scheduler->print(); - if (!isfeasible()) + if (!isfinalfeasible()) printf("INFEASIBLE EXECUTION!\n"); print_list(action_trace); printf("\n"); @@ -580,7 +721,7 @@ void ModelChecker::print_summary(void) int ModelChecker::add_thread(Thread *t) { - (*thread_map)[id_to_int(t->get_id())] = t; + thread_map->put(id_to_int(t->get_id()), t); scheduler->add_thread(t); return 0; }