From: mlaurent Date: Mon, 13 Feb 2023 14:33:49 +0000 (+0100) Subject: adding sleep sets to reduction techniques X-Git-Tag: v3.34~436^2~17 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/5a006fa396cfcc8a91a8284f0d625b2a9a2565c9 adding sleep sets to reduction techniques --- diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp index cee8581904..b71ccbd30d 100644 --- a/src/mc/api/ActorState.hpp +++ b/src/mc/api/ActorState.hpp @@ -52,7 +52,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_; } @@ -70,7 +70,7 @@ public: this->state_ = InterleavingType::todo; this->times_considered_ = 0; } - void set_done() { this->state_ = InterleavingType::done; } + void mark_done() { this->state_ = InterleavingType::done; } }; } // namespace simgrid::mc diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index eb193df584..f4cb228086 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -25,6 +25,36 @@ State::State(const RemoteApp& remote_app) : num_(++expended_states_) } } +State::State(const RemoteApp& remote_app, const State* previous_state) : num_(++expended_states_) +{ + + remote_app.get_actors_status(actors_to_run_); + + transition_.reset(new Transition()); + /* Stateful model checking */ + if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) { + system_state_ = std::make_shared(num_); + } + + for (auto & [aid, transition] : previous_state->get_sleep_set()) { + + XBT_DEBUG("Transition >>%s<< will be explored ?", transition.to_string().c_str()); + 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(); }); @@ -50,7 +80,7 @@ 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_) { /* 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()) { + 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); @@ -58,6 +88,10 @@ aid_t State::next_transition() const 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; diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 03b482dd36..c10ca6200f 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -29,9 +29,11 @@ class XBT_PRIVATE State : public xbt::Extendable { /** Snapshot of system state (if needed) */ std::shared_ptr system_state_; + 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; @@ -41,7 +43,7 @@ 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 set_done(aid_t actor) {actors_to_run_.at(actor).set_done();} + 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; @@ -54,6 +56,9 @@ public: 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 set_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/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index f1fa21bfeb..0e5dd646fc 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -136,7 +136,6 @@ void DFSExplorer::run() mc_model_checker->finalize_app(); XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(), state->get_num(), stack_.size()); - stack_.pop_back(); } @@ -144,6 +143,13 @@ void DFSExplorer::run() continue; } + XBT_VERB("Sleep set actually containing:"); + for (auto & [aid, transition] : state->get_sleep_set()) { + + XBT_VERB("###<%ld,%s>", aid, transition.to_string().c_str()); + + } + /* Actually answer the request: let's execute the selected request (MCed does one step) */ state->execute_next(next); on_transition_execute_signal(state->get_transition(), get_remote_app()); @@ -154,9 +160,23 @@ void DFSExplorer::run() state->get_transition()->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) */ - auto next_state = std::make_unique(get_remote_app()); + std::__detail::__unique_ptr_t next_state; + + /* If we want sleep set reduction, we pass it to old one to the new state */ + if (sleep_set_reduction_) + next_state = std::make_unique(get_remote_app(), state); + else + next_state = std::make_unique(get_remote_app()); + on_state_creation_signal(next_state.get(), get_remote_app()); + XBT_VERB("New sleep set containing:"); + for (auto & [aid, transition] : next_state->get_sleep_set()) { + + XBT_VERB("###<%ld,%s>", aid, transition.to_string().c_str()); + + } + if (_sg_mc_termination) this->check_non_termination(next_state.get()); @@ -168,7 +188,7 @@ void DFSExplorer::run() if (visited_state_ == nullptr) { /* Get an enabled process and insert it in the interleave set of the next state */ for (auto const& [aid, _] : next_state->get_actors_list()) { - if (next_state->is_actor_enabled(aid)) { + if (next_state->is_actor_enabled(aid) and not next_state->is_done(aid)) { next_state->mark_todo(aid); if (reduction_mode_ == ReductionMode::dpor) break; // With DPOR, we take the first enabled transition @@ -197,6 +217,9 @@ void DFSExplorer::backtrack() get_remote_app().check_deadlock(); + if (stack_.back()->get_transition()->aid_ == 0) + stack_.pop_back(); + /* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that * have it empty in the way. For each deleted state, check if the request that has generated it (from its * predecessor state), depends on any other previous request executed before it. If it does then add it to the @@ -204,8 +227,13 @@ void DFSExplorer::backtrack() bool found_backtracking_point = false; while (not stack_.empty() && not found_backtracking_point) { std::unique_ptr state = std::move(stack_.back()); + stack_.pop_back(); - state->set_done(state->get_transition()->aid_); + + XBT_DEBUG("Maarking Transition >>%s<< of process %ld done and addint it to the sleep set", state->get_transition()->to_string().c_str(), state->get_transition()->aid_); + state->mark_done(state->get_transition()->aid_); + state->set_sleep_set(state->get_transition()); + if (reduction_mode_ == ReductionMode::dpor) { aid_t issuer_id = state->get_transition()->aid_; for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) { diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp index 0a0d51e53d..924484270a 100644 --- a/src/mc/explo/DFSExplorer.hpp +++ b/src/mc/explo/DFSExplorer.hpp @@ -83,6 +83,7 @@ public: private: void check_non_termination(const State* current_state); void backtrack(); + bool sleep_set_reduction_ = true; /** Stack representing the position in the exploration graph */ std::list> stack_;