X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=a9ea7b0493071eebac0b034e7d84d23f3cd21d8f;hp=e11dcf716939e1a13f1dd08f6b252ab60fef1b9b;hb=7966c737f2a88e5e1a56817eb9f6fdaead3eca92;hpb=5d87d23f622d396fd2e1c94d61f901429c5f35ac diff --git a/model.cc b/model.cc index e11dcf71..a9ea7b04 100644 --- a/model.cc +++ b/model.cc @@ -1,5 +1,6 @@ #include #include +#include #include "model.h" #include "action.h" @@ -11,43 +12,90 @@ #include "cyclegraph.h" #include "promise.h" #include "datarace.h" -#include "mutex.h" -#include "threads.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), + nextThread(NULL), + 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 */ 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()), thread_map(new HashTable()), - obj_map(new HashTable()), - lock_waiters_map(new HashTable()), - obj_thrd_map(new HashTable, uintptr_t, 4 >()), + obj_map(new HashTable()), + lock_waiters_map(new HashTable()), + condvar_waiters_map(new HashTable()), + obj_thrd_map(new HashTable *, uintptr_t, 4 >()), promises(new std::vector< Promise *, SnapshotAlloc >()), 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 *)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); @@ -63,6 +111,7 @@ ModelChecker::~ModelChecker() delete obj_thrd_map; delete obj_map; delete lock_waiters_map; + delete condvar_waiters_map; delete action_trace; for (unsigned int i = 0; i < promises->size(); i++) @@ -72,9 +121,29 @@ ModelChecker::~ModelChecker() delete pending_rel_seqs; delete thrd_last_action; + delete thrd_last_fence_release; delete node_stack; delete scheduler; delete mo_graph; + 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(); + 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(); + hash->put(ptr, tmp); + } + return tmp; } /** @@ -85,10 +154,10 @@ 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(); + + /* Print all model-checker output before rollback */ + fflush(model_out); + snapshotObject->backTrackBeforeStep(0); } @@ -99,13 +168,13 @@ thread_id_t ModelChecker::get_next_id() } /** @return the number of user threads created during this execution */ -unsigned int ModelChecker::get_num_threads() +unsigned int ModelChecker::get_num_threads() const { return priv->next_thread_id; } /** @return The currently executing Thread. */ -Thread * ModelChecker::get_current_thread() +Thread * ModelChecker::get_current_thread() const { return scheduler->get_current_thread(); } @@ -116,6 +185,11 @@ modelclock_t ModelChecker::get_next_seq_num() return ++priv->used_sequence_numbers; } +Node * ModelChecker::get_curr_node() const +{ + return node_stack->get_head(); +} + /** * @brief Choose the next thread to execute. * @@ -158,7 +232,11 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) scheduler->update_sleep_set(prevnode); /* Reached divergence point */ - if (nextnode->increment_promise()) { + if (nextnode->increment_misc()) { + /* The next node will try to satisfy a different misc_index values. */ + tid = next->get_tid(); + node_stack->pop_restofstack(2); + } else if (nextnode->increment_promise()) { /* The next node will try to satisfy a different set of promises. */ tid = next->get_tid(); node_stack->pop_restofstack(2); @@ -198,7 +276,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) return thread_map->get(id_to_int(tid)); } -/** +/** * We need to know what the next actions of all threads in the sleep * set will be. This method computes them and stores the actions at * the corresponding thread object's pending action. @@ -208,7 +286,8 @@ void ModelChecker::execute_sleep_set() { for(unsigned int i=0;iget_enabled(thr) == THREAD_SLEEP_SET ) { + if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET && + thr->get_pending() == NULL ) { thr->set_state(THREAD_RUNNING); scheduler->next_thread(thr); Thread::swap(&system_context, thr); @@ -225,12 +304,175 @@ void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { Thread *thr=get_thread(tid); if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) { ModelAction *pending_act=thr->get_pending(); - if (pending_act->could_synchronize_with(curr)) { + 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 + * execution (there should be some ENABLED thread). + * + * @return True if program is in a deadlock; false otherwise + */ +bool ModelChecker::is_deadlocked() const +{ + bool blocking_threads = false; + for (unsigned int i = 0; i < get_num_threads(); i++) { + thread_id_t tid = int_to_id(i); + if (is_enabled(tid)) + return false; + Thread *t = get_thread(tid); + if (!t->is_model_thread() && t->get_pending()) + blocking_threads = true; + } + return blocking_threads; +} + +/** + * Check if this is a complete execution. That is, have all thread completed + * execution (rather than exiting because sleep sets have forced a redundant + * execution). + * + * @return True if the execution is complete. + */ +bool ModelChecker::is_complete_execution() const +{ + for (unsigned int i = 0; i < get_num_threads(); i++) + if (is_enabled(int_to_id(i))) + return false; + return true; +} + +/** + * @brief Assert a bug in the executing program. + * + * 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::assert_bug(const char *msg) +{ + priv->bugs.push_back(new bug_message(msg)); + + if (isfeasibleprefix()) { + set_assert(); + return true; + } + return false; +} + +/** + * @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 + model_print("(Not set)\n"); + + model_print("\n"); + print_stats(); + } + + /* Don't print invalid bugs */ + if (printbugs) + print_bugs(); + + model_print("\n"); + print_summary(); } /** @@ -243,31 +485,34 @@ void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { 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()); - num_executions++; - - if (isfinalfeasible()) { - printf("Earliest divergence point since last feasible execution:\n"); - if (earliest_diverge) - earliest_diverge->print(); - else - printf("(Not set)\n"); + /* End-of-execution bug checks */ + if (complete) { + if (is_deadlocked()) + assert_bug("Deadlock detected"); - earliest_diverge = NULL; - num_feasible_executions++; + checkDataRaces(); } - DEBUG("Number of acquires waiting on pending release sequences: %zu\n", - pending_rel_seqs->size()); + record_stats(); + + /* Output */ + if (DBG_ENABLED() || params.verbose || have_bug_reports()) + print_execution(complete); + else + clear_program_output(); - if (isfinalfeasible() || DBG_ENABLED()) - print_summary(); + 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(); } @@ -278,11 +523,15 @@ 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 = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -294,7 +543,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) case ATOMIC_LOCK: case ATOMIC_TRYLOCK: { /* linear search: from most recent to oldest */ - action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -305,7 +554,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) } case ATOMIC_UNLOCK: { /* linear search: from most recent to oldest */ - action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -314,6 +563,32 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) } break; } + case ATOMIC_WAIT: { + /* 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; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *prev = *rit; + if (!act->same_thread(prev)&&prev->is_failed_trylock()) + return prev; + if (!act->same_thread(prev)&&prev->is_notify()) + return prev; + } + break; + } + + case ATOMIC_NOTIFY_ALL: + case ATOMIC_NOTIFY_ONE: { + /* 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; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *prev = *rit; + if (!act->same_thread(prev)&&prev->is_wait()) + return prev; + } + break; + } default: break; } @@ -346,10 +621,14 @@ void ModelChecker::set_backtracking(ModelAction *act) 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. */ + if (i >= node->get_num_threads()) + break; + /* Don't backtrack into a point where the thread is disabled or sleeping. */ - if (node->get_enabled_array()[i]!=THREAD_ENABLED) + if (node->enabled_status(tid)!=THREAD_ENABLED) continue; - + /* Check if this has been explored already */ if (node->has_been_explored(tid)) continue; @@ -404,7 +683,7 @@ ModelAction * ModelChecker::get_next_backtrack() */ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) { - uint64_t value; + uint64_t value = VALUE_NONE; bool updated = false; while (true) { const ModelAction *reads_from = curr->get_node()->get_read_from(); @@ -420,13 +699,13 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) } - 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); @@ -435,7 +714,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool 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); + read_from(curr, NULL); Promise *valuepromise = new Promise(curr, value, expiration); promises->push_back(valuepromise); } @@ -461,8 +740,17 @@ 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 = (std::mutex *)curr->get_location(); - struct std::mutex_state *state = mutex->get_state(); + 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()) { + mutex = (std::mutex *)curr->get_value(); + state = mutex->get_state(); + } + switch (curr->get_type()) { case ATOMIC_TRYLOCK: { bool success = !state->islocked; @@ -475,10 +763,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 @@ -492,7 +778,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) { //unlock the lock state->islocked = false; //wake up the other threads - action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location()); + action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location()); //activate all the waiting threads for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { scheduler->wake(get_thread(*rit)); @@ -500,6 +786,43 @@ bool ModelChecker::process_mutex(ModelAction *curr) { waiters->clear(); break; } + case ATOMIC_WAIT: { + //unlock the lock + state->islocked = false; + //wake up the other threads + action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value()); + //activate all the waiting threads + for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { + scheduler->wake(get_thread(*rit)); + } + waiters->clear(); + //check whether we should go to sleep or not...simulate spurious failures + 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()); + } + break; + } + case ATOMIC_NOTIFY_ALL: { + action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location()); + //activate all the waiting threads + for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { + scheduler->wake(get_thread(*rit)); + } + waiters->clear(); + break; + } + 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(); + action_list_t::iterator it = waiters->begin(); + advance(it, wakeupthread); + scheduler->wake(get_thread(*it)); + waiters->erase(it); + break; + } + default: ASSERT(0); } @@ -650,8 +973,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(); } /** @@ -661,44 +983,53 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu * initializing clock vectors, and computing the promises to fulfill. * * @param curr The current action, as passed from the user context; may be - * freed/invalidated after the execution of this function - * @return The current action, as processed by the ModelChecker. Is only the - * same as the parameter @a curr if this is a newly-explored action. + * freed/invalidated after the execution of this function, with a different + * action "returned" its place (pass-by-reference) + * @return True if curr is a newly-explored action; false otherwise */ -ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) +bool ModelChecker::initialize_curr_action(ModelAction **curr) { ModelAction *newcurr; - if (curr->is_rmwc() || curr->is_rmw()) { - newcurr = process_rmw(curr); - delete curr; + if ((*curr)->is_rmwc() || (*curr)->is_rmw()) { + newcurr = process_rmw(*curr); + delete *curr; if (newcurr->is_rmw()) compute_promises(newcurr); - return newcurr; + + *curr = newcurr; + return false; } - curr->set_seq_number(get_next_seq_num()); + (*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()) - newcurr->copy_typeandorder(curr); + if ((*curr)->is_rmwr()) + newcurr->copy_typeandorder(*curr); - ASSERT(curr->get_location() == newcurr->get_location()); - newcurr->copy_from_new(curr); + ASSERT((*curr)->get_location() == newcurr->get_location()); + newcurr->copy_from_new(*curr); /* Discard duplicate ModelAction; use action from NodeStack */ - delete curr; + delete *curr; /* Always compute new clock vector */ newcurr->create_cv(get_parent_action(newcurr->get_tid())); + + *curr = newcurr; + return false; /* Action was explored previously */ } else { - newcurr = curr; + newcurr = *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 @@ -707,8 +1038,41 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) compute_promises(newcurr); else if (newcurr->is_relseq_fixup()) compute_relseq_breakwrites(newcurr); + else if (newcurr->is_wait()) + newcurr->get_node()->set_misc_max(2); + else if (newcurr->is_notify_one()) { + newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size()); + } + return true; /* This was a new ModelAction */ + } +} + +/** + * @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, &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 newcurr; + return false; } /** @@ -727,7 +1091,7 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { struct std::mutex_state * state = lock->get_state(); if (state->islocked) { //Stick the action in the appropriate waiting queue - lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr); + get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr); return false; } } else if (curr->get_type() == THREAD_JOIN) { @@ -741,6 +1105,16 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { return true; } +/** + * Stores the ModelAction for the current thread action. Call this + * immediately before switching from user- to system-context to pass + * data between them. + * @param act The ModelAction created by the user-thread action + */ +void ModelChecker::set_current_action(ModelAction *act) { + priv->current_action = act; +} + /** * This is the heart of the model checker routine. It performs model-checking * actions corresponding to a given "current action." Among other processes, it @@ -766,23 +1140,21 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) return get_next_thread(NULL); } - wake_up_sleeping_actions(curr); - - ModelAction *newcurr = initialize_curr_action(curr); + bool newly_explored = initialize_curr_action(&curr); + wake_up_sleeping_actions(curr); /* Add the action to lists before any other model-checking tasks */ if (!second_part_of_rmw) - add_action_to_lists(newcurr); + add_action_to_lists(curr); /* Build may_read_from set for newly-created actions */ - if (curr == newcurr && curr->is_read()) + if (newly_explored && curr->is_read()) build_reads_from_past(curr); - curr = newcurr; /* 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(); @@ -852,6 +1224,7 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) { Node *parnode = currnode->get_parent(); if ((!parnode->backtrack_empty() || + !currnode->misc_empty() || !currnode->read_from_empty() || !currnode->future_value_empty() || !currnode->promise_empty() || @@ -862,7 +1235,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) { } } -bool ModelChecker::promises_expired() { +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) { @@ -872,44 +1246,67 @@ bool ModelChecker::promises_expired() { return false; } -/** @return whether the current partial trace must be a prefix of a - * feasible trace. */ -bool ModelChecker::isfeasibleprefix() { - return promises->size() == 0 && pending_rel_seqs->size() == 0; +/** + * 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 pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq(); +} + +/** + * 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; } -/** @return whether the current partial trace is feasible. */ -bool ModelChecker::isfeasible() { +/** + * 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() && mo_graph->checkForRMWViolation()) DEBUG("Infeasible: RMW violation\n"); - return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW(); + return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW(); } -/** @return whether the current partial trace is feasible other than - * multiple RMW reading from the same store. */ -bool ModelChecker::isfeasibleotherthanRMW() { +/** + * 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 (failed_promise) + if (priv->failed_promise) DEBUG("Infeasible: failed promise\n"); - if (too_many_reads) + if (priv->too_many_reads) DEBUG("Infeasible: too many reads\n"); - if (bad_synchronization) + if (priv->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(); -} - -/** Returns whether the current completed trace is feasible. */ -bool ModelChecker::isfinalfeasible() { - if (DBG_ENABLED() && promises->size() != 0) - DEBUG("Infeasible: unrevolved promises\n"); - - return isfeasible() && promises->size() == 0; + return 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. */ @@ -941,9 +1338,9 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { 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 = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); int tid = id_to_int(curr->get_tid()); /* Skip checks */ @@ -967,7 +1364,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { ModelAction *act = *rit; if (!act->is_read()) return; - + if (act->get_reads_from() != rf) return; if (act->get_node()->get_read_from_size() <= 1) @@ -984,7 +1381,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { /* 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) @@ -998,7 +1395,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { 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(i)==write) { + if (act->get_node()->get_read_from_at(j)==write) { foundvalue = true; break; } @@ -1009,7 +1406,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { } } if (feasiblewrite) { - too_many_reads = true; + priv->too_many_reads = true; return; } } @@ -1035,19 +1432,53 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { */ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; 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; + } + /* 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; + } + /* 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; + } + } + /* * Include at most one act per-thread that "happens * before" curr. Don't consider reflexively. @@ -1094,7 +1525,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf */ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; ASSERT(curr->is_read()); @@ -1165,7 +1596,7 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio */ bool ModelChecker::w_modification_order(ModelAction *curr) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; bool added = false; ASSERT(curr->is_write()); @@ -1173,15 +1604,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; @@ -1192,7 +1631,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) * 1) If RMW and it actually read from something, then we * already have all relevant edges, so just skip to next * thread. - * + * * 2) If RMW and it didn't read from anything, we should * whatever edge we can get to speed up convergence. * @@ -1202,12 +1641,19 @@ bool ModelChecker::w_modification_order(ModelAction *curr) if (curr->is_rmw()) { if (curr->get_reads_from()!=NULL) break; - else + else continue; } else 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; + } + /* * Include at most one act per-thread that "happens * before" curr @@ -1221,7 +1667,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) */ if (act->is_write()) mo_graph->addEdge(act, curr); - else if (act->is_read()) { + else if (act->is_read()) { //if previous read accessed a null, just keep going if (act->get_reads_from() == NULL) continue; @@ -1244,8 +1690,8 @@ 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())) { + 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); } @@ -1278,33 +1724,42 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con return true; } -/** 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::mo_may_allow(const ModelAction * writer, const ModelAction *reader) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location()); - - //Get write that follows reader action - action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())]; - action_list_t::reverse_iterator rit; - ModelAction *first_write_after_read=NULL; +/** + * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places + * some constraints. This method checks one the following constraint (others + * require compiler support): + * + * If X --hb-> Y --mo-> Z, then X should not read from Z. + */ +bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader) +{ + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location()); + unsigned int i; + /* Iterate over all threads */ + for (i = 0; i < thrd_lists->size(); i++) { + const ModelAction *write_after_read = NULL; - for (rit = list->rbegin(); rit != list->rend(); rit++) { - ModelAction *act = *rit; - if (act==reader) - break; - if (act->is_write()) - first_write_after_read=act; - } + /* 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 (first_write_after_read==NULL) - return true; + if (!reader->happens_before(act)) + break; + else if (act->is_write()) + write_after_read = act; + else if (act->is_read() && act->get_reads_from() != NULL && act != reader) { + write_after_read = act->get_reads_from(); + } + } - return !mo_graph->checkReachable(first_write_after_read, writer); + if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer)) + return false; + } + return true; } - - /** * Finds the head(s) of the release sequence(s) containing a given ModelAction. * The ModelAction under consideration is expected to be taking part in @@ -1342,6 +1797,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 */ @@ -1367,10 +1824,19 @@ 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 = obj_thrd_map->get_safe_ptr(rf->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location()); action_list_t *list = &(*thrd_lists)[tid]; action_list_t::const_reverse_iterator rit; @@ -1378,14 +1844,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)); @@ -1405,7 +1878,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, ModelAction *last = get_last_action(int_to_id(i)); Thread *th = get_thread(int_to_id(i)); if ((last && rf->happens_before(last)) || - !scheduler->is_enabled(th) || + !is_enabled(th) || th->is_complete()) future_ordered = true; @@ -1421,8 +1894,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, continue; } - /* Only writes can break release sequences */ - if (!act->is_write()) + /* Only non-RMW writes can break release sequences */ + if (!act->is_write() || act->is_rmw()) continue; /* Check modification order */ @@ -1458,7 +1931,7 @@ 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 @@ -1549,9 +2022,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; } @@ -1568,9 +2039,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act) int tid = id_to_int(act->get_tid()); action_trace->push_back(act); - obj_map->get_safe_ptr(act->get_location())->push_back(act); + get_safe_ptr_action(obj_map, act->get_location())->push_back(act); - std::vector *vec = obj_thrd_map->get_safe_ptr(act->get_location()); + 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); @@ -1578,6 +2049,22 @@ void ModelChecker::add_action_to_lists(ModelAction *act) if ((int)thrd_last_action->size() <= tid) thrd_last_action->resize(get_num_threads()); (*thrd_last_action)[tid] = act; + + 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(); + 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); + } } /** @@ -1594,6 +2081,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 @@ -1602,10 +2103,10 @@ 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 = obj_map->get_safe_ptr(location); + action_list_t *list = get_safe_ptr_action(obj_map, location); /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */ action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) @@ -1614,6 +2115,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 @@ -1625,16 +2155,16 @@ ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const { void *location = curr->get_location(); - action_list_t *list = obj_map->get_safe_ptr(location); + action_list_t *list = get_safe_ptr_action(obj_map, location); /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */ action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) - if ((*rit)->is_unlock()) + if ((*rit)->is_unlock() || (*rit)->is_wait()) return *rit; 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) @@ -1647,7 +2177,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(); } @@ -1670,7 +2200,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); @@ -1680,7 +2210,7 @@ bool ModelChecker::resolve_promises(ModelAction *write) //Make sure the promise's value matches the write's value ASSERT(promise->get_value() == write->get_value()); delete(promise); - + promises->erase(promises->begin() + promise_index); threads_to_check.push_back(read->get_tid()); @@ -1713,8 +2243,9 @@ void ModelChecker::compute_promises(ModelAction *curr) act->is_read() && !act->could_synchronize_with(curr) && !act->same_thread(curr) && + act->get_location() == curr->get_location() && promise->get_value() == curr->get_value()) { - curr->get_node()->set_promise(i); + curr->get_node()->set_promise(i, act->is_rmw()); } } } @@ -1729,17 +2260,27 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec merge_cv->synchronized_since(act)) { if (promise->increment_threads(tid)) { //Promise has failed - failed_promise = true; + priv->failed_promise = true; return; } } } } +void ModelChecker::check_promises_thread_disabled() { + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + if (promise->check_promise()) { + priv->failed_promise = true; + return; + } + } +} + /** Checks promises in response to addition to modification order for threads. * Definitions: * pthread is the thread that performed the read that created the promise - * + * * pread is the read that created the promise * * pwrite is either the first write to same location as pread by @@ -1768,7 +2309,7 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) 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 ) continue; @@ -1779,20 +2320,25 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) //do we have a pwrite for the promise, if not, set it if (promise->get_write() == NULL ) { promise->set_write(write); + //The pwrite cannot happen before the promise + if (write->happens_before(act) && (write != act)) { + priv->failed_promise = true; + return; + } } if (mo_graph->checkPromise(write, promise)) { - failed_promise = true; + priv->failed_promise = true; return; } } - + //Don't do any lookups twice for the same thread if (promise->has_sync_thread(tid)) continue; - - if (mo_graph->checkReachable(promise->get_write(), write)) { + + if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) { if (promise->increment_threads(tid)) { - failed_promise = true; + priv->failed_promise = true; return; } } @@ -1831,20 +2377,20 @@ void ModelChecker::compute_relseq_breakwrites(ModelAction *curr) */ void ModelChecker::build_reads_from_past(ModelAction *curr) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); 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); + 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_seq_cst != NULL) + if (last_sc_write != NULL) initialized = true; } @@ -1861,18 +2407,20 @@ 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) { + 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) { DEBUG("Adding action to may_read_from:\n"); if (DBG_ENABLED()) { act->print(); curr->print(); } - - if (curr->get_sleep_flag()) { - if (sleep_can_read_from(curr, act)) - curr->get_node()->add_read_from(act); - } else - curr->get_node()->add_read_from(act); + curr->get_node()->add_read_from(act); } /* Include at most one act per-thread that "happens before" curr */ @@ -1883,26 +2431,23 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) } } - if (!initialized) { - /** @todo Need a more informative way of reporting errors. */ - printf("ERROR: may read from uninitialized atomic\n"); - } + if (!initialized) + assert_bug("May read from uninitialized atomic"); if (DBG_ENABLED() || !initialized) { - printf("Reached read action:\n"); + 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"); } - - ASSERT(initialized); } bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) { while(true) { Node *prevnode=write->get_node()->get_parent(); - bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET; + + bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET; if (write->is_release()&&thread_sleep) return true; if (!write->is_rmw()) { @@ -1914,31 +2459,33 @@ bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *wr } } -static void print_list(action_list_t *list) +static void print_list(action_list_t *list, int exec_num = -1) { action_list_t::iterator it; - printf("---------------------------------------------------------------------\n"); - printf("Trace:\n"); + model_print("---------------------------------------------------------------------\n"); + if (exec_num >= 0) + model_print("Execution %d:\n", exec_num); + unsigned int hash=0; - + for (it = list->begin(); it != list->end(); it++) { (*it)->print(); 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) { 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()); - + for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) { ModelAction *action=*it; if (action->is_read()) { @@ -1949,35 +2496,31 @@ void ModelChecker::dumpGraph(char *filename) { 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; } - fprintf(file,"}\n"); + fprintf(file,"}\n"); model_free(thread_array); - fclose(file); + 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); - dumpGraph(buffername); + sprintf(buffername, "graph%04u", stats.num_total); + dumpGraph(buffername); #endif - if (!isfinalfeasible()) - printf("INFEASIBLE EXECUTION!\n"); - print_list(action_trace); - printf("\n"); + if (!isfeasibleprefix()) + model_print("INFEASIBLE EXECUTION!\n"); + print_list(action_trace, stats.num_total); + model_print("\n"); } /** @@ -1992,7 +2535,7 @@ void ModelChecker::add_thread(Thread *t) } /** - * Removes a thread from the scheduler. + * Removes a thread from the scheduler. * @param the thread to remove. */ void ModelChecker::remove_thread(Thread *t) @@ -2020,6 +2563,26 @@ Thread * ModelChecker::get_thread(ModelAction *act) const return get_thread(act->get_tid()); } +/** + * @brief Check if a Thread is currently enabled + * @param t The Thread to check + * @return True if the Thread is currently enabled + */ +bool ModelChecker::is_enabled(Thread *t) const +{ + return scheduler->is_enabled(t); +} + +/** + * @brief Check if a Thread is currently enabled + * @param tid The ID of the Thread to check + * @return True if the Thread is currently enabled + */ +bool ModelChecker::is_enabled(thread_id_t tid) const +{ + return scheduler->is_enabled(tid); +} + /** * Switch from a user-context to the "master thread" context (a.k.a. system * context). This switch is made with the intention of exploring a particular @@ -2065,8 +2628,18 @@ bool ModelChecker::take_step() { Thread *next = scheduler->next_thread(priv->nextThread); /* 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) { + return false; + } + } DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1, next ? id_to_int(next->get_id()) : -1); @@ -2081,8 +2654,8 @@ bool ModelChecker::take_step() { * (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", + 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, @@ -2109,9 +2682,24 @@ bool ModelChecker::take_step() { return (Thread::swap(&system_context, next) == 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; + + /* Start user program */ + add_thread(new Thread(&user_thread, &user_main_wrapper, NULL)); + + /* Wait for all threads to complete */ + while (take_step()); + } while (next_execution()); - while (take_step()); + print_stats(); }