X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=7b8461226a8860d60a0311c2fa2538607c9b1363;hp=e285156fd15d1526d2492006354fd7527535df06;hb=da918c450a8fb8524ed99da0a35a7e417eb85777;hpb=cd6a138fadb0cf3e886fa1407a3d571578b60cbe diff --git a/execution.cc b/execution.cc index e285156f..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; @@ -178,28 +178,16 @@ void ModelExecution::wake_up_sleeping_actions(ModelAction *curr) /* Remove this thread from sleep set */ scheduler->remove_sleep(thr); if (thr->get_pending()->is_sleep()) - thr->set_pending(NULL); + 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 */ @@ -301,18 +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]; @@ -331,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(); @@ -662,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); @@ -731,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); @@ -761,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()); @@ -821,12 +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 Only check if the current action satisfies read - * modification order or not, without modifiying priorsetand canprune + * @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 check_only) +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; @@ -1157,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(); } } @@ -1182,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) @@ -1206,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); @@ -1217,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); @@ -1242,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); @@ -1296,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()) { @@ -1615,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);