X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/7fd6faa16a89c1019a9fe562be79942add51842e..976687c46605cb7f3513a3f9549ef43f737e4b7d:/src/mc/explo/DFSExplorer.cpp diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 849055bd41..2c72764301 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -84,6 +84,7 @@ RecordTrace DFSExplorer::get_record_trace() // override void DFSExplorer::restore_stack(std::shared_ptr state) { stack_.clear(); + execution_seq_ = odpor::Execution(); auto current_state = state; stack_.emplace_front(current_state); // condition corresponds to reaching initial state @@ -92,22 +93,18 @@ void DFSExplorer::restore_stack(std::shared_ptr state) stack_.emplace_front(current_state); } XBT_DEBUG("Replaced stack by %s", get_record_trace().to_string().c_str()); - if (reduction_mode_ == ReductionMode::sdpor || reduction_mode_ == ReductionMode::odpor) { - execution_seq_ = odpor::Execution(); - // NOTE: The outgoing transition for the top-most // state of the stack refers to that which was taken // as part of the last trace explored by the algorithm. // Thus, only the sequence of transitions leading up to, // but not including, the last state must be included // when reconstructing the Exploration for SDPOR. - for (auto iter = stack_.begin(); iter != stack_.end() - 1 and iter != stack_.end(); ++iter) { - const auto& state = *(iter); - execution_seq_.push_transition(state->get_transition_out().get()); + for (auto iter = std::next(stack_.begin()); iter != stack_.end(); ++iter) { + execution_seq_.push_transition((*iter)->get_transition_in()); } + XBT_DEBUG("Replaced SDPOR/ODPOR execution to reflect the new stack"); } - XBT_DEBUG("Additionally replaced corresponding SDPOR execution stack"); } void DFSExplorer::log_state() // override @@ -147,7 +144,7 @@ void DFSExplorer::run() XBT_ERROR("/!\\ Max depth of %d reached! THIS **WILL** BREAK the reduction, which is not sound " "when stopping at a fixed depth /!\\", _sg_mc_max_depth.get()); - XBT_ERROR("/!\\ If bad things happen, disable dpor with --cfg=model-check/reduction:none /!\\"); + XBT_ERROR("/!\\ If bad things happen, disable the reduction with --cfg=model-check/reduction:none /!\\"); } else { XBT_WARN("/!\\ Max depth reached ! /!\\ "); } @@ -173,6 +170,11 @@ void DFSExplorer::run() // (rather than following the partial execution of a // wakeup tree). This corresponds to lines 9 to 13 of // the ODPOR pseudocode + // + // INVARIANT: The execution sequence should be consistent + // with the state when seeding the tree. If the sequence + // gets out of sync with the state, selection will not + // work as we intend state->seed_wakeup_tree_if_needed(execution_seq_); } @@ -199,7 +201,7 @@ void DFSExplorer::run() if (_sg_mc_sleep_set && XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_verbose)) { XBT_VERB("Sleep set actually containing:"); for (auto& [aid, transition] : state->get_sleep_set()) - XBT_VERB(" <%ld,%s>", aid, transition.to_string().c_str()); + XBT_VERB(" <%ld,%s>", aid, transition->to_string().c_str()); } /* Actually answer the request: let's execute the selected request (MCed does one step) */ @@ -215,29 +217,24 @@ void DFSExplorer::run() auto next_state = std::make_shared(get_remote_app(), state); on_state_creation_signal(next_state.get(), get_remote_app()); - /* Sleep set procedure: - * adding the taken transition to the sleep set of the original state. - * Since the parent sleep set is used to compute the child sleep set, this need to be - * done after next_state creation */ - XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set", - state->get_transition_out()->to_string().c_str(), state->get_transition_out()->aid_); - state->add_sleep_set(state->get_transition_out()); // Actors are marked done when they are considered in ActorState - if (reduction_mode_ == ReductionMode::odpor) { - // With ODPOR, after taking a step forward, we must: - // 1. remove the subtree whose root is a single-process - // node of actor `next` (viz. the action we took) from - // the wakeup tree of `state` + // With ODPOR, after taking a step forward, we must + // assign a copy of that subtree to the next state. // - // 2. assign a copy of that subtree to the next state - // - // The latter evidently must be done BEFORE the former + // NOTE: We only add actions to the sleep set AFTER + // we've regenerated states. We must perform the search + // fully down a single path before we consider adding + // any elements to the sleep set according to the pseudocode next_state->sprout_tree_from_parent_state(); - state->remove_subtree_starting_with(next); - - // TODO: Consider what we have to do to handle transitions - // with multiple possible executions. We probably have to re-insert - // something into `state` and make note of that for later (opened_states_) + } else { + /* Sleep set procedure: + * adding the taken transition to the sleep set of the original state. + * Since the parent sleep set is used to compute the child sleep set, this need to be + * done after next_state creation */ + XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set", + state->get_transition_out()->to_string().c_str(), state->get_transition_out()->aid_); + state->add_sleep_set( + state->get_transition_out()); // Actors are marked done when they are considered in ActorState } /* DPOR persistent set procedure: @@ -295,44 +292,31 @@ void DFSExplorer::run() * The intuition is that some subsequence of `v` may enable `p`, so * we want to be sure that search "in that direction" */ - execution_seq_.push_transition(executed_transition.get()); + execution_seq_.push_transition(std::move(executed_transition)); + xbt_assert(execution_seq_.get_latest_event_handle().has_value(), "No events are contained in the SDPOR execution " + "even though one was just added"); - xbt_assert(execution_seq_.get_latest_event_handle().has_value(), - "No events are contained in the SDPOR/OPDPOR execution " - "even though one was just added"); - const aid_t p = executed_transition->aid_; const auto next_E_p = execution_seq_.get_latest_event_handle().value(); - - for (const auto racing_event_handle : execution_seq_.get_racing_events_of(next_E_p)) { - // To determine if the race is reversible, we have to ensure - // that actor `p` running `next_E_p` (viz. the event such that - // `racing_event -> (E_p) next_E_p` and no other event - // "happens-between" the two) is enabled in any equivalent - // execution where `racing_event` happens before `next_E_p`. - // - // Importantly, it is equivalent to checking if in ANY - // such equivalent execution sequence where `racing_event` - // happens-before `next_E_p` that `p` is enabled in `pre(racing_event, E.p)`. - // Thus it suffices to check THIS execution - // - // If the actor `p` is not enabled at s_[E'], it is not a *reversible* race - const std::shared_ptr prev_state = stack_[racing_event_handle]; - if (prev_state->is_actor_enabled(p)) { + for (const auto e_race : execution_seq_.get_reversible_races_of(next_E_p)) { + State* prev_state = stack_[e_race].get(); + const auto choices = execution_seq_.get_missing_source_set_actors_from(e_race, prev_state->get_backtrack_set()); + if (!choices.empty()) { // NOTE: To incorporate the idea of attempting to select the "best" // backtrack point into SDPOR, instead of selecting the `first` initial, // we should instead compute all choices and decide which is best - const std::optional q = - execution_seq_.get_first_sdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set()); - if (q.has_value()) { - prev_state->consider_one(q.value()); - opened_states_.emplace_back(std::move(prev_state)); - } + // + // Here, we choose the actor with the lowest ID to ensure + // we get deterministic results + const auto q = + std::min_element(choices.begin(), choices.end(), [](const aid_t a1, const aid_t a2) { return a1 < a2; }); + prev_state->consider_one(*q); + opened_states_.emplace_back(std::move(prev_state)); } } } else if (reduction_mode_ == ReductionMode::odpor) { // In the case of ODPOR, we simply observe the transition that was executed // until we've reached a maximal trace - execution_seq_.push_transition(executed_transition.get()); + execution_seq_.push_transition(std::move(executed_transition)); } // Before leaving that state, if the transition we just took can be taken multiple times, we @@ -409,6 +393,21 @@ std::shared_ptr DFSExplorer::best_opened_state() return best_state; } +std::shared_ptr DFSExplorer::next_odpor_state() +{ + for (auto iter = stack_.rbegin(); iter != stack_.rend(); ++iter) { + const auto& state = *iter; + state->do_odpor_unwind(); + XBT_DEBUG("\tPerformed ODPOR 'clean-up'. Sleep set has:"); + for (auto& [aid, transition] : state->get_sleep_set()) + XBT_DEBUG("\t <%ld,%s>", aid, transition->to_string().c_str()); + if (!state->has_empty_tree()) { + return state; + } + } + return nullptr; +} + void DFSExplorer::backtrack() { if (const auto last_event = execution_seq_.get_latest_event_handle(); @@ -424,28 +423,40 @@ void DFSExplorer::backtrack() * an as equivalent to `C` ("eventually looks like C", viz. the `~_E` * relation) */ - for (auto e_prime = static_cast(0); e_prime <= last_event; e_prime++) { - for (const auto e : execution_seq_.get_racing_events_of(e_prime)) { - // To determine if the race is reversible, we have to ensure - // that actor `p` running `e_i` (viz. the event such that - // `racing_event -> (E_p) e_i` and no other event - // "happens-between" the two) is enabled in any equivalent - // execution where `racing_event` happens before `e_i`. - // - // Importantly, it is equivalent to checking if in ANY - // such equivalent execution sequence where `racing_event` - // happens-before `next_E_p` that `p` is enabled in `pre(racing_event, E.p)`. - // Thus it suffices to check THIS execution - // - // If the actor `p` is not enabled at s_[E'], it is not a *reversible* race - const aid_t p = execution_seq_.get_actor_with_handle(e_prime); - const std::shared_ptr prev_state = stack_[e]; - if (prev_state->is_actor_enabled(p)) { - const std::optional v = execution_seq_.get_odpor_extension_from( - e, e_prime, prev_state->get_sleeping_set(), prev_state->get_enabled_actors()); - if (v.has_value()) { - prev_state->mark_path_interesting_for_odpor(v.value(), execution_seq_.get_prefix_before(e)); + for (auto e_prime = static_cast(0); e_prime <= last_event.value(); ++e_prime) { + for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) { + XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime); + State& prev_state = *stack_[e]; + if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) { + const auto result = prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e)); + switch (result) { + case odpor::WakeupTree::InsertionResult::root: { + XBT_DEBUG("ODPOR: Reversible race with `%u` unaccounted for in the wakeup tree for " + "the execution prior to event `%u`:", + e_prime, e); + break; + } + case odpor::WakeupTree::InsertionResult::interior_node: { + XBT_DEBUG("ODPOR: Reversible race with `%u` partially accounted for in the wakeup tree for " + "the execution prior to event `%u`:", + e_prime, e); + break; + } + case odpor::WakeupTree::InsertionResult::leaf: { + XBT_DEBUG("ODPOR: Reversible race with `%u` accounted for in the wakeup tree for " + "the execution prior to event `%u`:", + e_prime, e); + break; + } } + for (const auto& seq : simgrid::mc::odpor::get_textual_trace(v.value())) { + XBT_DEBUG(" %s", seq.c_str()); + } + } else { + XBT_DEBUG("ODPOR: Ignoring race: `sleep(E')` intersects `WI_[E'](v := notdep(%u, E))`", e); + XBT_DEBUG("Sleep set contains:"); + for (auto& [aid, transition] : prev_state.get_sleep_set()) + XBT_DEBUG(" <%ld,%s>", aid, transition->to_string().c_str()); } } } @@ -458,7 +469,7 @@ void DFSExplorer::backtrack() get_remote_app().check_deadlock(); // Take the point with smallest distance - auto backtracking_point = best_opened_state(); + auto backtracking_point = reduction_mode_ == ReductionMode::odpor ? next_odpor_state() : best_opened_state(); // if no backtracking point, then set the stack_ to empty so we can end the exploration if (not backtracking_point) { @@ -550,6 +561,14 @@ DFSExplorer::DFSExplorer(const std::vector& args, ReductionMode mode, boo } if (stack_.back()->count_todo_multiples() > 1) opened_states_.emplace_back(stack_.back()); + + if (mode == ReductionMode::odpor && !_sg_mc_sleep_set) { + // ODPOR requires the use of sleep sets; SDPOR + // "likes" using sleep sets but it is not strictly + // required + XBT_INFO("Forcing the use of sleep sets for use with ODPOR"); + _sg_mc_sleep_set = true; + } } Exploration* create_dfs_exploration(const std::vector& args, ReductionMode mode)