From: mlaurent Date: Mon, 20 Feb 2023 09:41:27 +0000 (+0100) Subject: Merge branch 'master' of https://framagit.org/simgrid/simgrid X-Git-Tag: v3.34~436^2~5 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/8c6bbb14f44b8daed5ea43d80880c6bf2155118b?hp=-c Merge branch 'master' of https://framagit.org/simgrid/simgrid --- 8c6bbb14f44b8daed5ea43d80880c6bf2155118b diff --combined src/mc/api/ActorState.hpp index 7f3bc11ec2,6af8bccbdd..495cf0eb47 --- a/src/mc/api/ActorState.hpp +++ b/src/mc/api/ActorState.hpp @@@ -26,7 -26,6 +26,6 @@@ namespace simgrid::mc * is important in cases */ class ActorState { - /** * @brief The transitions that the actor is allowed to execute from this * state, viz. those that are enabled for this actor @@@ -95,7 -94,7 +94,7 @@@ public unsigned int do_consider() { if (max_consider_ <= times_considered_ + 1) - set_done(); + mark_done(); return times_considered_++; } unsigned int get_times_considered() const { return times_considered_; } @@@ -113,7 -112,7 +112,7 @@@ this->state_ = InterleavingType::todo; this->times_considered_ = 0; } - void set_done() { this->state_ = InterleavingType::done; } + void mark_done() { this->state_ = InterleavingType::done; } inline Transition* get_transition(unsigned times_considered) { diff --combined src/mc/api/State.cpp index 36535b1f38,dfb48f399a..98c229f7ad --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@@ -14,73 -14,24 +14,68 @@@ namespace simgrid::mc long State::expended_states_ = 0; - State::State(const RemoteApp& remote_app) : default_transition(std::make_unique()), num_(++expended_states_) + State::State(const RemoteApp& remote_app) : num_(++expended_states_) { remote_app.get_actors_status(actors_to_run_); - transition_ = default_transition.get(); - /* Stateful model checking */ if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) { system_state_ = std::make_shared(num_); } } +State::State(const RemoteApp& remote_app, const State* previous_state) + : default_transition(std::make_unique()), num_(++expended_states_) +{ + + remote_app.get_actors_status(actors_to_run_); + + transition_ = default_transition.get(); + + /* Stateful model checking */ + if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) { + system_state_ = std::make_shared(num_); + } + + /* 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] : previous_state->get_sleep_set()) { + + if (not previous_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(), previous_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(); }); } +void State::mark_all_todo() +{ + for (auto & [aid, actor] : actors_to_run_) { + + if (actor.is_enabled() and not actor.is_done() and not actor.is_todo()) + actor.mark_todo(); + + } +} + Transition* State::get_transition() const { - if (transition_ == nullptr) { - return default_transition.get(); - } - return transition_; + return transition_; } aid_t State::next_transition() const @@@ -88,22 -39,8 +83,22 @@@ XBT_DEBUG("Search for an actor to run. %zu actors to consider", actors_to_run_.size()); for (auto const& [aid, actor] : 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()) - continue; + if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) { + + if (not actor.is_todo()) + XBT_DEBUG("Can't run actor %ld because it is not todo", aid); + + if (not actor.is_enabled()) + XBT_DEBUG("Can't run actor %ld because it is not enabled", aid); + + if (actor.is_done()) + XBT_DEBUG("Can't run actor %ld because it has already been done", aid); + + + continue; + + + } return aid; } diff --combined src/mc/api/State.hpp index 723a5f11e7,8a7d97e785..168ee8de44 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@@ -17,6 -17,11 +17,11 @@@ namespace simgrid::mc class XBT_PRIVATE State : public xbt::Extendable { static long expended_states_; /* Count total amount of states, for stats */ + /** + * @brief An empty transition that leads to this state by default + */ + const std::unique_ptr default_transition_ = std::make_unique(); + /** * @brief The outgoing transition: what was the last transition that * we took to leave this state? @@@ -25,12 -30,7 +30,7 @@@ * or a reference to the internal default transition `Transition()` if no transition has been * set */ - Transition* transition_ = nullptr; - - /** - * @brief An empty transition that leads to this state by default - */ - const std::unique_ptr default_transition; + Transition* transition_ = default_transition_.get(); /** Sequential state ID (used for debugging) */ long num_ = 0; @@@ -42,14 -42,9 +42,14 @@@ /** Snapshot of system state (if needed) */ std::shared_ptr system_state_; + /* 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(const RemoteApp& remote_app); - + explicit State(const RemoteApp& remote_app, const State* previous_state); /* Returns a positive number if there is another transition to pick, or -1 if not */ aid_t next_transition() const; @@@ -59,8 -54,6 +59,8 @@@ 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_done(aid_t actor) { actors_to_run_.at(actor).mark_done();} + void mark_all_todo(); bool is_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); } Transition* get_transition() const; void set_transition(Transition* t) { transition_ = t; } @@@ -72,9 -65,6 +72,9 @@@ 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_)); } + /* Returns the total amount of states created so far (for statistics) */ static long get_expanded_states() { return expended_states_; } }; diff --combined src/mc/mc_config.cpp index 6b6ea8b919,681137ef33..b4900fe947 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@@ -5,8 -5,8 +5,8 @@@ #include "src/mc/mc_config.hpp" #include "src/mc/mc_replay.hpp" + #include "src/simgrid/sg_config.hpp" #include - #include #if SIMGRID_HAVE_MC #include @@@ -48,10 -48,6 +48,10 @@@ static simgrid::config::Flag _sg_mc_sleep_set{ + "model-check/sleep-set", "Whether to enable the use of sleep-set in the reduction algorithm", false, + [](bool) { _mc_cfg_cb_check("value to enable/disable the use of sleep-set in the reduction algorithm"); }}; + simgrid::config::Flag _sg_mc_checkpoint{ "model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking " "(default: 0 => stateless verification). If value=1, one checkpoint is saved for each "