X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=f8aa4f0a4fd49b6eb487539c9fece2d15146e2a0;hp=e394865e26c01d75b05853a55a4b2b7a23c3e853;hb=0e98bb1bcba9294c9674fd011e92555b2524f34d;hpb=98952a7c75650993548c6fda82273e3460268a86 diff --git a/model.cc b/model.cc index e394865..f8aa4f0 100644 --- a/model.cc +++ b/model.cc @@ -1,5 +1,6 @@ #include #include +#include #include "model.h" #include "action.h" @@ -11,7 +12,6 @@ #include "cyclegraph.h" #include "promise.h" #include "datarace.h" -#include "mutex.h" #include "threads-model.h" #define INITIAL_THREAD_ID 0 @@ -31,6 +31,7 @@ ModelChecker::ModelChecker(struct model_params params) : thread_map(new HashTable()), 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 >()), @@ -63,6 +64,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++) @@ -116,6 +118,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 +164,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); @@ -315,6 +325,32 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) } break; } + case ATOMIC_WAIT: { + /* linear search: from most recent to oldest */ + action_list_t *list = obj_map->get_safe_ptr(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 = obj_map->get_safe_ptr(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; } @@ -462,8 +498,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; @@ -501,6 +546,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 = lock_waiters_map->get_safe_ptr((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) { + condvar_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr); + //disable us + scheduler->sleep(get_current_thread()); + } + break; + } + case ATOMIC_NOTIFY_ALL: { + action_list_t *waiters = condvar_waiters_map->get_safe_ptr(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 = condvar_waiters_map->get_safe_ptr(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); } @@ -708,6 +790,11 @@ 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(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size()); + } } return newcurr; } @@ -852,6 +939,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() || @@ -1421,8 +1509,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 */ @@ -1578,6 +1666,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(); + obj_map->get_safe_ptr(mutex_loc)->push_back(act); + + std::vector *vec = obj_thrd_map->get_safe_ptr(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; + } } /** @@ -1629,7 +1731,7 @@ ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const /* 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; } @@ -1713,6 +1815,7 @@ 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); } @@ -1891,6 +1994,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) { @@ -1900,8 +2004,6 @@ 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) {