X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=e4757bc6f0d0b919417e60ed9018e0bcd0e86301;hp=02518eef53078cc2618a56e0f75d4c00a2a27ccc;hb=f71cd7c31df98cfc814254da887de9a30c53b31e;hpb=70525635cea4c0622d30571c7028c1c293950bb5 diff --git a/model.cc b/model.cc index 02518eef..e4757bc6 100644 --- a/model.cc +++ b/model.cc @@ -32,7 +32,7 @@ ModelChecker::ModelChecker(struct model_params params) : obj_thrd_map(new HashTable, uintptr_t, 4 >()), promises(new std::vector()), futurevalues(new std::vector()), - lazy_sync_with_release(new HashTable()), + pending_acq_rel_seq(new std::vector()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), mo_graph(new CycleGraph()), @@ -44,8 +44,6 @@ ModelChecker::ModelChecker(struct model_params params) : priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv)); /* First thread created will have id INITIAL_THREAD_ID */ priv->next_thread_id = INITIAL_THREAD_ID; - - lazy_sync_size = &priv->lazy_sync_size; } /** @brief Destructor */ @@ -64,7 +62,7 @@ ModelChecker::~ModelChecker() delete (*promises)[i]; delete promises; - delete lazy_sync_with_release; + delete pending_acq_rel_seq; delete thrd_last_action; delete node_stack; @@ -86,19 +84,19 @@ void ModelChecker::reset_to_initial_state() snapshotObject->backTrackBeforeStep(0); } -/** @returns a thread ID for a new Thread */ +/** @return a thread ID for a new Thread */ thread_id_t ModelChecker::get_next_id() { return priv->next_thread_id++; } -/** @returns the number of user threads created during this execution */ +/** @return the number of user threads created during this execution */ int ModelChecker::get_num_threads() { return priv->next_thread_id; } -/** @returns a sequence number for a new ModelAction */ +/** @return a sequence number for a new ModelAction */ modelclock_t ModelChecker::get_next_seq_num() { return ++priv->used_sequence_numbers; @@ -200,9 +198,10 @@ bool ModelChecker::next_execution() ModelAction * ModelChecker::get_last_conflict(ModelAction *act) { - action_type type = act->get_type(); - - if (type==ATOMIC_READ||type==ATOMIC_WRITE||type==ATOMIC_RMW) { + switch (act->get_type()) { + case ATOMIC_READ: + 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::reverse_iterator rit; @@ -211,7 +210,10 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) if (act->is_synchronizing(prev)) return prev; } - } else if (type==ATOMIC_LOCK||type==ATOMIC_TRYLOCK) { + break; + } + 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::reverse_iterator rit; @@ -220,7 +222,9 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) if (act->is_conflicting_lock(prev)) return prev; } - } else if (type==ATOMIC_UNLOCK) { + break; + } + 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::reverse_iterator rit; @@ -229,10 +233,21 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) if (!act->same_thread(prev)&&prev->is_failed_trylock()) return prev; } + break; + } + default: + break; } return NULL; } +/** This method find backtracking points where we should try to + * reorder the parameter ModelAction against. + * + * @param the ModelAction to find backtracking points for. + */ + + void ModelChecker::set_backtracking(ModelAction *act) { Thread *t = get_thread(act); @@ -244,26 +259,26 @@ void ModelChecker::set_backtracking(ModelAction *act) int low_tid, high_tid; if (node->is_enabled(t)) { - low_tid=id_to_int(act->get_tid()); - high_tid=low_tid+1; + low_tid = id_to_int(act->get_tid()); + high_tid = low_tid+1; } else { - low_tid=0; - high_tid=get_num_threads(); + low_tid = 0; + high_tid = get_num_threads(); } - - for(int i=low_tid;iis_enabled(tid)) continue; /* Check if this has been explored already */ if (node->has_been_explored(tid)) continue; - + /* Cache the latest backtracking point */ if (!priv->next_backtrack || *prev > *priv->next_backtrack) priv->next_backtrack = prev; - + /* If this is a new backtracking point, mark the tree */ if (!node->set_backtrack(tid)) continue; @@ -334,12 +349,26 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) } } +/** + * Processes a lock, trylock, or unlock model action. @param curr is + * the read model action to process. + * + * The try lock operation checks whether the lock is taken. If not, + * it falls to the normal lock operation case. If so, it returns + * fail. + * + * The lock operation has already been checked that it is enabled, so + * it just grabs the lock and synchronizes with the previous unlock. + * + * The unlock operation has to re-enable all of the threads that are + * waiting on the lock. + */ void ModelChecker::process_mutex(ModelAction *curr) { - std::mutex * mutex=(std::mutex *) curr->get_location(); - struct std::mutex_state * state=mutex->get_state(); - switch(curr->get_type()) { + std::mutex *mutex = (std::mutex *)curr->get_location(); + struct std::mutex_state *state = mutex->get_state(); + switch (curr->get_type()) { case ATOMIC_TRYLOCK: { - bool success=!state->islocked; + bool success = !state->islocked; curr->set_try_lock(success); if (!success) { get_thread(curr)->set_return_value(0); @@ -349,25 +378,25 @@ void ModelChecker::process_mutex(ModelAction *curr) { } //otherwise fall into the lock case case ATOMIC_LOCK: { - if (curr->get_cv()->getClock(state->alloc_tid)<=state->alloc_clock) { + if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) { printf("Lock access before initialization\n"); set_assert(); } - state->islocked=true; - ModelAction *unlock=get_last_unlock(curr); + state->islocked = true; + ModelAction *unlock = get_last_unlock(curr); //synchronize with the previous unlock statement - if ( unlock != NULL ) + if (unlock != NULL) curr->synchronize_with(unlock); break; } case ATOMIC_UNLOCK: { //unlock the lock - state->islocked=false; + 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 = lock_waiters_map->get_safe_ptr(curr->get_location()); //activate all the waiting threads - for(action_list_t::iterator rit = waiters->begin(); rit!=waiters->end(); rit++) { - add_thread(get_thread((*rit)->get_tid())); + for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { + scheduler->add_thread(get_thread((*rit)->get_tid())); } waiters->clear(); break; @@ -377,7 +406,6 @@ void ModelChecker::process_mutex(ModelAction *curr) { } } - /** * Process a write ModelAction * @param curr The ModelAction to process @@ -389,7 +417,7 @@ bool ModelChecker::process_write(ModelAction *curr) bool updated_promises = resolve_promises(curr); if (promises->size() == 0) { - for (unsigned int i = 0; isize(); i++) { + for (unsigned int i = 0; i < futurevalues->size(); i++) { struct PendingFutureValue pfv = (*futurevalues)[i]; if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) && (!priv->next_backtrack || *pfv.act > *priv->next_backtrack)) @@ -431,7 +459,7 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) if (curr->is_rmwr()) newcurr->copy_typeandorder(curr); - ASSERT(curr->get_location()==newcurr->get_location()); + ASSERT(curr->get_location() == newcurr->get_location()); newcurr->copy_from_new(curr); /* Discard duplicate ModelAction; use action from NodeStack */ @@ -453,9 +481,17 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) return newcurr; } +/** + * This method checks whether a model action is enabled at the given point. + * At this point, it checks whether a lock operation would be successful at this point. + * If not, it puts the thread in a waiter list. + * @param curr is the ModelAction to check whether it is enabled. + * @return a bool that indicates whether the action is enabled. + */ + bool ModelChecker::check_action_enabled(ModelAction *curr) { if (curr->is_lock()) { - std::mutex * lock=(std::mutex *) curr->get_location(); + std::mutex * lock = (std::mutex *)curr->get_location(); struct std::mutex_state * state = lock->get_state(); if (state->islocked) { //Stick the action in the appropriate waiting queue @@ -558,7 +594,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (act->is_write() && process_write(act)) updated = true; - if (act->is_mutex_op()) + if (act->is_mutex_op()) process_mutex(act); if (updated) @@ -636,18 +672,18 @@ bool ModelChecker::promises_expired() { return false; } -/** @returns whether the current partial trace must be a prefix of a +/** @return whether the current partial trace must be a prefix of a * feasible trace. */ bool ModelChecker::isfeasibleprefix() { - return promises->size() == 0 && *lazy_sync_size == 0; + return promises->size() == 0 && pending_acq_rel_seq->size() == 0; } -/** @returns whether the current partial trace is feasible. */ +/** @return whether the current partial trace is feasible. */ bool ModelChecker::isfeasible() { return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW(); } -/** @returns whether the current partial trace is feasible other than +/** @return whether the current partial trace is feasible other than * multiple RMW reading from the same store. */ bool ModelChecker::isfeasibleotherthanRMW() { if (DBG_ENABLED()) { @@ -779,7 +815,7 @@ void ModelChecker::check_recency(ModelAction *curr) { /** * Updates the mo_graph with the constraints imposed from the current - * read. + * read. * * Basic idea is the following: Go through each other thread and find * the lastest action that happened before our read. Two cases: @@ -838,7 +874,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf * promises. The basic problem is that actions that occur after the * read curr could not property add items to the modification order * for our read. - * + * * So for each thread, we find the earliest item that happens after * the read curr. This is the item we have to fix up with additional * constraints. If that action is write, we add a MO edge between @@ -974,7 +1010,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) */ if (thin_air_constraint_may_allow(curr, act)) { if (isfeasible() || - (curr->is_rmw() && act->is_rmw() && curr->get_reads_from()==act->get_reads_from() && isfeasibleotherthanRMW())) { + (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) { struct PendingFutureValue pfv = {curr->get_value(),curr->get_seq_number()+params.maxfuturedelay,act}; futurevalues->push_back(pfv); } @@ -998,7 +1034,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con return true; for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) { - if (search==reader) + if (search == reader) return false; if (search->get_tid() == reader->get_tid() && search->happens_before(reader)) @@ -1085,10 +1121,12 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel * the release seq? */ bool future_ordered = false; + ModelAction *last = get_last_action(int_to_id(i)); + if (last && rf->happens_before(last)) + future_ordered = true; + for (rit = list->rbegin(); rit != list->rend(); rit++) { const ModelAction *act = *rit; - if (!act->is_write()) - continue; /* Reach synchronization -> this thread is complete */ if (act->happens_before(release)) break; @@ -1097,6 +1135,10 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel continue; } + /* Only writes can break release sequences */ + if (!act->is_write()) + continue; + /* Check modification order */ if (mo_graph->checkReachable(rf, act)) { /* rf --mo--> act */ @@ -1141,10 +1183,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel complete = release_seq_head(rf, release_heads); if (!complete) { /* add act to 'lazy checking' list */ - action_list_t *list; - list = lazy_sync_with_release->get_safe_ptr(act->get_location()); - list->push_back(act); - (*lazy_sync_size)++; + pending_acq_rel_seq->push_back(act); } } @@ -1155,7 +1194,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel * modification order information is present at the time an action occurs. * * @param location The location/object that should be checked for release - * sequence resolutions + * sequence resolutions. A NULL value means to check all locations. * @param work_queue The work queue to which to add work items as they are * generated * @return True if any updates occurred (new synchronization, new mo_graph @@ -1163,15 +1202,17 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel */ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue) { - action_list_t *list; - list = lazy_sync_with_release->getptr(location); - if (!list) - return false; - bool updated = false; - action_list_t::iterator it = list->begin(); - while (it != list->end()) { + std::vector::iterator it = pending_acq_rel_seq->begin(); + while (it != pending_acq_rel_seq->end()) { ModelAction *act = *it; + + /* Only resolve sequences on the given location, if provided */ + if (location && act->get_location() != location) { + it++; + continue; + } + const ModelAction *rf = act->get_reads_from(); rel_heads_list_t release_heads; bool complete; @@ -1189,7 +1230,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ /* propagate synchronization to later actions */ action_list_t::reverse_iterator it = action_trace->rbegin(); - while ((*it) != act) { + for (; (*it) != act; it++) { ModelAction *propagate = *it; if (act->happens_before(propagate)) { propagate->synchronize_with(act); @@ -1198,10 +1239,9 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ } } } - if (complete) { - it = list->erase(it); - (*lazy_sync_size)--; - } else + if (complete) + it = pending_acq_rel_seq->erase(it); + else it++; } @@ -1237,10 +1277,15 @@ void ModelChecker::add_action_to_lists(ModelAction *act) (*thrd_last_action)[tid] = act; } -ModelAction * ModelChecker::get_last_action(thread_id_t tid) +/** + * @brief Get the last action performed by a particular Thread + * @param tid The thread ID of the Thread in question + * @return The last action in the thread + */ +ModelAction * ModelChecker::get_last_action(thread_id_t tid) const { - int threadid=id_to_int(tid); - if (threadid<(int)thrd_last_action->size()) + int threadid = id_to_int(tid); + if (threadid < (int)thrd_last_action->size()) return (*thrd_last_action)[id_to_int(tid)]; else return NULL; @@ -1254,7 +1299,7 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) * check * @return The last seq_cst write */ -ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) +ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const { void *location = curr->get_location(); action_list_t *list = obj_map->get_safe_ptr(location); @@ -1266,11 +1311,19 @@ ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) return NULL; } -ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) +/** + * Gets the last unlock operation performed on a particular mutex (i.e., memory + * location). This function identifies the mutex according to the current + * action, which is presumed to perform on the same mutex. + * @param curr The current ModelAction; also denotes the object location to + * check + * @return The last unlock operation + */ +ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const { void *location = curr->get_location(); action_list_t *list = obj_map->get_safe_ptr(location); - /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */ + /* 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++) if ((*rit)->is_unlock()) @@ -1407,7 +1460,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) continue; /* 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) { + 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(); @@ -1463,7 +1516,7 @@ void ModelChecker::print_summary() #if SUPPORT_MOD_ORDER_DUMP scheduler->print(); char buffername[100]; - sprintf(buffername, "exec%u",num_executions); + sprintf(buffername, "exec%04u", num_executions); mo_graph->dumpGraphToFile(buffername); #endif @@ -1484,6 +1537,11 @@ void ModelChecker::add_thread(Thread *t) scheduler->add_thread(t); } +/** + * Removes a thread from the scheduler. + * @param the thread to remove. + */ + void ModelChecker::remove_thread(Thread *t) { scheduler->remove_thread(t);