From 59a2292cca5e121a5db0c933112d4c421ded712a Mon Sep 17 00:00:00 2001 From: mlaurent Date: Sat, 18 Mar 2023 11:14:35 +0100 Subject: [PATCH] Add GuidedState abstract class; move ActorState management --- src/mc/api/State.cpp | 60 +++++++++++++++++--------------- src/mc/api/State.hpp | 28 ++++++++------- src/mc/api/guide/BasicGuide.hpp | 21 +++++++++++ src/mc/api/guide/GuidedState.hpp | 24 +++++++++++++ 4 files changed, 91 insertions(+), 42 deletions(-) create mode 100644 src/mc/api/guide/BasicGuide.hpp create mode 100644 src/mc/api/guide/GuidedState.hpp diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 90045f501b..ba6c78784d 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -4,6 +4,7 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/api/State.hpp" +#include "src/mc/api/guide/BasicGuide.hpp" #include "src/mc/explo/Exploration.hpp" #include "src/mc/mc_config.hpp" @@ -15,9 +16,9 @@ namespace simgrid::mc { long State::expended_states_ = 0; -State::State(RemoteApp& remote_app) : num_(++expended_states_) +State::State(RemoteApp& remote_app) : num_(++expended_states_), guide(std::make_unique()) { - remote_app.get_actors_status(actors_to_run_); + remote_app.get_actors_status(guide->actors_to_run_); /* Stateful model checking */ if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) @@ -26,48 +27,47 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_) } State::State(RemoteApp& remote_app, const State* parent_state) - : num_(++expended_states_), parent_state_(parent_state) + : num_(++expended_states_), parent_state_(parent_state), guide(std::make_unique()) { - remote_app.get_actors_status(actors_to_run_); + remote_app.get_actors_status(guide->actors_to_run_); /* 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()); - - /* If we want sleep set reduction, copy the sleep set and eventually removes things from it */ - if (_sg_mc_sleep_set) { - /* 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 - * it is not explored*/ - for (auto& [aid, transition] : parent_state_->get_sleep_set()) { - - if (not parent_state_->get_transition()->depends(&transition)) { - - sleep_set_.emplace(aid, transition); - if (actors_to_run_.count(aid) != 0) { - XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid); - - actors_to_run_.at(aid).mark_done(); - } - } else - XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with >>%s<<", - transition.to_string().c_str(), parent_state_->get_transition()->to_string().c_str()); - } + /* If we want sleep set reduction, copy the sleep set and eventually removes things from it */ + if (_sg_mc_sleep_set) { + /* 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 + * it is not explored*/ + for (auto& [aid, transition] : parent_state_->get_sleep_set()) { + + if (not parent_state_->get_transition()->depends(&transition)) { + + sleep_set_.emplace(aid, transition); + if (guide->actors_to_run_.count(aid) != 0) { + XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid); + + guide->actors_to_run_.at(aid).mark_done(); + } + } else + XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with >>%s<<", + transition.to_string().c_str(), parent_state_->get_transition()->to_string().c_str()); + } } } std::size_t State::count_todo() const { - return boost::range::count_if(this->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); }); + return boost::range::count_if(this->guide->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); }); } void State::mark_all_enabled_todo() { for (auto const& [aid, _] : this->get_actors_list()) { - if (this->is_actor_enabled(aid) and not is_actor_done(aid)) { + if (this->is_actor_enabled(aid) and not is_actor_done(aid)) { this->mark_todo(aid); } } @@ -78,10 +78,11 @@ Transition* State::get_transition() const return transition_; } +// This should be intierely done in GuidedState aid_t State::next_transition() const { - XBT_DEBUG("Search for an actor to run. %zu actors to consider", actors_to_run_.size()); - for (auto const& [aid, actor] : actors_to_run_) { + XBT_DEBUG("Search for an actor to run. %zu actors to consider", guide->actors_to_run_.size()); + for (auto const& [aid, actor] : guide->actors_to_run_) { /* 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() || actor.is_done()) { @@ -102,13 +103,14 @@ aid_t State::next_transition() const return -1; } +// This should be done in GuidedState, or at least interact with it void State::execute_next(aid_t next, RemoteApp& app) { // This actor is ready to be executed. Execution involves three phases: // 1. Identify the appropriate ActorState to prepare for execution // when simcall_handle will be called on it - auto& actor_state = actors_to_run_.at(next); + auto& actor_state = guide->actors_to_run_.at(next); const unsigned times_considered = actor_state.do_consider(); const auto* expected_executed_transition = actor_state.get_transition(times_considered); xbt_assert(expected_executed_transition != nullptr, diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 2f4407fb3a..a9dd2c43d0 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -8,6 +8,7 @@ #include "src/mc/api/ActorState.hpp" #include "src/mc/api/RemoteApp.hpp" +#include "src/mc/api/guide/GuidedState.hpp" #include "src/mc/sosp/Snapshot.hpp" #include "src/mc/transition/Transition.hpp" @@ -35,22 +36,20 @@ class XBT_PRIVATE State : public xbt::Extendable { /** Sequential state ID (used for debugging) */ long num_ = 0; - /** State's exploration status by actor. Not all the actors are there, only the ones that are ready-to-run in this - * state */ - std::map actors_to_run_; - /** 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 */ const State* parent_state_; - + + std::unique_ptr guide; + /* Sleep sets are composed of the actor and the corresponding transition that made it being added to the sleep * set. With this information, it is check whether it should be removed from it or not when exploring a new * transition */ std::map sleep_set_; - + public: explicit State(RemoteApp& remote_app); explicit State(RemoteApp& remote_app, const State* parent_state); @@ -63,22 +62,25 @@ public: long get_num() const { return num_; } std::size_t count_todo() const; - void mark_todo(aid_t actor) { actors_to_run_.at(actor).mark_todo(); } + void mark_todo(aid_t actor) { guide->actors_to_run_.at(actor).mark_todo(); } void mark_all_enabled_todo(); - bool is_actor_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); } + bool is_actor_done(aid_t actor) const { return guide->actors_to_run_.at(actor).is_done(); } Transition* get_transition() const; void set_transition(Transition* t) { transition_ = t; } - std::map const& get_actors_list() const { return actors_to_run_; } + std::map const& get_actors_list() const { return guide->actors_to_run_; } - unsigned long get_actor_count() const { return actors_to_run_.size(); } - bool is_actor_enabled(aid_t actor) { return actors_to_run_.at(actor).is_enabled(); } + unsigned long get_actor_count() const { return guide->actors_to_run_.size(); } + bool is_actor_enabled(aid_t actor) { return guide->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); } std::map const& get_sleep_set() const { return sleep_set_; } - void add_sleep_set(Transition* t) {sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); } - + void add_sleep_set(Transition* t) + { + sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); + } + /* Returns the total amount of states created so far (for statistics) */ static long get_expanded_states() { return expended_states_; } }; diff --git a/src/mc/api/guide/BasicGuide.hpp b/src/mc/api/guide/BasicGuide.hpp new file mode 100644 index 0000000000..631db3360b --- /dev/null +++ b/src/mc/api/guide/BasicGuide.hpp @@ -0,0 +1,21 @@ +/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_BASICGUIDE_HPP +#define SIMGRID_MC_BASICGUIDE_HPP + +namespace simgrid::mc { + +/** Basic MC guiding class which corresponds to no guide at all (random choice) */ +// Not Yet fully implemented +class BasicGuide : public GuidedState { +public: + std::pair next_transition() const override { return std::make_pair(0, 0); } + virtual void execute_next(aid_t aid) override { return; } +}; + +} // namespace simgrid::mc + +#endif diff --git a/src/mc/api/guide/GuidedState.hpp b/src/mc/api/guide/GuidedState.hpp new file mode 100644 index 0000000000..81dc19bd74 --- /dev/null +++ b/src/mc/api/guide/GuidedState.hpp @@ -0,0 +1,24 @@ +/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_GUIDEDSTATE_HPP +#define SIMGRID_MC_GUIDEDSTATE_HPP + +namespace simgrid::mc { + +class GuidedState { + /** State's exploration status by actor. Not all the actors are there, only the ones that are ready-to-run in this + * state */ + std::map actors_to_run_; + +public: + virtual std::pair next_transition() const = 0; + virtual void execute_next(aid_t aid) = 0; + friend class State; +}; + +} // namespace simgrid::mc + +#endif -- 2.20.1