X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/fa84bee017477630eea9a93890e0e2abf3855bf9..97fed1ab7cb584d61415854ce500f2176679c5ac:/src/mc/api.cpp diff --git a/src/mc/api.cpp b/src/mc/api.cpp index ce7b065d37..6f54255a5c 100644 --- a/src/mc/api.cpp +++ b/src/mc/api.cpp @@ -2,14 +2,15 @@ #include "src/kernel/activity/MailboxImpl.hpp" #include "src/kernel/activity/MutexImpl.hpp" +#include "src/kernel/actor/SimcallObserver.hpp" #include "src/mc/Session.hpp" #include "src/mc/checker/Checker.hpp" -#include "src/mc/checker/SimcallObserver.hpp" #include "src/mc/mc_comm_pattern.hpp" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_pattern.hpp" #include "src/mc/mc_private.hpp" #include "src/mc/remote/RemoteProcess.hpp" +#include "src/surf/HostImpl.hpp" #include #include @@ -47,6 +48,33 @@ static std::string buff_size_to_string(size_t buff_size) static void simcall_translate(smx_simcall_t req, simgrid::mc::Remote& buffered_comm); +static bool request_is_enabled_by_idx(const RemoteProcess& process, smx_simcall_t req, unsigned int idx) +{ + kernel::activity::CommImpl* remote_act = nullptr; + switch (req->call_) { + case Simcall::COMM_WAIT: + /* FIXME: check also that src and dst processes are not suspended */ + remote_act = simcall_comm_wait__getraw__comm(req); + break; + + case Simcall::COMM_WAITANY: + remote_act = process.read(remote(simcall_comm_waitany__get__comms(req) + idx)); + break; + + case Simcall::COMM_TESTANY: + remote_act = process.read(remote(simcall_comm_testany__get__comms(req) + idx)); + break; + + default: + return true; + } + + Remote temp_comm; + process.read(temp_comm, remote(remote_act)); + const kernel::activity::CommImpl* comm = temp_comm.get_buffer(); + return comm->src_actor_.get() && comm->dst_actor_.get(); +} + /* Search an enabled transition for the given process. * * This can be seen as an iterator returning the next transition of the process. @@ -59,11 +87,12 @@ static void simcall_translate(smx_simcall_t req, * Things can get muddled with the WAITANY and TESTANY simcalls, that are rewritten on the fly to a bunch of WAIT * (resp TEST) transitions using the transition.argument field to remember what was the last returned sub-transition. */ -static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::State* state, smx_actor_t actor) +static inline smx_simcall_t MC_state_choose_request_for_process(const RemoteProcess& process, simgrid::mc::State* state, + smx_actor_t actor) { /* reset the outgoing transition */ simgrid::mc::ActorState* procstate = &state->actor_states_[actor->get_pid()]; - state->transition_.pid_ = -1; + state->transition_.aid_ = -1; state->transition_.times_considered_ = -1; state->transition_.textual[0] = '\0'; state->executed_req_.call_ = Simcall::NONE; @@ -83,7 +112,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta case Simcall::COMM_WAITANY: state->transition_.times_considered_ = -1; while (procstate->times_considered < simcall_comm_waitany__get__count(&actor->simcall_)) { - if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall_, procstate->times_considered)) { + if (simgrid::mc::request_is_enabled_by_idx(process, &actor->simcall_, procstate->times_considered)) { state->transition_.times_considered_ = procstate->times_considered; ++procstate->times_considered; break; @@ -100,7 +129,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta case Simcall::COMM_TESTANY: state->transition_.times_considered_ = -1; while (procstate->times_considered < simcall_comm_testany__get__count(&actor->simcall_)) { - if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall_, procstate->times_considered)) { + if (simgrid::mc::request_is_enabled_by_idx(process, &actor->simcall_, procstate->times_considered)) { state->transition_.times_considered_ = procstate->times_considered; ++procstate->times_considered; break; @@ -118,7 +147,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta simgrid::mc::RemotePtr remote_act = remote(simcall_comm_wait__get__comm(&actor->simcall_)); simgrid::mc::Remote temp_act; - mc_model_checker->get_remote_process().read(temp_act, remote_act); + process.read(temp_act, remote_act); const simgrid::kernel::activity::CommImpl* act = temp_act.get_buffer(); if (act->src_actor_.get() && act->dst_actor_.get()) state->transition_.times_considered_ = 0; // OK @@ -141,7 +170,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta if (not req) return nullptr; - state->transition_.pid_ = actor->get_pid(); + state->transition_.aid_ = actor->get_pid(); state->executed_req_ = *req; // Fetch the data of the request and translate it: @@ -337,13 +366,16 @@ xbt::string const& Api::get_actor_host_name(smx_actor_t actor) const // Read the simgrid::xbt::string in the MCed process: simgrid::mc::ActorInformation* info = actor_info_cast(actor); - auto remote_string_address = - remote(reinterpret_cast(&actor->get_host()->get_name())); - simgrid::xbt::string_data remote_string = process->read(remote_string_address); - std::vector hostname(remote_string.len + 1); - // no need to read the terminating null byte, and thus hostname[remote_string.len] is guaranteed to be '\0' - process->read_bytes(hostname.data(), remote_string.len, remote(remote_string.data)); - info->hostname = &mc_model_checker->get_host_name(hostname.data()); + + if (not info->hostname) { + Remote temp_host = process->read(remote(actor->get_host())); + auto remote_string_address = remote(&xbt::string::to_string_data(temp_host.get_buffer()->get_impl()->get_name())); + simgrid::xbt::string_data remote_string = process->read(remote_string_address); + std::vector hostname(remote_string.len + 1); + // no need to read the terminating null byte, and thus hostname[remote_string.len] is guaranteed to be '\0' + process->read_bytes(hostname.data(), remote_string.len, remote(remote_string.data)); + info->hostname = &mc_model_checker->get_host_name(hostname.data()); + } return *info->hostname; } @@ -386,14 +418,14 @@ std::string Api::get_actor_dot_label(smx_actor_t actor) const simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const { - simgrid::mc::session = new simgrid::mc::Session([argv] { + auto session = new simgrid::mc::Session([argv] { int i = 1; while (argv[i] != nullptr && argv[i][0] == '-') i++; xbt_assert(argv[i] != nullptr, "Unable to find a binary to exec on the command line. Did you only pass config flags?"); execvp(argv[i], argv + i); - xbt_die("The model-checked process failed to exec(): %s", strerror(errno)); + xbt_die("The model-checked process failed to exec(%s): %s", argv[i], strerror(errno)); }); simgrid::mc::Checker* checker; @@ -418,6 +450,7 @@ simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm THROW_IMPOSSIBLE; } + simgrid::mc::session_singleton = session; mc_model_checker->setChecker(checker); return checker; } @@ -427,22 +460,9 @@ std::vector& Api::get_actors() const return mc_model_checker->get_remote_process().actors(); } -bool Api::actor_is_enabled(aid_t pid) const -{ - return session->actor_is_enabled(pid); -} - unsigned long Api::get_maxpid() const { - static const char* name = nullptr; - if (not name) { - name = "simgrid::kernel::actor::maxpid"; - if (mc_model_checker->get_remote_process().find_variable(name) == nullptr) - name = "maxpid"; // We seem to miss the namespaces when compiling with GCC - } - unsigned long maxpid; - mc_model_checker->get_remote_process().read_variable(name, &maxpid, sizeof(maxpid)); - return maxpid; + return mc_model_checker->get_remote_process().get_maxpid(); } int Api::get_actors_size() const @@ -545,11 +565,6 @@ std::size_t Api::get_remote_heap_bytes() const return heap_bytes_used; } -void Api::session_initialize() const -{ - session->initialize(); -} - void Api::mc_inc_visited_states() const { mc_model_checker->visited_states++; @@ -661,12 +676,13 @@ void Api::dump_record_path() const smx_simcall_t Api::mc_state_choose_request(simgrid::mc::State* state) const { - for (auto& actor : mc_model_checker->get_remote_process().actors()) { + RemoteProcess& process = mc_model_checker->get_remote_process(); + for (auto& actor : process.actors()) { /* Only consider the actors that were marked as interleaving by the checker algorithm */ if (not state->actor_states_[actor.copy.get_buffer()->get_pid()].is_todo()) continue; - smx_simcall_t res = MC_state_choose_request_for_process(state, actor.copy.get_buffer()); + smx_simcall_t res = MC_state_choose_request_for_process(process, state, actor.copy.get_buffer()); if (res) return res; } @@ -914,7 +930,7 @@ void Api::restore_state(std::shared_ptr system_state) con void Api::log_state() const { - session->log_state(); + session_singleton->log_state(); } bool Api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const @@ -930,27 +946,20 @@ simgrid::mc::Snapshot* Api::take_snapshot(int num_state) const void Api::s_close() const { - session->close(); -} - -void Api::restore_initial_state() const -{ - session->restore_initial_state(); + session_singleton->close(); } void Api::execute(Transition& transition, smx_simcall_t simcall) const { /* FIXME: once all simcalls have observers, kill the simcall parameter and use mc_model_checker->simcall_to_string() */ transition.textual = request_to_string(simcall, transition.times_considered_); - session->execute(transition); + session_singleton->execute(transition); } -#if SIMGRID_HAVE_MC void Api::automaton_load(const char* file) const { MC_automaton_load(file); } -#endif std::vector Api::automaton_propositional_symbol_evaluate() const {