#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 {
std::unique_ptr<AppSide> AppSide::instance_;
-AppSide* AppSide::initialize(xbt_dynar_t actors_addr)
+AppSide* AppSide::initialize()
{
if (not std::getenv(MC_ENV_SOCKET_FD)) // We are not in MC mode: don't initialize the MC world
return nullptr;
if (instance_)
return instance_.get();
- _sg_do_model_check = 1;
+ simgrid::mc::cfg_do_model_check = true;
setvbuf(stdout, nullptr, _IOLBF, 0);
strerror(errno));
s_mc_message_initial_addresses_t message{MessageType::INITIAL_ADDRESSES, mmalloc_get_current_heap(),
- kernel::actor::ActorImpl::get_maxpid_addr(), actors_addr};
+ kernel::actor::ActorImpl::get_maxpid_addr()};
xbt_assert(instance_->channel_.send(message) == 0, "Could not send the initial message with addresses.");
instance_->handle_messages();
void AppSide::handle_deadlock_check(const s_mc_message_t*) const
{
- const auto& actor_list = kernel::EngineImpl::get_instance()->get_actor_list();
+ 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");
xbt_assert(channel_.send(answer) == 0, "Could not send response");
}
-void AppSide::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) const
-{
- bool res = mc::actor_is_enabled(kernel::EngineImpl::get_instance()->get_actor_by_pid(msg->aid));
- s_mc_message_int_t answer{MessageType::ACTOR_ENABLED_REPLY, res};
- xbt_assert(channel_.send(answer) == 0, "Could not send ACTOR_ENABLED_REPLY");
-}
-
void AppSide::handle_finalize(const s_mc_message_int_t* msg) const
{
bool terminate_asap = msg->value;
#endif
}
coverage_checkpoint();
- xbt_assert(channel_.send(MessageType::DEADLOCK_CHECK_REPLY) == 0, // DEADLOCK_CHECK_REPLY, really?
- "Could not answer to FINALIZE");
+ xbt_assert(channel_.send(MessageType::FINALIZE_REPLY) == 0, "Could not answer to FINALIZE");
std::fflush(stdout);
if (terminate_asap)
::_Exit(0);
}
+void AppSide::handle_actors_status() const
+{
+ 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
+ };
+ std::vector<s_mc_message_actors_status_one_t> status(count);
+ int i = 0;
+ for (auto const& [aid, actor] : actor_list) {
+ status[i].aid = aid;
+ status[i].enabled = mc::actor_is_enabled(actor);
+ status[i].max_considered = actor->simcall_.observer_->get_max_consider();
+ i++;
+ }
+ xbt_assert(channel_.send(answer) == 0, "Could not send ACTORS_STATUS_REPLY msg");
+ if (answer.count > 0) {
+ size_t size = status.size() * sizeof(s_mc_message_actors_status_one_t);
+ xbt_assert(channel_.send(status.data(), size) == 0, "Could not send ACTORS_STATUS_REPLY data");
+ }
+}
#define assert_msg_size(_name_, _type_) \
xbt_assert(received_size == sizeof(_type_), "Unexpected size for " _name_ " (%zd != %zu)", received_size, \
handle_simcall_execute((s_mc_message_simcall_execute_t*)message_buffer.data());
break;
- case MessageType::ACTOR_ENABLED:
- assert_msg_size("ACTOR_ENABLED", s_mc_message_actor_enabled_t);
- handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer.data());
- break;
-
case MessageType::FINALIZE:
assert_msg_size("FINALIZE", s_mc_message_int_t);
handle_finalize((s_mc_message_int_t*)message_buffer.data());
break;
+ case MessageType::ACTORS_STATUS:
+ assert_msg_size("ACTORS_STATUS", s_mc_message_t);
+ handle_actors_status();
+ break;
+
default:
xbt_die("Received unexpected message %s (%i)", to_c_str(message->type), static_cast<int>(message->type));
break;
void AppSide::ignore_memory(void* addr, std::size_t size) const
{
+ if (not MC_is_active())
+ return;
+
s_mc_message_ignore_memory_t message;
message.type = MessageType::IGNORE_MEMORY;
message.addr = (std::uintptr_t)addr;
void AppSide::ignore_heap(void* address, std::size_t size) const
{
+ if (not MC_is_active())
+ return;
+
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
s_mc_message_ignore_heap_t message;
void AppSide::unignore_heap(void* address, std::size_t size) const
{
+ if (not MC_is_active())
+ return;
+
s_mc_message_ignore_memory_t message;
message.type = MessageType::UNIGNORE_HEAP;
message.addr = (std::uintptr_t)address;
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");
}
+/** Register a stack in the model checker
+ *
+ * The stacks are allocated in the heap. The MC handle them specifically
+ * when we analyze/compare the content of the heap so it must be told where
+ * they are with this function.
+ */
void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context) const
{
+ if (not MC_is_active())
+ return;
+
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
s_stack_region_t region;
