X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=94620ea9d0400fcee239973705361210542040f5;hb=6b87c110fbda87ccec4f58b1e292d5f9434c8691;hp=2aaa1c26dbea3ad9e78720683635a117d83243f1;hpb=55eb20c50ec656d385fb6e94c01aea55e9514917;p=model-checker.git diff --git a/model.cc b/model.cc index 2aaa1c2..94620ea 100644 --- a/model.cc +++ b/model.cc @@ -101,7 +101,7 @@ thread_id_t ModelChecker::get_next_id() } /** @return the number of user threads created during this execution */ -unsigned int ModelChecker::get_num_threads() +unsigned int ModelChecker::get_num_threads() const { return priv->next_thread_id; } @@ -208,7 +208,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) return thread_map->get(id_to_int(tid)); } -/** +/** * We need to know what the next actions of all threads in the sleep * set will be. This method computes them and stores the actions at * the corresponding thread object's pending action. @@ -218,7 +218,8 @@ void ModelChecker::execute_sleep_set() { for(unsigned int i=0;iget_enabled(thr) == THREAD_SLEEP_SET ) { + if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET && + thr->get_pending() == NULL ) { thr->set_state(THREAD_RUNNING); scheduler->next_thread(thr); Thread::swap(&system_context, thr); @@ -235,12 +236,32 @@ void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { Thread *thr=get_thread(tid); if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) { ModelAction *pending_act=thr->get_pending(); - if (pending_act->could_synchronize_with(curr)) { + if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) { //Remove this thread from sleep set scheduler->remove_sleep(thr); } } - } + } +} + +/** + * 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 *t = get_thread(int_to_id(i)); + if (scheduler->is_enabled(t) != THREAD_DISABLED) + return false; + else if (!t->is_model_thread() && t->get_pending()) + blocking_threads = true; + } + return blocking_threads; } /** @@ -256,6 +277,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) @@ -271,8 +294,10 @@ bool ModelChecker::next_execution() pending_rel_seqs->size()); - if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) + if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) { + checkDataRaces(); print_summary(); + } if ((diverge = get_next_backtrack()) == NULL) return false; @@ -383,10 +408,14 @@ void ModelChecker::set_backtracking(ModelAction *act) for(int i = low_tid; i < high_tid; i++) { thread_id_t tid = int_to_id(i); + /* Make sure this thread can be enabled here. */ + if (i >= node->get_num_threads()) + break; + /* Don't backtrack into a point where the thread is disabled or sleeping. */ - if (node->get_enabled_array()[i]!=THREAD_ENABLED) + if (node->enabled_status(tid)!=THREAD_ENABLED) continue; - + /* Check if this has been explored already */ if (node->has_been_explored(tid)) continue; @@ -441,7 +470,7 @@ ModelAction * ModelChecker::get_next_backtrack() */ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) { - uint64_t value; + uint64_t value = VALUE_NONE; bool updated = false; while (true) { const ModelAction *reads_from = curr->get_node()->get_read_from(); @@ -744,41 +773,46 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu * 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. + * freed/invalidated after the execution of this function, with a different + * action "returned" its place (pass-by-reference) + * @return True if curr is a newly-explored action; false otherwise */ -ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) +bool ModelChecker::initialize_curr_action(ModelAction **curr) { ModelAction *newcurr; - if (curr->is_rmwc() || curr->is_rmw()) { - newcurr = process_rmw(curr); - delete curr; + if ((*curr)->is_rmwc() || (*curr)->is_rmw()) { + newcurr = process_rmw(*curr); + delete *curr; if (newcurr->is_rmw()) compute_promises(newcurr); - return newcurr; + + *curr = newcurr; + return false; } - curr->set_seq_number(get_next_seq_num()); + (*curr)->set_seq_number(get_next_seq_num()); - newcurr = node_stack->explore_action(curr, scheduler->get_enabled()); + 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); + if ((*curr)->is_rmwr()) + newcurr->copy_typeandorder(*curr); - ASSERT(curr->get_location() == newcurr->get_location()); - newcurr->copy_from_new(curr); + ASSERT((*curr)->get_location() == newcurr->get_location()); + newcurr->copy_from_new(*curr); /* Discard duplicate ModelAction; use action from NodeStack */ - delete curr; + delete *curr; /* Always compute new clock vector */ newcurr->create_cv(get_parent_action(newcurr->get_tid())); + + *curr = newcurr; + return false; /* Action was explored previously */ } else { - newcurr = curr; + newcurr = *curr; /* Always compute new clock vector */ newcurr->create_cv(get_parent_action(newcurr->get_tid())); @@ -795,8 +829,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) else if (newcurr->is_notify_one()) { newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size()); } + return true; /* This was a new ModelAction */ } - return newcurr; } /** @@ -854,18 +888,17 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) return get_next_thread(NULL); } - ModelAction *newcurr = initialize_curr_action(curr); + bool newly_explored = initialize_curr_action(&curr); wake_up_sleeping_actions(curr); /* Add the action to lists before any other model-checking tasks */ if (!second_part_of_rmw) - add_action_to_lists(newcurr); + add_action_to_lists(curr); /* Build may_read_from set for newly-created actions */ - if (curr == newcurr && curr->is_read()) + if (newly_explored && curr->is_read()) build_reads_from_past(curr); - curr = newcurr; /* Initialize work_queue with the "current action" work */ work_queue_t work_queue(1, CheckCurrWorkEntry(curr)); @@ -963,7 +996,7 @@ bool ModelChecker::promises_expired() { /** @return whether the current partial trace must be a prefix of a * feasible trace. */ bool ModelChecker::isfeasibleprefix() { - return promises->size() == 0 && pending_rel_seqs->size() == 0; + return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible(); } /** @return whether the current partial trace is feasible. */ @@ -1055,7 +1088,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { ModelAction *act = *rit; if (!act->is_read()) return; - + if (act->get_reads_from() != rf) return; if (act->get_node()->get_read_from_size() <= 1) @@ -1086,7 +1119,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { ModelAction *act=*rit; bool foundvalue = false; for (int j = 0; jget_node()->get_read_from_size(); j++) { - if (act->get_node()->get_read_from_at(i)==write) { + if (act->get_node()->get_read_from_at(j)==write) { foundvalue = true; break; } @@ -1280,7 +1313,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) * 1) If RMW and it actually read from something, then we * already have all relevant edges, so just skip to next * thread. - * + * * 2) If RMW and it didn't read from anything, we should * whatever edge we can get to speed up convergence. * @@ -1290,7 +1323,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) if (curr->is_rmw()) { if (curr->get_reads_from()!=NULL) break; - else + else continue; } else continue; @@ -1309,7 +1342,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) */ if (act->is_write()) mo_graph->addEdge(act, curr); - else if (act->is_read()) { + else if (act->is_read()) { //if previous read accessed a null, just keep going if (act->get_reads_from() == NULL) continue; @@ -1366,33 +1399,42 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con return true; } -/** Arbitrary reads from the future are not allowed. Section 29.3 - * part 9 places some constraints. This method checks one result of constraint - * constraint. Others require compiler support. */ -bool ModelChecker::mo_may_allow(const ModelAction * writer, const ModelAction *reader) { +/** + * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places + * some constraints. This method checks one the following constraint (others + * require compiler support): + * + * If X --hb-> Y --mo-> Z, then X should not read from Z. + */ +bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader) +{ std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location()); + unsigned int i; + /* Iterate over all threads */ + for (i = 0; i < thrd_lists->size(); i++) { + const ModelAction *write_after_read = NULL; - //Get write that follows reader action - action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())]; - action_list_t::reverse_iterator rit; - ModelAction *first_write_after_read=NULL; - - for (rit = list->rbegin(); rit != list->rend(); rit++) { - ModelAction *act = *rit; - if (act==reader) - break; - if (act->is_write()) - first_write_after_read=act; - } + /* Iterate over actions in thread, starting from most recent */ + action_list_t *list = &(*thrd_lists)[i]; + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *act = *rit; - if (first_write_after_read==NULL) - return true; + if (!reader->happens_before(act)) + break; + else if (act->is_write()) + write_after_read = act; + else if (act->is_read() && act->get_reads_from() != NULL && act != reader) { + write_after_read = act->get_reads_from(); + } + } - return !mo_graph->checkReachable(first_write_after_read, writer); + if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer)) + return false; + } + return true; } - - /** * Finds the head(s) of the release sequence(s) containing a given ModelAction. * The ModelAction under consideration is expected to be taking part in @@ -1509,8 +1551,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, continue; } - /* Only writes can break release sequences */ - if (!act->is_write()) + /* Only non-RMW writes can break release sequences */ + if (!act->is_write() || act->is_rmw()) continue; /* Check modification order */ @@ -1670,7 +1712,7 @@ 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); - + std::vector *vec = obj_thrd_map->get_safe_ptr(mutex_loc); if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); @@ -1782,7 +1824,7 @@ bool ModelChecker::resolve_promises(ModelAction *write) //Make sure the promise's value matches the write's value ASSERT(promise->get_value() == write->get_value()); delete(promise); - + promises->erase(promises->begin() + promise_index); threads_to_check.push_back(read->get_tid()); @@ -1815,8 +1857,9 @@ void ModelChecker::compute_promises(ModelAction *curr) act->is_read() && !act->could_synchronize_with(curr) && !act->same_thread(curr) && + act->get_location() == curr->get_location() && promise->get_value() == curr->get_value()) { - curr->get_node()->set_promise(i); + curr->get_node()->set_promise(i, act->is_rmw()); } } } @@ -1838,10 +1881,20 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec } } +void ModelChecker::check_promises_thread_disabled() { + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + if (promise->check_promise()) { + failed_promise = true; + return; + } + } +} + /** Checks promises in response to addition to modification order for threads. * Definitions: * pthread is the thread that performed the read that created the promise - * + * * pread is the read that created the promise * * pwrite is either the first write to same location as pread by @@ -1870,7 +1923,7 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; const ModelAction *act = promise->get_action(); - + //Is this promise on the same location? if ( act->get_location() != location ) continue; @@ -1892,12 +1945,12 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) return; } } - + //Don't do any lookups twice for the same thread if (promise->has_sync_thread(tid)) continue; - - if (mo_graph->checkReachable(promise->get_write(), write)) { + + if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) { if (promise->increment_threads(tid)) { failed_promise = true; return; @@ -1969,17 +2022,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 */ @@ -1993,6 +2043,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) if (!initialized) { /** @todo Need a more informative way of reporting errors. */ printf("ERROR: may read from uninitialized atomic\n"); + set_assert(); } if (DBG_ENABLED() || !initialized) { @@ -2002,14 +2053,13 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) curr->get_node()->print_may_read_from(); printf("End printing may_read_from\n"); } - - ASSERT(initialized); } bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) { while(true) { Node *prevnode=write->get_node()->get_parent(); - bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET; + + bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET; if (write->is_release()&&thread_sleep) return true; if (!write->is_rmw()) { @@ -2028,7 +2078,7 @@ static void print_list(action_list_t *list) printf("---------------------------------------------------------------------\n"); printf("Trace:\n"); unsigned int hash=0; - + for (it = list->begin(); it != list->end(); it++) { (*it)->print(); hash=hash^(hash<<3)^((*it)->hash()); @@ -2040,12 +2090,12 @@ static void print_list(action_list_t *list) #if SUPPORT_MOD_ORDER_DUMP void ModelChecker::dumpGraph(char *filename) { char buffer[200]; - sprintf(buffer, "%s.dot",filename); - FILE *file=fopen(buffer, "w"); - fprintf(file, "digraph %s {\n",filename); + sprintf(buffer, "%s.dot",filename); + FILE *file=fopen(buffer, "w"); + fprintf(file, "digraph %s {\n",filename); 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++) { ModelAction *action=*it; if (action->is_read()) { @@ -2056,12 +2106,12 @@ void ModelChecker::dumpGraph(char *filename) { if (thread_array[action->get_tid()] != NULL) { fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number()); } - + thread_array[action->get_tid()]=action; } - fprintf(file,"}\n"); + fprintf(file,"}\n"); model_free(thread_array); - fclose(file); + fclose(file); } #endif @@ -2078,7 +2128,7 @@ void ModelChecker::print_summary() sprintf(buffername, "exec%04u", num_executions); mo_graph->dumpGraphToFile(buffername); sprintf(buffername, "graph%04u", num_executions); - dumpGraph(buffername); + dumpGraph(buffername); #endif if (!isfinalfeasible()) @@ -2099,7 +2149,7 @@ void ModelChecker::add_thread(Thread *t) } /** - * Removes a thread from the scheduler. + * Removes a thread from the scheduler. * @param the thread to remove. */ void ModelChecker::remove_thread(Thread *t)