X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/3d2dd6e7d47e6483839df0159c1329a22d3f8fb1..ff4bc56d5d0d4b1bf3e5c83e5af51ac3cc119789:/src/mc/explo/DFSExplorer.cpp diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 80bd80481a..6fe0b46ab4 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -10,11 +10,6 @@ #include "src/mc/mc_record.hpp" #include "src/mc/transition/Transition.hpp" -#if SIMGRID_HAVE_STATEFUL_MC -#include "src/mc/VisitedState.hpp" -#endif - -#include "src/xbt/mmalloc/mmprivate.h" #include "xbt/log.h" #include "xbt/string.hpp" #include "xbt/sysdep.h" @@ -44,30 +39,6 @@ xbt::signal DFSExplorer::on_transition_execute_si xbt::signal DFSExplorer::on_log_state_signal; -void DFSExplorer::check_non_termination(const State* current_state) -{ -#if SIMGRID_HAVE_STATEFUL_MC - for (auto const& state : stack_) { - if (state->get_system_state()->equals_to(*current_state->get_system_state(), - *get_remote_app().get_remote_process_memory())) { - XBT_INFO("Non-progressive cycle: state %ld -> state %ld", state->get_num(), current_state->get_num()); - XBT_INFO("******************************************"); - XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***"); - XBT_INFO("******************************************"); - XBT_INFO("Counter-example execution trace:"); - for (auto const& s : get_textual_trace()) - XBT_INFO(" %s", s.c_str()); - XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with " - "--cfg=model-check/replay:'%s'", - get_record_trace().to_string().c_str()); - log_state(); - - throw McError(ExitStatus::NON_TERMINATION); - } - } -#endif -} - RecordTrace DFSExplorer::get_record_trace() // override { RecordTrace res; @@ -113,7 +84,7 @@ void DFSExplorer::log_state() // override XBT_INFO("DFS exploration ended. %ld unique states visited; %lu backtracks (%lu transition replays, %lu states " "visited overall)", State::get_expanded_states(), backtrack_count_, Transition::get_replayed_transitions(), - visited_states_count_); + visited_states_count_); Exploration::log_state(); } @@ -152,18 +123,6 @@ void DFSExplorer::run() continue; } -#if SIMGRID_HAVE_STATEFUL_MC - // Backtrack if we are revisiting a state we saw previously while applying state-equality reduction - if (visited_state_ != nullptr) { - XBT_DEBUG("State already visited (equal to state %ld), exploration stopped on this path.", - visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_); - - visited_state_ = nullptr; - this->backtrack(); - continue; - } -#endif - if (reduction_mode_ == ReductionMode::odpor) { // In the case of ODPOR, the wakeup tree for this // state may be empty if we're exploring new territory @@ -205,12 +164,12 @@ void DFSExplorer::run() } /* Actually answer the request: let's execute the selected request (MCed does one step) */ - const auto executed_transition = state->execute_next(next, get_remote_app()); + auto executed_transition = state->execute_next(next, get_remote_app()); on_transition_execute_signal(state->get_transition_out().get(), get_remote_app()); // If there are processes to interleave and the maximum depth has not been // reached then perform one step of the exploration algorithm. - XBT_VERB("Execute %ld: %.60s (stack depth: %zu, state: %ld, %zu interleaves)", state->get_transition_out()->aid_, + XBT_VERB("Execute %ld: %.150s (stack depth: %zu, state: %ld, %zu interleaves)", state->get_transition_out()->aid_, state->get_transition_out()->to_string().c_str(), stack_.size(), state->get_num(), state->count_todo()); /* Create the new expanded state (copy the state of MCed into our MCer data) */ @@ -253,8 +212,10 @@ void DFSExplorer::run() continue; } else if (prev_state->get_transition_out()->depends(state->get_transition_out().get())) { XBT_VERB("Dependent Transitions:"); - XBT_VERB(" %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num()); - XBT_VERB(" %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num()); + XBT_VERB(" #%ld %s (state=%ld)", prev_state->get_transition_out()->aid_, + prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num()); + XBT_VERB(" #%ld %s (state=%ld)", state->get_transition_out()->aid_, + state->get_transition_out()->to_string().c_str(), state->get_num()); if (prev_state->is_actor_enabled(issuer_id)) { if (not prev_state->is_actor_done(issuer_id)) { @@ -273,8 +234,10 @@ void DFSExplorer::run() break; } else { XBT_VERB("INDEPENDENT Transitions:"); - XBT_VERB(" %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num()); - XBT_VERB(" %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num()); + XBT_VERB(" #%ld %s (state=%ld)", prev_state->get_transition_out()->aid_, + prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num()); + XBT_VERB(" #%ld %s (state=%ld)", state->get_transition_out()->aid_, + state->get_transition_out()->to_string().c_str(), state->get_num()); } tmp_stack.pop_back(); } @@ -300,7 +263,7 @@ void DFSExplorer::run() 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()) { + if (not 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 @@ -324,36 +287,18 @@ void DFSExplorer::run() if (stack_.back()->count_todo_multiples() > 0) opened_states_.emplace_back(stack_.back()); - if (_sg_mc_termination) - this->check_non_termination(next_state.get()); - -#if SIMGRID_HAVE_STATEFUL_MC - /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) - */ - if (_sg_mc_max_visited_states > 0) - visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get(), get_remote_app()); -#endif - stack_.emplace_back(std::move(next_state)); /* If this is a new state (or if we don't care about state-equality reduction) */ - if (visited_state_ == nullptr) { - /* Get an enabled process and insert it in the interleave set of the next state */ - if (reduction_mode_ == ReductionMode::dpor) - stack_.back()->consider_best(); // Take only one transition if DPOR: others may be considered later if required - else { - stack_.back()->consider_all(); - } - - dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), stack_.back()->get_num(), - state->get_transition_out()->dot_string().c_str()); -#if SIMGRID_HAVE_STATEFUL_MC - } else { - dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), - visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_, - state->get_transition_out()->dot_string().c_str()); -#endif + /* Get an enabled process and insert it in the interleave set of the next state */ + if (reduction_mode_ == ReductionMode::dpor) + stack_.back()->consider_best(); // Take only one transition if DPOR: others may be considered later if required + else { + stack_.back()->consider_all(); } + + dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), stack_.back()->get_num(), + state->get_transition_out()->dot_string().c_str()); } log_state(); } @@ -401,7 +346,9 @@ std::shared_ptr DFSExplorer::next_odpor_state() XBT_DEBUG("\tPerformed ODPOR 'clean-up'. Sleep set has:"); for (const auto& [aid, transition] : state->get_sleep_set()) XBT_DEBUG("\t <%ld,%s>", aid, transition->to_string().c_str()); - if (!state->has_empty_tree()) { + if (not state->has_empty_tree()) { + XBT_DEBUG("\t found the following non-empty WuT:\n" + "%s", state->string_of_wut().c_str()); return state; } } @@ -424,15 +371,19 @@ void DFSExplorer::backtrack() * relation) */ 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: Now considering all possible race with `%u`", 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()) { switch (prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e))) { 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); + XBT_DEBUG("ODPOR: Reversible race with `%u`(%ld: %.20s) unaccounted for in the wakeup tree for " + "the execution prior to event `%u`(%ld: %.20s):", + e_prime, stack_[e_prime]->get_transition_out()->aid_, + stack_[e_prime]->get_transition_out()->to_string(true).c_str(), e, + prev_state.get_transition_out()->aid_, + prev_state.get_transition_out()->to_string(true).c_str()); break; } case odpor::WakeupTree::InsertionResult::interior_node: { @@ -481,41 +432,16 @@ void DFSExplorer::backtrack() backtrack_count_++; XBT_DEBUG("Backtracking to state#%ld", backtracking_point->get_num()); -#if SIMGRID_HAVE_STATEFUL_MC - /* If asked to rollback on a state that has a snapshot, restore it */ - if (const auto* system_state = backtracking_point->get_system_state()) { - system_state->restore(*get_remote_app().get_remote_process_memory()); - on_restore_system_state_signal(backtracking_point.get(), get_remote_app()); - this->restore_stack(backtracking_point); - return; - } -#endif - // Search how to restore the backtracking point - State* init_state = nullptr; std::deque replay_recipe; for (auto* s = backtracking_point.get(); s != nullptr; s = s->get_parent_state().get()) { -#if SIMGRID_HAVE_STATEFUL_MC - if (s->get_system_state() != nullptr) { // Found a state that I can restore - init_state = s; - break; - } -#endif if (s->get_transition_in() != nullptr) // The root has no transition_in replay_recipe.push_front(s->get_transition_in().get()); } - // Restore the init_state, if any - if (init_state != nullptr) { -#if SIMGRID_HAVE_STATEFUL_MC - const auto* system_state = init_state->get_system_state(); - system_state->restore(*get_remote_app().get_remote_process_memory()); - on_restore_system_state_signal(init_state, get_remote_app()); -#endif - } else { // Restore the initial state if no intermediate state was found - get_remote_app().restore_initial_state(); - on_restore_initial_state_signal(get_remote_app()); - } + // Restore the initial state if no intermediate state was found + get_remote_app().restore_initial_state(); + on_restore_initial_state_signal(get_remote_app()); /* if no snapshot, we need to restore the initial state and replay the transitions */ /* Traverse the stack from the state at position start and re-execute the transitions */ @@ -527,23 +453,9 @@ void DFSExplorer::backtrack() this->restore_stack(backtracking_point); } -DFSExplorer::DFSExplorer(const std::vector& args, ReductionMode mode, bool need_memory_info) - : Exploration(args, need_memory_info || _sg_mc_termination -#if SIMGRID_HAVE_STATEFUL_MC - || _sg_mc_checkpoint > 0 -#endif - ) - , reduction_mode_(mode) +DFSExplorer::DFSExplorer(const std::vector& args, ReductionMode mode) : Exploration(args), reduction_mode_(mode) { - if (_sg_mc_termination) { - if (mode != ReductionMode::none) { - XBT_INFO("Check non progressive cycles (turning DPOR off)"); - reduction_mode_ = ReductionMode::none; - } else { - XBT_INFO("Check non progressive cycles"); - } - } else - XBT_INFO("Start a DFS exploration. Reduction is: %s.", to_c_str(reduction_mode_)); + XBT_INFO("Start a DFS exploration. Reduction is: %s.", to_c_str(reduction_mode_)); auto initial_state = std::make_shared(get_remote_app());