X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=e6203cb548861653ed600b83238f112f4e42d667;hp=70261b0faf7d35ca1a0694a0f3d6193b573bc84d;hb=a7b4dab68db8b1fc466a7ca4098d5a6fb006e353;hpb=7594d7ae8eda38fbb5a3ac3d6f33fffbb365b7bd diff --git a/execution.cc b/execution.cc index 70261b0f..e6203cb5 100644 --- a/execution.cc +++ b/execution.cc @@ -15,6 +15,7 @@ #include "bugmessage.h" #include "history.h" #include "fuzzer.h" +#include "newfuzzer.h" #define INITIAL_THREAD_ID 0 @@ -64,7 +65,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : thrd_last_fence_release(), priv(new struct model_snapshot_members ()), mo_graph(new CycleGraph()), - fuzzer(new Fuzzer()), + fuzzer(new NewFuzzer()), thrd_func_list(), thrd_func_act_lists(), isfinished(false) @@ -73,6 +74,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : model_thread = new Thread(get_next_id()); add_thread(model_thread); scheduler->register_engine(this); + fuzzer->register_engine(m->get_history(), this); } /** @brief Destructor */ @@ -90,7 +92,7 @@ int ModelExecution::get_execution_number() const return model->get_execution_number(); } -static action_list_t * get_safe_ptr_action(HashTable * hash, void * ptr) +static action_list_t * get_safe_ptr_action(HashTable * hash, void * ptr) { action_list_t *tmp = hash->get(ptr); if (tmp == NULL) { @@ -100,7 +102,7 @@ static action_list_t * get_safe_ptr_action(HashTable * get_safe_ptr_vect_action(HashTable *, uintptr_t, 4> * hash, void * ptr) +static SnapVector * get_safe_ptr_vect_action(HashTable *, uintptr_t, 2> * hash, void * ptr) { SnapVector *tmp = hash->get(ptr); if (tmp == NULL) { @@ -128,6 +130,12 @@ modelclock_t ModelExecution::get_next_seq_num() return ++priv->used_sequence_numbers; } +/** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */ +void ModelExecution::restore_last_seq_num() +{ + priv->used_sequence_numbers--; +} + /** * @brief Should the current action wake up a given thread? * @@ -166,9 +174,12 @@ void ModelExecution::wake_up_sleeping_actions(ModelAction *curr) for (unsigned int i = 0;i < get_num_threads();i++) { Thread *thr = get_thread(int_to_id(i)); if (scheduler->is_sleep_set(thr)) { - if (should_wake_up(curr, thr)) + if (should_wake_up(curr, thr)) { /* Remove this thread from sleep set */ scheduler->remove_sleep(thr); + if (thr->get_pending()->is_sleep()) + thr->set_pending(NULL); + } } } } @@ -197,16 +208,6 @@ bool ModelExecution::have_bug_reports() const return priv->bugs.size() != 0; } -/** @return True, if any fatal bugs have been reported for this execution. - * Any bug other than a data race is considered a fatal bug. Data races - * are not considered fatal unless the number of races is exceeds - * a threshold (temporarily set as 15). - */ -bool ModelExecution::have_fatal_bug_reports() const -{ - return priv->bugs.size() != 0; -} - SnapVector * ModelExecution::get_bugs() const { return &priv->bugs; @@ -280,6 +281,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) { add_normal_write_to_lists(act); add_write_to_lists(act); w_modification_order(act); + model->get_history()->process_action(act, act->get_tid()); return act; } @@ -289,7 +291,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) { * @param rf_set is the set of model actions we can possibly read from * @return True if processing this read updates the mo_graph. */ -void ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) +bool ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) { SnapVector * priorset = new SnapVector(); bool hasnonatomicstore = hasNonAtomicStore(curr->get_location()); @@ -298,10 +300,21 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set->push_back(nonatomicstore); } + // Remove writes that violate read modification order + for (uint i = 0; i < rf_set->size(); i++) { + ModelAction * rf = (*rf_set)[i]; + if (!r_modification_order(curr, rf, NULL, NULL, true)) { + (*rf_set)[i] = rf_set->back(); + rf_set->pop_back(); + } + } + while(true) { int index = fuzzer->selectWrite(curr, rf_set); - ModelAction *rf = (*rf_set)[index]; + if (index == -1) // no feasible write exists + return false; + ModelAction *rf = (*rf_set)[index]; ASSERT(rf); bool canprune = false; @@ -316,7 +329,7 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector * int tid = id_to_int(curr->get_tid()); (*obj_thrd_map.get(curr->get_location()))[tid].pop_back(); } - return; + return true; } priorset->clear(); (*rf_set)[index] = rf_set->back(); @@ -372,7 +385,27 @@ bool ModelExecution::process_mutex(ModelAction *curr) } break; } - case ATOMIC_WAIT: + case ATOMIC_WAIT: { + /* wake up the other threads */ + for (unsigned int i = 0;i < get_num_threads();i++) { + Thread *t = get_thread(int_to_id(i)); + Thread *curr_thrd = get_thread(curr); + if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock()) + scheduler->wake(t); + } + + /* unlock the lock - after checking who was waiting on it */ + state->locked = NULL; + + if (fuzzer->shouldWait(curr)) { + /* disable this thread */ + get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr); + scheduler->sleep(get_thread(curr)); + } + + break; + } + case ATOMIC_TIMEDWAIT: case ATOMIC_UNLOCK: { //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS MUST EVENMTUALLY RELEASE... @@ -386,10 +419,6 @@ bool ModelExecution::process_mutex(ModelAction *curr) /* unlock the lock - after checking who was waiting on it */ state->locked = NULL; - - if (!curr->is_wait()) - break;/* The rest is only for ATOMIC_WAIT */ - break; } case ATOMIC_NOTIFY_ALL: { @@ -548,6 +577,12 @@ void ModelExecution::process_thread_action(ModelAction *curr) case THREAD_START: { break; } + case THREAD_SLEEP: { + Thread *th = get_thread(curr); + th->set_pending(curr); + scheduler->add_sleep(th); + break; + } default: break; } @@ -684,26 +719,35 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) wake_up_sleeping_actions(curr); - /* Add the action to lists before any other model-checking tasks */ - if (!second_part_of_rmw && curr->get_type() != NOOP) - add_action_to_lists(curr); - - if (curr->is_write()) - add_write_to_lists(curr); + /* Add uninitialized actions to lists */ + if (!second_part_of_rmw) + add_uninit_action_to_lists(curr); SnapVector * rf_set = NULL; /* Build may_read_from set for newly-created actions */ if (newly_explored && curr->is_read()) rf_set = build_may_read_from(curr); - process_thread_action(curr); - if (curr->is_read() && !second_part_of_rmw) { process_read(curr, rf_set); delete rf_set; - } else { + +/* bool success = process_read(curr, rf_set); + delete rf_set; + if (!success) + return curr; // Do not add action to lists +*/ + } else ASSERT(rf_set == NULL); - } + + /* Add the action to lists */ + if (!second_part_of_rmw) + add_action_to_lists(curr); + + if (curr->is_write()) + add_write_to_lists(curr); + + process_thread_action(curr); if (curr->is_write()) process_write(curr); @@ -777,10 +821,13 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) { * * @param curr The current action. Must be a read. * @param rf The ModelAction or Promise that curr reads from. Must be a write. + * @param check_only If true, then only check whether the current action satisfies + * read modification order or not, without modifiying priorset and canprune. + * False by default. * @return True if modification order edges were added; false otherwise */ -bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector * priorset, bool * canprune) +bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector * priorset, bool * canprune, bool check_only) { SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; @@ -833,7 +880,8 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * *act < *last_sc_fence_thread_local) { if (mo_graph->checkReachable(rf, act)) return false; - priorset->push_back(act); + if (!check_only) + priorset->push_back(act); break; } /* C++, Section 29.3 statement 4 */ @@ -841,7 +889,8 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * *act < *last_sc_fence_local) { if (mo_graph->checkReachable(rf, act)) return false; - priorset->push_back(act); + if (!check_only) + priorset->push_back(act); break; } /* C++, Section 29.3 statement 6 */ @@ -849,7 +898,8 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * *act < *last_sc_fence_thread_before) { if (mo_graph->checkReachable(rf, act)) return false; - priorset->push_back(act); + if (!check_only) + priorset->push_back(act); break; } } @@ -868,17 +918,20 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * if (act->is_write()) { if (mo_graph->checkReachable(rf, act)) return false; - priorset->push_back(act); + if (!check_only) + priorset->push_back(act); } else { const ModelAction *prevrf = act->get_reads_from(); if (!prevrf->equals(rf)) { if (mo_graph->checkReachable(rf, prevrf)) return false; - priorset->push_back(prevrf); + if (!check_only) + priorset->push_back(prevrf); } else { if (act->get_tid() == curr->get_tid()) { //Can prune curr from obj list - *canprune = true; + if (!check_only) + *canprune = true; } } } @@ -1092,13 +1145,15 @@ ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const { } /** - * Performs various bookkeeping operations for the current ModelAction. For - * instance, adds action to the per-object, per-thread action vector and to the - * action trace list of all thread actions. + * Performs various bookkeeping operations for the current ModelAction when it is + * the first atomic action occurred at its memory location. * - * @param act is the ModelAction to add. + * For instance, adds uninitialized action to the per-object, per-thread action vector + * and to the action trace list of all thread actions. + * + * @param act is the ModelAction to process. */ -void ModelExecution::add_action_to_lists(ModelAction *act) +void ModelExecution::add_uninit_action_to_lists(ModelAction *act) { int tid = id_to_int(act->get_tid()); ModelAction *uninit = NULL; @@ -1109,40 +1164,69 @@ void ModelExecution::add_action_to_lists(ModelAction *act) uninit_id = id_to_int(uninit->get_tid()); list->push_front(uninit); SnapVector *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location()); - if (uninit_id >= (int)vec->size()) { + if ((int)vec->size() <= uninit_id) { int oldsize = (int) vec->size(); vec->resize(uninit_id + 1); - for(int i=oldsize;ipush_back(act); // Update action trace, a total order of all actions - action_trace.push_back(act); if (uninit) action_trace.push_front(uninit); // Update obj_thrd_map, a per location, per thread, order of actions SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); - if (tid >= (int)vec->size()) { - uint oldsize =vec->size(); + if ((int)vec->size() <= tid) { + uint oldsize = vec->size(); vec->resize(priv->next_thread_id); - for(uint i=oldsize;inext_thread_id;i++) + for(uint i = oldsize; i < priv->next_thread_id; i++) new (&(*vec)[i]) action_list_t(); } - (*vec)[tid].push_back(act); if (uninit) (*vec)[uninit_id].push_front(uninit); // Update thrd_last_action, the last action taken by each thrad if ((int)thrd_last_action.size() <= tid) thrd_last_action.resize(get_num_threads()); - thrd_last_action[tid] = act; if (uninit) thrd_last_action[uninit_id] = uninit; +} + + +/** + * Performs various bookkeeping operations for the current ModelAction. For + * instance, adds action to the per-object, per-thread action vector and to the + * action trace list of all thread actions. + * + * @param act is the ModelAction to add. + */ +void ModelExecution::add_action_to_lists(ModelAction *act) +{ + int tid = id_to_int(act->get_tid()); + action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); + list->push_back(act); + + // Update action trace, a total order of all actions + action_trace.push_back(act); + + // Update obj_thrd_map, a per location, per thread, order of actions + SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); + if ((int)vec->size() <= tid) { + uint oldsize = vec->size(); + vec->resize(priv->next_thread_id); + for(uint i = oldsize; i < priv->next_thread_id; i++) + new (&(*vec)[i]) action_list_t(); + } + (*vec)[tid].push_back(act); + + // Update thrd_last_action, the last action taken by each thrad + if ((int)thrd_last_action.size() <= tid) + thrd_last_action.resize(get_num_threads()); + thrd_last_action[tid] = act; // Update thrd_last_fence_release, the last release fence taken by each thread if (act->is_fence() && act->is_release()) { @@ -1156,10 +1240,10 @@ void ModelExecution::add_action_to_lists(ModelAction *act) get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act); SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc); - if (tid >= (int)vec->size()) { + if ((int)vec->size() <= tid) { uint oldsize = vec->size(); vec->resize(priv->next_thread_id); - for(uint i=oldsize;inext_thread_id;i++) + for(uint i = oldsize; i < priv->next_thread_id; i++) new (&(*vec)[i]) action_list_t(); } (*vec)[tid].push_back(act); @@ -1634,7 +1718,7 @@ bool ModelExecution::is_enabled(thread_id_t tid) const Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const { /* Do not split atomic RMW */ - if (curr->is_rmwr()) + if (curr->is_rmwr() && !paused_by_fuzzer(curr)) return get_thread(curr); /* Follow CREATE with the created thread */ /* which is not needed, because model.cc takes care of this */ @@ -1646,6 +1730,15 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons return NULL; } +/** @param act A read atomic action */ +bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const +{ + ASSERT(act->is_read()); + + // Actions paused by fuzzer have their sequence number reset to 0 + return act->get_seq_number() == 0; +} + /** * Takes the next step in the execution, if possible. * @param curr The current step to take @@ -1661,7 +1754,7 @@ Thread * ModelExecution::take_step(ModelAction *curr) curr = check_current_action(curr); ASSERT(curr); - /* Process this action in ModelHistory for records*/ + /* Process this action in ModelHistory for records */ model->get_history()->process_action( curr, curr->get_tid() ); if (curr_thrd->is_blocked() || curr_thrd->is_complete())