X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=7b8461226a8860d60a0311c2fa2538607c9b1363;hp=87dbe69eeeea320257cda85dc16b905665502529;hb=da918c450a8fb8524ed99da0a35a7e417eb85777;hpb=a9c4af542eaa752dc356f364f6256c7bee2da5ed diff --git a/execution.cc b/execution.cc index 87dbe69e..7b846122 100644 --- a/execution.cc +++ b/execution.cc @@ -28,7 +28,6 @@ struct model_snapshot_members { next_thread_id(INITIAL_THREAD_ID), used_sequence_numbers(0), bugs(), - bad_synchronization(false), asserted(false) { } @@ -42,7 +41,6 @@ struct model_snapshot_members { modelclock_t used_sequence_numbers; SnapVector bugs; /** @brief Incorrectly-ordered synchronization was made */ - bool bad_synchronization; bool asserted; SNAPSHOTALLOC @@ -66,15 +64,16 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : priv(new struct model_snapshot_members ()), mo_graph(new CycleGraph()), fuzzer(new NewFuzzer()), - thrd_func_list(), - thrd_func_act_lists(), isfinished(false) { /* Initialize a model-checker thread, for special ModelActions */ model_thread = new Thread(get_next_id()); add_thread(model_thread); - scheduler->register_engine(this); fuzzer->register_engine(m->get_history(), this); + scheduler->register_engine(this); +#ifdef TLS + pthread_key_create(&pthreadkey, tlsdestructor); +#endif } /** @brief Destructor */ @@ -161,6 +160,7 @@ bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *threa if (fence_release && *(get_last_action(thread->get_id())) < *fence_release) return true; } + /* The sleep is literally sleeping */ if (asleep->is_sleep()) { if (fuzzer->shouldWake(asleep)) return true; @@ -174,29 +174,20 @@ 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_wakeup_state(true); + } } } } -/** @brief Alert the model-checker that an incorrectly-ordered - * synchronization was made */ -void ModelExecution::set_bad_synchronization() -{ - priv->bad_synchronization = true; -} - -bool ModelExecution::assert_bug(const char *msg) +void ModelExecution::assert_bug(const char *msg) { priv->bugs.push_back(new bug_message(msg)); - - if (isfeasibleprefix()) { - set_assert(); - return true; - } - return false; + set_assert(); } /** @return True, if any bugs have been reported for this execution */ @@ -297,10 +288,19 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set->push_back(nonatomicstore); } + // Remove writes that violate read modification order + uint i = 0; + while (i < rf_set->size()) { + ModelAction * rf = (*rf_set)[i]; + if (!r_modification_order(curr, rf, NULL, NULL, true)) { + (*rf_set)[i] = rf_set->back(); + rf_set->pop_back(); + } else + i++; + } + while(true) { int index = fuzzer->selectWrite(curr, rf_set); - if (index == -1) // no feasible write exists - return false; ModelAction *rf = (*rf_set)[index]; @@ -319,6 +319,9 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * } return true; } + + ASSERT(false); + /* TODO: Following code not needed anymore */ priorset->clear(); (*rf_set)[index] = rf_set->back(); rf_set->pop_back(); @@ -565,6 +568,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; } @@ -644,7 +653,7 @@ void ModelExecution::read_from(ModelAction *act, ModelAction *rf) bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second) { if (*second < *first) { - set_bad_synchronization(); + ASSERT(0); //This should not happend return false; } return second->synchronize_with(first); @@ -702,7 +711,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) wake_up_sleeping_actions(curr); /* Add uninitialized actions to lists */ - if (!second_part_of_rmw && curr->get_type() != NOOP) + if (!second_part_of_rmw) add_uninit_action_to_lists(curr); SnapVector * rf_set = NULL; @@ -711,15 +720,13 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) rf_set = build_may_read_from(curr); if (curr->is_read() && !second_part_of_rmw) { - bool success = process_read(curr, rf_set); + 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 && curr->get_type() != NOOP) + if (!second_part_of_rmw) add_action_to_lists(curr); if (curr->is_write()) @@ -739,42 +746,6 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) return curr; } -/** - * This is the strongest feasibility check available. - * @return whether the current trace (partial or complete) must be a prefix of - * a feasible trace. - */ -bool ModelExecution::isfeasibleprefix() const -{ - return !is_infeasible(); -} - -/** - * Print disagnostic information about an infeasible execution - * @param prefix A string to prefix the output with; if NULL, then a default - * message prefix will be provided - */ -void ModelExecution::print_infeasibility(const char *prefix) const -{ - char buf[100]; - char *ptr = buf; - if (priv->bad_synchronization) - ptr += sprintf(ptr, "[bad sw ordering]"); - if (ptr != buf) - model_print("%s: %s", prefix ? prefix : "Infeasible", buf); -} - -/** - * Check if the current partial trace is infeasible. Does not check any - * end-of-execution flags, which might rule out the execution. Thus, this is - * useful only for ruling an execution as infeasible. - * @return whether the current partial trace is infeasible. - */ -bool ModelExecution::is_infeasible() const -{ - return priv->bad_synchronization; -} - /** Close out a RMWR by converting previous RMWR into a RMW or READ. */ ModelAction * ModelExecution::process_rmw(ModelAction *act) { ModelAction *lastread = get_last_action(act->get_tid()); @@ -799,10 +770,14 @@ 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; @@ -855,7 +830,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 */ @@ -863,7 +839,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 */ @@ -871,7 +848,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; } } @@ -890,17 +868,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; } } } @@ -1127,16 +1108,15 @@ void ModelExecution::add_uninit_action_to_lists(ModelAction *act) int tid = id_to_int(act->get_tid()); ModelAction *uninit = NULL; int uninit_id = -1; - action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); - if (list->empty() && act->is_atomic_var()) { + SnapVector *objvec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); + if (objvec->empty() && act->is_atomic_var()) { uninit = get_uninitialized_action(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 ((int)vec->size() <= uninit_id) { int oldsize = (int) vec->size(); vec->resize(uninit_id + 1); - for(int i = oldsize; i < uninit_id + 1; i++) { + for(int i = oldsize;i < uninit_id + 1;i++) { new (&(*vec)[i]) action_list_t(); } } @@ -1152,7 +1132,7 @@ void ModelExecution::add_uninit_action_to_lists(ModelAction *act) 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++) + for(uint i = oldsize;i < priv->next_thread_id;i++) new (&(*vec)[i]) action_list_t(); } if (uninit) @@ -1176,8 +1156,10 @@ void ModelExecution::add_uninit_action_to_lists(ModelAction *act) 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); + if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) { + 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); @@ -1187,7 +1169,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act) 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++) + for(uint i = oldsize;i < priv->next_thread_id;i++) new (&(*vec)[i]) action_list_t(); } (*vec)[tid].push_back(act); @@ -1212,7 +1194,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act) 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++) + for(uint i = oldsize;i < priv->next_thread_id;i++) new (&(*vec)[i]) action_list_t(); } (*vec)[tid].push_back(act); @@ -1266,9 +1248,6 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act) int tid = id_to_int(act->get_tid()); insertIntoActionListAndSetCV(&action_trace, act); - action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); - insertIntoActionList(list, 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 (tid >= (int)vec->size()) { @@ -1585,13 +1564,11 @@ void ModelExecution::print_summary() #endif model_print("Execution trace %d:", get_execution_number()); - if (isfeasibleprefix()) { - if (scheduler->all_threads_sleeping()) - model_print(" SLEEP-SET REDUNDANT"); - if (have_bug_reports()) - model_print(" DETECTED BUG(S)"); - } else - print_infeasibility(" INFEASIBLE"); + if (scheduler->all_threads_sleeping()) + model_print(" SLEEP-SET REDUNDANT"); + if (have_bug_reports()) + model_print(" DETECTED BUG(S)"); + model_print("\n"); print_list(&action_trace);