From: Martin Quinson Date: Mon, 7 Feb 2022 08:55:04 +0000 (+0100) Subject: Move the selection of the next transition to execute to mc::State X-Git-Tag: v3.31~474 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/157b17ef4d7aa7d34625418c27861f3f139010bd Move the selection of the next transition to execute to mc::State --- diff --git a/include/simgrid/forward.h b/include/simgrid/forward.h index c6333a242c..e9f6f61676 100644 --- a/include/simgrid/forward.h +++ b/include/simgrid/forward.h @@ -196,6 +196,7 @@ class Profile; } // namespace kernel namespace mc { class CommunicationDeterminismChecker; +class State; } } // namespace simgrid diff --git a/src/mc/Transition.cpp b/src/mc/Transition.cpp index 019bd142b9..5c6a80eb65 100644 --- a/src/mc/Transition.cpp +++ b/src/mc/Transition.cpp @@ -6,8 +6,12 @@ #include "src/mc/Transition.hpp" #include "src/mc/ModelChecker.hpp" #include "src/mc/Session.hpp" +#include "src/mc/mc_state.hpp" +#include "src/mc/remote/RemoteProcess.hpp" #include "xbt/asserts.h" +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_transition, mc, "Logging specific to MC transitions"); + namespace simgrid { namespace mc { unsigned long Transition::executed_transitions_ = 0; @@ -18,9 +22,34 @@ std::string Transition::to_string() return textual_; } -RemotePtr Transition::execute() +RemotePtr Transition::execute(simgrid::mc::State* state, int next) { + std::vector& actors = mc_model_checker->get_remote_process().actors(); + + kernel::actor::ActorImpl* actor = actors[next].copy.get_buffer(); + aid_t aid = actor->get_pid(); + + simgrid::mc::ActorState* actor_state = &state->actor_states_[aid]; + /* This actor is ready to be executed. Prepare its execution when simcall_handle will be called on it */ + if (actor->simcall_.observer_ != nullptr) { + state->transition_.times_considered_ = actor_state->get_times_considered_and_inc(); + if (actor->simcall_.mc_max_consider_ <= actor_state->get_times_considered()) + actor_state->set_done(); + } else { + state->transition_.times_considered_ = 0; + actor_state->set_done(); + } + + aid_ = aid; + state->executed_req_ = actor->simcall_; + textual_ = mc_model_checker->simcall_to_string(aid_, times_considered_); + XBT_DEBUG("Let's run actor %ld, going for transition %s", aid, textual_.c_str()); + + return replay(); +} +RemotePtr Transition::replay() +{ executed_transitions_++; simgrid::mc::RemotePtr res = mc_model_checker->handle_simcall(*this); @@ -28,5 +57,6 @@ RemotePtr Transition::execute() return res; } + } // namespace mc } // namespace simgrid diff --git a/src/mc/Transition.hpp b/src/mc/Transition.hpp index 44c86e6b10..a51e996db2 100644 --- a/src/mc/Transition.hpp +++ b/src/mc/Transition.hpp @@ -41,8 +41,13 @@ public: int times_considered_ = 0; std::string to_string(); - RemotePtr execute(); + /* Explore a new path */ + RemotePtr execute(simgrid::mc::State* state, int next); + /* Moves the application toward a path that was already explored, but don't change the current transition */ + RemotePtr replay(); + + /* Returns the total amount of transitions executed so far (for statistics) */ static unsigned long get_executed_transitions() { return executed_transitions_; } }; diff --git a/src/mc/api.cpp b/src/mc/api.cpp index e014bedb8e..ea947943b0 100644 --- a/src/mc/api.cpp +++ b/src/mc/api.cpp @@ -364,47 +364,6 @@ void Api::dump_record_path() const simgrid::mc::dumpRecordPath(); } -/* Search for an enabled transition amongst actors - * - * This is the first actor marked TODO by the checker, and currently enabled in the application. - * - * Once we found it, prepare its execution (increase the times_considered of its observer and remove it as done on need) - * - * If we can't find any actor, return false - */ - -bool Api::mc_state_choose_request(simgrid::mc::State* state) const -{ - RemoteProcess& process = mc_model_checker->get_remote_process(); - XBT_DEBUG("Search for an actor to run. %zu actors to consider", process.actors().size()); - for (auto& actor_info : process.actors()) { - auto actor = actor_info.copy.get_buffer(); - simgrid::mc::ActorState* actor_state = &state->actor_states_[actor->get_pid()]; - - /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application*/ - if (not actor_state->is_todo() || not simgrid::mc::actor_is_enabled(actor)) - continue; - - /* This actor is ready to be executed. Prepare its execution when simcall_handle will be called on it */ - if (actor->simcall_.observer_ != nullptr) { - state->transition_.times_considered_ = actor_state->get_times_considered_and_inc(); - if (actor->simcall_.mc_max_consider_ <= actor_state->get_times_considered()) - actor_state->set_done(); - } else { - state->transition_.times_considered_ = 0; - actor_state->set_done(); - } - - state->transition_.aid_ = actor->get_pid(); - state->executed_req_ = actor->simcall_; - - XBT_DEBUG("Let's run actor %ld, going for transition %s", actor->get_pid(), - SIMIX_simcall_name(state->executed_req_)); - return true; - } - return false; -} - std::string Api::request_get_dot_output(aid_t aid, int value) const { const char* color = get_color(aid - 1); diff --git a/src/mc/api.hpp b/src/mc/api.hpp index 199f4568eb..f0a2d95486 100644 --- a/src/mc/api.hpp +++ b/src/mc/api.hpp @@ -100,7 +100,6 @@ public: void mc_check_deadlock() const; XBT_ATTRIB_NORETURN void mc_exit(int status) const; void dump_record_path() const; - bool mc_state_choose_request(simgrid::mc::State* state) const; // SIMCALL APIs bool requests_are_dependent(RemotePtr obs1, diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index a1a136b39f..3ac7e22014 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -369,7 +369,7 @@ void CommunicationDeterminismChecker::restoreState() /* TODO : handle test and testany simcalls */ CallType call = MC_get_call_type(req); - state->transition_.execute(); + state->transition_.replay(); handle_comm_pattern(call, req, req_num, 1); /* Update statistics */ @@ -418,11 +418,13 @@ void CommunicationDeterminismChecker::real_run() /* Update statistics */ api::get().mc_inc_visited_states(); - bool found_transition = false; + int next_transition = -1; if (stack_.size() <= (std::size_t)_sg_mc_max_depth) - found_transition = api::get().mc_state_choose_request(cur_state); + next_transition = cur_state->next_transition(); + + if (next_transition >= 0 && visited_state == nullptr) { + cur_state->transition_.execute(cur_state, next_transition); - if (found_transition && visited_state == nullptr) { aid_t aid = cur_state->transition_.aid_; int req_num = cur_state->transition_.times_considered_; smx_simcall_t req = &cur_state->executed_req_; @@ -438,10 +440,6 @@ void CommunicationDeterminismChecker::real_run() if (_sg_mc_comms_determinism || _sg_mc_send_determinism) call = MC_get_call_type(req); - /* Answer the request */ - cur_state->transition_.execute(); - /* After this call req is no longer useful */ - handle_comm_pattern(call, req, req_num, 0); /* Create the new expanded state */ diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index 8eff59c2c0..e5f59bbd41 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -122,7 +122,7 @@ void LivenessChecker::replay() std::shared_ptr state = pair->graph_state; if (pair->exploration_started) { - state->transition_.execute(); + state->transition_.replay(); XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->transition_.to_string().c_str(), state.get()); } @@ -336,9 +336,13 @@ void LivenessChecker::run() } } - api::get().mc_state_choose_request(current_pair->graph_state.get()); - aid_t aid = current_pair->graph_state->transition_.aid_; - int req_num = current_pair->graph_state->transition_.times_considered_; + int next = current_pair->graph_state->next_transition(); + + current_pair->graph_state->transition_.execute(current_pair->graph_state.get(), next); + + aid_t aid = current_pair->graph_state->transition_.aid_; + int req_num = current_pair->graph_state->transition_.times_considered_; + XBT_DEBUG("Execute: %s", current_pair->graph_state->transition_.to_string().c_str()); if (dot_output != nullptr) { if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) { @@ -353,9 +357,6 @@ void LivenessChecker::run() fflush(dot_output); } - current_pair->graph_state->transition_.execute(); - XBT_DEBUG("Execute: %s", current_pair->graph_state->transition_.to_string().c_str()); - if (not current_pair->exploration_started) visited_pairs_count_++; diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index e444260b26..9f3a8f74da 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -109,10 +109,10 @@ void SafetyChecker::run() continue; } - // Search for the next transition. If found, state is modified accordingly (transition and executed_req are set) - // If there is no more transition in the current state, backtrack. + // Search for the next transition + int next = state->next_transition(); - if (not api::get().mc_state_choose_request(state)) { + if (next < 0) { // If there is no more transition in the current state, backtrack. XBT_DEBUG("There remains %zu actors, but none to interleave (depth %zu).", mc_model_checker->get_remote_process().actors().size(), stack_.size() + 1); @@ -124,7 +124,7 @@ void SafetyChecker::run() } /* Actually answer the request: let execute the selected request (MCed does one step) */ - auto remote_observer = state->transition_.execute(); + auto remote_observer = state->transition_.execute(state, next); // If there are processes to interleave and the maximum depth has not been // reached then perform one step of the exploration algorithm. @@ -246,7 +246,7 @@ void SafetyChecker::restore_state() for (std::unique_ptr const& state : stack_) { if (state == stack_.back()) break; - state->transition_.execute(); + state->transition_.replay(); /* Update statistics */ api::get().mc_inc_visited_states(); } diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index dff1bee2d8..154511c32a 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -4,11 +4,14 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/mc_state.hpp" -#include "src/mc/mc_config.hpp" +#include "src/mc/Session.hpp" #include "src/mc/api.hpp" +#include "src/mc/mc_config.hpp" #include +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc, "Logging specific to MC states"); + using simgrid::mc::remote; using api = simgrid::mc::Api; @@ -40,6 +43,23 @@ Transition State::get_transition() const return this->transition_; } +int 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++) { + aid_t aid = actors[i].copy.get_buffer()->get_pid(); + const ActorState* actor_state = &actor_states_[aid]; + + /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application*/ + if (not actor_state->is_todo() || not simgrid::mc::session_singleton->actor_is_enabled(aid)) + continue; + + return i; + } + return -1; +} + void State::copy_incomplete_comm_pattern() { incomplete_comm_pattern_.clear(); diff --git a/src/mc/mc_state.hpp b/src/mc/mc_state.hpp index d5bc4bd0ca..ae21f24078 100644 --- a/src/mc/mc_state.hpp +++ b/src/mc/mc_state.hpp @@ -39,6 +39,9 @@ public: explicit State(unsigned long state_number); + /* Returns a positive number if there is another transition to pick, or -1 if not */ + int next_transition() const; + std::size_t count_todo() const; void mark_todo(aid_t actor) { this->actor_states_[actor].mark_todo(); } Transition get_transition() const;