#include "src/kernel/actor/ActorImpl.hpp"
#include "src/kernel/actor/SimcallObserver.hpp"
#include "src/mc/mc_base.hpp"
+#include "src/mc/mc_config.hpp"
#include "src/mc/remote/RemoteProcess.hpp"
#if HAVE_SMPI
#include "src/smpi/include/private.hpp"
#include <sys/types.h>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
+XBT_LOG_EXTERNAL_CATEGORY(mc_global);
namespace simgrid::mc {
if (instance_)
return instance_.get();
- _sg_do_model_check = 1;
+ simgrid::mc::cfg_do_model_check = true;
setvbuf(stdout, nullptr, _IOLBF, 0);
void AppSide::handle_deadlock_check(const s_mc_message_t*) const
{
- const auto& actor_list = kernel::EngineImpl::get_instance()->get_actor_list();
+ const auto* engine = kernel::EngineImpl::get_instance();
+ const auto& actor_list = engine->get_actor_list();
bool deadlock = not actor_list.empty() && std::none_of(begin(actor_list), end(actor_list), [](const auto& kv) {
return mc::actor_is_enabled(kv.second);
});
+ if (deadlock) {
+ XBT_CINFO(mc_global, "**************************");
+ XBT_CINFO(mc_global, "*** DEADLOCK DETECTED ***");
+ XBT_CINFO(mc_global, "**************************");
+ engine->display_all_actor_status();
+ }
// Send result:
s_mc_message_int_t answer{MessageType::DEADLOCK_CHECK_REPLY, deadlock};
xbt_assert(channel_.send(answer) == 0, "Could not send response");
{
auto const& actor_list = kernel::EngineImpl::get_instance()->get_actor_list();
int count = actor_list.size();
+ XBT_DEBUG("Serialize the actors to answer ACTORS_STATUS from the checker. %d actors to go.", count);
struct s_mc_message_actors_status_answer_t answer {
MessageType::ACTORS_STATUS_REPLY, count
void AppSide::declare_symbol(const char* name, int* value) const
{
+ if (not MC_is_active())
+ return;
+
s_mc_message_register_symbol_t message;
memset(&message, 0, sizeof(message));
message.type = MessageType::REGISTER_SYMBOL;
xbt_assert(strlen(name) + 1 <= message.name.size(), "Symbol is too long");
- strncpy(message.name.data(), name, message.name.size());
+ strncpy(message.name.data(), name, message.name.size() - 1);
message.callback = nullptr;
message.data = value;
xbt_assert(channel_.send(message) == 0, "Could send REGISTER_SYMBOL message to model-checker");