X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=2b8ab3cc870a6f0fc9dae9ec5758f7b2e00f8092;hp=8c88a05469515e92c9f324ef3afb619ee90c0344;hb=24d17393dc45f60f6f6660159f2f329d1cc5d15a;hpb=67e374f0a24b266f2ea81913770e89a4aac68ff3 diff --git a/model.cc b/model.cc index 8c88a054..2b8ab3cc 100644 --- a/model.cc +++ b/model.cc @@ -1,6 +1,7 @@ #include #include #include +#include #include "model.h" #include "action.h" @@ -42,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(), @@ -61,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; @@ -128,19 +127,21 @@ ModelChecker::~ModelChecker() delete priv; } -static action_list_t * get_safe_ptr_action(HashTable * hash, void * ptr) { - action_list_t * tmp=hash->get(ptr); - if (tmp==NULL) { - tmp=new action_list_t(); +static action_list_t * get_safe_ptr_action(HashTable * hash, void * ptr) +{ + action_list_t *tmp = hash->get(ptr); + if (tmp == NULL) { + tmp = new action_list_t(); hash->put(ptr, tmp); } return tmp; } -static std::vector * get_safe_ptr_vect_action(HashTable *, uintptr_t, 4> * hash, void * ptr) { - std::vector * tmp=hash->get(ptr); - if (tmp==NULL) { - tmp=new std::vector(); +static std::vector * get_safe_ptr_vect_action(HashTable *, uintptr_t, 4> * hash, void * ptr) +{ + std::vector *tmp = hash->get(ptr); + if (tmp == NULL) { + tmp = new std::vector(); hash->put(ptr, tmp); } return tmp; @@ -158,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 */ @@ -173,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(); @@ -207,13 +213,12 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) { thread_id_t tid; - if (curr!=NULL) { + if (curr != NULL) { /* Do not split atomic actions. */ if (curr->is_rmwr()) return thread_current(); - /* The THREAD_CREATE action points to the created Thread */ else if (curr->get_type() == THREAD_CREATE) - return (Thread *)curr->get_location(); + return curr->get_thread_operand(); } /* Have we completed exploring the preselected path? */ @@ -225,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(); @@ -253,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. */ @@ -282,12 +288,12 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) * the corresponding thread object's pending action. */ -void ModelChecker::execute_sleep_set() { - for(unsigned int i=0;iget_enabled(thr) == THREAD_SLEEP_SET && - thr->get_pending() == NULL ) { +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); @@ -295,19 +301,17 @@ void ModelChecker::execute_sleep_set() { thr->set_pending(priv->current_action); } } - priv->current_action = NULL; } -void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { - for(unsigned int i=0;iget_enabled(thr) == THREAD_SLEEP_SET ) { - ModelAction *pending_act=thr->get_pending(); - if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) { +void ModelChecker::wake_up_sleeping_actions(ModelAction *curr) +{ + for (unsigned int i = 0; i < get_num_threads(); i++) { + Thread *thr = get_thread(int_to_id(i)); + if (scheduler->is_sleep_set(thr)) { + ModelAction *pending_act = thr->get_pending(); + if ((!curr->is_rmwr()) && pending_act->could_synchronize_with(curr)) //Remove this thread from sleep set scheduler->remove_sleep(thr); - } } } } @@ -500,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(); @@ -558,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; @@ -569,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; @@ -584,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; @@ -603,22 +607,22 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) void ModelChecker::set_backtracking(ModelAction *act) { Thread *t = get_thread(act); - ModelAction * prev = get_last_conflict(act); + ModelAction *prev = get_last_conflict(act); if (prev == NULL) return; - Node * node = prev->get_node()->get_parent(); + 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. */ @@ -626,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 */ @@ -635,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; } } @@ -647,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)) @@ -663,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. @@ -698,8 +721,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; @@ -707,16 +729,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->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(); - read_from(curr, 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; @@ -739,14 +764,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(); } @@ -797,10 +823,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; } @@ -815,7 +841,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)); @@ -829,6 +855,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 @@ -842,22 +889,68 @@ 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; } +/** + * Process a fence ModelAction + * @param curr The ModelAction to process + * @return True if synchronization was updated + */ +bool ModelChecker::process_fence(ModelAction *curr) +{ + /* + * fence-relaxed: no-op + * fence-release: only log the occurence (not in this function), for + * use in later synchronization + * fence-acquire (this function): search for hypothetical release + * sequences + */ + bool updated = false; + if (curr->is_acquire()) { + action_list_t *list = action_trace; + action_list_t::reverse_iterator rit; + /* Find X : is_read(X) && X --sb-> curr */ + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *act = *rit; + if (act == curr) + continue; + if (act->get_tid() != curr->get_tid()) + continue; + /* Stop at the beginning of the thread */ + if (act->is_thread_start()) + break; + /* Stop once we reach a prior fence-acquire */ + if (act->is_fence() && act->is_acquire()) + break; + if (!act->is_read()) + continue; + /* read-acquire will find its own release sequences */ + if (act->is_acquire()) + continue; + + /* Establish hypothetical release sequences */ + rel_heads_list_t release_heads; + get_release_seq_heads(curr, act, &release_heads); + for (unsigned int i = 0; i < release_heads.size(); i++) + if (!curr->synchronize_with(release_heads[i])) + set_bad_synchronization(); + if (release_heads.size() != 0) + updated = true; + } + } + return updated; +} + /** * @brief Process the current action for thread-related activity * @@ -875,12 +968,18 @@ 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); + /* 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 */ @@ -893,6 +992,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; } @@ -1063,7 +1169,7 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf) act->set_read_from(rf); if (rf != NULL && act->is_acquire()) { rel_heads_list_t release_heads; - get_release_seq_heads(act, &release_heads); + get_release_seq_heads(act, act, &release_heads); int num_heads = release_heads.size(); for (unsigned int i = 0; i < release_heads.size(); i++) if (!act->synchronize_with(release_heads[i])) { @@ -1087,8 +1193,8 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf) */ bool ModelChecker::check_action_enabled(ModelAction *curr) { if (curr->is_lock()) { - std::mutex * lock = (std::mutex *)curr->get_location(); - struct std::mutex_state * state = lock->get_state(); + std::mutex *lock = (std::mutex *)curr->get_location(); + struct std::mutex_state *state = lock->get_state(); if (state->islocked) { //Stick the action in the appropriate waiting queue get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr); @@ -1123,11 +1229,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(); @@ -1135,13 +1240,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 */ @@ -1173,6 +1282,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (act->is_write() && process_write(act)) update = true; + if (act->is_fence() && process_fence(act)) + update_all = true; + if (act->is_mutex_op() && process_mutex(act)) update_all = true; @@ -1195,8 +1307,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)) @@ -1216,32 +1334,30 @@ 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) { +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; } @@ -1256,15 +1372,37 @@ 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->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; } @@ -1276,36 +1414,10 @@ 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->failed_promise || + priv->too_many_reads || + priv->bad_synchronization || promises_expired(); } @@ -1313,8 +1425,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; @@ -1331,9 +1446,9 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) { * * If so, we decide that the execution is no longer feasible. */ -void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { +void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) +{ if (params.maxreads != 0) { - if (curr->get_node()->get_read_from_size() <= 1) return; //Must make sure that execution is currently feasible... We could @@ -1358,8 +1473,8 @@ 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++) { - if (rit==list->rend()) + for (; count < params.maxreads; rit++, count++) { + if (rit == list->rend()) return; ModelAction *act = *rit; if (!act->is_read()) @@ -1370,15 +1485,15 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { if (act->get_node()->get_read_from_size() <= 1) return; } - for (int i = 0; iget_node()->get_read_from_size(); i++) { - //Get write - const ModelAction * write = curr->get_node()->get_read_from_at(i); + for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) { + /* Get write */ + const ModelAction *write = curr->get_node()->get_read_from_at(i); - //Need a different write - if (write==rf) + /* Need a different write */ + 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(); @@ -1391,11 +1506,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++) { - ModelAction *act=*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; } @@ -1418,7 +1533,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. @@ -1427,10 +1542,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; @@ -1458,24 +1574,24 @@ 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; } } @@ -1485,9 +1601,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(); @@ -1495,9 +1610,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; @@ -1508,70 +1622,6 @@ 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; - } - - /* 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; - } - } -} - /** * Updates the mo_graph with the constraints imposed from the current write. * @@ -1606,8 +1656,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; } } @@ -1639,7 +1688,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; @@ -1650,8 +1699,8 @@ 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; } /* @@ -1666,14 +1715,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)) { @@ -1690,23 +1738,32 @@ 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; } /** 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::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) { +bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader) +{ if (!writer->is_rmw()) return true; @@ -1745,16 +1802,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; @@ -1797,6 +1854,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, if (rf->is_release()) release_heads->push_back(rf); + else if (rf->get_last_fence_release()) + release_heads->push_back(rf->get_last_fence_release()); if (!rf->is_rmw()) break; /* End of RMW chain */ @@ -1822,8 +1881,17 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, if (rf->is_release()) return true; /* complete */ - /* else relaxed write; check modification order for contiguous subsequence - * -> rf must be same thread as release */ + /* else relaxed write + * - check for fence-release in the same thread (29.8, stmt. 3) + * - check modification order for contiguous subsequence + * -> rf must be same thread as release */ + + const ModelAction *fence_release = rf->get_last_fence_release(); + /* Synchronize with a fence-release unconditionally; we don't need to + * find any more "contiguous subsequence..." for it */ + if (fence_release) + release_heads->push_back(fence_release); + int tid = id_to_int(rf->get_tid()); std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location()); action_list_t *list = &(*thrd_lists)[tid]; @@ -1833,14 +1901,21 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rit = std::find(list->rbegin(), list->rend(), rf); ASSERT(rit != list->rend()); - /* Find the last write/release */ - for (; rit != list->rend(); rit++) + /* Find the last {write,fence}-release */ + for (; rit != list->rend(); rit++) { + if (fence_release && *(*rit) < *fence_release) + break; if ((*rit)->is_release()) break; + } if (rit == list->rend()) { /* No write-release in this thread */ return true; /* complete */ - } + } else if (fence_release && *(*rit) < *fence_release) { + /* The fence-release is more recent (and so, "stronger") than + * the most recent write-release */ + return true; /* complete */ + } /* else, need to establish contiguous release sequence */ ModelAction *release = *rit; ASSERT(rf->same_thread(release)); @@ -1917,18 +1992,25 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, * given ModelAction must synchronize. This function only returns a non-empty * result when it can locate a release sequence head with certainty. Otherwise, * it may mark the internal state of the ModelChecker so that it will handle - * the release sequence at a later time, causing @a act to update its + * the release sequence at a later time, causing @a acquire to update its * synchronization at some later point in execution. - * @param act The 'acquire' action that may read from a release sequence + * + * @param acquire The 'acquire' action that may synchronize with a release + * sequence + * @param read The read action that may read from a release sequence; this may + * be the same as acquire, or else an earlier action in the same thread (i.e., + * when 'acquire' is a fence-acquire) * @param release_heads A pass-by-reference return parameter. Will be filled * with the head(s) of the release sequence(s), if they exists with certainty. * @see ModelChecker::release_seq_heads */ -void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads) +void ModelChecker::get_release_seq_heads(ModelAction *acquire, + ModelAction *read, rel_heads_list_t *release_heads) { - const ModelAction *rf = act->get_reads_from(); + const ModelAction *rf = read->get_reads_from(); struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq)); - sequence->acquire = act; + sequence->acquire = acquire; + sequence->read = read; if (!release_seq_heads(rf, release_heads, sequence)) { /* add act to 'lazy checking' list */ @@ -1957,21 +2039,22 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ std::vector< struct release_seq *, SnapshotAlloc >::iterator it = pending_rel_seqs->begin(); while (it != pending_rel_seqs->end()) { struct release_seq *pending = *it; - ModelAction *act = pending->acquire; + ModelAction *acquire = pending->acquire; + const ModelAction *read = pending->read; /* Only resolve sequences on the given location, if provided */ - if (location && act->get_location() != location) { + if (location && read->get_location() != location) { it++; continue; } - const ModelAction *rf = act->get_reads_from(); + const ModelAction *rf = read->get_reads_from(); rel_heads_list_t release_heads; bool complete; complete = release_seq_heads(rf, &release_heads, pending); for (unsigned int i = 0; i < release_heads.size(); i++) { - if (!act->has_synchronized_with(release_heads[i])) { - if (act->synchronize_with(release_heads[i])) + if (!acquire->has_synchronized_with(release_heads[i])) { + if (acquire->synchronize_with(release_heads[i])) updated = true; else set_bad_synchronization(); @@ -1981,15 +2064,16 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ if (updated) { /* Re-check all pending release sequences */ work_queue->push_back(CheckRelSeqWorkEntry(NULL)); - /* Re-check act for mo_graph edges */ - work_queue->push_back(MOEdgeWorkEntry(act)); + /* Re-check read-acquire for mo_graph edges */ + if (acquire->is_read()) + work_queue->push_back(MOEdgeWorkEntry(acquire)); /* propagate synchronization to later actions */ action_list_t::reverse_iterator rit = action_trace->rbegin(); - for (; (*rit) != act; rit++) { + for (; (*rit) != acquire; rit++) { ModelAction *propagate = *rit; - if (act->happens_before(propagate)) { - propagate->synchronize_with(act); + if (acquire->happens_before(propagate)) { + propagate->synchronize_with(acquire); /* Re-check 'propagate' for mo_graph edges */ work_queue->push_back(MOEdgeWorkEntry(propagate)); } @@ -2019,18 +2103,32 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ void ModelChecker::add_action_to_lists(ModelAction *act) { int tid = id_to_int(act->get_tid()); - action_trace->push_back(act); + ModelAction *uninit = NULL; + int uninit_id = -1; + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + if (list->empty() && act->is_atomic_var()) { + uninit = new_uninitialized_action(act->get_location()); + uninit_id = id_to_int(uninit->get_tid()); + list->push_back(uninit); + } + list->push_back(act); - get_safe_ptr_action(obj_map, act->get_location())->push_back(act); + action_trace->push_back(act); + if (uninit) + action_trace->push_front(uninit); std::vector *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location()); if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); + if (uninit) + (*vec)[uninit_id].push_front(uninit); if ((int)thrd_last_action->size() <= tid) thrd_last_action->resize(get_num_threads()); (*thrd_last_action)[tid] = act; + if (uninit) + (*thrd_last_action)[uninit_id] = uninit; if (act->is_fence() && act->is_release()) { if ((int)thrd_last_fence_release->size() <= tid) @@ -2039,7 +2137,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); @@ -2172,42 +2270,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;iget_tid(), write, read); + } - return resolved; + return haveResolved; } /** @@ -2240,7 +2340,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; @@ -2249,29 +2349,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. * @@ -2280,46 +2385,50 @@ void ModelChecker::check_promises_thread_disabled() { * cannot perform a future write that will resolve the promise due to * modificatin order constraints. * - * @parem 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. * - * @parem 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 * location = write->get_location(); +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_available(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; } @@ -2365,16 +2474,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) ModelAction *last_sc_write = NULL; - /* Track whether this object has been initialized */ - bool initialized = false; - - if (curr->is_seqcst()) { + if (curr->is_seqcst()) last_sc_write = get_last_seq_cst_write(curr); - /* We have to at least see the last sequentially consistent write, - so we are initialized. */ - if (last_sc_write != NULL) - initialized = true; - } /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { @@ -2396,27 +2497,16 @@ 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)) { - initialized = true; + if (act->happens_before(curr)) break; - } } } - if (!initialized) - assert_bug("May read from uninitialized atomic"); - - if (DBG_ENABLED() || !initialized) { + if (DBG_ENABLED()) { model_print("Reached read action:\n"); curr->print(); model_print("Printing may_read_from\n"); @@ -2425,63 +2515,79 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) } } -bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) { - while(true) { - Node *prevnode=write->get_node()->get_parent(); +bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *write) +{ + while (true) { + /* UNINIT actions don't have a Node, and they never sleep */ + if (write->is_uninitialized()) + return true; + Node *prevnode = write->get_node()->get_parent(); - bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET; - if (write->is_release()&&thread_sleep) + bool thread_sleep = prevnode->enabled_status(curr->get_tid()) == THREAD_SLEEP_SET; + if (write->is_release() && thread_sleep) return true; if (!write->is_rmw()) { return false; } - if (write->get_reads_from()==NULL) + if (write->get_reads_from() == NULL) return true; - write=write->get_reads_from(); + write = write->get_reads_from(); } } -static void print_list(action_list_t *list, int exec_num = -1) +/** + * @brief Create a new action representing an uninitialized atomic + * @param location The memory location of the atomic object + * @return A pointer to a new ModelAction + */ +ModelAction * ModelChecker::new_uninitialized_action(void *location) const +{ + ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction)); + act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread); + act->create_cv(NULL); + return act; +} + +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=\"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()); } 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); } @@ -2491,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); @@ -2499,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"); } @@ -2540,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()); } @@ -2574,40 +2682,35 @@ bool ModelChecker::is_enabled(thread_id_t tid) const * @param act The current action that will be explored. May be NULL only if * trace is exiting via an assertion (see ModelChecker::set_assert and * ModelChecker::has_asserted). - * @return Return status from the 'swap' call (i.e., success/fail, 0/-1) + * @return Return the value returned by the current action */ -int ModelChecker::switch_to_master(ModelAction *act) +uint64_t ModelChecker::switch_to_master(ModelAction *act) { DBG(); Thread *old = thread_current(); set_current_action(act); old->set_state(THREAD_READY); - return Thread::swap(old, &system_context); + if (Thread::swap(old, &system_context) < 0) { + perror("swap threads"); + exit(EXIT_FAILURE); + } + return old->get_return_value(); } /** * 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); - - priv->nextThread = check_current_action(priv->current_action); - priv->current_action = NULL; + Thread *curr_thrd = get_thread(curr); + ASSERT(curr_thrd->get_state() == THREAD_READY); - 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()) @@ -2617,14 +2720,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: @@ -2635,7 +2742,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()); @@ -2646,22 +2753,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 */ @@ -2675,12 +2782,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();