From: mlaurent Date: Tue, 7 Nov 2023 12:20:10 +0000 (+0100) Subject: Merge branch 'master' of https://framagit.org/simgrid/simgrid X-Git-Tag: v3.35~89 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/fa33c62c831c17237ac38960b24596560ad3804d?hp=-c Merge branch 'master' of https://framagit.org/simgrid/simgrid --- fa33c62c831c17237ac38960b24596560ad3804d diff --combined src/mc/api/State.cpp index 866a1d0400,fd60a3c599..aff9d5cb60 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@@ -25,6 -25,7 +25,6 @@@ State::State(RemoteApp& remote_app) : n { XBT_VERB("Creating a guide for the state"); - if (_sg_mc_strategy == "none") strategy_ = std::make_shared(); else if (_sg_mc_strategy == "max_match_comm") @@@ -32,19 -33,13 +32,12 @@@ else if (_sg_mc_strategy == "min_match_comm") strategy_ = std::make_shared(); else if (_sg_mc_strategy == "uniform") { - xbt::random::set_mersenne_seed(_sg_mc_random_seed); + xbt::random::set_mersenne_seed(_sg_mc_random_seed); strategy_ = std::make_shared(); - } - else + } else THROW_IMPOSSIBLE; remote_app.get_actors_status(strategy_->actors_to_run_); - - #if SIMGRID_HAVE_STATEFUL_MC - /* Stateful model checking */ - if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) - system_state_ = std::make_shared(num_, remote_app.get_page_store(), - *remote_app.get_remote_process_memory()); - #endif } State::State(RemoteApp& remote_app, std::shared_ptr parent_state) @@@ -56,7 -51,7 +49,7 @@@ strategy_ = std::make_shared(); else if (_sg_mc_strategy == "min_match_comm") strategy_ = std::make_shared(); - else if (_sg_mc_strategy == "uniform") + else if (_sg_mc_strategy == "uniform") strategy_ = std::make_shared(); else THROW_IMPOSSIBLE; @@@ -64,12 -59,6 +57,6 @@@ remote_app.get_actors_status(strategy_->actors_to_run_); - #if SIMGRID_HAVE_STATEFUL_MC /* Stateful model checking */ - if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) - system_state_ = std::make_shared(num_, remote_app.get_page_store(), - *remote_app.get_remote_process_memory()); - #endif - /* Copy the sleep set and eventually removes things from it: */ /* For each actor in the previous sleep set, keep it if it is not dependent with current transition. * And if we kept it and the actor is enabled in this state, mark the actor as already done, so that @@@ -212,9 -201,6 +199,9 @@@ void State::seed_wakeup_tree_if_needed( { // TODO: It would be better not to have such a flag. if (has_initialized_wakeup_tree) { + XBT_DEBUG("Reached a node with the following initialized WuT:"); + XBT_DEBUG("\n%s", wakeup_tree_.string_of_whole_tree().c_str()); + return; } // TODO: Note that the next action taken by the actor may be updated @@@ -240,11 -226,6 +227,11 @@@ void State::sprout_tree_from_parent_state() { + + XBT_DEBUG("Initializing Wut with parent one:"); + XBT_DEBUG("\n%s", parent_state_->wakeup_tree_.string_of_whole_tree().c_str()); + + xbt_assert(parent_state_ != nullptr, "Attempting to construct a wakeup tree for the root state " "(or what appears to be, rather for state without a parent defined)"); const auto min_process_node = parent_state_->wakeup_tree_.get_min_single_process_node(); @@@ -252,14 -233,18 +239,18 @@@ "parent with an empty wakeup tree. This indicates either that ODPOR " "actor selection in State.cpp is incorrect, or that the code " "deciding when to make subtrees in ODPOR is incorrect"); - xbt_assert((get_transition_in()->aid_ == min_process_node.value()->get_actor()) && - (get_transition_in()->type_ == min_process_node.value()->get_action()->type_), - "We tried to make a subtree from a parent state who claimed to have executed `%s` on actor %ld " - "but whose wakeup tree indicates it should have executed `%s` on actor %ld. This indicates " - "that exploration is not following ODPOR. Are you sure you're choosing actors " - "to schedule from the wakeup tree?", - get_transition_in()->to_string(false).c_str(), get_transition_in()->aid_, - min_process_node.value()->get_action()->to_string(false).c_str(), min_process_node.value()->get_actor()); + if (not(get_transition_in()->aid_ == min_process_node.value()->get_actor() && + get_transition_in()->type_ == min_process_node.value()->get_action()->type_)) { + XBT_ERROR("We tried to make a subtree from a parent state who claimed to have executed `%s` on actor %ld " + "but whose wakeup tree indicates it should have executed `%s` on actor %ld. This indicates " + "that exploration is not following ODPOR. Are you sure you're choosing actors " + "to schedule from the wakeup tree? Trace so far:", + get_transition_in()->to_string(false).c_str(), get_transition_in()->aid_, + min_process_node.value()->get_action()->to_string(false).c_str(), min_process_node.value()->get_actor()); + for (auto elm : Exploration::get_instance()->get_textual_trace()) + XBT_ERROR("%s", elm.c_str()); + xbt_abort(); + } this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value()); } diff --combined src/mc/api/State.hpp index f10d7bd51d,ca77b513a7..de11f78e88 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@@ -13,10 -13,6 +13,6 @@@ #include "src/mc/explo/odpor/WakeupTree.hpp" #include "src/mc/transition/Transition.hpp" - #if SIMGRID_HAVE_STATEFUL_MC - #include "src/mc/sosp/Snapshot.hpp" - #endif - namespace simgrid::mc { /* A node in the exploration graph (kind-of) */ @@@ -32,9 -28,6 +28,6 @@@ class XBT_PRIVATE State : public xbt::E /** Sequential state ID (used for debugging) */ long num_ = 0; - /** Snapshot of system state (if needed) */ - std::shared_ptr system_state_; - /** Unique parent of this state. Required both for sleep set computation and for guided model-checking */ std::shared_ptr parent_state_ = nullptr; @@@ -98,9 -91,6 +91,6 @@@ public unsigned long get_actor_count() const { return strategy_->actors_to_run_.size(); } bool is_actor_enabled(aid_t actor) const { return strategy_->actors_to_run_.at(actor).is_enabled(); } - Snapshot* get_system_state() const { return system_state_.get(); } - void set_system_state(std::shared_ptr state) { system_state_ = std::move(state); } - /** * @brief Computes the backtrack set for this state * according to its definition in SimGrid. @@@ -154,9 -144,7 +144,9 @@@ */ void remove_subtree_using_current_out_transition(); bool has_empty_tree() const { return this->wakeup_tree_.empty(); } + std::string string_of_wut() const { return this->wakeup_tree_.string_of_whole_tree(); } + /** * @brief */ diff --combined src/mc/explo/DFSExplorer.cpp index b23ce48938,ffa682f2da..f82d8da149 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@@ -10,11 -10,6 +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 +39,6 @@@ 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 +84,7 @@@ void DFSExplorer::log_state() // overri 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 +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 @@@ -210,7 -169,7 +169,7 @@@ // 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 +212,10 @@@ 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 +234,10 @@@ 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(); } @@@ -324,36 -287,18 +287,18 @@@ 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(); } @@@ -402,8 -347,6 +347,8 @@@ std::shared_ptr DFSExplorer::nex for (const auto& [aid, transition] : state->get_sleep_set()) XBT_DEBUG("\t <%ld,%s>", aid, transition->to_string().c_str()); 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; } } @@@ -432,12 -375,9 +377,12 @@@ void DFSExplorer::backtrack( 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: { @@@ -486,41 -426,16 +431,16 @@@ 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 */ @@@ -532,23 -447,9 +452,9 @@@ 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()); diff --combined src/mc/transition/TransitionSynchro.cpp index 21ea4ec8af,5e7ded2aed..bd5788665a --- a/src/mc/transition/TransitionSynchro.cpp +++ b/src/mc/transition/TransitionSynchro.cpp @@@ -32,7 -32,7 +32,7 @@@ bool BarrierTransition::depends(const T // Actions executed by the same actor are always dependent if (o->aid_ == aid_) return true; - + if (const auto* other = dynamic_cast(o)) { if (bar_ != other->bar_) return false; @@@ -128,7 -128,7 +128,11 @@@ bool SemaphoreTransition::depends(cons // Actions executed by the same actor are always dependent if (o->aid_ == aid_) return true; ++<<<<<<< HEAD + ++======= + ++>>>>>>> dfafe652e9ae62c35cd0fc084b117fc987b3e8dc if (const auto* other = dynamic_cast(o)) { if (sem_ != other->sem_) return false;