X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e9a884e745ad230410dde4af838d5727fd33edd0..f0c07d4ab3b94286d109ff88493b01c082ad70cb:/src/mc/api.cpp diff --git a/src/mc/api.cpp b/src/mc/api.cpp index b6cee6c9ba..073e2421a0 100644 --- a/src/mc/api.cpp +++ b/src/mc/api.cpp @@ -1,15 +1,22 @@ +/* Copyright (c) 2020-2022. 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. */ + #include "api.hpp" #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_base.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 @@ -20,6 +27,7 @@ #endif XBT_LOG_NEW_DEFAULT_SUBCATEGORY(Api, mc, "Logging specific to MC Facade APIs "); +XBT_LOG_EXTERNAL_CATEGORY(mc_global); using Simcall = simgrid::simix::Simcall; @@ -91,7 +99,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(const RemoteProc { /* 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; @@ -101,42 +109,37 @@ static inline smx_simcall_t MC_state_choose_request_for_process(const RemoteProc smx_simcall_t req = nullptr; if (actor->simcall_.observer_ != nullptr) { - state->transition_.times_considered_ = procstate->times_considered; - procstate->times_considered++; - if (actor->simcall_.mc_max_consider_ <= procstate->times_considered) + state->transition_.times_considered_ = procstate->get_times_considered_and_inc(); + if (actor->simcall_.mc_max_consider_ <= procstate->get_times_considered()) procstate->set_done(); req = &actor->simcall_; } else switch (actor->simcall_.call_) { 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(process, &actor->simcall_, procstate->times_considered)) { - state->transition_.times_considered_ = procstate->times_considered; - ++procstate->times_considered; + while (procstate->get_times_considered() < simcall_comm_waitany__get__count(&actor->simcall_)) { + if (simgrid::mc::request_is_enabled_by_idx(process, &actor->simcall_, procstate->get_times_considered())) { + state->transition_.times_considered_ = procstate->get_times_considered_and_inc(); break; } - ++procstate->times_considered; + procstate->get_times_considered_and_inc(); } - if (procstate->times_considered >= simcall_comm_waitany__get__count(&actor->simcall_)) + if (procstate->get_times_considered() >= simcall_comm_waitany__get__count(&actor->simcall_)) procstate->set_done(); if (state->transition_.times_considered_ != -1) req = &actor->simcall_; break; 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(process, &actor->simcall_, procstate->times_considered)) { - state->transition_.times_considered_ = procstate->times_considered; - ++procstate->times_considered; + while (procstate->get_times_considered() < simcall_comm_testany__get__count(&actor->simcall_)) { + if (simgrid::mc::request_is_enabled_by_idx(process, &actor->simcall_, procstate->get_times_considered())) { + state->transition_.times_considered_ = procstate->get_times_considered_and_inc(); break; } - ++procstate->times_considered; + procstate->get_times_considered_and_inc(); } - if (procstate->times_considered >= simcall_comm_testany__get__count(&actor->simcall_)) + if (procstate->get_times_considered() >= simcall_comm_testany__get__count(&actor->simcall_)) procstate->set_done(); if (state->transition_.times_considered_ != -1) req = &actor->simcall_; @@ -150,11 +153,9 @@ static inline smx_simcall_t MC_state_choose_request_for_process(const RemoteProc 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 - else if (act->src_actor_.get() == nullptr && act->state_ == simgrid::kernel::activity::State::READY && + else if (act->src_actor_.get() == nullptr && act->get_state() == simgrid::kernel::activity::State::READY && act->detached()) state->transition_.times_considered_ = 0; // OK - else - state->transition_.times_considered_ = -1; // timeout procstate->set_done(); req = &actor->simcall_; break; @@ -169,7 +170,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(const RemoteProc 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: @@ -365,20 +366,23 @@ 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; } -std::string Api::get_actor_name(smx_actor_t actor) const +xbt::string const& Api::get_actor_name(smx_actor_t actor) const { if (mc_model_checker == nullptr) - return actor->get_cname(); + return actor->get_name(); simgrid::mc::ActorInformation* info = actor_info_cast(actor); if (info->name.empty()) { @@ -396,7 +400,7 @@ std::string Api::get_actor_string(smx_actor_t actor) const if (actor) { res = "(" + std::to_string(actor->get_pid()) + ")"; if (actor->get_host()) - res += std::string(get_actor_host_name(actor)) + " (" + get_actor_name(actor) + ")"; + res += std::string(get_actor_host_name(actor)) + " (" + std::string(get_actor_name(actor)) + ")"; else res += get_actor_name(actor); } else @@ -414,7 +418,7 @@ 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++; @@ -427,25 +431,27 @@ simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm simgrid::mc::Checker* checker; switch (algo) { case CheckerAlgorithm::CommDeterminism: - checker = simgrid::mc::createCommunicationDeterminismChecker(session); + checker = simgrid::mc::create_communication_determinism_checker(session); break; case CheckerAlgorithm::UDPOR: - checker = simgrid::mc::createUdporChecker(session); + checker = simgrid::mc::create_udpor_checker(session); break; case CheckerAlgorithm::Safety: - checker = simgrid::mc::createSafetyChecker(session); + checker = simgrid::mc::create_safety_checker(session); break; case CheckerAlgorithm::Liveness: - checker = simgrid::mc::createLivenessChecker(session); + checker = simgrid::mc::create_liveness_checker(session); break; default: THROW_IMPOSSIBLE; } + // FIXME: session and checker are never deleted + simgrid::mc::session_singleton = session; mc_model_checker->setChecker(checker); return checker; } @@ -455,22 +461,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 @@ -539,10 +532,10 @@ std::vector Api::get_pattern_comm_data(RemotePtr mpi_request; mc_model_checker->get_remote_process().read( - &mpi_request, remote(static_cast(simcall_comm_isend__get__data(simcall)))); - return mpi_request.detached(); + mpi_request, remote(static_cast(simcall_comm_isend__get__data(simcall)))); + return mpi_request.get_buffer()->detached(); } #endif @@ -596,7 +589,14 @@ unsigned long Api::mc_get_executed_trans() const void Api::mc_check_deadlock() const { if (mc_model_checker->checkDeadlock()) { - MC_show_deadlock(); + XBT_CINFO(mc_global, "**************************"); + XBT_CINFO(mc_global, "*** DEADLOCK DETECTED ***"); + XBT_CINFO(mc_global, "**************************"); + XBT_CINFO(mc_global, "Counter-example execution trace:"); + for (auto const& s : mc_model_checker->getChecker()->get_textual_trace()) + XBT_CINFO(mc_global, " %s", s.c_str()); + simgrid::mc::dumpRecordPath(); + simgrid::mc::session_singleton->log_state(); throw DeadlockError(); } } @@ -628,11 +628,6 @@ smx_actor_t Api::simcall_get_issuer(s_smx_simcall const* req) const xbt_die("Issuer not found"); } -long Api::simcall_get_actor_id(s_smx_simcall const* req) const -{ - return simcall_get_issuer(req)->get_pid(); -} - RemotePtr Api::get_mbox_remote_addr(smx_simcall_t const req) const { if (req->call_ == Simcall::COMM_ISEND) @@ -651,17 +646,6 @@ RemotePtr Api::get_comm_remote_addr(smx_simcall_ THROW_IMPOSSIBLE; } -bool Api::mc_is_null() const -{ - auto is_null = (mc_model_checker == nullptr) ? true : false; - return is_null; -} - -Checker* Api::mc_get_checker() const -{ - return mc_model_checker->getChecker(); -} - void Api::handle_simcall(Transition const& transition) const { mc_model_checker->handle_simcall(transition); @@ -835,7 +819,7 @@ std::string Api::request_to_string(smx_simcall_t req, int value) const break; default: - type = SIMIX_simcall_name(req->call_); + type = SIMIX_simcall_name(*req); args = "??"; break; } @@ -920,14 +904,14 @@ std::string Api::request_get_dot_output(smx_simcall_t req, int value) const #if HAVE_SMPI int Api::get_smpi_request_tag(smx_simcall_t const& simcall, simgrid::simix::Simcall type) const { - simgrid::smpi::Request mpi_request; void* simcall_data = nullptr; if (type == Simcall::COMM_ISEND) simcall_data = simcall_comm_isend__get__data(simcall); else if (type == Simcall::COMM_IRECV) simcall_data = simcall_comm_irecv__get__data(simcall); - mc_model_checker->get_remote_process().read(&mpi_request, remote(static_cast(simcall_data))); - return mpi_request.tag(); + Remote mpi_request; + mc_model_checker->get_remote_process().read(mpi_request, remote(static_cast(simcall_data))); + return mpi_request.get_buffer()->tag(); } #endif @@ -938,7 +922,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 @@ -954,14 +938,14 @@ simgrid::mc::Snapshot* Api::take_snapshot(int num_state) const void Api::s_close() const { - session->close(); + 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); } void Api::automaton_load(const char* file) const