-/* Copyright (c) 2015-2021. The SimGrid Team. All rights reserved. */
+/* Copyright (c) 2015-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 "src/mc/Session.hpp"
-#include "src/mc/checker/Checker.hpp"
-#include "src/mc/mc_config.hpp"
#include "src/internal_config.h" // HAVE_SMPI
+#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/mc_config.hpp"
#if HAVE_SMPI
#include "smpi/smpi.h"
+#include "src/smpi/include/private.hpp"
#endif
+#include "src/mc/api/State.hpp"
+#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
-#include "src/mc/mc_state.hpp"
#include "xbt/log.h"
#include "xbt/system_error.hpp"
+#include "signal.h"
#include <array>
#include <memory>
#include <string>
#endif
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
+XBT_LOG_EXTERNAL_CATEGORY(mc_global);
namespace simgrid {
namespace mc {
// between the model-checker process (ourselves) and the model-checked
// process:
int sockets[2];
- int res = socketpair(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0, sockets);
- xbt_assert(res != -1, "Could not create socketpair");
+ xbt_assert(socketpair(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0, sockets) != -1, "Could not create socketpair");
pid_t pid = fork();
xbt_assert(pid >= 0, "Could not fork model-checked process");
initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0);
}
-void Session::execute(Transition const& transition) const
-{
- model_checker_->handle_simcall(transition);
- model_checker_->wait_for_requests();
-}
-
void Session::restore_initial_state() const
{
this->initial_snapshot_->restore(&model_checker_->get_remote_process());
void Session::log_state() const
{
- model_checker_->getChecker()->log_state();
+ model_checker_->get_exploration()->log_state();
if (not _sg_mc_dot_output_file.get().empty()) {
fprintf(dot_output, "}\n");
bool Session::actor_is_enabled(aid_t pid) const
{
- s_mc_message_actor_enabled_t msg{};
+ s_mc_message_actor_enabled_t msg;
+ memset(&msg, 0, sizeof msg);
msg.type = simgrid::mc::MessageType::ACTOR_ENABLED;
msg.aid = pid;
model_checker_->channel().send(msg);
return ((s_mc_message_int_t*)buff.data())->value;
}
-simgrid::mc::Session* session_singleton;
+void Session::check_deadlock() const
+{
+ xbt_assert(model_checker_->channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state");
+ s_mc_message_int_t message;
+ ssize_t s = model_checker_->channel().receive(message);
+ xbt_assert(s != -1, "Could not receive message");
+ xbt_assert(s == sizeof(message) && message.type == MessageType::DEADLOCK_CHECK_REPLY,
+ "Received unexpected message %s (%i, size=%i) "
+ "expected MessageType::DEADLOCK_CHECK_REPLY (%i, size=%i)",
+ to_c_str(message.type), (int)message.type, (int)s, (int)MessageType::DEADLOCK_CHECK_REPLY,
+ (int)sizeof(message));
+
+ if (message.value != 0) {
+ 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& frame : model_checker_->get_exploration()->get_textual_trace())
+ XBT_CINFO(mc_global, " %s", frame.c_str());
+ XBT_CINFO(mc_global, "Path = %s", model_checker_->get_exploration()->get_record_trace().to_string().c_str());
+ log_state();
+ throw DeadlockError();
+ }
+}
}
}