X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=40b25d0d635a32a5fdd2832001c638c3ee1986fc;hb=ffb2033ac6b31407810703b65ae0fbaeb9c0da59;hp=e36426721ca44b53b7029cedb7de53ee79b22634;hpb=b35625b0499717b3caab5344d7278a31fbee9cb6;p=model-checker.git diff --git a/model.cc b/model.cc index e364267..40b25d0 100644 --- a/model.cc +++ b/model.cc @@ -43,7 +43,6 @@ struct model_snapshot_members { /* 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(), @@ -62,7 +61,6 @@ struct model_snapshot_members { 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; @@ -161,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 */ @@ -176,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(); @@ -214,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? */ @@ -228,7 +230,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) if (next == diverge) { if (earliest_diverge == NULL || *diverge < *earliest_diverge) - earliest_diverge=diverge; + earliest_diverge = diverge; Node *nextnode = next->get_node(); Node *prevnode = nextnode->get_parent(); @@ -256,13 +258,14 @@ 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); - if (diverge==earliest_diverge) { - earliest_diverge=prevnode->get_action(); + if (diverge == earliest_diverge) { + earliest_diverge = prevnode->get_action(); } } /* The correct sleep set is in the parent node. */ @@ -298,7 +301,6 @@ void ModelChecker::execute_sleep_set() thr->set_pending(priv->current_action); } } - priv->current_action = NULL; } void ModelChecker::wake_up_sleeping_actions(ModelAction *curr) @@ -502,7 +504,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 +562,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 +573,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 +588,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,15 +614,15 @@ 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; + high_tid = low_tid + 1; } else { low_tid = 0; 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. */ @@ -628,7 +630,7 @@ void ModelChecker::set_backtracking(ModelAction *act) break; /* Don't backtrack into a point where the thread is disabled or sleeping. */ - if (node->enabled_status(tid)!=THREAD_ENABLED) + if (node->enabled_status(tid) != THREAD_ENABLED) continue; /* Check if this has been explored already */ @@ -637,11 +639,11 @@ void ModelChecker::set_backtracking(ModelAction *act) /* See if fairness allows */ if (model->params.fairwindow != 0 && !node->has_priority(tid)) { - bool unfair=false; - for(int t=0;tget_num_threads();t++) { - thread_id_t tother=int_to_id(t); + bool unfair = false; + for (int t = 0; t < node->get_num_threads(); t++) { + thread_id_t tother = int_to_id(t); if (node->is_enabled(tother) && node->has_priority(tother)) { - unfair=true; + unfair = true; break; } } @@ -649,8 +651,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 +666,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. @@ -701,7 +722,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) } - 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 +730,15 @@ 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->get_tid(), reads_from, NULL); 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(); + struct future_value fv = curr->get_node()->get_future_value(); + value = fv.value; curr->set_read_from(NULL); - Promise *valuepromise = new Promise(curr, value, expiration); - promises->push_back(valuepromise); + promises->push_back(new Promise(curr, fv)); } get_thread(curr)->set_return_value(value); return updated; @@ -741,14 +761,15 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) * * @return True if synchronization was updated; false otherwise */ -bool ModelChecker::process_mutex(ModelAction *curr) { - std::mutex *mutex=NULL; - struct std::mutex_state *state=NULL; +bool ModelChecker::process_mutex(ModelAction *curr) +{ + std::mutex *mutex = NULL; + struct std::mutex_state *state = NULL; 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(); } @@ -799,10 +820,10 @@ bool ModelChecker::process_mutex(ModelAction *curr) { } waiters->clear(); //check whether we should go to sleep or not...simulate spurious failures - if (curr->get_node()->get_misc()==0) { + 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; } @@ -817,7 +838,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) { } case ATOMIC_NOTIFY_ONE: { action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location()); - int wakeupthread=curr->get_node()->get_misc(); + int wakeupthread = curr->get_node()->get_misc(); action_list_t::iterator it = waiters->begin(); advance(it, wakeupthread); scheduler->wake(get_thread(*it)); @@ -831,6 +852,19 @@ 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)) { + struct future_value fv = { + writer->get_value(), + writer->get_seq_number() + params.maxfuturedelay, + }; + if (reader->get_node()->add_future_value(fv)) + set_latest_backtrack(reader); + } +} + /** * Process a write ModelAction * @param curr The ModelAction to process @@ -844,17 +878,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->get_tid(), curr, NULL); get_thread(curr)->set_return_value(VALUE_NONE); return updated_mod_order || updated_promises; @@ -927,12 +957,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 */ @@ -1175,11 +1205,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(); @@ -1187,13 +1216,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 */ @@ -1271,7 +1304,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) @@ -1279,25 +1312,22 @@ 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); } } bool ModelChecker::promises_expired() const { - for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) { - Promise *promise = (*promises)[promise_index]; - if (promise->get_expiration()used_sequence_numbers) { + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + if (promise->get_expiration() < priv->used_sequence_numbers) return true; - } } return false; } @@ -1312,15 +1342,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; } @@ -1332,9 +1386,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(); } @@ -1348,18 +1399,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(); @@ -1369,7 +1408,7 @@ 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) { + if (act->is_rmw() && lastread->get_reads_from() != NULL) { mo_graph->addRMWEdge(lastread->get_reads_from(), lastread); mo_graph->commitChanges(); } @@ -1414,7 +1453,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,7 +1473,7 @@ 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*/ + /* Test to see whether this is a feasible write to read from */ mo_graph->startChanges(); r_modification_order(curr, write); bool feasiblereadfrom = !is_infeasible(); @@ -1447,11 +1486,11 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) 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++) { - if (act->get_node()->get_read_from_at(j)==write) { + 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; } @@ -1606,7 +1645,7 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio /* Include at most one act per-thread that "happens before" curr */ if (lastact != NULL) { - if (lastact==curr) { + 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 @@ -1617,13 +1656,13 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio //is mod ordered after rf const ModelAction *postreadfrom = lastact->get_reads_from(); - if (postreadfrom != NULL&&rf != postreadfrom) + 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) + if (lastact != rf) mo_graph->addEdge(rf, lastact); } break; @@ -1698,7 +1737,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) * continue processing list. */ if (curr->is_rmw()) { - if (curr->get_reads_from()!=NULL) + if (curr->get_reads_from() != NULL) break; else continue; @@ -1752,8 +1791,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)); } } } @@ -1806,16 +1844,16 @@ 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)) + if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer)) return false; } return true; @@ -2141,7 +2179,7 @@ void ModelChecker::add_action_to_lists(ModelAction *act) } if (act->is_wait()) { - void *mutex_loc=(void *) act->get_value(); + void *mutex_loc = (void *) act->get_value(); get_safe_ptr_action(obj_map, mutex_loc)->push_back(act); std::vector *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc); @@ -2275,7 +2313,7 @@ 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; + std::vector< ModelAction *, ModelAlloc > actions_to_check; for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) { Promise *promise = (*promises)[promise_index]; @@ -2296,7 +2334,7 @@ bool ModelChecker::resolve_promises(ModelAction *write) delete(promise); promises->erase(promises->begin() + promise_index); - threads_to_check.push_back(read->get_tid()); + actions_to_check.push_back(read); resolved = true; } else @@ -2306,8 +2344,10 @@ bool ModelChecker::resolve_promises(ModelAction *write) //Check whether reading these writes has made threads unable to //resolve promises - for(unsigned int i=0;iget_tid(), write, read); + } return resolved; } @@ -2342,7 +2382,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,29 +2391,34 @@ 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. +/** + * @brief 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.. + * pthread that is sequenced after pread or the write read by the + * first read to the same location 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 + * 1. If tid=pthread, then we check what other threads are reachable + * through the mod order starting with pwrite. Those threads cannot * perform a write that will resolve the promise due to modification * order constraints. * @@ -2382,46 +2427,50 @@ void ModelChecker::check_promises_thread_disabled() { * cannot perform a future write that will resolve the promise due to * modificatin order constraints. * - * @param tid The thread that either read from the model action - * write, or actually did the model action write. + * @param tid The thread that either read from the model action write, or + * actually did the model action write. * - * @param write The ModelAction representing the relevant write. + * @param write The ModelAction representing the relevant write. + * @param read The ModelAction that reads a promised write, or NULL otherwise. */ -void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) +void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction *read) { void *location = write->get_location(); 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 ) + // Is this promise on the same location? + if (act->get_location() != location) continue; - //same thread as the promise - if ( act->get_tid()==tid ) { + // same thread as the promise + if (act->get_tid() == tid) { + // make sure that the reader of this write happens after the promise + if ((read == NULL) || (promise->get_action()->happens_before(read))) { + // 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; + } + } - //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)) { + if (mo_graph->checkPromise(write, promise)) { priv->failed_promise = true; return; } } - if (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_eliminated(tid)) continue; - if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) { - if (promise->increment_threads(tid)) { + if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) { + if (promise->eliminate_thread(tid)) { priv->failed_promise = true; return; } @@ -2490,14 +2539,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)) @@ -2530,7 +2573,7 @@ bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *wri } if (write->get_reads_from() == NULL) return true; - write=write->get_reads_from(); + write = write->get_reads_from(); } } @@ -2547,47 +2590,46 @@ 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; + unsigned int hash = 0; for (it = list->begin(); it != list->end(); it++) { (*it)->print(); - hash=hash^(hash<<3)^((*it)->hash()); + hash = hash^(hash<<3)^((*it)->hash()); } model_print("HASH %u\n", hash); model_print("---------------------------------------------------------------------\n"); } #if SUPPORT_MOD_ORDER_DUMP -void ModelChecker::dumpGraph(char *filename) { +void ModelChecker::dumpGraph(char *filename) const +{ 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()); + 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; + 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()); - if (action->get_reads_from()!=NULL) + fprintf(file, "N%u [label=\"%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()); } 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; + thread_array[action->get_tid()] = action; } - fprintf(file,"}\n"); + fprintf(file, "}\n"); model_free(thread_array); fclose(file); } @@ -2605,9 +2647,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 +2691,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()); } @@ -2697,27 +2742,18 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act) /** * Takes the next step in the execution, if possible. + * @param curr The current step to take * @return Returns true (success) if a step was taken and false otherwise. */ -bool ModelChecker::take_step() { +bool ModelChecker::take_step(ModelAction *curr) +{ if (has_asserted()) return false; - Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL; - if (curr) { - if (curr->get_state() == THREAD_READY) { - ASSERT(priv->current_action); + Thread *curr_thrd = get_thread(curr); + ASSERT(curr_thrd->get_state() == THREAD_READY); - priv->nextThread = check_current_action(priv->current_action); - priv->current_action = NULL; - - if (curr->is_blocked() || curr->is_complete()) - scheduler->remove_thread(curr); - } else { - ASSERT(false); - } - } - Thread *next = scheduler->next_thread(priv->nextThread); + curr = check_current_action(curr); /* Infeasible -> don't take any more steps */ if (is_infeasible()) @@ -2727,14 +2763,18 @@ bool ModelChecker::take_step() { 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; - } - } - DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1, - next ? id_to_int(next->get_id()) : -1); + 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); /* * Launch end-of-execution release sequence fixups only when there are: @@ -2745,7 +2785,7 @@ bool ModelChecker::take_step() { * (3) pending assertions (i.e., data races) * (4) no pending promises */ - if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) && + if (!pending_rel_seqs->empty() && (!next_thrd || next_thrd->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()); @@ -2756,22 +2796,22 @@ bool ModelChecker::take_step() { return true; } - /* next == NULL -> don't take any more steps */ - if (!next) + /* next_thrd == NULL -> don't take any more steps */ + if (!next_thrd) return false; - next->set_state(THREAD_RUNNING); + next_thrd->set_state(THREAD_RUNNING); - if (next->get_pending() != NULL) { + if (next_thrd->get_pending() != NULL) { /* restart a pending action */ - set_current_action(next->get_pending()); - next->set_pending(NULL); - next->set_state(THREAD_READY); + set_current_action(next_thrd->get_pending()); + next_thrd->set_pending(NULL); + next_thrd->set_state(THREAD_READY); return true; } /* Return false only if swap fails with an error */ - return (Thread::swap(&system_context, next) == 0); + return (Thread::swap(&system_context, next_thrd) == 0); } /** Wrapper to run the user's main function, with appropriate arguments */ @@ -2785,12 +2825,16 @@ void ModelChecker::run() { do { thrd_t user_thread; + Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL); + + add_thread(t); - /* Start user program */ - add_thread(new Thread(&user_thread, &user_main_wrapper, NULL)); + /* Run user thread up to its first action */ + scheduler->next_thread(t); + Thread::swap(&system_context, t); /* Wait for all threads to complete */ - while (take_step()); + while (take_step(priv->current_action)); } while (next_execution()); print_stats();