X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=0bccd833ff843e40fd700f8ea3f198b1a2f4e065;hp=059a5228590f260813a50b28707d542cc20da4a3;hb=8d9a43be3bc794d7c9096dbda88640eb2fa99ee6;hpb=9ab812e65ac3bdf679247f01611f21d1af8968b9 diff --git a/model.cc b/model.cc index 059a5228..0bccd833 100644 --- a/model.cc +++ b/model.cc @@ -39,16 +39,15 @@ struct bug_message { */ struct model_snapshot_members { model_snapshot_members() : - current_action(NULL), /* First thread created will have id INITIAL_THREAD_ID */ next_thread_id(INITIAL_THREAD_ID), used_sequence_numbers(0), - nextThread(NULL), next_backtrack(NULL), bugs(), stats(), failed_promise(false), too_many_reads(false), + no_valid_reads(false), bad_synchronization(false), asserted(false) { } @@ -59,15 +58,14 @@ struct model_snapshot_members { bugs.clear(); } - ModelAction *current_action; unsigned int next_thread_id; modelclock_t used_sequence_numbers; - Thread *nextThread; ModelAction *next_backtrack; std::vector< bug_message *, SnapshotAlloc > bugs; struct execution_stats stats; bool failed_promise; bool too_many_reads; + bool no_valid_reads; /** @brief Incorrectly-ordered synchronization was made */ bool bad_synchronization; bool asserted; @@ -161,7 +159,15 @@ void ModelChecker::reset_to_initial_state() /* Print all model-checker output before rollback */ fflush(model_out); - snapshotObject->backTrackBeforeStep(0); + /** + * FIXME: if we utilize partial rollback, we will need to free only + * those pending actions which were NOT pending before the rollback + * point + */ + for (unsigned int i = 0; i < get_num_threads(); i++) + delete get_thread(int_to_id(i))->get_pending(); + + snapshot_backtrack_before(0); } /** @return a thread ID for a new Thread */ @@ -176,7 +182,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(); @@ -200,11 +211,14 @@ Node * ModelChecker::get_curr_node() const * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be * followed by a THREAD_START, or it can enforce execution replay/backtracking. * The model-checker may have no preference regarding the next thread (i.e., - * when exploring a new execution ordering), in which case this will return - * NULL. - * @param curr The current ModelAction. This action might guide the choice of - * next thread. - * @return The next thread to run. If the model-checker has no preference, NULL. + * when exploring a new execution ordering), in which case we defer to the + * scheduler. + * + * @param curr Optional: The current ModelAction. Only used if non-NULL and it + * might guide the choice of next thread (i.e., THREAD_CREATE should be + * followed by THREAD_START, or ATOMIC_RMWR followed by ATOMIC_{RMW,RMWC}) + * @return The next chosen thread to run, if any exist. Or else if no threads + * remain to be executed, return NULL. */ Thread * ModelChecker::get_next_thread(ModelAction *curr) { @@ -213,15 +227,17 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) if (curr != NULL) { /* Do not split atomic actions. */ if (curr->is_rmwr()) - return thread_current(); - /* The THREAD_CREATE action points to the created Thread */ + return get_thread(curr); else if (curr->get_type() == THREAD_CREATE) - return (Thread *)curr->get_location(); + return curr->get_thread_operand(); } - /* Have we completed exploring the preselected path? */ + /* + * Have we completed exploring the preselected path? Then let the + * scheduler decide + */ if (diverge == NULL) - return NULL; + return scheduler->select_next_thread(); /* Else, we are trying to replay an execution */ ModelAction *next = node_stack->get_next()->get_action(); @@ -256,8 +272,9 @@ 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(thread_map->get(id_to_int(next->get_tid()))); + scheduler->add_sleep(get_thread(next->get_tid())); tid = prevnode->get_next_backtrack(); /* Make sure the backtracked thread isn't sleeping. */ node_stack->pop_restofstack(1); @@ -290,15 +307,10 @@ void ModelChecker::execute_sleep_set() for (unsigned int i = 0; i < get_num_threads(); i++) { thread_id_t tid = int_to_id(i); Thread *thr = get_thread(tid); - if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) { - thr->set_state(THREAD_RUNNING); - scheduler->next_thread(thr); - Thread::swap(&system_context, thr); - priv->current_action->set_sleep_flag(); - thr->set_pending(priv->current_action); + if (scheduler->is_sleep_set(thr) && thr->get_pending()) { + thr->get_pending()->set_sleep_flag(); } } - priv->current_action = NULL; } void ModelChecker::wake_up_sleeping_actions(ModelAction *curr) @@ -321,11 +333,22 @@ void ModelChecker::set_bad_synchronization() priv->bad_synchronization = true; } +/** + * Check whether the current trace has triggered an assertion which should halt + * its execution. + * + * @return True, if the execution should be aborted; false otherwise + */ bool ModelChecker::has_asserted() const { return priv->asserted; } +/** + * Trigger a trace assertion which should cause this execution to be halted. + * This can be due to a detected bug or due to an infeasibility that should + * halt ASAP. + */ void ModelChecker::set_assert() { priv->asserted = true; @@ -502,7 +525,7 @@ bool ModelChecker::next_execution() record_stats(); /* Output */ - if (DBG_ENABLED() || params.verbose || have_bug_reports()) + if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports())) print_execution(complete); else clear_program_output(); @@ -560,7 +583,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; - if (!act->same_thread(prev)&&prev->is_failed_trylock()) + if (!act->same_thread(prev) && prev->is_failed_trylock()) return prev; } break; @@ -571,9 +594,9 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; - if (!act->same_thread(prev)&&prev->is_failed_trylock()) + if (!act->same_thread(prev) && prev->is_failed_trylock()) return prev; - if (!act->same_thread(prev)&&prev->is_notify()) + if (!act->same_thread(prev) && prev->is_notify()) return prev; } break; @@ -586,7 +609,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; - if (!act->same_thread(prev)&&prev->is_wait()) + if (!act->same_thread(prev) && prev->is_wait()) return prev; } break; @@ -612,7 +635,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 { @@ -620,7 +643,7 @@ void ModelChecker::set_backtracking(ModelAction *act) high_tid = get_num_threads(); } - for(int i = low_tid; i < high_tid; i++) { + 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. */ @@ -649,8 +672,7 @@ void ModelChecker::set_backtracking(ModelAction *act) continue; } /* Cache the latest backtracking point */ - if (!priv->next_backtrack || *prev > *priv->next_backtrack) - priv->next_backtrack = prev; + set_latest_backtrack(prev); /* If this is a new backtracking point, mark the tree */ if (!node->set_backtrack(tid)) @@ -665,6 +687,26 @@ void ModelChecker::set_backtracking(ModelAction *act) } } +/** + * @brief Cache the a backtracking point as the "most recent", if eligible + * + * Note that this does not prepare the NodeStack for this backtracking + * operation, it only caches the action on a per-execution basis + * + * @param act The operation at which we should explore a different next action + * (i.e., backtracking point) + * @return True, if this action is now the most recent backtracking point; + * false otherwise + */ +bool ModelChecker::set_latest_backtrack(ModelAction *act) +{ + if (!priv->next_backtrack || *act > *priv->next_backtrack) { + priv->next_backtrack = act; + return true; + } + return false; +} + /** * Returns last backtracking point. The model checker will explore a different * path for this point in the next execution. @@ -700,8 +742,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) r_status = r_modification_order(curr, reads_from); } - - if (!second_part_of_rmw&&is_infeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) { + if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) { mo_graph->rollbackChanges(); priv->too_many_reads = false; continue; @@ -709,16 +750,19 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) read_from(curr, reads_from); mo_graph->commitChanges(); - mo_check_promises(curr->get_tid(), reads_from); + mo_check_promises(curr, true); updated |= r_status; } else if (!second_part_of_rmw) { /* Read from future value */ - value = curr->get_node()->get_future_value(); - modelclock_t expiration = curr->get_node()->get_future_value_expiration(); - curr->set_read_from(NULL); - Promise *valuepromise = new Promise(curr, value, expiration); - promises->push_back(valuepromise); + struct future_value fv = curr->get_node()->get_future_value(); + Promise *promise = new Promise(curr, fv); + value = fv.value; + curr->set_read_from_promise(promise); + promises->push_back(promise); + mo_graph->startChanges(); + updated = r_modification_order(curr, promise); + mo_graph->commitChanges(); } get_thread(curr)->set_return_value(value); return updated; @@ -749,7 +793,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) { mutex = (std::mutex *)curr->get_location(); state = mutex->get_state(); - } else if(curr->is_wait()) { + } else if (curr->is_wait()) { mutex = (std::mutex *)curr->get_value(); state = mutex->get_state(); } @@ -803,7 +847,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; } @@ -832,6 +876,27 @@ 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)) { + Node *node = reader->get_node(); + + /* Find an ancestor thread which exists at the time of the reader */ + Thread *write_thread = get_thread(writer); + while (id_to_int(write_thread->get_id()) >= node->get_num_threads()) + write_thread = write_thread->get_parent(); + + struct future_value fv = { + writer->get_value(), + writer->get_seq_number() + params.maxfuturedelay, + write_thread->get_id(), + }; + if (node->add_future_value(fv)) + set_latest_backtrack(reader); + } +} + /** * Process a write ModelAction * @param curr The ModelAction to process @@ -845,17 +910,13 @@ 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) && - (!priv->next_backtrack || *pfv.act > *priv->next_backtrack)) - priv->next_backtrack = pfv.act; + add_future_value(pfv.writer, pfv.act); } - futurevalues->resize(0); + futurevalues->clear(); } mo_graph->commitChanges(); - mo_check_promises(curr->get_tid(), curr); + mo_check_promises(curr, false); get_thread(curr)->set_return_value(VALUE_NONE); return updated_mod_order || updated_promises; @@ -928,12 +989,21 @@ bool ModelChecker::process_thread_action(ModelAction *curr) switch (curr->get_type()) { case THREAD_CREATE: { - Thread *th = (Thread *)curr->get_location(); + thrd_t *thrd = (thrd_t *)curr->get_location(); + struct thread_params *params = (struct thread_params *)curr->get_value(); + Thread *th = new Thread(thrd, params->func, params->arg); + add_thread(th); th->set_creation(curr); + /* Promises can be satisfied by children */ + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + if (promise->thread_is_available(curr->get_tid())) + promise->add_thread(th->get_id()); + } 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 */ @@ -946,6 +1016,13 @@ bool ModelChecker::process_thread_action(ModelAction *curr) scheduler->wake(get_thread(act)); } th->complete(); + /* Completed thread can't satisfy promises */ + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + if (promise->thread_is_available(th->get_id())) + if (promise->eliminate_thread(th->get_id())) + priv->failed_promise = true; + } updated = true; /* trigger rel-seq checks */ break; } @@ -1158,16 +1235,6 @@ 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 @@ -1176,11 +1243,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(); @@ -1188,13 +1254,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 */ @@ -1251,8 +1321,14 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (act->is_read()) { const ModelAction *rf = act->get_reads_from(); - if (rf != NULL && r_modification_order(act, rf)) - updated = true; + const Promise *promise = act->get_reads_from_promise(); + if (rf) { + if (r_modification_order(act, rf)) + updated = true; + } else if (promise) { + if (r_modification_order(act, promise)) + updated = true; + } } if (act->is_write()) { if (w_modification_order(act)) @@ -1272,7 +1348,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) @@ -1280,15 +1356,13 @@ 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() || !currnode->promise_empty() || - !currnode->relseq_break_empty()) - && (!priv->next_backtrack || - *curr > *priv->next_backtrack)) { - priv->next_backtrack = curr; + !currnode->relseq_break_empty()) { + set_latest_backtrack(curr); } } @@ -1312,15 +1386,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->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->no_valid_reads) + ptr += sprintf(ptr, "[no valid reads-from]"); + 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; } @@ -1332,36 +1430,11 @@ 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(); -} - -/** - * Check If the current partial trace is infeasible, while ignoring - * infeasibility related to 2 RMW's reading from the same store. It does not - * check end-of-execution feasibility. - * @see ModelChecker::is_infeasible - * @return whether the current partial trace is infeasible, ignoring multiple - * RMWs reading from the same store. - * */ -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 || + return mo_graph->checkForCycles() || + priv->no_valid_reads || + priv->failed_promise || + priv->too_many_reads || + priv->bad_synchronization || promises_expired(); } @@ -1369,8 +1442,11 @@ bool ModelChecker::is_infeasible_ignoreRMW() const ModelAction * ModelChecker::process_rmw(ModelAction *act) { ModelAction *lastread = get_last_action(act->get_tid()); lastread->process_rmw(act); - if (act->is_rmw() && lastread->get_reads_from() != NULL) { - mo_graph->addRMWEdge(lastread->get_reads_from(), lastread); + if (act->is_rmw()) { + if (lastread->get_reads_from()) + mo_graph->addRMWEdge(lastread->get_reads_from(), lastread); + else + mo_graph->addRMWEdge(lastread->get_reads_from_promise(), lastread); mo_graph->commitChanges(); } return lastread; @@ -1414,7 +1490,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) action_list_t::reverse_iterator ritcopy = rit; //See if we have enough reads from the same value int count = 0; - for (; count < params.maxreads; rit++,count++) { + for (; count < params.maxreads; rit++, count++) { if (rit == list->rend()) return; ModelAction *act = *rit; @@ -1434,23 +1510,19 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) if (write == rf) continue; - /* Test to see whether this is a feasible write to read from*/ - mo_graph->startChanges(); - r_modification_order(curr, write); - bool feasiblereadfrom = !is_infeasible(); - mo_graph->rollbackChanges(); + /* Test to see whether this is a feasible write to read from */ + /** NOTE: all members of read-from set should be + * feasible, so we no longer check it here **/ - if (!feasiblereadfrom) - continue; rit = ritcopy; bool feasiblewrite = true; //new we need to see if this write works for everyone - for (int loop = count; loop>0; loop--,rit++) { + for (int loop = count; loop > 0; loop--, rit++) { ModelAction *act = *rit; bool foundvalue = false; - for (int j = 0; jget_node()->get_read_from_size(); j++) { + for (int j = 0; j < act->get_node()->get_read_from_size(); j++) { if (act->get_node()->get_read_from_at(j) == write) { foundvalue = true; break; @@ -1474,7 +1546,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) * read. * * Basic idea is the following: Go through each other thread and find - * the lastest action that happened before our read. Two cases: + * the last action that happened before our read. Two cases: * * (1) The action is a write => that write must either occur before * the write we read from or be the write we read from. @@ -1483,10 +1555,11 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) * must occur before the write we read from or be the same write. * * @param curr The current action. Must be a read. - * @param rf The action that curr reads from. Must be a write. + * @param rf The ModelAction or Promise that curr reads from. Must be a write. * @return True if modification order edges were added; false otherwise */ -bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf) +template +bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf) { std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; @@ -1514,26 +1587,23 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; - if (act->is_write() && act != rf && act != curr) { + if (act->is_write() && !act->equals(rf) && act != curr) { /* C++, Section 29.3 statement 5 */ if (curr->is_seqcst() && last_sc_fence_thread_local && *act < *last_sc_fence_thread_local) { - mo_graph->addEdge(act, rf); - added = true; + added = mo_graph->addEdge(act, rf) || added; break; } /* C++, Section 29.3 statement 4 */ else if (act->is_seqcst() && last_sc_fence_local && *act < *last_sc_fence_local) { - mo_graph->addEdge(act, rf); - added = true; + added = mo_graph->addEdge(act, rf) || added; break; } /* C++, Section 29.3 statement 6 */ else if (last_sc_fence_thread_before && *act < *last_sc_fence_thread_before) { - mo_graph->addEdge(act, rf); - added = true; + added = mo_graph->addEdge(act, rf) || added; break; } } @@ -1544,9 +1614,8 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf */ if (act->happens_before(curr) && act != curr) { if (act->is_write()) { - if (rf != act) { - mo_graph->addEdge(act, rf); - added = true; + if (!act->equals(rf)) { + added = mo_graph->addEdge(act, rf) || added; } } else { const ModelAction *prevreadfrom = act->get_reads_from(); @@ -1554,9 +1623,8 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf if (prevreadfrom == NULL) continue; - if (rf != prevreadfrom) { - mo_graph->addEdge(prevreadfrom, rf); - added = true; + if (!prevreadfrom->equals(rf)) { + added = mo_graph->addEdge(prevreadfrom, rf) || added; } } break; @@ -1564,71 +1632,15 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf } } - return added; -} - -/** This method fixes up the modification order when we resolve a - * 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 - * the Action rf and that action. If the action is a read, we add a - * MO edge between the Action rf, and whatever the read accessed. - * - * @param curr is the read ModelAction that we are fixing up MO edges for. - * @param rf is the write ModelAction that curr reads from. - * - */ -void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf) -{ - std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); - unsigned int i; - ASSERT(curr->is_read()); - - /* Iterate over all threads */ - for (i = 0; i < thrd_lists->size(); i++) { - /* Iterate over actions in thread, starting from most recent */ - action_list_t *list = &(*thrd_lists)[i]; - action_list_t::reverse_iterator rit; - ModelAction *lastact = NULL; - - /* Find last action that happens after curr that is either not curr or a rmw */ - for (rit = list->rbegin(); rit != list->rend(); rit++) { - ModelAction *act = *rit; - if (curr->happens_before(act) && (curr != act || curr->is_rmw())) { - lastact = act; - } else - break; - } + /* + * All compatible, thread-exclusive promises must be ordered after any + * concrete loads from the same thread + */ + for (unsigned int i = 0; i < promises->size(); i++) + if ((*promises)[i]->is_compatible_exclusive(curr)) + added = mo_graph->addEdge(rf, (*promises)[i]) || added; - /* Include at most one act per-thread that "happens before" curr */ - if (lastact != NULL) { - if (lastact== curr) { - //Case 1: The resolved read is a RMW, and we need to make sure - //that the write portion of the RMW mod order after rf - - mo_graph->addEdge(rf, lastact); - } else if (lastact->is_read()) { - //Case 2: The resolved read is a normal read and the next - //operation is a read, and we need to make sure the value read - //is mod ordered after rf - - const ModelAction *postreadfrom = lastact->get_reads_from(); - if (postreadfrom != NULL && rf != postreadfrom) - mo_graph->addEdge(rf, postreadfrom); - } else { - //Case 3: The resolved read is a normal read and the next - //operation is a write, and we need to make sure that the - //write is mod ordered after rf - if (lastact != rf) - mo_graph->addEdge(rf, lastact); - } - break; - } - } + return added; } /** @@ -1665,8 +1677,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) so we are initialized. */ ModelAction *last_seq_cst = get_last_seq_cst_write(curr); if (last_seq_cst != NULL) { - mo_graph->addEdge(last_seq_cst, curr); - added = true; + added = mo_graph->addEdge(last_seq_cst, curr) || added; } } @@ -1709,8 +1720,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) /* C++, Section 29.3 statement 7 */ if (last_sc_fence_thread_before && act->is_write() && *act < *last_sc_fence_thread_before) { - mo_graph->addEdge(act, curr); - added = true; + added = mo_graph->addEdge(act, curr) || added; break; } @@ -1726,14 +1736,13 @@ bool ModelChecker::w_modification_order(ModelAction *curr) * readfrom(act) --mo--> act */ if (act->is_write()) - mo_graph->addEdge(act, curr); + added = mo_graph->addEdge(act, curr) || added; else if (act->is_read()) { //if previous read accessed a null, just keep going if (act->get_reads_from() == NULL) continue; - mo_graph->addEdge(act->get_reads_from(), curr); + added = mo_graph->addEdge(act->get_reads_from(), curr) || added; } - added = true; break; } else if (act->is_read() && !act->could_synchronize_with(curr) && !act->same_thread(curr)) { @@ -1750,16 +1759,24 @@ 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); - } + if (!is_infeasible()) + futurevalues->push_back(PendingFutureValue(curr, act)); + else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from()) + add_future_value(curr, act); } } } } + /* + * All compatible, thread-exclusive promises must be ordered after any + * concrete stores to the same thread, or else they can be merged with + * this store later + */ + for (unsigned int i = 0; i < promises->size(); i++) + if ((*promises)[i]->is_compatible_exclusive(curr)) + added = mo_graph->addEdge(curr, (*promises)[i]) || added; + return added; } @@ -1806,13 +1823,13 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; - if (!reader->happens_before(act)) + /* Don't disallow due to act == reader */ + if (!reader->happens_before(act) || reader == act) break; else if (act->is_write()) write_after_read = act; - else if (act->is_read() && act->get_reads_from() != NULL && act != reader) { + else if (act->is_read() && act->get_reads_from() != NULL) write_after_read = act->get_reads_from(); - } } if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer)) @@ -2274,42 +2291,44 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) const */ bool ModelChecker::resolve_promises(ModelAction *write) { - bool resolved = false; - std::vector< thread_id_t, ModelAlloc > threads_to_check; + bool haveResolved = false; + std::vector< ModelAction *, ModelAlloc > actions_to_check; + promise_list_t mustResolve, resolved; for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) { Promise *promise = (*promises)[promise_index]; if (write->get_node()->get_promise(i)) { ModelAction *read = promise->get_action(); - if (read->is_rmw()) { - mo_graph->addRMWEdge(write, read); - } read_from(read, write); - //First fix up the modification order for actions that happened - //before the read - r_modification_order(read, write); - //Next fix up the modification order for actions that happened - //after the read. - post_r_modification_order(read, write); //Make sure the promise's value matches the write's value - ASSERT(promise->get_value() == write->get_value()); - delete(promise); + ASSERT(promise->is_compatible(write)); + mo_graph->resolvePromise(read, write, &mustResolve); + resolved.push_back(promise); promises->erase(promises->begin() + promise_index); - threads_to_check.push_back(read->get_tid()); + actions_to_check.push_back(read); - resolved = true; + haveResolved = true; } else promise_index++; } + for (unsigned int i = 0; i < mustResolve.size(); i++) { + if (std::find(resolved.begin(), resolved.end(), mustResolve[i]) + == resolved.end()) + priv->failed_promise = true; + } + for (unsigned int i = 0; i < resolved.size(); i++) + delete resolved[i]; //Check whether reading these writes has made threads unable to //resolve promises - for (unsigned int i = 0; i < threads_to_check.size(); i++) - mo_check_promises(threads_to_check[i], write); + for (unsigned int i = 0; i < actions_to_check.size(); i++) { + ModelAction *read = actions_to_check[i]; + mo_check_promises(read, true); + } - return resolved; + return haveResolved; } /** @@ -2342,7 +2361,7 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec const ModelAction *act = promise->get_action(); if ((old_cv == NULL || !old_cv->synchronized_since(act)) && merge_cv->synchronized_since(act)) { - if (promise->increment_threads(tid)) { + if (promise->eliminate_thread(tid)) { //Promise has failed priv->failed_promise = true; return; @@ -2351,77 +2370,54 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec } } -void ModelChecker::check_promises_thread_disabled() { +void ModelChecker::check_promises_thread_disabled() +{ for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; - if (promise->check_promise()) { + if (promise->has_failed()) { priv->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 - * pthread that is sequenced after pread or the value read by the - * first read to the same lcoation as pread by pthread that is - * sequenced after pread.. - * - * 1. If tid=pthread, then we check what other threads are reachable - * through the mode order starting with pwrite. Those threads cannot - * perform a write that will resolve the promise due to modification - * order constraints. - * - * 2. If the tid is not pthread, we check whether pwrite can reach the - * action write through the modification order. If so, that thread - * cannot perform a future write that will resolve the promise due to - * modificatin order constraints. +/** + * @brief Checks promises in response to addition to modification order for + * threads. * - * @param tid The thread that either read from the model action - * write, or actually did the model action write. + * We test whether threads are still available for satisfying promises after an + * addition to our modification order constraints. Those that are unavailable + * are "eliminated". Once all threads are eliminated from satisfying a promise, + * that promise has failed. * - * @param write The ModelAction representing the relevant write. + * @param act The ModelAction which updated the modification order + * @param is_read_check Should be true if act is a read and we must check for + * updates to the store from which it read (there is a distinction here for + * RMW's, which are both a load and a store) */ -void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) +void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check) { - void *location = write->get_location(); + const ModelAction *write = is_read_check ? act->get_reads_from() : act; + for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; - const ModelAction *act = promise->get_action(); + const ModelAction *pread = promise->get_action(); - //Is this promise on the same location? - if ( act->get_location() != location ) + // Is this promise on the same location? + if (!pread->same_var(write)) continue; - //same thread as the promise - if ( act->get_tid() == tid ) { - - //do we have a pwrite for the promise, if not, set it - if (promise->get_write() == NULL ) { - promise->set_write(write); - //The pwrite cannot happen before the promise - if (write->happens_before(act) && (write != act)) { - priv->failed_promise = true; - return; - } - } - if (mo_graph->checkPromise(write, promise)) { - priv->failed_promise = true; - return; - } + if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) { + priv->failed_promise = true; + return; } - //Don't do any lookups twice for the same thread - if (promise->has_sync_thread(tid)) + // Don't do any lookups twice for the same thread + if (!promise->thread_is_available(act->get_tid())) continue; - if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) { - if (promise->increment_threads(tid)) { + if (mo_graph->checkReachable(promise, write)) { + if (mo_graph->checkPromise(write, promise)) { priv->failed_promise = true; return; } @@ -2491,12 +2487,12 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) allow_read = false; if (allow_read) { - DEBUG("Adding action to may_read_from:\n"); - if (DBG_ENABLED()) { - act->print(); - curr->print(); - } - curr->get_node()->add_read_from(act); + /* Only add feasible reads */ + mo_graph->startChanges(); + r_modification_order(curr, act); + if (!is_infeasible()) + curr->get_node()->add_read_from(act); + mo_graph->rollbackChanges(); } /* Include at most one act per-thread that "happens before" curr */ @@ -2504,6 +2500,11 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) break; } } + /* We may find no valid may-read-from only if the execution is doomed */ + if (!curr->get_node()->get_read_from_size()) { + priv->no_valid_reads = true; + set_assert(); + } if (DBG_ENABLED()) { model_print("Reached read action:\n"); @@ -2547,13 +2548,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; @@ -2566,18 +2565,19 @@ static void print_list(action_list_t *list, int exec_num = -1) } #if SUPPORT_MOD_ORDER_DUMP -void ModelChecker::dumpGraph(char *filename) { +void ModelChecker::dumpGraph(char *filename) const +{ char buffer[200]; - sprintf(buffer, "%s.dot",filename); + sprintf(buffer, "%s.dot", filename); FILE *file = fopen(buffer, "w"); - fprintf(file, "digraph %s {\n",filename); + fprintf(file, "digraph %s {\n", filename); mo_graph->dumpNodes(file); - ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads()); + 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()) { - fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid()); + fprintf(file, "N%u [label=\"N%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid()); if (action->get_reads_from() != NULL) fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number()); } @@ -2587,7 +2587,7 @@ void ModelChecker::dumpGraph(char *filename) { thread_array[action->get_tid()] = action; } - fprintf(file,"}\n"); + fprintf(file, "}\n"); model_free(thread_array); fclose(file); } @@ -2597,7 +2597,6 @@ void ModelChecker::dumpGraph(char *filename) { void ModelChecker::print_summary() const { #if SUPPORT_MOD_ORDER_DUMP - scheduler->print(); char buffername[100]; sprintf(buffername, "exec%04u", stats.num_total); mo_graph->dumpGraphToFile(buffername); @@ -2605,9 +2604,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"); } @@ -2646,7 +2648,7 @@ Thread * ModelChecker::get_thread(thread_id_t tid) const * @param act The ModelAction * @return A Thread reference */ -Thread * ModelChecker::get_thread(ModelAction *act) const +Thread * ModelChecker::get_thread(const ModelAction *act) const { return get_thread(act->get_tid()); } @@ -2671,6 +2673,19 @@ bool ModelChecker::is_enabled(thread_id_t tid) const return scheduler->is_enabled(tid); } +/** + * Switch from a model-checker context to a user-thread context. This is the + * complement of ModelChecker::switch_to_master and must be called from the + * model-checker context + * + * @param thread The user-thread to switch to + */ +void ModelChecker::switch_from_master(Thread *thread) +{ + scheduler->set_current_thread(thread); + Thread::swap(&system_context, thread); +} + /** * 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 @@ -2686,8 +2701,8 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) { DBG(); Thread *old = thread_current(); - set_current_action(act); - old->set_state(THREAD_READY); + ASSERT(!old->get_pending()); + old->set_pending(act); if (Thread::swap(old, &system_context) < 0) { perror("swap threads"); exit(EXIT_FAILURE); @@ -2697,77 +2712,37 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) /** * Takes the next step in the execution, if possible. - * @return Returns true (success) if a step was taken and false otherwise. + * @param curr The current step to take + * @return Returns the next Thread to run, if any; NULL if this execution + * should terminate */ -bool ModelChecker::take_step() { - if (has_asserted()) - return false; - - Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL; - if (curr) { - ASSERT(curr->get_state() == THREAD_READY); - - priv->nextThread = check_current_action(priv->current_action); - priv->current_action = NULL; +Thread * ModelChecker::take_step(ModelAction *curr) +{ + Thread *curr_thrd = get_thread(curr); + ASSERT(curr_thrd->get_state() == THREAD_READY); - if (curr->is_blocked() || curr->is_complete()) - scheduler->remove_thread(curr); - } - Thread *next = scheduler->next_thread(priv->nextThread); + curr = check_current_action(curr); /* Infeasible -> don't take any more steps */ if (is_infeasible()) - return false; + return NULL; else if (isfeasibleprefix() && have_bug_reports()) { set_assert(); - return false; - } - - if (params.bound != 0) { - if (priv->used_sequence_numbers > params.bound) { - return false; - } + return NULL; } - DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1, - next ? id_to_int(next->get_id()) : -1); + if (params.bound != 0 && priv->used_sequence_numbers > params.bound) + return NULL; - /* - * Launch end-of-execution release sequence fixups only when there are: - * - * (1) no more user threads to run (or when execution replay chooses - * the 'model_thread') - * (2) pending release sequences - * (3) pending assertions (i.e., data races) - * (4) no pending promises - */ - if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) && - is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) { - model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n", - pending_rel_seqs->size()); - ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ, - std::memory_order_seq_cst, NULL, VALUE_NONE, - model_thread); - set_current_action(fixup); - return true; - } + if (curr_thrd->is_blocked() || curr_thrd->is_complete()) + scheduler->remove_thread(curr_thrd); - /* next == NULL -> don't take any more steps */ - if (!next) - return false; + Thread *next_thrd = get_next_thread(curr); - next->set_state(THREAD_RUNNING); + DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1, + next_thrd ? id_to_int(next_thrd->get_id()) : -1); - 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); + return next_thrd; } /** Wrapper to run the user's main function, with appropriate arguments */ @@ -2781,13 +2756,57 @@ void ModelChecker::run() { do { thrd_t user_thread; + Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL); + add_thread(t); + + do { + /* + * Stash next pending action(s) for thread(s). There + * should only need to stash one thread's action--the + * thread which just took a step--plus the first step + * for any newly-created thread + */ + for (unsigned int i = 0; i < get_num_threads(); i++) { + thread_id_t tid = int_to_id(i); + Thread *thr = get_thread(tid); + if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) { + switch_from_master(thr); + } + } + + /* Catch assertions from prior take_step or from + * between-ModelAction bugs (e.g., data races) */ + if (has_asserted()) + break; - /* Start user program */ - add_thread(new Thread(&user_thread, &user_main_wrapper, NULL)); + /* Consume the next action for a Thread */ + ModelAction *curr = t->get_pending(); + t->set_pending(NULL); + t = take_step(curr); + } while (t && !t->is_model_thread()); - /* Wait for all threads to complete */ - while (take_step()); + /* + * Launch end-of-execution release sequence fixups only when + * the execution is otherwise feasible AND there are: + * + * (1) pending release sequences + * (2) pending assertions that could be invalidated by a change + * in clock vectors (i.e., data races) + * (3) no pending promises + */ + while (!pending_rel_seqs->empty() && + is_feasible_prefix_ignore_relseq() && + !unrealizedraces.empty()) { + model_print("*** WARNING: release sequence fixup action " + "(%zu pending release seuqence(s)) ***\n", + pending_rel_seqs->size()); + ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ, + std::memory_order_seq_cst, NULL, VALUE_NONE, + model_thread); + take_step(fixup); + }; } while (next_execution()); + model_print("******* Model-checking complete: *******\n"); print_stats(); }