X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=651d32d5b9c7bf74a63bbfda817419009a1e6049;hp=954c07dd6dacdfc9473a4aa3f5e0a2f8db38bcbf;hb=9ba28a8ef15225525c30c5303c859f64602820a3;hpb=202074f941d19cef894068e7f79d76b2df598f4b diff --git a/model.cc b/model.cc index 954c07d..651d32d 100644 --- a/model.cc +++ b/model.cc @@ -11,6 +11,7 @@ #include "cyclegraph.h" #include "promise.h" #include "datarace.h" +#include "mutex.h" #define INITIAL_THREAD_ID 0 @@ -27,10 +28,11 @@ ModelChecker::ModelChecker(struct model_params params) : action_trace(new action_list_t()), thread_map(new HashTable()), obj_map(new HashTable()), + lock_waiters_map(new HashTable()), obj_thrd_map(new HashTable, uintptr_t, 4 >()), promises(new std::vector()), futurevalues(new std::vector()), - lazy_sync_with_release(new HashTable, uintptr_t, 4>()), + lazy_sync_with_release(new HashTable()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), mo_graph(new CycleGraph()), @@ -55,6 +57,7 @@ ModelChecker::~ModelChecker() delete obj_thrd_map; delete obj_map; + delete lock_waiters_map; delete action_trace; for (unsigned int i = 0; i < promises->size(); i++) @@ -118,12 +121,14 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) { thread_id_t tid; - /* Do not split atomic actions. */ - if (curr->is_rmwr()) - return thread_current(); - /* The THREAD_CREATE action points to the created Thread */ - else if (curr->get_type() == THREAD_CREATE) - return (Thread *)curr->get_location(); + if (curr!=NULL) { + /* Do not split atomic actions. */ + if (curr->is_rmwr()) + return thread_current(); + /* The THREAD_CREATE action points to the created Thread */ + else if (curr->get_type() == THREAD_CREATE) + return (Thread *)curr->get_location(); + } /* Have we completed exploring the preselected path? */ if (diverge == NULL) @@ -197,21 +202,33 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) { action_type type = act->get_type(); - switch (type) { - case ATOMIC_READ: - case ATOMIC_WRITE: - case ATOMIC_RMW: - break; - default: - return NULL; - } - /* 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; - for (rit = list->rbegin(); rit != list->rend(); rit++) { - ModelAction *prev = *rit; - if (act->is_synchronizing(prev)) - return prev; + if (type==ATOMIC_READ||type==ATOMIC_WRITE||type==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; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *prev = *rit; + if (act->is_synchronizing(prev)) + return prev; + } + } else if (type==ATOMIC_LOCK||type==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; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *prev = *rit; + if (prev->is_success_lock()) + return prev; + } + } else if (type==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; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *prev = *rit; + if (prev->is_failed_trylock()) + return prev; + } } return NULL; } @@ -281,7 +298,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) bool r_status = false; if (!second_part_of_rmw) { - check_recency(curr,false); + check_recency(curr); r_status = r_modification_order(curr, reads_from); } @@ -308,6 +325,42 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) } } +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()) { + case ATOMIC_TRYLOCK: { + bool success=!state->islocked; + curr->set_try_lock(success); + if (!success) + break; + } + //otherwise fall into the lock case + case ATOMIC_LOCK: { + state->islocked=true; + ModelAction *unlock=get_last_unlock(curr); + //synchronize with the previous unlock statement + curr->synchronize_with(unlock); + break; + } + case ATOMIC_UNLOCK: { + //unlock the lock + state->islocked=false; + //wake up the other threads + 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())); + } + waiters->clear(); + break; + } + default: + ASSERT(0); + } +} + + /** * Process a write ModelAction * @param curr The ModelAction to process @@ -333,6 +386,68 @@ bool ModelChecker::process_write(ModelAction *curr) return updated_mod_order || updated_promises; } +/** + * Initialize the current action by performing one or more of the following + * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward + * in the NodeStack, manipulating backtracking sets, allocating and + * initializing clock vectors, and computing the promises to fulfill. + * + * @param curr The current action, as passed from the user context; may be + * freed/invalidated after the execution of this function + * @return The current action, as processed by the ModelChecker. Is only the + * same as the parameter @a curr if this is a newly-explored action. + */ +ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) +{ + ModelAction *newcurr; + + if (curr->is_rmwc() || curr->is_rmw()) { + newcurr = process_rmw(curr); + delete curr; + compute_promises(newcurr); + return newcurr; + } + + newcurr = node_stack->explore_action(curr, scheduler->get_enabled()); + if (newcurr) { + /* First restore type and order in case of RMW operation */ + if (curr->is_rmwr()) + newcurr->copy_typeandorder(curr); + + ASSERT(curr->get_location()==newcurr->get_location()); + /* Discard duplicate ModelAction; use action from NodeStack */ + delete curr; + + /* If we have diverged, we need to reset the clock vector. */ + if (diverge == NULL) + newcurr->create_cv(get_parent_action(newcurr->get_tid())); + } else { + newcurr = curr; + /* + * Perform one-time actions when pushing new ModelAction onto + * NodeStack + */ + curr->create_cv(get_parent_action(curr->get_tid())); + if (curr->is_write()) + compute_promises(curr); + } + return newcurr; +} + +bool ModelChecker::check_action_enabled(ModelAction *curr) { + if (curr->is_lock()) { + 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 + lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr); + return false; + } + } + + return true; +} + /** * This is the heart of the model checker routine. It performs model-checking * actions corresponding to a given "current action." Among other processes, it @@ -347,44 +462,29 @@ bool ModelChecker::process_write(ModelAction *curr) */ Thread * ModelChecker::check_current_action(ModelAction *curr) { - bool second_part_of_rmw = false; - ASSERT(curr); - if (curr->is_rmwc() || curr->is_rmw()) { - ModelAction *tmp = process_rmw(curr); - second_part_of_rmw = true; - delete curr; - curr = tmp; - compute_promises(curr); - } else { - ModelAction *tmp = node_stack->explore_action(curr); - if (tmp) { - /* Discard duplicate ModelAction; use action from NodeStack */ - /* 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 { - /* - * Perform one-time actions when pushing new ModelAction onto - * NodeStack - */ - curr->create_cv(get_parent_action(curr->get_tid())); - /* Build may_read_from set */ - if (curr->is_read()) - build_reads_from_past(curr); - if (curr->is_write()) - compute_promises(curr); - } + bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw(); + + if (!check_action_enabled(curr)) { + //we'll make the execution look like we chose to run this action + //much later...when a lock is actually available to relese + remove_thread(get_current_thread()); + get_current_thread()->set_pending(curr); + return get_next_thread(NULL); } + ModelAction *newcurr = initialize_curr_action(curr); + + /* Add the action to lists before any other model-checking tasks */ + if (!second_part_of_rmw) + add_action_to_lists(newcurr); + + /* Build may_read_from set for newly-created actions */ + if (curr == newcurr && curr->is_read()) + build_reads_from_past(curr); + curr = newcurr; + /* Thread specific actions */ switch (curr->get_type()) { case THREAD_CREATE: { @@ -399,6 +499,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (!blocking->is_complete()) { blocking->push_wait_list(curr); scheduler->sleep(waiting); + } else { + do_complete_join(curr); } break; } @@ -408,6 +510,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) ModelAction *act = th->pop_wait_list(); Thread *wake = get_thread(act); scheduler->wake(wake); + do_complete_join(act); } th->complete(); break; @@ -436,6 +539,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (act->is_write() && process_write(act)) updated = true; + if (act->is_mutex_op()) + process_mutex(act); + if (updated) work_queue.push_back(CheckRelSeqWorkEntry(act->get_location())); break; @@ -443,18 +549,30 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) case WORK_CHECK_RELEASE_SEQ: resolve_release_sequences(work.location, &work_queue); break; - case WORK_CHECK_MO_EDGES: - /** @todo Perform follow-up mo_graph checks */ + case WORK_CHECK_MO_EDGES: { + /** @todo Complete verification of work_queue */ + ModelAction *act = work.action; + bool updated = false; + + if (act->is_read()) { + if (r_modification_order(act, act->get_reads_from())) + updated = true; + } + if (act->is_write()) { + if (w_modification_order(act)) + updated = true; + } + + if (updated) + work_queue.push_back(CheckRelSeqWorkEntry(act->get_location())); + break; + } default: ASSERT(false); break; } } - /* Add action to list. */ - if (!second_part_of_rmw) - add_action_to_lists(curr); - check_curr_backtracking(curr); set_backtracking(curr); @@ -462,6 +580,19 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) return get_next_thread(curr); } +/** + * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH + * operation from the Thread it is joining with. Must be called after the + * completion of the Thread in question. + * @param join The THREAD_JOIN action + */ +void ModelChecker::do_complete_join(ModelAction *join) +{ + Thread *blocking = (Thread *)join->get_location(); + ModelAction *act = get_last_action(blocking->get_id()); + join->synchronize_with(act); +} + void ModelChecker::check_curr_backtracking(ModelAction * curr) { Node *currnode = curr->get_node(); Node *parnode = currnode->get_parent(); @@ -500,11 +631,24 @@ bool ModelChecker::isfeasible() { /** @returns whether the current partial trace is feasible other than * multiple RMW reading from the same store. */ bool ModelChecker::isfeasibleotherthanRMW() { + if (DBG_ENABLED()) { + if (mo_graph->checkForCycles()) + DEBUG("Infeasible: modification order cycles\n"); + if (failed_promise) + DEBUG("Infeasible: failed promise\n"); + if (too_many_reads) + DEBUG("Infeasible: too many reads\n"); + if (promises_expired()) + DEBUG("Infeasible: promises expired\n"); + } return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired(); } /** Returns whether the current completed trace is feasible. */ bool ModelChecker::isfinalfeasible() { + if (DBG_ENABLED() && promises->size() != 0) + DEBUG("Infeasible: unrevolved promises\n"); + return isfeasible() && promises->size() == 0; } @@ -531,7 +675,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) { * * If so, we decide that the execution is no longer feasible. */ -void ModelChecker::check_recency(ModelAction *curr, bool already_added) { +void ModelChecker::check_recency(ModelAction *curr) { if (params.maxreads != 0) { if (curr->get_node()->get_read_from_size() <= 1) return; @@ -552,12 +696,10 @@ void ModelChecker::check_recency(ModelAction *curr, bool already_added) { action_list_t::reverse_iterator rit = list->rbegin(); /* Skip past curr */ - if (already_added) { - for (; (*rit) != curr; rit++) - ; - /* go past curr now */ - rit++; - } + for (; (*rit) != curr; rit++) + ; + /* go past curr now */ + rit++; action_list_t::reverse_iterator ritcopy = rit; //See if we have enough reads from the same value @@ -648,10 +790,13 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; - /* Include at most one act per-thread that "happens before" curr */ - if (act->happens_before(curr)) { + /* + * Include at most one act per-thread that "happens + * before" curr. Don't consider reflexively. + */ + if (act->happens_before(curr) && act != curr) { if (act->is_write()) { - if (rf != act && act != curr) { + if (rf != act) { mo_graph->addEdge(act, rf); added = true; } @@ -662,7 +807,6 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf added = true; } } - break; } } @@ -755,7 +899,7 @@ bool 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()); + ModelAction *last_seq_cst = get_last_seq_cst(curr); if (last_seq_cst != NULL) { mo_graph->addEdge(last_seq_cst, curr); added = true; @@ -769,8 +913,23 @@ bool ModelChecker::w_modification_order(ModelAction *curr) action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; + if (act == curr) { + /* + * If RMW, we already have all relevant edges, + * so just skip to next thread. + * If normal write, we need to look at earlier + * actions, so continue processing list. + */ + if (curr->is_rmw()) + break; + else + continue; + } - /* Include at most one act per-thread that "happens before" curr */ + /* + * Include at most one act per-thread that "happens + * before" curr + */ if (act->happens_before(curr)) { /* * Note: if act is RMW, just add edge: @@ -778,11 +937,9 @@ bool ModelChecker::w_modification_order(ModelAction *curr) * The following edge should be handled elsewhere: * readfrom(act) --mo--> act */ - if (act->is_write()) { - //RMW shouldn't have an edge to themselves - if (act!=curr) - mo_graph->addEdge(act, curr); - } else if (act->is_read() && act->get_reads_from() != NULL) + if (act->is_write()) + mo_graph->addEdge(act, curr); + else if (act->is_read() && act->get_reads_from() != NULL) mo_graph->addEdge(act->get_reads_from(), curr); added = true; break; @@ -853,8 +1010,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con * @return true, if the ModelChecker is certain that release_heads is complete; * false otherwise */ -bool ModelChecker::release_seq_head(const ModelAction *rf, - std::vector< const ModelAction *, MyAlloc > *release_heads) const +bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const { if (!rf) { /* read from future: need to settle this later */ @@ -959,15 +1115,14 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, * with the head(s) of the release sequence(s), if they exists with certainty. * @see ModelChecker::release_seq_head */ -void ModelChecker::get_release_seq_heads(ModelAction *act, - std::vector< const ModelAction *, MyAlloc > *release_heads) +void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads) { const ModelAction *rf = act->get_reads_from(); bool complete; complete = release_seq_head(rf, release_heads); if (!complete) { /* add act to 'lazy checking' list */ - std::list *list; + action_list_t *list; list = lazy_sync_with_release->get_safe_ptr(act->get_location()); list->push_back(act); (*lazy_sync_size)++; @@ -989,17 +1144,17 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, */ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue) { - std::list *list; + action_list_t *list; list = lazy_sync_with_release->getptr(location); if (!list) return false; bool updated = false; - std::list::iterator it = list->begin(); + action_list_t::iterator it = list->begin(); while (it != list->end()) { ModelAction *act = *it; const ModelAction *rf = act->get_reads_from(); - std::vector< const ModelAction *, MyAlloc > release_heads; + rel_heads_list_t release_heads; bool complete; complete = release_seq_head(rf, &release_heads); for (unsigned int i = 0; i < release_heads.size(); i++) { @@ -1065,25 +1220,41 @@ void ModelChecker::add_action_to_lists(ModelAction *act) ModelAction * ModelChecker::get_last_action(thread_id_t tid) { - int nthreads = get_num_threads(); - if ((int)thrd_last_action->size() < nthreads) - thrd_last_action->resize(nthreads); - return (*thrd_last_action)[id_to_int(tid)]; + int threadid=id_to_int(tid); + if (threadid<(int)thrd_last_action->size()) + return (*thrd_last_action)[id_to_int(tid)]; + else + return NULL; } /** - * Gets the last memory_order_seq_cst action (in the total global sequence) - * performed on a particular object (i.e., memory location). - * @param location The object location to check - * @return The last seq_cst action performed + * Gets the last memory_order_seq_cst write (in the total global sequence) + * performed on a particular object (i.e., memory location), not including the + * current action. + * @param curr The current ModelAction; also denotes the object location to + * check + * @return The last seq_cst write */ -ModelAction * ModelChecker::get_last_seq_cst(const void *location) +ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) +{ + 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)}) */ + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) + if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr) + return *rit; + return NULL; +} + +ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) { + 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)}) */ action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) - if ((*rit)->is_write() && (*rit)->is_seqcst()) + if ((*rit)->is_unlock()) return *rit; return NULL; } @@ -1197,7 +1368,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) bool initialized = false; if (curr->is_seqcst()) { - last_seq_cst = get_last_seq_cst(curr->get_location()); + last_seq_cst = get_last_seq_cst(curr); /* We have to at least see the last sequentially consistent write, so we are initialized. */ if (last_seq_cst != NULL) @@ -1213,7 +1384,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) ModelAction *act = *rit; /* Only consider 'write' actions */ - if (!act->is_write()) + if (!act->is_write() || act == curr) continue; /* Don't consider more than one seq_cst write if we are a seq_cst read. */ @@ -1321,25 +1492,23 @@ int ModelChecker::switch_to_master(ModelAction *act) * @return Returns true (success) if a step was taken and false otherwise. */ bool ModelChecker::take_step() { - Thread *curr, *next; - if (has_asserted()) return false; - curr = thread_current(); + Thread * curr = thread_current(); if (curr) { if (curr->get_state() == THREAD_READY) { ASSERT(priv->current_action); priv->nextThread = check_current_action(priv->current_action); priv->current_action = NULL; - if (!curr->is_blocked() && !curr->is_complete()) - scheduler->add_thread(curr); + if (curr->is_blocked() || curr->is_complete()) + scheduler->remove_thread(curr); } else { ASSERT(false); } } - next = scheduler->next_thread(priv->nextThread); + Thread * next = scheduler->next_thread(priv->nextThread); /* Infeasible -> don't take any more steps */ if (!isfeasible()) @@ -1352,6 +1521,15 @@ bool ModelChecker::take_step() { /* next == NULL -> don't take any more steps */ if (!next) return false; + + if ( next->get_pending() != NULL ) { + //restart a pending action + set_current_action(next->get_pending()); + next->set_pending(NULL); + next->set_state(THREAD_READY); + return true; + } + /* Return false only if swap fails with an error */ return (Thread::swap(&system_context, next) == 0); }