X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/92cfd3dc96cc1a8f7c69707c80aaf70d61cbcbbf..f0c07d4ab3b94286d109ff88493b01c082ad70cb:/src/mc/api.cpp diff --git a/src/mc/api.cpp b/src/mc/api.cpp index ec0b7e3011..073e2421a0 100644 --- a/src/mc/api.cpp +++ b/src/mc/api.cpp @@ -1,3 +1,8 @@ +/* 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" @@ -5,6 +10,7 @@ #include "src/kernel/actor/SimcallObserver.hpp" #include "src/mc/Session.hpp" #include "src/mc/checker/Checker.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" @@ -21,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; @@ -102,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_; @@ -151,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; @@ -431,19 +431,19 @@ 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: @@ -532,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 @@ -589,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(); } } @@ -621,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) @@ -644,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); @@ -828,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; } @@ -913,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