X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=e5c8a55033289bf7393094c514d9e85658489342;hp=31e0694e459b018da371ae4ff8c484369582f49d;hb=826d667b8d232223d7418f5614a8e30e9ce74c89;hpb=7da7d6e22d9e7dcdc65711c4459a6e9af30c1458 diff --git a/model.cc b/model.cc index 31e0694..e5c8a55 100644 --- a/model.cc +++ b/model.cc @@ -1,5 +1,6 @@ #include #include +#include #include "model.h" #include "action.h" @@ -11,13 +12,23 @@ #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; +/** + * 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; +}; + /** @brief Constructor */ ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ @@ -29,13 +40,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), @@ -63,6 +75,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++) @@ -77,6 +90,24 @@ ModelChecker::~ModelChecker() delete mo_graph; } +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; +} + /** * Restores user program to initial state and resets all model-checker data * structures. @@ -99,7 +130,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 +147,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 +193,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 +218,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 +237,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 +247,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 +265,33 @@ 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; } /** @@ -246,6 +307,8 @@ bool ModelChecker::next_execution() num_executions++; + if (is_deadlocked()) + printf("ERROR: DEADLOCK\n"); if (isfinalfeasible()) { printf("Earliest divergence point since last feasible execution:\n"); if (earliest_diverge) @@ -260,8 +323,11 @@ bool ModelChecker::next_execution() DEBUG("Number of acquires waiting on pending release sequences: %zu\n", pending_rel_seqs->size()); - if (isfinalfeasible() || DBG_ENABLED()) + + if (isfinalfeasible() || DBG_ENABLED()) { + checkDataRaces(); print_summary(); + } if ((diverge = get_next_backtrack()) == NULL) return false; @@ -282,7 +348,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 +360,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 +371,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 +380,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,9 +438,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 +500,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 +557,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; @@ -491,7 +597,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 +632,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 +661,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 +699,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 */ @@ -667,41 +803,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 +854,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 +879,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 +893,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 +922,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 +1007,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() || @@ -885,7 +1036,7 @@ 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; + return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible(); } /** @return whether the current partial trace is feasible. */ @@ -953,7 +1104,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 +1128,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 +1159,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 +1196,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 +1255,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 +1326,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 +1353,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 +1363,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 +1382,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 +1398,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 +1439,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 @@ -1349,7 +1540,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; @@ -1384,7 +1575,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; @@ -1400,8 +1591,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 */ @@ -1478,7 +1669,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; @@ -1547,9 +1738,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); @@ -1557,6 +1748,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; + } } /** @@ -1584,7 +1789,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++) @@ -1604,11 +1809,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; } @@ -1640,7 +1845,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]; @@ -1659,7 +1864,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()); @@ -1692,8 +1897,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()); } } } @@ -1715,10 +1921,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 @@ -1747,7 +1963,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; @@ -1758,18 +1974,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; @@ -1810,7 +2031,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()); @@ -1841,12 +2062,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 */ @@ -1860,6 +2083,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) { @@ -1869,8 +2093,22 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) curr->get_node()->print_may_read_from(); printf("End printing may_read_from\n"); } +} + +bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) { + while(true) { + Node *prevnode=write->get_node()->get_parent(); - ASSERT(initialized); + 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) @@ -1879,22 +2117,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()) { @@ -1905,12 +2146,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 @@ -1927,7 +2168,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()) @@ -1948,7 +2189,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) @@ -1976,6 +2217,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 +2285,12 @@ bool ModelChecker::take_step() { if (!isfeasible()) 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);