X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=52eab24c6790fdc472bdfc30937fa356aa319fed;hb=b133a2b2e11e6b95dfa805b9b90a4e53dce3d81d;hp=ee3ce992cef8aa816fde0466ce67b42e5f6161c5;hpb=ee0f520bb244e2aa820e6b5a7e24c43c396b0905;p=c11tester.git diff --git a/model.cc b/model.cc index ee3ce992..52eab24c 100644 --- a/model.cc +++ b/model.cc @@ -1,5 +1,6 @@ #include #include +#include #include "model.h" #include "action.h" @@ -11,8 +12,7 @@ #include "cyclegraph.h" #include "promise.h" #include "datarace.h" -#include "mutex.h" -#include "threads.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); @@ -260,7 +270,8 @@ 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() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) print_summary(); if ((diverge = get_next_backtrack()) == NULL) @@ -314,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; } @@ -404,7 +441,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(); @@ -461,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; @@ -500,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); } @@ -707,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; } @@ -766,10 +854,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) return get_next_thread(NULL); } - wake_up_sleeping_actions(curr); - ModelAction *newcurr = 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) @@ -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() || @@ -1278,32 +1366,40 @@ 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) { +/** + * 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 = obj_thrd_map->get_safe_ptr(reader->get_location()); + unsigned int i; - //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; - - 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 all threads */ + for (i = 0; i < thrd_lists->size(); i++) { + ModelAction *write_after_read = NULL; - if (first_write_after_read==NULL) - return true; + /* 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; - return !mo_graph->checkReachable(first_write_after_read, writer); -} + if (!reader->happens_before(act)) + break; + else if (act->is_write()) + write_after_read = act; + } + if (write_after_read && mo_graph->checkReachable(write_after_read, writer)) + return false; + } + return true; +} /** * Finds the head(s) of the release sequence(s) containing a given ModelAction. @@ -1421,8 +1517,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 +1674,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 +1739,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 +1823,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); } @@ -1873,7 +1984,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) curr->print(); } - if (curr->get_sleep_flag()) { + if (curr->get_sleep_flag() && ! curr->is_seqcst()) { if (sleep_can_read_from(curr, act)) curr->get_node()->add_read_from(act); } else @@ -1891,6 +2002,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 +2012,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) { @@ -2073,6 +2183,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);