X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=9e611fae96367283e33d7b927224eb259b52a27e;hp=3ed8203fe9a2111618ced00d3ac07bf0cc5a6ac1;hb=3b3533a76db06884f44b3e70ccdbad647275fcc4;hpb=45656107dfb389a4a8b017e0c4bacf8e70a8ebf3 diff --git a/model.cc b/model.cc index 3ed8203f..9e611fae 100644 --- a/model.cc +++ b/model.cc @@ -1,6 +1,7 @@ #include #include #include +#include #include "model.h" #include "action.h" @@ -13,20 +14,63 @@ #include "promise.h" #include "datarace.h" #include "threads-model.h" +#include "output.h" #define INITIAL_THREAD_ID 0 ModelChecker *model; +struct bug_message { + bug_message(const char *str) { + const char *fmt = " [BUG] %s\n"; + msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str)); + sprintf(msg, fmt, str); + } + ~bug_message() { if (msg) snapshot_free(msg); } + + char *msg; + void print() { model_print("%s", msg); } + + SNAPSHOTALLOC +}; + /** * Structure for holding small ModelChecker members that should be snapshotted */ struct model_snapshot_members { + model_snapshot_members() : + current_action(NULL), + /* First thread created will have id INITIAL_THREAD_ID */ + next_thread_id(INITIAL_THREAD_ID), + used_sequence_numbers(0), + next_backtrack(NULL), + bugs(), + stats(), + failed_promise(false), + too_many_reads(false), + bad_synchronization(false), + asserted(false) + { } + + ~model_snapshot_members() { + for (unsigned int i = 0; i < bugs.size(); i++) + delete bugs[i]; + bugs.clear(); + } + ModelAction *current_action; unsigned int next_thread_id; modelclock_t used_sequence_numbers; - Thread *nextThread; ModelAction *next_backtrack; + std::vector< bug_message *, SnapshotAlloc > bugs; + struct execution_stats stats; + bool failed_promise; + bool too_many_reads; + /** @brief Incorrectly-ordered synchronization was made */ + bool bad_synchronization; + bool asserted; + + SNAPSHOTALLOC }; /** @brief Constructor */ @@ -34,8 +78,6 @@ ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ params(params), scheduler(new Scheduler()), - num_executions(0), - num_feasible_executions(0), diverge(NULL), earliest_diverge(NULL), action_trace(new action_list_t()), @@ -48,18 +90,11 @@ ModelChecker::ModelChecker(struct model_params params) : futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc >()), pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc >()), thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc >(1)), + thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc >()), node_stack(new NodeStack()), - mo_graph(new CycleGraph()), - failed_promise(false), - too_many_reads(false), - asserted(false), - bad_synchronization(false) + priv(new struct model_snapshot_members()), + mo_graph(new CycleGraph()) { - /* Allocate this "size" on the snapshotting heap */ - priv = (struct model_snapshot_members *)snapshot_calloc(1, sizeof(*priv)); - /* First thread created will have id INITIAL_THREAD_ID */ - priv->next_thread_id = INITIAL_THREAD_ID; - /* Initialize a model-checker thread, for special ModelActions */ model_thread = new Thread(get_next_id()); thread_map->put(id_to_int(model_thread->get_id()), model_thread); @@ -85,26 +120,28 @@ ModelChecker::~ModelChecker() delete pending_rel_seqs; delete thrd_last_action; + delete thrd_last_fence_release; delete node_stack; delete scheduler; delete mo_graph; - - snapshot_free(priv); + 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; @@ -118,11 +155,11 @@ void ModelChecker::reset_to_initial_state() { DEBUG("+++ Resetting to initial state +++\n"); node_stack->reset_execution(); - failed_promise = false; - too_many_reads = false; - bad_synchronization = false; - reset_asserted(); - snapshotObject->backTrackBeforeStep(0); + + /* Print all model-checker output before rollback */ + fflush(model_out); + + snapshot_backtrack_before(0); } /** @return a thread ID for a new Thread */ @@ -137,8 +174,13 @@ unsigned int ModelChecker::get_num_threads() const return priv->next_thread_id; } -/** @return The currently executing Thread. */ -Thread * ModelChecker::get_current_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(); } @@ -149,7 +191,8 @@ modelclock_t ModelChecker::get_next_seq_num() return ++priv->used_sequence_numbers; } -Node * ModelChecker::get_curr_node() { +Node * ModelChecker::get_curr_node() const +{ return node_stack->get_head(); } @@ -170,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? */ @@ -188,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(); @@ -216,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. */ @@ -245,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); @@ -258,23 +301,38 @@ 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); - } } } } +/** @brief Alert the model-checker that an incorrectly-ordered + * synchronization was made */ +void ModelChecker::set_bad_synchronization() +{ + priv->bad_synchronization = true; +} + +bool ModelChecker::has_asserted() const +{ + return priv->asserted; +} + +void ModelChecker::set_assert() +{ + priv->asserted = true; +} + /** * Check if we are in a deadlock. Should only be called at the end of an * execution, although it should not give false positives in the middle of an @@ -312,42 +370,153 @@ bool ModelChecker::is_complete_execution() const } /** - * Queries the model-checker for more executions to explore and, if one - * exists, resets the model-checker state to execute a new execution. + * @brief Assert a bug in the executing program. * - * @return If there are more executions to explore, return true. Otherwise, - * return false. + * Use this function to assert any sort of bug in the user program. If the + * current trace is feasible (actually, a prefix of some feasible execution), + * then this execution will be aborted, printing the appropriate message. If + * the current trace is not yet feasible, the error message will be stashed and + * printed if the execution ever becomes feasible. + * + * @param msg Descriptive message for the bug (do not include newline char) + * @return True if bug is immediately-feasible */ -bool ModelChecker::next_execution() +bool ModelChecker::assert_bug(const char *msg) { - DBG(); + priv->bugs.push_back(new bug_message(msg)); - num_executions++; + if (isfeasibleprefix()) { + set_assert(); + return true; + } + return false; +} - if (is_deadlocked()) - printf("ERROR: DEADLOCK\n"); - if (isfinalfeasible()) { - printf("Earliest divergence point since last feasible execution:\n"); +/** + * @brief Assert a bug in the executing program, asserted by a user thread + * @see ModelChecker::assert_bug + * @param msg Descriptive message for the bug (do not include newline char) + */ +void ModelChecker::assert_user_bug(const char *msg) +{ + /* If feasible bug, bail out now */ + if (assert_bug(msg)) + switch_to_master(NULL); +} + +/** @return True, if any bugs have been reported for this execution */ +bool ModelChecker::have_bug_reports() const +{ + return priv->bugs.size() != 0; +} + +/** @brief Print bug report listing for this execution (if any bugs exist) */ +void ModelChecker::print_bugs() const +{ + if (have_bug_reports()) { + model_print("Bug report: %zu bug%s detected\n", + priv->bugs.size(), + priv->bugs.size() > 1 ? "s" : ""); + for (unsigned int i = 0; i < priv->bugs.size(); i++) + priv->bugs[i]->print(); + } +} + +/** + * @brief Record end-of-execution stats + * + * Must be run when exiting an execution. Records various stats. + * @see struct execution_stats + */ +void ModelChecker::record_stats() +{ + stats.num_total++; + if (!isfeasibleprefix()) + stats.num_infeasible++; + else if (have_bug_reports()) + stats.num_buggy_executions++; + else if (is_complete_execution()) + stats.num_complete++; + else + stats.num_redundant++; +} + +/** @brief Print execution stats */ +void ModelChecker::print_stats() const +{ + model_print("Number of complete, bug-free executions: %d\n", stats.num_complete); + model_print("Number of redundant executions: %d\n", stats.num_redundant); + model_print("Number of buggy executions: %d\n", stats.num_buggy_executions); + model_print("Number of infeasible executions: %d\n", stats.num_infeasible); + model_print("Total executions: %d\n", stats.num_total); + model_print("Total nodes created: %d\n", node_stack->get_total_nodes()); +} + +/** + * @brief End-of-exeuction print + * @param printbugs Should any existing bugs be printed? + */ +void ModelChecker::print_execution(bool printbugs) const +{ + print_program_output(); + + if (DBG_ENABLED() || params.verbose) { + model_print("Earliest divergence point since last feasible execution:\n"); if (earliest_diverge) earliest_diverge->print(); else - printf("(Not set)\n"); + model_print("(Not set)\n"); - earliest_diverge = NULL; - num_feasible_executions++; + model_print("\n"); + print_stats(); } + /* Don't print invalid bugs */ + if (printbugs) + print_bugs(); + + model_print("\n"); + print_summary(); +} + +/** + * Queries the model-checker for more executions to explore and, if one + * exists, resets the model-checker state to execute a new execution. + * + * @return If there are more executions to explore, return true. Otherwise, + * return false. + */ +bool ModelChecker::next_execution() +{ + DBG(); + /* Is this execution a feasible execution that's worth bug-checking? */ + bool complete = isfeasibleprefix() && (is_complete_execution() || + have_bug_reports()); + + /* End-of-execution bug checks */ + if (complete) { + if (is_deadlocked()) + assert_bug("Deadlock detected"); - if (isfinalfeasible() || DBG_ENABLED()) { checkDataRaces(); - print_summary(); } + record_stats(); + + /* Output */ + if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports())) + print_execution(complete); + else + clear_program_output(); + + if (complete) + earliest_diverge = NULL; + if ((diverge = get_next_backtrack()) == NULL) return false; if (DBG_ENABLED()) { - printf("Next execution will diverge at:\n"); + model_print("Next execution will diverge at:\n"); diverge->print(); } @@ -358,9 +527,13 @@ bool ModelChecker::next_execution() ModelAction * ModelChecker::get_last_conflict(ModelAction *act) { switch (act->get_type()) { + case ATOMIC_FENCE: case ATOMIC_READ: case ATOMIC_WRITE: case ATOMIC_RMW: { + /* Optimization: relaxed operations don't need backtracking */ + if (act->is_relaxed()) + return NULL; /* linear search: from most recent to oldest */ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; @@ -389,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; @@ -400,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; @@ -415,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; @@ -434,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. */ @@ -457,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 */ @@ -466,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; } } @@ -478,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)) @@ -494,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. @@ -529,25 +721,24 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) r_status = r_modification_order(curr, reads_from); } - - if (!second_part_of_rmw&&!isfeasible()&&(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(); - too_many_reads = false; + priv->too_many_reads = false; continue; } - curr->read_from(reads_from); + 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(); - curr->read_from(NULL); - Promise *valuepromise = new Promise(curr, value, expiration); - promises->push_back(valuepromise); + struct future_value fv = curr->get_node()->get_future_value(); + value = fv.value; + curr->set_value(fv.value); + curr->set_read_from(NULL); + promises->push_back(new Promise(curr, fv)); } get_thread(curr)->set_return_value(value); return updated; @@ -570,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(); } @@ -594,10 +786,8 @@ bool ModelChecker::process_mutex(ModelAction *curr) { } //otherwise fall into the lock case case ATOMIC_LOCK: { - if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) { - printf("Lock access before initialization\n"); - set_assert(); - } + if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) + assert_bug("Lock access before initialization"); state->islocked = true; ModelAction *unlock = get_last_unlock(curr); //synchronize with the previous unlock statement @@ -630,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; } @@ -648,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)); @@ -662,6 +852,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 @@ -675,22 +886,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 * @@ -708,12 +965,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 */ @@ -726,6 +989,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; } @@ -806,8 +1076,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu } /* See if we have realized a data race */ - if (checkDataRaces()) - set_assert(); + checkDataRaces(); } /** @@ -838,7 +1107,7 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr) (*curr)->set_seq_number(get_next_seq_num()); - newcurr = node_stack->explore_action(*curr, scheduler->get_enabled()); + newcurr = node_stack->explore_action(*curr, scheduler->get_enabled_array()); if (newcurr) { /* First restore type and order in case of RMW operation */ if ((*curr)->is_rmwr()) @@ -860,6 +1129,10 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr) /* Always compute new clock vector */ newcurr->create_cv(get_parent_action(newcurr->get_tid())); + + /* Assign most recent release fence */ + newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid())); + /* * Perform one-time actions when pushing new ModelAction onto * NodeStack @@ -877,6 +1150,34 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr) } } +/** + * @brief Establish reads-from relation between two actions + * + * Perform basic operations involved with establishing a concrete rf relation, + * including setting the ModelAction data and checking for release sequences. + * + * @param act The action that is reading (must be a read) + * @param rf The action from which we are reading (must be a write) + * + * @return True if this read established synchronization + */ +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, 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])) { + set_bad_synchronization(); + num_heads--; + } + return num_heads > 0; + } + return false; +} + /** * @brief Check whether a model action is enabled. * @@ -889,8 +1190,8 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr) */ 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); @@ -925,11 +1226,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(); @@ -937,13 +1237,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 */ @@ -956,7 +1260,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) /* Initialize work_queue with the "current action" work */ work_queue_t work_queue(1, CheckCurrWorkEntry(curr)); - while (!work_queue.empty()) { + while (!work_queue.empty() && !has_asserted()) { WorkQueueEntry work = work_queue.front(); work_queue.pop_front(); @@ -975,6 +1279,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; @@ -1018,85 +1325,101 @@ 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; } -/** @return whether the current partial trace must be a prefix of a - * feasible trace. */ +/** + * This is the strongest feasibility check available. + * @return whether the current trace (partial or complete) must be a prefix of + * a feasible trace. + */ bool ModelChecker::isfeasibleprefix() const { - return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible(); + return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq(); } -/** @return whether the current partial trace is feasible. */ -bool ModelChecker::isfeasible() const +/** + * 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 { - if (DBG_ENABLED() && mo_graph->checkForRMWViolation()) - DEBUG("Infeasible: RMW violation\n"); - - return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW(); + 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); } -/** @return whether the current partial trace is feasible other than - * multiple RMW reading from the same store. */ -bool ModelChecker::isfeasibleotherthanRMW() const +/** + * Returns whether the current completed trace is feasible, except for pending + * release sequences. + */ +bool ModelChecker::is_feasible_prefix_ignore_relseq() const { - if (DBG_ENABLED()) { - if (mo_graph->checkForCycles()) - DEBUG("Infeasible: modification order cycles\n"); - if (failed_promise) - DEBUG("Infeasible: failed promise\n"); - if (too_many_reads) - DEBUG("Infeasible: too many reads\n"); - if (bad_synchronization) - DEBUG("Infeasible: bad synchronization ordering\n"); - if (promises_expired()) - DEBUG("Infeasible: promises expired\n"); - } - return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired(); + return !is_infeasible() && promises->size() == 0; } -/** Returns whether the current completed trace is feasible. */ -bool ModelChecker::isfinalfeasible() const +/** + * Check if the current partial trace is infeasible. Does not check any + * end-of-execution flags, which might rule out the execution. Thus, this is + * useful only for ruling an execution as infeasible. + * @return whether the current partial trace is infeasible. + */ +bool ModelChecker::is_infeasible() const { - if (DBG_ENABLED() && promises->size() != 0) - DEBUG("Infeasible: unrevolved promises\n"); - - return isfeasible() && promises->size() == 0; + return mo_graph->checkForRMWViolation() || + mo_graph->checkForCycles() || + priv->failed_promise || + priv->too_many_reads || + priv->bad_synchronization || + promises_expired(); } /** Close out a RMWR by converting previous RMWR into a RMW or READ. */ 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(); } @@ -1114,14 +1437,14 @@ 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 //accidentally clear by rolling back - if (!isfeasible()) + if (is_infeasible()) return; std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); int tid = id_to_int(curr->get_tid()); @@ -1141,8 +1464,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()) @@ -1153,18 +1476,18 @@ 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 = isfeasible(); + bool feasiblereadfrom = !is_infeasible(); mo_graph->rollbackChanges(); if (!feasiblereadfrom) @@ -1174,11 +1497,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; } @@ -1189,7 +1512,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { } } if (feasiblewrite) { - too_many_reads = true; + priv->too_many_reads = true; return; } } @@ -1220,14 +1543,51 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf bool added = false; ASSERT(curr->is_read()); + /* Last SC fence in the current thread */ + ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL); + /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { + /* Last SC fence in thread i */ + ModelAction *last_sc_fence_thread_local = NULL; + if (int_to_id((int)i) != curr->get_tid()) + last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL); + + /* Last SC fence in thread i, before last SC fence in current thread */ + ModelAction *last_sc_fence_thread_before = NULL; + if (last_sc_fence_local) + last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local); + /* Iterate over actions in thread, starting from most recent */ action_list_t *list = &(*thrd_lists)[i]; action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; + if (act->is_write() && act != 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; + 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; + 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; + break; + } + } + /* * Include at most one act per-thread that "happens * before" curr. Don't consider reflexively. @@ -1296,7 +1656,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 @@ -1307,13 +1667,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; @@ -1353,15 +1713,23 @@ bool ModelChecker::w_modification_order(ModelAction *curr) if (curr->is_seqcst()) { /* We have to at least see the last sequentially consistent write, so we are initialized. */ - ModelAction *last_seq_cst = get_last_seq_cst(curr); + ModelAction *last_seq_cst = get_last_seq_cst_write(curr); if (last_seq_cst != NULL) { mo_graph->addEdge(last_seq_cst, curr); added = true; } } + /* Last SC fence in the current thread */ + ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL); + /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { + /* Last SC fence in thread i, before last SC fence in current thread */ + ModelAction *last_sc_fence_thread_before = NULL; + if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid()) + last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local); + /* Iterate over actions in thread, starting from most recent */ action_list_t *list = &(*thrd_lists)[i]; action_list_t::reverse_iterator rit; @@ -1380,7 +1748,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; @@ -1388,6 +1756,14 @@ bool ModelChecker::w_modification_order(ModelAction *curr) continue; } + /* 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; + break; + } + /* * Include at most one act per-thread that "happens * before" curr @@ -1424,11 +1800,10 @@ bool ModelChecker::w_modification_order(ModelAction *curr) */ if (thin_air_constraint_may_allow(curr, act)) { - if (isfeasible() || - (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) { - 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); } } } @@ -1440,7 +1815,8 @@ bool ModelChecker::w_modification_order(ModelAction *curr) /** 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; @@ -1479,16 +1855,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; @@ -1531,6 +1907,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 */ @@ -1556,8 +1934,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]; @@ -1567,14 +1954,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)); @@ -1647,22 +2041,29 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, } /** - * A public interface for getting the release sequence head(s) with which a + * An interface for getting the release sequence head(s) with which a * 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 */ @@ -1691,21 +2092,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(); @@ -1715,15 +2117,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)); } @@ -1738,9 +2141,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ } // If we resolved promises or data races, see if we have realized a data race. - if (checkDataRaces()) { - set_assert(); - } + checkDataRaces(); return updated; } @@ -1755,31 +2156,47 @@ 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) + thrd_last_fence_release->resize(get_num_threads()); + (*thrd_last_fence_release)[tid] = 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); if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); - - if ((int)thrd_last_action->size() <= tid) - thrd_last_action->resize(get_num_threads()); - (*thrd_last_action)[tid] = act; } } @@ -1797,6 +2214,20 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) const return NULL; } +/** + * @brief Get the last fence release performed by a particular Thread + * @param tid The thread ID of the Thread in question + * @return The last fence release in the thread, if one exists; NULL otherwise + */ +ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const +{ + int threadid = id_to_int(tid); + if (threadid < (int)thrd_last_fence_release->size()) + return (*thrd_last_fence_release)[id_to_int(tid)]; + else + return NULL; +} + /** * Gets the last memory_order_seq_cst write (in the total global sequence) * performed on a particular object (i.e., memory location), not including the @@ -1805,7 +2236,7 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) const * check * @return The last seq_cst write */ -ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const +ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const { void *location = curr->get_location(); action_list_t *list = get_safe_ptr_action(obj_map, location); @@ -1817,6 +2248,35 @@ ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const return NULL; } +/** + * Gets the last memory_order_seq_cst fence (in the total global sequence) + * performed in a particular thread, prior to a particular fence. + * @param tid The ID of the thread to check + * @param before_fence The fence from which to begin the search; if NULL, then + * search for the most recent fence in the thread. + * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL + */ +ModelAction * ModelChecker::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const +{ + /* All fences should have NULL location */ + action_list_t *list = get_safe_ptr_action(obj_map, NULL); + action_list_t::reverse_iterator rit = list->rbegin(); + + if (before_fence) { + for (; rit != list->rend(); rit++) + if (*rit == before_fence) + break; + + ASSERT(*rit == before_fence); + rit++; + } + + for (; rit != list->rend(); rit++) + if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst()) + return *rit; + return NULL; +} + /** * Gets the last unlock operation performed on a particular mutex (i.e., memory * location). This function identifies the mutex according to the current @@ -1837,7 +2297,7 @@ ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const return NULL; } -ModelAction * ModelChecker::get_parent_action(thread_id_t tid) +ModelAction * ModelChecker::get_parent_action(thread_id_t tid) const { ModelAction *parent = get_last_action(tid); if (!parent) @@ -1850,7 +2310,7 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid) * @param tid The thread whose clock vector we want * @return Desired clock vector */ -ClockVector * ModelChecker::get_cv(thread_id_t tid) +ClockVector * ModelChecker::get_cv(thread_id_t tid) const { return get_parent_action(tid)->get_cv(); } @@ -1864,7 +2324,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) 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]; @@ -1873,7 +2333,7 @@ bool ModelChecker::resolve_promises(ModelAction *write) if (read->is_rmw()) { mo_graph->addRMWEdge(write, read); } - read->read_from(write); + read_from(read, write); //First fix up the modification order for actions that happened //before the read r_modification_order(read, write); @@ -1885,7 +2345,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 @@ -1895,8 +2355,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; } @@ -1931,38 +2393,43 @@ 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 - failed_promise = true; + priv->failed_promise = true; return; } } } } -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()) { - failed_promise = true; + 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. * @@ -1971,47 +2438,51 @@ 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)) { - failed_promise = true; + if (mo_graph->checkPromise(write, promise)) { + priv->failed_promise = true; return; } } - if (mo_graph->checkPromise(write, promise)) { - 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)) { - failed_promise = true; + if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) { + if (promise->eliminate_thread(tid)) { + priv->failed_promise = true; return; } } @@ -2054,18 +2525,10 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) unsigned int i; ASSERT(curr->is_read()); - ModelAction *last_seq_cst = NULL; + ModelAction *last_sc_write = NULL; - /* Track whether this object has been initialized */ - bool initialized = false; - - if (curr->is_seqcst()) { - last_seq_cst = get_last_seq_cst(curr); - /* We have to at least see the last sequentially consistent write, - so we are initialized. */ - if (last_seq_cst != NULL) - initialized = true; - } + if (curr->is_seqcst()) + last_sc_write = get_last_seq_cst_write(curr); /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { @@ -2080,120 +2543,128 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) continue; /* Don't consider more than one seq_cst write if we are a seq_cst read. */ - if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) { - if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) { - DEBUG("Adding action to may_read_from:\n"); - if (DBG_ENABLED()) { - act->print(); - curr->print(); - } - curr->get_node()->add_read_from(act); - } - } + bool allow_read = true; + + if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write) + allow_read = false; + else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act)) + allow_read = false; + + 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) { - /** @todo Need a more informative way of reporting errors. */ - printf("ERROR: may read from uninitialized atomic\n"); - set_assert(); - } - - if (DBG_ENABLED() || !initialized) { - printf("Reached read action:\n"); + if (DBG_ENABLED()) { + model_print("Reached read action:\n"); curr->print(); - printf("Printing may_read_from\n"); + model_print("Printing may_read_from\n"); curr->get_node()->print_may_read_from(); - printf("End printing may_read_from\n"); + model_print("End printing may_read_from\n"); } } -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(); } } +/** + * @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; - printf("---------------------------------------------------------------------\n"); - printf("Trace:\n"); - unsigned int hash=0; + model_print("---------------------------------------------------------------------\n"); + + 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()); } - printf("HASH %u\n", hash); - printf("---------------------------------------------------------------------\n"); + 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); } #endif -void ModelChecker::print_summary() +/** @brief Prints an execution trace summary. */ +void ModelChecker::print_summary() const { - printf("\n"); - printf("Number of executions: %d\n", num_executions); - printf("Number of feasible executions: %d\n", num_feasible_executions); - printf("Total nodes created: %d\n", node_stack->get_total_nodes()); - #if SUPPORT_MOD_ORDER_DUMP scheduler->print(); char buffername[100]; - sprintf(buffername, "exec%04u", num_executions); + sprintf(buffername, "exec%04u", stats.num_total); mo_graph->dumpGraphToFile(buffername); - sprintf(buffername, "graph%04u", num_executions); + sprintf(buffername, "graph%04u", stats.num_total); dumpGraph(buffername); #endif - if (!isfinalfeasible()) - printf("INFEASIBLE EXECUTION!\n"); + model_print("Execution %d:", stats.num_total); + if (isfeasibleprefix()) + model_print("\n"); + else + print_infeasibility(" INFEASIBLE"); print_list(action_trace); - printf("\n"); + model_print("\n"); } /** @@ -2231,7 +2702,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()); } @@ -2265,53 +2736,56 @@ 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); + 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 (!isfeasible()) + if (is_infeasible()) + return false; + else if (isfeasibleprefix() && have_bug_reports()) { + set_assert(); 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: @@ -2322,9 +2796,9 @@ 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()) && - isfinalfeasible() && !unrealizedraces.empty()) { - printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n", + 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()); ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ, std::memory_order_seq_cst, NULL, VALUE_NONE, @@ -2333,27 +2807,46 @@ 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); } -/** Runs the current execution until threre are no more steps to take. */ -void ModelChecker::finish_execution() { - DBG(); +/** Wrapper to run the user's main function, with appropriate arguments */ +void user_main_wrapper(void *) +{ + user_main(model->params.argc, model->params.argv); +} + +/** @brief Run ModelChecker for the user program */ +void ModelChecker::run() +{ + do { + thrd_t user_thread; + Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL); + + add_thread(t); + + /* 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(priv->current_action)); + } while (next_execution()); - while (take_step()); + print_stats(); }