X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=7b8461226a8860d60a0311c2fa2538607c9b1363;hp=606b9642ebb6ba39bc50581df6c86f6d70bd61af;hb=da918c450a8fb8524ed99da0a35a7e417eb85777;hpb=e296778cb3574eeafdd20e0c25a4081c8d1ab0dc diff --git a/execution.cc b/execution.cc index 606b9642..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,8 +64,6 @@ 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 */ @@ -75,6 +71,9 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : add_thread(model_thread); fuzzer->register_engine(m->get_history(), this); scheduler->register_engine(this); +#ifdef TLS + pthread_key_create(&pthreadkey, tlsdestructor); +#endif } /** @brief Destructor */ @@ -185,22 +184,10 @@ void ModelExecution::wake_up_sleeping_actions(ModelAction *curr) } } -/** @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 */ @@ -282,7 +269,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()); + model->get_history()->process_action(act, act->get_tid()); return act; } @@ -302,19 +289,18 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * } // Remove writes that violate read modification order - /* - for (uint i = 0; i < rf_set->size(); i++) { + 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]; @@ -333,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(); @@ -664,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); @@ -733,12 +722,6 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (curr->is_read() && !second_part_of_rmw) { process_read(curr, rf_set); delete rf_set; - -/* 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); @@ -763,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()); @@ -830,7 +777,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) { */ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, - SnapVector * priorset, bool * canprune, bool check_only) + SnapVector * priorset, bool * canprune, bool check_only) { SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; @@ -1161,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(); } } @@ -1186,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) @@ -1210,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); @@ -1221,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); @@ -1246,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); @@ -1300,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()) { @@ -1619,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); @@ -1758,7 +1701,7 @@ Thread * ModelExecution::take_step(ModelAction *curr) ASSERT(curr); /* Process this action in ModelHistory for records */ -// model->get_history()->process_action( curr, curr->get_tid() ); + model->get_history()->process_action( curr, curr->get_tid() ); if (curr_thrd->is_blocked() || curr_thrd->is_complete()) scheduler->remove_thread(curr_thrd);