X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=e6df37f8372949f610057599181402ddf673ce84;hb=ceac3a2484741a39bcb00f8593514f65be8bbe85;hp=4d6e8af72b388dedf2502b13d732b9d801365a94;hpb=c685b2d29f203fd55e6ca2ad5db0f0a06e31aa79;p=model-checker.git diff --git a/model.cc b/model.cc index 4d6e8af..e6df37f 100644 --- a/model.cc +++ b/model.cc @@ -159,7 +159,7 @@ void ModelChecker::reset_to_initial_state() /* Print all model-checker output before rollback */ fflush(model_out); - snapshotObject->backTrackBeforeStep(0); + snapshot_backtrack_before(0); } /** @return a thread ID for a new Thread */ @@ -174,7 +174,12 @@ unsigned int ModelChecker::get_num_threads() const return priv->next_thread_id; } -/** @return The currently executing Thread. */ +/** + * Must be called from user-thread context (e.g., through the global + * thread_current() interface) + * + * @return The currently executing Thread. + */ Thread * ModelChecker::get_current_thread() const { return scheduler->get_current_thread(); @@ -212,9 +217,8 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) /* 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(); + return curr->get_thread_operand(); } /* Have we completed exploring the preselected path? */ @@ -254,6 +258,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) tid = next->get_tid(); node_stack->pop_restofstack(2); } else { + ASSERT(prevnode); /* Make a different thread execute for next step */ scheduler->add_sleep(get_thread(next->get_tid())); tid = prevnode->get_next_backtrack(); @@ -609,7 +614,7 @@ void ModelChecker::set_backtracking(ModelAction *act) Node *node = prev->get_node()->get_parent(); int low_tid, high_tid; - if (node->is_enabled(t)) { + if (node->enabled_status(t->get_id()) == THREAD_ENABLED) { low_tid = id_to_int(act->get_tid()); high_tid = low_tid + 1; } else { @@ -819,7 +824,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) if (curr->get_node()->get_misc() == 0) { get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr); //disable us - scheduler->sleep(get_current_thread()); + scheduler->sleep(get_thread(curr)); } break; } @@ -848,6 +853,15 @@ bool ModelChecker::process_mutex(ModelAction *curr) return false; } +void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader) +{ + /* Do more ambitious checks now that mo is more complete */ + if (mo_may_allow(writer, reader) && + reader->get_node()->add_future_value(writer->get_value(), + writer->get_seq_number() + params.maxfuturedelay)) + set_latest_backtrack(reader); +} + /** * Process a write ModelAction * @param curr The ModelAction to process @@ -861,12 +875,9 @@ bool ModelChecker::process_write(ModelAction *curr) if (promises->size() == 0) { for (unsigned int i = 0; i < futurevalues->size(); i++) { struct PendingFutureValue pfv = (*futurevalues)[i]; - //Do more ambitious checks now that mo is more complete - if (mo_may_allow(pfv.writer, pfv.act) && - pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number() + params.maxfuturedelay)) - set_latest_backtrack(pfv.act); + add_future_value(pfv.writer, pfv.act); } - futurevalues->resize(0); + futurevalues->clear(); } mo_graph->commitChanges(); @@ -943,12 +954,12 @@ bool ModelChecker::process_thread_action(ModelAction *curr) switch (curr->get_type()) { case THREAD_CREATE: { - Thread *th = (Thread *)curr->get_location(); + Thread *th = curr->get_thread_operand(); th->set_creation(curr); break; } case THREAD_JOIN: { - Thread *blocking = (Thread *)curr->get_location(); + Thread *blocking = curr->get_thread_operand(); ModelAction *act = get_last_action(blocking->get_id()); curr->synchronize_with(act); updated = true; /* trigger rel-seq checks */ @@ -1191,11 +1202,10 @@ void ModelChecker::set_current_action(ModelAction *act) { * execution when running permutations of previously-observed executions. * * @param curr The current action to process - * @return The next Thread that must be executed. May be NULL if ModelChecker - * makes no choice (e.g., according to replay execution, combining RMW actions, - * etc.) + * @return The ModelAction that is actually executed; may be different than + * curr; may be NULL, if the current action is not enabled to run */ -Thread * ModelChecker::check_current_action(ModelAction *curr) +ModelAction * ModelChecker::check_current_action(ModelAction *curr) { ASSERT(curr); bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw(); @@ -1203,13 +1213,17 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (!check_action_enabled(curr)) { /* Make the execution look like we chose to run this action * much later, when a lock/join can succeed */ - get_current_thread()->set_pending(curr); - scheduler->sleep(get_current_thread()); - return get_next_thread(NULL); + get_thread(curr)->set_pending(curr); + scheduler->sleep(get_thread(curr)); + return NULL; } bool newly_explored = initialize_curr_action(&curr); + DBG(); + if (DBG_ENABLED()) + curr->print(); + wake_up_sleeping_actions(curr); /* Add the action to lists before any other model-checking tasks */ @@ -1287,7 +1301,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) check_curr_backtracking(curr); set_backtracking(curr); - return get_next_thread(curr); + return curr; } void ModelChecker::check_curr_backtracking(ModelAction *curr) @@ -1295,7 +1309,7 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr) Node *currnode = curr->get_node(); Node *parnode = currnode->get_parent(); - if (!parnode->backtrack_empty() || + if ((parnode && !parnode->backtrack_empty()) || !currnode->misc_empty() || !currnode->read_from_empty() || !currnode->future_value_empty() || @@ -1325,15 +1339,39 @@ bool ModelChecker::isfeasibleprefix() const return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq(); } +/** + * Print disagnostic information about an infeasible execution + * @param prefix A string to prefix the output with; if NULL, then a default + * message prefix will be provided + */ +void ModelChecker::print_infeasibility(const char *prefix) const +{ + char buf[100]; + char *ptr = buf; + if (mo_graph->checkForRMWViolation()) + ptr += sprintf(ptr, "[RMW atomicity]"); + if (mo_graph->checkForCycles()) + ptr += sprintf(ptr, "[mo cycle]"); + if (priv->failed_promise) + ptr += sprintf(ptr, "[failed promise]"); + if (priv->too_many_reads) + ptr += sprintf(ptr, "[too many reads]"); + if (priv->bad_synchronization) + ptr += sprintf(ptr, "[bad sw ordering]"); + if (promises_expired()) + ptr += sprintf(ptr, "[promise expired]"); + if (promises->size() != 0) + ptr += sprintf(ptr, "[unresolved promise]"); + if (ptr != buf) + model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf); +} + /** * Returns whether the current completed trace is feasible, except for pending * release sequences. */ bool ModelChecker::is_feasible_prefix_ignore_relseq() const { - if (DBG_ENABLED() && promises->size() != 0) - DEBUG("Infeasible: unrevolved promises\n"); - return !is_infeasible() && promises->size() == 0; } @@ -1345,9 +1383,6 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const */ bool ModelChecker::is_infeasible() const { - if (DBG_ENABLED() && mo_graph->checkForRMWViolation()) - DEBUG("Infeasible: RMW violation\n"); - return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW(); } @@ -1361,18 +1396,6 @@ bool ModelChecker::is_infeasible() const * */ bool ModelChecker::is_infeasible_ignoreRMW() const { - if (DBG_ENABLED()) { - if (mo_graph->checkForCycles()) - DEBUG("Infeasible: modification order cycles\n"); - if (priv->failed_promise) - DEBUG("Infeasible: failed promise\n"); - if (priv->too_many_reads) - DEBUG("Infeasible: too many reads\n"); - if (priv->bad_synchronization) - DEBUG("Infeasible: bad synchronization ordering\n"); - if (promises_expired()) - DEBUG("Infeasible: promises expired\n"); - } return mo_graph->checkForCycles() || priv->failed_promise || priv->too_many_reads || priv->bad_synchronization || promises_expired(); @@ -1765,8 +1788,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) if (thin_air_constraint_may_allow(curr, act)) { if (!is_infeasible() || (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) { - struct PendingFutureValue pfv = {curr, act}; - futurevalues->push_back(pfv); + futurevalues->push_back(PendingFutureValue(curr, act)); } } } @@ -2503,14 +2525,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act)) allow_read = false; - if (allow_read) { - DEBUG("Adding action to may_read_from:\n"); - if (DBG_ENABLED()) { - act->print(); - curr->print(); - } + if (allow_read) curr->get_node()->add_read_from(act); - } /* Include at most one act per-thread that "happens before" curr */ if (act->happens_before(curr)) @@ -2560,13 +2576,11 @@ ModelAction * ModelChecker::new_uninitialized_action(void *location) const return act; } -static void print_list(action_list_t *list, int exec_num = -1) +static void print_list(action_list_t *list) { action_list_t::iterator it; model_print("---------------------------------------------------------------------\n"); - if (exec_num >= 0) - model_print("Execution %d:\n", exec_num); unsigned int hash = 0; @@ -2619,9 +2633,12 @@ void ModelChecker::print_summary() const dumpGraph(buffername); #endif - if (!isfeasibleprefix()) - model_print("INFEASIBLE EXECUTION!\n"); - print_list(action_trace, stats.num_total); + model_print("Execution %d:", stats.num_total); + if (isfeasibleprefix()) + model_print("\n"); + else + print_infeasibility(" INFEASIBLE"); + print_list(action_trace); model_print("\n"); } @@ -2722,12 +2739,7 @@ bool ModelChecker::take_step(ModelAction *curr) Thread *curr_thrd = get_thread(curr); ASSERT(curr_thrd->get_state() == THREAD_READY); - Thread *next_thrd = check_current_action(curr); - - if (curr_thrd->is_blocked() || curr_thrd->is_complete()) - scheduler->remove_thread(curr_thrd); - - next_thrd = scheduler->next_thread(next_thrd); + curr = check_current_action(curr); /* Infeasible -> don't take any more steps */ if (is_infeasible()) @@ -2737,11 +2749,15 @@ bool ModelChecker::take_step(ModelAction *curr) return false; } - if (params.bound != 0) { - if (priv->used_sequence_numbers > params.bound) { + if (params.bound != 0) + if (priv->used_sequence_numbers > params.bound) return false; - } - } + + if (curr_thrd->is_blocked() || curr_thrd->is_complete()) + scheduler->remove_thread(curr_thrd); + + Thread *next_thrd = get_next_thread(curr); + next_thrd = scheduler->next_thread(next_thrd); DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1, next_thrd ? id_to_int(next_thrd->get_id()) : -1);