+/* 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/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"
#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;
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_;
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;
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:
#if HAVE_SMPI
bool Api::check_send_request_detached(smx_simcall_t const& simcall) const
{
- simgrid::smpi::Request mpi_request;
+ Remote<simgrid::smpi::Request> mpi_request;
mc_model_checker->get_remote_process().read(
- &mpi_request, remote(static_cast<smpi::Request*>(simcall_comm_isend__get__data(simcall))));
- return mpi_request.detached();
+ mpi_request, remote(static_cast<smpi::Request*>(simcall_comm_isend__get__data(simcall))));
+ return mpi_request.get_buffer()->detached();
}
#endif
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();
}
}
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<kernel::activity::MailboxImpl> Api::get_mbox_remote_addr(smx_simcall_t const req) const
{
if (req->call_ == Simcall::COMM_ISEND)
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);
break;
default:
- type = SIMIX_simcall_name(req->call_);
+ type = SIMIX_simcall_name(*req);
args = "??";
break;
}
#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<smpi::Request*>(simcall_data)));
- return mpi_request.tag();
+ Remote<simgrid::smpi::Request> mpi_request;
+ mc_model_checker->get_remote_process().read(mpi_request, remote(static_cast<smpi::Request*>(simcall_data)));
+ return mpi_request.get_buffer()->tag();
}
#endif