X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=e5c8a55033289bf7393094c514d9e85658489342;hb=dbb1bb205f35f076cf2d82ec443415d858b22e2f;hp=bcc10e20e3d854673c69be58337a2d39764bd68a;hpb=3effbe640f5f299e97c5154b418c58cb809aee6d;p=model-checker.git diff --git a/model.cc b/model.cc index bcc10e2..e5c8a55 100644 --- a/model.cc +++ b/model.cc @@ -18,6 +18,17 @@ ModelChecker *model; +/** + * Structure for holding small ModelChecker members that should be snapshotted + */ +struct model_snapshot_members { + ModelAction *current_action; + unsigned int next_thread_id; + modelclock_t used_sequence_numbers; + Thread *nextThread; + ModelAction *next_backtrack; +}; + /** @brief Constructor */ ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ @@ -29,10 +40,10 @@ ModelChecker::ModelChecker(struct model_params params) : earliest_diverge(NULL), action_trace(new action_list_t()), thread_map(new HashTable()), - obj_map(new HashTable()), - lock_waiters_map(new HashTable()), - condvar_waiters_map(new HashTable()), - obj_thrd_map(new HashTable, uintptr_t, 4 >()), + obj_map(new HashTable()), + lock_waiters_map(new HashTable()), + condvar_waiters_map(new HashTable()), + obj_thrd_map(new HashTable *, uintptr_t, 4 >()), promises(new std::vector< Promise *, SnapshotAlloc >()), futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc >()), pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc >()), @@ -79,6 +90,24 @@ ModelChecker::~ModelChecker() delete mo_graph; } +static action_list_t * get_safe_ptr_action(HashTable * hash, void * ptr) { + action_list_t * tmp=hash->get(ptr); + if (tmp==NULL) { + tmp=new action_list_t(); + hash->put(ptr, tmp); + } + return tmp; +} + +static std::vector * get_safe_ptr_vect_action(HashTable *, uintptr_t, 4> * hash, void * ptr) { + std::vector * tmp=hash->get(ptr); + if (tmp==NULL) { + tmp=new std::vector(); + hash->put(ptr, tmp); + } + return tmp; +} + /** * Restores user program to initial state and resets all model-checker data * structures. @@ -244,6 +273,27 @@ void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { } } +/** + * Check if we are in a deadlock. Should only be called at the end of an + * execution, although it should not give false positives in the middle of an + * execution (there should be some ENABLED thread). + * + * @return True if program is in a deadlock; false otherwise + */ +bool ModelChecker::is_deadlocked() const +{ + bool blocking_threads = false; + for (unsigned int i = 0; i < get_num_threads(); i++) { + thread_id_t tid = int_to_id(i); + if (is_enabled(tid)) + return false; + Thread *t = get_thread(tid); + if (!t->is_model_thread() && t->get_pending()) + blocking_threads = true; + } + return blocking_threads; +} + /** * Queries the model-checker for more executions to explore and, if one * exists, resets the model-checker state to execute a new execution. @@ -257,6 +307,8 @@ bool ModelChecker::next_execution() num_executions++; + if (is_deadlocked()) + printf("ERROR: DEADLOCK\n"); if (isfinalfeasible()) { printf("Earliest divergence point since last feasible execution:\n"); if (earliest_diverge) @@ -272,7 +324,7 @@ bool ModelChecker::next_execution() pending_rel_seqs->size()); - if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) { + if (isfinalfeasible() || DBG_ENABLED()) { checkDataRaces(); print_summary(); } @@ -296,7 +348,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) case ATOMIC_WRITE: case ATOMIC_RMW: { /* linear search: from most recent to oldest */ - action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -308,7 +360,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) case ATOMIC_LOCK: case ATOMIC_TRYLOCK: { /* linear search: from most recent to oldest */ - action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -319,7 +371,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) } case ATOMIC_UNLOCK: { /* linear search: from most recent to oldest */ - action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -330,7 +382,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) } case ATOMIC_WAIT: { /* linear search: from most recent to oldest */ - action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -345,7 +397,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) case ATOMIC_NOTIFY_ALL: case ATOMIC_NOTIFY_ONE: { /* linear search: from most recent to oldest */ - action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -545,7 +597,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) { //unlock the lock state->islocked = false; //wake up the other threads - action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location()); + action_list_t *waiters = get_safe_ptr_action(lock_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)); @@ -557,7 +609,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) { //unlock the lock state->islocked = false; //wake up the other threads - action_list_t *waiters = lock_waiters_map->get_safe_ptr((void *) curr->get_value()); + action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value()); //activate all the waiting threads for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { scheduler->wake(get_thread(*rit)); @@ -565,14 +617,14 @@ bool ModelChecker::process_mutex(ModelAction *curr) { waiters->clear(); //check whether we should go to sleep or not...simulate spurious failures if (curr->get_node()->get_misc()==0) { - condvar_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr); + get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr); //disable us scheduler->sleep(get_current_thread()); } break; } case ATOMIC_NOTIFY_ALL: { - action_list_t *waiters = condvar_waiters_map->get_safe_ptr(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)); @@ -581,7 +633,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) { break; } case ATOMIC_NOTIFY_ONE: { - action_list_t *waiters = condvar_waiters_map->get_safe_ptr(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); @@ -805,7 +857,7 @@ bool ModelChecker::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(condvar_waiters_map->get_safe_ptr(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 */ } @@ -827,7 +879,7 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { struct std::mutex_state * state = lock->get_state(); if (state->islocked) { //Stick the action in the appropriate waiting queue - lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr); + get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr); return false; } } else if (curr->get_type() == THREAD_JOIN) { @@ -841,6 +893,16 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { return true; } +/** + * Stores the ModelAction for the current thread action. Call this + * immediately before switching from user- to system-context to pass + * data between them. + * @param act The ModelAction created by the user-thread action + */ +void ModelChecker::set_current_action(ModelAction *act) { + priv->current_action = act; +} + /** * This is the heart of the model checker routine. It performs model-checking * actions corresponding to a given "current action." Among other processes, it @@ -1042,7 +1104,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { //accidentally clear by rolling back if (!isfeasible()) return; - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); int tid = id_to_int(curr->get_tid()); /* Skip checks */ @@ -1134,7 +1196,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { */ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; bool added = false; ASSERT(curr->is_read()); @@ -1193,7 +1255,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf */ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; ASSERT(curr->is_read()); @@ -1264,7 +1326,7 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio */ bool ModelChecker::w_modification_order(ModelAction *curr) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; bool added = false; ASSERT(curr->is_write()); @@ -1386,7 +1448,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con */ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location()); unsigned int i; /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { @@ -1478,7 +1540,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, /* else relaxed write; check modification order for contiguous subsequence * -> rf must be same thread as release */ int tid = id_to_int(rf->get_tid()); - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location()); action_list_t *list = &(*thrd_lists)[tid]; action_list_t::const_reverse_iterator rit; @@ -1513,7 +1575,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, ModelAction *last = get_last_action(int_to_id(i)); Thread *th = get_thread(int_to_id(i)); if ((last && rf->happens_before(last)) || - !scheduler->is_enabled(th) || + !is_enabled(th) || th->is_complete()) future_ordered = true; @@ -1676,9 +1738,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act) int tid = id_to_int(act->get_tid()); action_trace->push_back(act); - obj_map->get_safe_ptr(act->get_location())->push_back(act); + get_safe_ptr_action(obj_map, act->get_location())->push_back(act); - std::vector *vec = obj_thrd_map->get_safe_ptr(act->get_location()); + std::vector *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); @@ -1689,9 +1751,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act) if (act->is_wait()) { void *mutex_loc=(void *) act->get_value(); - obj_map->get_safe_ptr(mutex_loc)->push_back(act); + get_safe_ptr_action(obj_map, mutex_loc)->push_back(act); - std::vector *vec = obj_thrd_map->get_safe_ptr(mutex_loc); + std::vector *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); @@ -1727,7 +1789,7 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) const ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const { void *location = curr->get_location(); - action_list_t *list = obj_map->get_safe_ptr(location); + action_list_t *list = get_safe_ptr_action(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++) @@ -1747,7 +1809,7 @@ ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const { void *location = curr->get_location(); - action_list_t *list = obj_map->get_safe_ptr(location); + action_list_t *list = get_safe_ptr_action(obj_map, 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++) @@ -1969,7 +2031,7 @@ void ModelChecker::compute_relseq_breakwrites(ModelAction *curr) */ void ModelChecker::build_reads_from_past(ModelAction *curr) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; ASSERT(curr->is_read()); @@ -2000,17 +2062,14 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) /* Don't consider more than one seq_cst write if we are a seq_cst read. */ if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) { - DEBUG("Adding action to may_read_from:\n"); - if (DBG_ENABLED()) { - act->print(); - curr->print(); - } - - if (curr->get_sleep_flag() && ! curr->is_seqcst()) { - if (sleep_can_read_from(curr, act)) - curr->get_node()->add_read_from(act); - } else + if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) { + DEBUG("Adding action to may_read_from:\n"); + if (DBG_ENABLED()) { + act->print(); + curr->print(); + } curr->get_node()->add_read_from(act); + } } /* Include at most one act per-thread that "happens before" curr */ @@ -2158,6 +2217,26 @@ Thread * ModelChecker::get_thread(ModelAction *act) const return get_thread(act->get_tid()); } +/** + * @brief Check if a Thread is currently enabled + * @param t The Thread to check + * @return True if the Thread is currently enabled + */ +bool ModelChecker::is_enabled(Thread *t) const +{ + return scheduler->is_enabled(t); +} + +/** + * @brief Check if a Thread is currently enabled + * @param tid The ID of the Thread to check + * @return True if the Thread is currently enabled + */ +bool ModelChecker::is_enabled(thread_id_t tid) const +{ + return scheduler->is_enabled(tid); +} + /** * 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