X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=a74147be4bbe7e068a9ddd05a58ff459ccb1a7c8;hb=3a4e118d45bf83a3b4c3a0a73d1071fa8fe5476d;hp=41fdfc77b6b07bf9eb2754f230f11560225962bb;hpb=0cf7ad4007b76a90747f067c45cfcd0a66ffc47a;p=model-checker.git diff --git a/execution.cc b/execution.cc index 41fdfc7..a74147b 100644 --- a/execution.cc +++ b/execution.cc @@ -64,11 +64,11 @@ ModelExecution::ModelExecution(ModelChecker *m, model(m), params(params), scheduler(scheduler), - action_trace(new action_list_t()), - thread_map(new HashTable()), - obj_map(new HashTable()), - condvar_waiters_map(new HashTable()), - obj_thrd_map(new HashTable *, uintptr_t, 4 >()), + action_trace(), + thread_map(2), /* We'll always need at least 2 threads */ + obj_map(), + condvar_waiters_map(), + obj_thrd_map(), promises(), futurevalues(), pending_rel_seqs(), @@ -80,21 +80,16 @@ ModelExecution::ModelExecution(ModelChecker *m, { /* Initialize a model-checker thread, for special ModelActions */ model_thread = new Thread(get_next_id()); - thread_map->put(id_to_int(model_thread->get_id()), model_thread); + add_thread(model_thread); scheduler->register_engine(this); + node_stack->register_engine(this); } /** @brief Destructor */ ModelExecution::~ModelExecution() { for (unsigned int i = 0; i < get_num_threads(); i++) - delete thread_map->get(i); - delete thread_map; - - delete obj_thrd_map; - delete obj_map; - delete condvar_waiters_map; - delete action_trace; + delete get_thread(int_to_id(i)); for (unsigned int i = 0; i < promises.size(); i++) delete promises[i]; @@ -130,7 +125,7 @@ static SnapVector * get_safe_ptr_vect_action(HashTable *wrv=obj_thrd_map->get(obj); + SnapVector *wrv = obj_thrd_map.get(obj); if (wrv==NULL) return NULL; unsigned int thread=id_to_int(tid); @@ -312,8 +307,8 @@ ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const return NULL; /* Skip past the release */ - action_list_t *list = action_trace; - action_list_t::reverse_iterator rit; + const action_list_t *list = &action_trace; + action_list_t::const_reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) if (*rit == last_release) break; @@ -371,17 +366,22 @@ ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const { switch (act->get_type()) { - /* case ATOMIC_FENCE: fences don't directly cause backtracking */ + case ATOMIC_FENCE: + /* Only seq-cst fences can (directly) cause backtracking */ + if (!act->is_seqcst()) + break; case ATOMIC_READ: case ATOMIC_WRITE: case ATOMIC_RMW: { ModelAction *ret = NULL; /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; + if (prev == act) + continue; if (prev->could_synchronize_with(act)) { ret = prev; break; @@ -400,7 +400,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const case ATOMIC_LOCK: case ATOMIC_TRYLOCK: { /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -411,7 +411,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const } case ATOMIC_UNLOCK: { /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -422,7 +422,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const } case ATOMIC_WAIT: { /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -437,7 +437,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const case ATOMIC_NOTIFY_ALL: case ATOMIC_NOTIFY_ONE: { /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -697,14 +697,14 @@ bool ModelExecution::process_mutex(ModelAction *curr) /* Should we go to sleep? (simulate spurious failures) */ if (curr->get_node()->get_misc() == 0) { - get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr); + get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr); /* disable us */ scheduler->sleep(get_thread(curr)); } break; } case ATOMIC_NOTIFY_ALL: { - action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location()); + action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); //activate all the waiting threads for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { scheduler->wake(get_thread(*rit)); @@ -713,7 +713,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) break; } case ATOMIC_NOTIFY_ONE: { - action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location()); + action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); int wakeupthread = curr->get_node()->get_misc(); action_list_t::iterator it = waiters->begin(); advance(it, wakeupthread); @@ -859,7 +859,7 @@ bool ModelExecution::process_fence(ModelAction *curr) */ bool updated = false; if (curr->is_acquire()) { - action_list_t *list = action_trace; + action_list_t *list = &action_trace; action_list_t::reverse_iterator rit; /* Find X : is_read(X) && X --sb-> curr */ for (rit = list->rbegin(); rit != list->rend(); rit++) { @@ -1007,7 +1007,7 @@ void ModelExecution::process_relseq_fixup(ModelAction *curr, work_queue_t *work_ work_queue->push_back(MOEdgeWorkEntry(acquire)); /* propagate synchronization to later actions */ - action_list_t::reverse_iterator rit = action_trace->rbegin(); + action_list_t::reverse_iterator rit = action_trace.rbegin(); for (; (*rit) != acquire; rit++) { ModelAction *propagate = *rit; if (acquire->happens_before(propagate)) { @@ -1092,7 +1092,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) else if (newcurr->is_wait()) newcurr->get_node()->set_misc_max(2); else if (newcurr->is_notify_one()) { - newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size()); + newcurr->get_node()->set_misc_max(get_safe_ptr_action(&condvar_waiters_map, newcurr->get_location())->size()); } return true; /* This was a new ModelAction */ } @@ -1214,7 +1214,7 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) { * * @param curr The current action to process * @return The ModelAction that is actually executed; may be different than - * curr; may be NULL, if the current action is not enabled to run + * curr */ ModelAction * ModelExecution::check_current_action(ModelAction *curr) { @@ -1437,7 +1437,7 @@ bool ModelExecution::should_read_instead(const ModelAction *curr, const T *rf, c if (!mo_graph->checkReachable(rf, other_rf)) return false; - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); action_list_t *list = &(*thrd_lists)[id_to_int(curr->get_tid())]; action_list_t::reverse_iterator rit = list->rbegin(); ASSERT((*rit) == curr); @@ -1480,7 +1480,7 @@ bool ModelExecution::check_recency(ModelAction *curr, const T *rf) const curr->get_node()->get_read_from_promise_size() <= 1) return true; - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); int tid = id_to_int(curr->get_tid()); ASSERT(tid < (int)thrd_lists->size()); action_list_t *list = &(*thrd_lists)[tid]; @@ -1537,7 +1537,7 @@ bool ModelExecution::check_recency(ModelAction *curr, const T *rf) const template bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) { - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; bool added = false; ASSERT(curr->is_read()); @@ -1663,7 +1663,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) */ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVector *send_fv) { - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; bool added = false; ASSERT(curr->is_write()); @@ -1807,7 +1807,7 @@ bool ModelExecution::thin_air_constraint_may_allow(const ModelAction *writer, co */ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader) { - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(reader->get_location()); unsigned int i; /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { @@ -1908,7 +1908,7 @@ bool ModelExecution::release_seq_heads(const ModelAction *rf, release_heads->push_back(fence_release); int tid = id_to_int(rf->get_tid()); - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(rf->get_location()); action_list_t *list = &(*thrd_lists)[tid]; action_list_t::const_reverse_iterator rit; @@ -2080,7 +2080,7 @@ bool ModelExecution::resolve_release_sequences(void *location, work_queue_t *wor work_queue->push_back(MOEdgeWorkEntry(acquire)); /* propagate synchronization to later actions */ - action_list_t::reverse_iterator rit = action_trace->rbegin(); + action_list_t::reverse_iterator rit = action_trace.rbegin(); for (; (*rit) != acquire; rit++) { ModelAction *propagate = *rit; if (acquire->happens_before(propagate)) { @@ -2116,7 +2116,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act) int tid = id_to_int(act->get_tid()); ModelAction *uninit = NULL; int uninit_id = -1; - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); if (list->empty() && act->is_atomic_var()) { uninit = get_uninitialized_action(act); uninit_id = id_to_int(uninit->get_tid()); @@ -2124,11 +2124,11 @@ void ModelExecution::add_action_to_lists(ModelAction *act) } list->push_back(act); - action_trace->push_back(act); + action_trace.push_back(act); if (uninit) - action_trace->push_front(uninit); + action_trace.push_front(uninit); - SnapVector *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location()); + SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); @@ -2149,9 +2149,9 @@ void ModelExecution::add_action_to_lists(ModelAction *act) if (act->is_wait()) { void *mutex_loc = (void *) act->get_value(); - get_safe_ptr_action(obj_map, mutex_loc)->push_back(act); + get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act); - SnapVector *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc); + SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc); if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); @@ -2197,7 +2197,7 @@ ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const { void *location = curr->get_location(); - action_list_t *list = get_safe_ptr_action(obj_map, location); + action_list_t *list = obj_map.get(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) != curr; rit++) @@ -2219,8 +2219,12 @@ ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const */ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const { - /* All fences should have NULL location */ - action_list_t *list = get_safe_ptr_action(obj_map, NULL); + /* All fences should have location FENCE_LOCATION */ + action_list_t *list = obj_map.get(FENCE_LOCATION); + + if (!list) + return NULL; + action_list_t::reverse_iterator rit = list->rbegin(); if (before_fence) { @@ -2249,7 +2253,7 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const { void *location = curr->get_location(); - action_list_t *list = get_safe_ptr_action(obj_map, location); + action_list_t *list = obj_map.get(location); /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */ action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) @@ -2474,7 +2478,7 @@ void ModelExecution::compute_relseq_breakwrites(ModelAction *curr) */ void ModelExecution::build_may_read_from(ModelAction *curr) { - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; ASSERT(curr->is_read()); @@ -2584,9 +2588,9 @@ ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) return act; } -static void print_list(action_list_t *list) +static void print_list(const action_list_t *list) { - action_list_t::iterator it; + action_list_t::const_iterator it; model_print("---------------------------------------------------------------------\n"); @@ -2612,7 +2616,7 @@ void ModelExecution::dumpGraph(char *filename) const mo_graph->dumpNodes(file); ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads()); - for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) { + for (action_list_t::iterator it = action_trace.begin(); it != action_trace.end(); it++) { ModelAction *act = *it; if (act->is_read()) { mo_graph->dot_print_node(file, act); @@ -2660,7 +2664,7 @@ void ModelExecution::print_summary() const model_print("\n"); } else print_infeasibility(" INFEASIBLE"); - print_list(action_trace); + print_list(&action_trace); model_print("\n"); if (!promises.empty()) { model_print("Pending promises:\n"); @@ -2679,7 +2683,10 @@ void ModelExecution::print_summary() const */ void ModelExecution::add_thread(Thread *t) { - thread_map->put(id_to_int(t->get_id()), t); + unsigned int i = id_to_int(t->get_id()); + if (i >= thread_map.size()) + thread_map.resize(i + 1); + thread_map[i] = t; if (!t->is_model_thread()) scheduler->add_thread(t); } @@ -2691,7 +2698,10 @@ void ModelExecution::add_thread(Thread *t) */ Thread * ModelExecution::get_thread(thread_id_t tid) const { - return thread_map->get(id_to_int(tid)); + unsigned int i = id_to_int(tid); + if (i < thread_map.size()) + return thread_map[i]; + return NULL; } /**