X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=model.cc;h=417252c3f92ceb3a4bb7948612ca3592f1be49de;hb=1798c510e77f37e3d79cba6a1fdad3b13ccc9674;hp=4f2719f338c8afa9ba05d2f0835fd565bd6dfbd2;hpb=b8b39c87557325a384faa45d0cae56a6f71f52b1;p=model-checker.git diff --git a/model.cc b/model.cc index 4f2719f..417252c 100644 --- a/model.cc +++ b/model.cc @@ -1,5 +1,6 @@ #include #include +#include #include "model.h" #include "action.h" @@ -11,13 +12,36 @@ #include "cyclegraph.h" #include "promise.h" #include "datarace.h" -#include "mutex.h" -#include "threads.h" +#include "threads-model.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() { printf("%s", msg); } +}; + +/** + * Structure for holding small ModelChecker members that should be snapshotted + */ +struct model_snapshot_members { + ModelAction *current_action; + unsigned int next_thread_id; + modelclock_t used_sequence_numbers; + Thread *nextThread; + ModelAction *next_backtrack; + std::vector< bug_message *, SnapshotAlloc > bugs; +}; + /** @brief Constructor */ ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ @@ -29,13 +53,14 @@ ModelChecker::ModelChecker(struct model_params params) : 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 >()), - promises(new std::vector()), - futurevalues(new std::vector()), - pending_rel_seqs(new std::vector()), - thrd_last_action(new std::vector(1)), + 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)), node_stack(new NodeStack()), mo_graph(new CycleGraph()), failed_promise(false), @@ -44,7 +69,7 @@ ModelChecker::ModelChecker(struct model_params params) : bad_synchronization(false) { /* Allocate this "size" on the snapshotting heap */ - priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv)); + 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; @@ -63,6 +88,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++) @@ -75,6 +101,29 @@ ModelChecker::~ModelChecker() delete node_stack; delete scheduler; delete mo_graph; + + for (unsigned int i = 0; i < priv->bugs.size(); i++) + delete priv->bugs[i]; + priv->bugs.clear(); + snapshot_free(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; } /** @@ -99,7 +148,7 @@ 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; } @@ -116,6 +165,10 @@ modelclock_t ModelChecker::get_next_seq_num() return ++priv->used_sequence_numbers; } +Node * ModelChecker::get_curr_node() { + return node_stack->get_head(); +} + /** * @brief Choose the next thread to execute. * @@ -158,7 +211,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); @@ -179,7 +236,6 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid()))); tid = prevnode->get_next_backtrack(); /* Make sure the backtracked thread isn't sleeping. */ - scheduler->remove_sleep(thread_map->get(id_to_int(tid))); node_stack->pop_restofstack(1); if (diverge==earliest_diverge) { earliest_diverge=prevnode->get_action(); @@ -199,7 +255,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. @@ -209,10 +265,12 @@ 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); + priv->current_action->set_sleep_flag(); thr->set_pending(priv->current_action); } } @@ -225,12 +283,114 @@ 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); } } - } + } +} + +/** + * 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. + * + * This function can also be used to immediately trigger the bug; that is, we + * don't wait for a feasible execution before aborting. Only use the + * "immediate" option when you know that the infeasibility is justified (e.g., + * pending release sequences are not a problem) + * + * @param msg Descriptive message for the bug (do not include newline char) + * @param user_thread Was this assertion triggered from a user thread? + * @param immediate Should this bug be triggered immediately? + */ +void ModelChecker::assert_bug(const char *msg, bool user_thread, bool immediate) +{ + priv->bugs.push_back(new bug_message(msg)); + + if (immediate || isfeasibleprefix()) { + set_assert(); + if (user_thread) + switch_to_master(NULL); + } +} + +/** + * @brief Assert a bug in the executing program, with a default message + * @see ModelChecker::assert_bug + * @param user_thread Was this assertion triggered from a user thread? + */ +void ModelChecker::assert_bug(bool user_thread) +{ + assert_bug("bug detected", user_thread); +} + +/** + * @brief Assert a bug in the executing program immediately + * @see ModelChecker::assert_bug + * @param msg Descriptive message for the bug (do not include newline char) + */ +void ModelChecker::assert_bug_immediate(const char *msg) +{ + printf("Feasible: %s\n", isfeasibleprefix() ? "yes" : "no"); + assert_bug(msg, false, true); +} + +/** @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()) { + printf("Bug report: %zu bugs detected\n", priv->bugs.size()); + for (unsigned int i = 0; i < priv->bugs.size(); i++) + priv->bugs[i]->print(); + } } /** @@ -246,7 +406,7 @@ bool ModelChecker::next_execution() num_executions++; - if (isfinalfeasible()) { + if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) { printf("Earliest divergence point since last feasible execution:\n"); if (earliest_diverge) earliest_diverge->print(); @@ -255,13 +415,16 @@ bool ModelChecker::next_execution() earliest_diverge = NULL; num_feasible_executions++; - } - DEBUG("Number of acquires waiting on pending release sequences: %zu\n", - pending_rel_seqs->size()); + if (is_deadlocked()) + assert_bug("Deadlock detected"); - if (isfinalfeasible() || DBG_ENABLED()) + print_bugs(); + checkDataRaces(); print_summary(); + } else if (DBG_ENABLED()) { + print_summary(); + } if ((diverge = get_next_backtrack()) == NULL) return false; @@ -282,7 +445,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) case ATOMIC_WRITE: case ATOMIC_RMW: { /* 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 +457,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,12 +468,38 @@ 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; + if (!act->same_thread(prev)&&prev->is_failed_trylock()) + return prev; + } + 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; } @@ -346,9 +535,14 @@ void ModelChecker::set_backtracking(ModelAction *act) for(int i = low_tid; i < high_tid; i++) { thread_id_t tid = int_to_id(i); - if (!node->is_enabled(tid)) + /* 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->enabled_status(tid)!=THREAD_ENABLED) continue; - + /* Check if this has been explored already */ if (node->has_been_explored(tid)) continue; @@ -403,7 +597,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(); @@ -460,8 +654,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; @@ -474,10 +677,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 @@ -491,7 +692,34 @@ 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)); + } + 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)); @@ -499,6 +727,16 @@ bool ModelChecker::process_mutex(ModelAction *curr) { 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); } @@ -518,7 +756,9 @@ bool ModelChecker::process_write(ModelAction *curr) if (promises->size() == 0) { for (unsigned int i = 0; i < futurevalues->size(); i++) { struct PendingFutureValue pfv = (*futurevalues)[i]; - if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) && + //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; } @@ -554,26 +794,17 @@ bool ModelChecker::process_thread_action(ModelAction *curr) break; } case THREAD_JOIN: { - Thread *waiting, *blocking; - waiting = get_thread(curr); - blocking = (Thread *)curr->get_location(); - if (!blocking->is_complete()) { - blocking->push_wait_list(curr); - scheduler->sleep(waiting); - } else { - do_complete_join(curr); - updated = true; /* trigger rel-seq checks */ - } + Thread *blocking = (Thread *)curr->get_location(); + ModelAction *act = get_last_action(blocking->get_id()); + curr->synchronize_with(act); + updated = true; /* trigger rel-seq checks */ break; } case THREAD_FINISH: { Thread *th = get_thread(curr); while (!th->wait_list_empty()) { ModelAction *act = th->pop_wait_list(); - Thread *wake = get_thread(act); - scheduler->wake(wake); - do_complete_join(act); - updated = true; /* trigger rel-seq checks */ + scheduler->wake(get_thread(act)); } th->complete(); updated = true; /* trigger rel-seq checks */ @@ -657,7 +888,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(); + assert_bug("Datarace"); } /** @@ -667,41 +898,46 @@ 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()); 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())); @@ -713,14 +949,22 @@ 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 */ } - return newcurr; } /** - * This method checks whether a model action is enabled at the given point. - * At this point, it checks whether a lock operation would be successful at this point. - * If not, it puts the thread in a waiter list. + * @brief Check whether a model action is enabled. + * + * Checks whether a lock or join operation would be successful (i.e., is the + * lock already locked, or is the joined thread already complete). If not, put + * the action in a waiter list. + * * @param curr is the ModelAction to check whether it is enabled. * @return a bool that indicates whether the action is enabled. */ @@ -730,7 +974,13 @@ 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) { + Thread *blocking = (Thread *)curr->get_location(); + if (!blocking->is_complete()) { + blocking->push_wait_list(curr); return false; } } @@ -738,6 +988,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 @@ -757,25 +1017,23 @@ 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 is actually available to release */ + * much later, when a lock/join can succeed */ get_current_thread()->set_pending(curr); scheduler->sleep(get_current_thread()); 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)); @@ -844,24 +1102,12 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) return get_next_thread(curr); } -/** - * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH - * operation from the Thread it is joining with. Must be called after the - * completion of the Thread in question. - * @param join The THREAD_JOIN action - */ -void ModelChecker::do_complete_join(ModelAction *join) -{ - Thread *blocking = (Thread *)join->get_location(); - ModelAction *act = get_last_action(blocking->get_id()); - join->synchronize_with(act); -} - void ModelChecker::check_curr_backtracking(ModelAction * curr) { Node *currnode = curr->get_node(); Node *parnode = currnode->get_parent(); if ((!parnode->backtrack_empty() || + !currnode->misc_empty() || !currnode->read_from_empty() || !currnode->future_value_empty() || !currnode->promise_empty() || @@ -872,7 +1118,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) { @@ -884,12 +1131,14 @@ bool ModelChecker::promises_expired() { /** @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; +bool ModelChecker::isfeasibleprefix() const +{ + return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible(); } /** @return whether the current partial trace is feasible. */ -bool ModelChecker::isfeasible() { +bool ModelChecker::isfeasible() const +{ if (DBG_ENABLED() && mo_graph->checkForRMWViolation()) DEBUG("Infeasible: RMW violation\n"); @@ -898,7 +1147,8 @@ bool ModelChecker::isfeasible() { /** @return whether the current partial trace is feasible other than * multiple RMW reading from the same store. */ -bool ModelChecker::isfeasibleotherthanRMW() { +bool ModelChecker::isfeasibleotherthanRMW() const +{ if (DBG_ENABLED()) { if (mo_graph->checkForCycles()) DEBUG("Infeasible: modification order cycles\n"); @@ -915,7 +1165,8 @@ bool ModelChecker::isfeasibleotherthanRMW() { } /** Returns whether the current completed trace is feasible. */ -bool ModelChecker::isfinalfeasible() { +bool ModelChecker::isfinalfeasible() const +{ if (DBG_ENABLED() && promises->size() != 0) DEBUG("Infeasible: unrevolved promises\n"); @@ -953,7 +1204,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { //accidentally clear by rolling back if (!isfeasible()) 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 */ @@ -977,7 +1228,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) @@ -1008,7 +1259,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; } @@ -1045,7 +1296,7 @@ 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()); @@ -1104,7 +1355,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()); @@ -1175,7 +1426,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()); @@ -1202,7 +1453,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. * @@ -1212,7 +1463,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) if (curr->is_rmw()) { if (curr->get_reads_from()!=NULL) break; - else + else continue; } else continue; @@ -1231,7 +1482,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; @@ -1247,12 +1498,16 @@ bool ModelChecker::w_modification_order(ModelAction *curr) (3) cannot synchronize with us (4) is in a different thread => - that read could potentially read from our write. + that read could potentially read from our write. Note that + these checks are overly conservative at this point, we'll + do more checks before actually removing the + pendingfuturevalue. + */ 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->get_value(),curr->get_seq_number()+params.maxfuturedelay,act}; + struct PendingFutureValue pfv = {curr,act}; futurevalues->push_back(pfv); } } @@ -1284,6 +1539,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 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; + + /* 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 (!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(); + } + } + + 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 @@ -1296,7 +1587,6 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con * "returns" two pieces of data: a pass-by-reference vector of @a release_heads * and a boolean representing certainty. * - * @todo Finish lazy updating, when promises are fulfilled in the future * @param rf The action that might be part of a release sequence. Must be a * write. * @param release_heads A pass-by-reference style return parameter. After @@ -1350,7 +1640,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, /* else relaxed write; check modification order for contiguous subsequence * -> rf must be same thread as 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; @@ -1385,7 +1675,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; @@ -1401,8 +1691,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 */ @@ -1479,7 +1769,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue) { bool updated = false; - std::vector::iterator it = pending_rel_seqs->begin(); + 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; @@ -1529,9 +1819,8 @@ 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(); - } + if (checkDataRaces()) + assert_bug("Datarace"); return updated; } @@ -1548,9 +1837,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); @@ -1558,6 +1847,20 @@ 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_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); + + if ((int)thrd_last_action->size() <= tid) + thrd_last_action->resize(get_num_threads()); + (*thrd_last_action)[tid] = act; + } } /** @@ -1585,7 +1888,7 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) const ModelAction * ModelChecker::get_last_seq_cst(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++) @@ -1605,11 +1908,11 @@ 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; } @@ -1641,7 +1944,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) bool ModelChecker::resolve_promises(ModelAction *write) { bool resolved = false; - std::vector threads_to_check; + std::vector< thread_id_t, ModelAlloc > threads_to_check; for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) { Promise *promise = (*promises)[promise_index]; @@ -1660,7 +1963,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()); @@ -1693,8 +1996,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()); } } } @@ -1716,10 +2020,20 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec } } +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; + 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 @@ -1748,7 +2062,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; @@ -1759,18 +2073,23 @@ 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)) { + 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)) 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; return; @@ -1811,7 +2130,7 @@ 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()); @@ -1842,12 +2161,14 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) /* 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) { - DEBUG("Adding action to may_read_from:\n"); - if (DBG_ENABLED()) { - act->print(); - curr->print(); + 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); } - curr->get_node()->add_read_from(act); } /* Include at most one act per-thread that "happens before" curr */ @@ -1861,6 +2182,7 @@ 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"); + set_assert(); } if (DBG_ENABLED() || !initialized) { @@ -1870,8 +2192,22 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) curr->get_node()->print_may_read_from(); printf("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->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) + return true; + write=write->get_reads_from(); + } } static void print_list(action_list_t *list) @@ -1880,22 +2216,25 @@ static void print_list(action_list_t *list) printf("---------------------------------------------------------------------\n"); printf("Trace:\n"); + 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"); } #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()) { @@ -1906,12 +2245,12 @@ 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 @@ -1928,7 +2267,7 @@ void ModelChecker::print_summary() sprintf(buffername, "exec%04u", num_executions); mo_graph->dumpGraphToFile(buffername); sprintf(buffername, "graph%04u", num_executions); - dumpGraph(buffername); + dumpGraph(buffername); #endif if (!isfinalfeasible()) @@ -1949,7 +2288,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) @@ -1977,6 +2316,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 @@ -2024,6 +2383,16 @@ bool ModelChecker::take_step() { /* Infeasible -> don't take any more steps */ if (!isfeasible()) 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);