From 11b3aba7be638c39ab0a5238883fc6bd688d86c5 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sat, 30 Jul 2022 16:04:23 +0200 Subject: [PATCH] Reduce the amount of MC locations reading the memory of the App We still read the remote memory, but (almost) only when creating a new State representing that state of the App. The goal is then to get those info through message passing instead of through memory reading. That should help reducing the bizarre things done by the MC, maybe allowing to run the App in valgrind or so. As a side effect, the exploration code becomes much more readable by using the info from the mc::State instead of invocking low-level things to retrive those info. --- src/mc/api/State.cpp | 42 +++++++++++++++++--------------- src/mc/api/State.hpp | 18 ++++++++------ src/mc/explo/DFSExplorer.cpp | 20 ++++++--------- src/mc/explo/LivenessChecker.cpp | 10 +++----- src/mc/mc_pattern.hpp | 22 ++++++++++++++--- 5 files changed, 64 insertions(+), 48 deletions(-) diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index fac456f4af..262e0108d6 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -15,10 +15,18 @@ namespace simgrid::mc { long State::expended_states_ = 0; -State::State() : num_(++expended_states_) +State::State(Session& session) : num_(++expended_states_) { - const unsigned long maxpid = Api::get().get_maxpid(); - actor_states_.resize(maxpid); + auto actors = mc_model_checker->get_remote_process().actors(); + + for (unsigned int i = 0; i < actors.size(); i++) { + auto remote_actor = actors[i].copy.get_buffer(); + aid_t aid = remote_actor->get_pid(); + + actor_states_.insert( + std::make_pair(aid, ActorState(aid, session.actor_is_enabled(aid), remote_actor->simcall_.mc_max_consider_))); + } + transition_.reset(new Transition()); /* Stateful model checking */ if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) { @@ -29,7 +37,7 @@ State::State() : num_(++expended_states_) std::size_t State::count_todo() const { - return boost::range::count_if(this->actor_states_, [](simgrid::mc::ActorState const& a) { return a.is_todo(); }); + return boost::range::count_if(this->actor_states_, [](auto& pair) { return pair.second.is_todo(); }); } Transition* State::get_transition() const @@ -37,34 +45,28 @@ Transition* State::get_transition() const return transition_.get(); } -int State::next_transition() const +aid_t State::next_transition() const { - std::vector& actors = mc_model_checker->get_remote_process().actors(); - XBT_DEBUG("Search for an actor to run. %zu actors to consider", actors.size()); - for (unsigned int i = 0; i < actors.size(); i++) { - /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application*/ - if (aid_t aid = actors[i].copy.get_buffer()->get_pid(); - not actor_states_[aid].is_todo() || not Api::get().get_session().actor_is_enabled(aid)) + XBT_DEBUG("Search for an actor to run. %zu actors to consider", actor_states_.size()); + for (auto const& [aid, actor] : actor_states_) { + /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */ + if (not actor.is_todo() || not actor.is_enabled()) continue; - return i; + return aid; } return -1; } -void State::execute_next(int next) +void State::execute_next(aid_t next) { - std::vector& actors = mc_model_checker->get_remote_process().actors(); - const kernel::actor::ActorImpl* actor = actors[next].copy.get_buffer(); - const aid_t aid = actor->get_pid(); - /* This actor is ready to be executed. Prepare its execution when simcall_handle will be called on it */ - const unsigned times_considered = actor_states_[aid].do_consider(actor->simcall_.mc_max_consider_); + const unsigned times_considered = actor_states_.at(next).do_consider(); - XBT_DEBUG("Let's run actor %ld (times_considered = %u)", aid, times_considered); + XBT_DEBUG("Let's run actor %ld (times_considered = %u)", next, times_considered); Transition::executed_transitions_++; - transition_.reset(mc_model_checker->handle_simcall(aid, times_considered, true)); + transition_.reset(mc_model_checker->handle_simcall(next, times_considered, true)); mc_model_checker->wait_for_requests(); } } // namespace simgrid::mc diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 84322067ad..93cb03638c 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -19,30 +19,34 @@ class XBT_PRIVATE State : public xbt::Extendable { /* Outgoing transition: what was the last transition that we took to leave this state? */ std::unique_ptr transition_; - /** Sequential state number (used for debugging) */ + /** Sequential state ID (used for debugging) */ long num_ = 0; /** State's exploration status by process */ - std::vector actor_states_; + std::map actor_states_; /** Snapshot of system state (if needed) */ std::shared_ptr system_state_; public: - explicit State(); + explicit State(Session& session); /* Returns a positive number if there is another transition to pick, or -1 if not */ - int next_transition() const; + aid_t next_transition() const; /* Explore a new path; the parameter must be the result of a previous call to next_transition() */ - void execute_next(int next); + void execute_next(aid_t next); long get_num() const { return num_; } std::size_t count_todo() const; - void mark_todo(aid_t actor) { this->actor_states_[actor].mark_todo(); } - bool is_done(aid_t actor) const { return this->actor_states_[actor].is_done(); } + void mark_todo(aid_t actor) { actor_states_.at(actor).mark_todo(); } + bool is_done(aid_t actor) const { return actor_states_.at(actor).is_done(); } Transition* get_transition() const; void set_transition(Transition* t) { transition_.reset(t); } + std::map const& get_actors_list() { return actor_states_; } + + int get_actor_count() { return actor_states_.size(); } + bool is_actor_enabled(int actor) { return actor_states_.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); } diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 900c40ea2f..64b095ed07 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -152,7 +152,7 @@ void DFSExplorer::run() req_str = state->get_transition()->dot_string(); /* Create the new expanded state (copy the state of MCed into our MCer data) */ - auto next_state = std::make_unique(); + auto next_state = std::make_unique(get_session()); on_state_creation_signal(next_state.get()); if (_sg_mc_termination) @@ -165,11 +165,9 @@ void DFSExplorer::run() /* 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 */ - auto actors = mc_model_checker->get_remote_process().actors(); - for (auto& remoteActor : actors) { - auto actor = remoteActor.copy.get_buffer(); - if (get_session().actor_is_enabled(actor->get_pid())) { - next_state->mark_todo(actor->get_pid()); + for (auto const& [aid, _] : next_state->get_actors_list()) { + if (next_state->is_actor_enabled(aid)) { + next_state->mark_todo(aid); if (reductionMode_ == ReductionMode::dpor) break; // With DPOR, we take the first enabled transition } @@ -291,16 +289,14 @@ DFSExplorer::DFSExplorer(Session* session) : Exploration(session) XBT_DEBUG("Starting the DFS exploration"); - auto initial_state = std::make_unique(); + auto initial_state = std::make_unique(get_session()); XBT_DEBUG("**************************************************"); /* Get an enabled actor and insert it in the interleave set of the initial state */ - auto actors = mc_model_checker->get_remote_process().actors(); - XBT_DEBUG("Initial state. %zu actors to consider", actors.size()); - for (auto& actor : actors) { - aid_t aid = actor.copy.get_buffer()->get_pid(); - if (get_session().actor_is_enabled(aid)) { + XBT_DEBUG("Initial state. %d actors to consider", initial_state->get_actor_count()); + for (auto const& [aid, _] : initial_state->get_actors_list()) { + if (initial_state->is_actor_enabled(aid)) { initial_state->mark_todo(aid); if (reductionMode_ == ReductionMode::dpor) { XBT_DEBUG("Actor %ld is TODO, DPOR is ON so let's go for this one.", aid); diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp index 0d7acc6b06..64d9f3635f 100644 --- a/src/mc/explo/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -224,18 +224,16 @@ std::shared_ptr LivenessChecker::create_pair(const Pair* current_pair, xbt ++expanded_pairs_count_; auto next_pair = std::make_shared(expanded_pairs_count_); next_pair->automaton_state = state; - next_pair->graph_state = std::make_shared(); + next_pair->graph_state = std::make_shared(get_session()); next_pair->atomic_propositions = std::move(propositions); if (current_pair) next_pair->depth = current_pair->depth + 1; else next_pair->depth = 1; /* Add all enabled actors to the interleave set of the initial state */ - for (auto& act : mc_model_checker->get_remote_process().actors()) { - auto actor = act.copy.get_buffer(); - if (get_session().actor_is_enabled(actor->get_pid())) - next_pair->graph_state->mark_todo(actor->get_pid()); - } + for (auto const& [aid, _] : next_pair->graph_state->get_actors_list()) + if (next_pair->graph_state->is_actor_enabled(aid)) + next_pair->graph_state->mark_todo(aid); next_pair->requests = next_pair->graph_state->count_todo(); /* FIXME : get search_cycle value for each accepting state */ diff --git a/src/mc/mc_pattern.hpp b/src/mc/mc_pattern.hpp index e29895cb9b..acb4d7c0ea 100644 --- a/src/mc/mc_pattern.hpp +++ b/src/mc/mc_pattern.hpp @@ -16,6 +16,7 @@ namespace simgrid::mc { * an actor cannot have more than one enabled transition at a given time. */ class ActorState { + /* Possible exploration status of an actor transition in a state. * Either the checker did not consider the transition, or it was considered and still to do, or considered and done. */ @@ -31,18 +32,33 @@ class ActorState { /** Exploration control information */ InterleavingType state_ = InterleavingType::disabled; - /** Number of times that the process was considered to be executed */ + aid_t aid_; + /** Number of times that the actor was considered to be executed in previous explorations of the state space */ unsigned int times_considered_ = 0; + /** Maximal amount of times that the actor can be considered for execution in this state. + * If times_considered==max_consider, we fully explored that part of the state space */ + unsigned int max_consider_ = 0; + + /** Whether that actor is initially enabled in this state */ + bool enabled_; public: - unsigned int do_consider(unsigned int max_consider) + ActorState(aid_t aid, bool enabled, unsigned int max_consider) + : aid_(aid), max_consider_(max_consider), enabled_(enabled) + { + } + + unsigned int do_consider() { - if (max_consider <= times_considered_ + 1) + if (max_consider_ <= times_considered_ + 1) set_done(); return times_considered_++; } unsigned int get_times_considered() const { return times_considered_; } + /* returns whether the actor is marked as enabled in the application side */ + bool is_enabled() const { return enabled_; } + /* returns whether the actor is marked as disabled by the exploration algorithm */ bool is_disabled() const { return this->state_ == InterleavingType::disabled; } bool is_done() const { return this->state_ == InterleavingType::done; } bool is_todo() const { return this->state_ == InterleavingType::todo; } -- 2.20.1