From: Martin Quinson Date: Sat, 1 Apr 2023 21:45:32 +0000 (+0200) Subject: Ignore empty replay path + hide a global (to avoid init fiasco) X-Git-Tag: v3.34~224 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/cfa35c4fa9a6bcfa6aa8f8cf21da6ab292ea21ad Ignore empty replay path + hide a global (to avoid init fiasco) I was observing that the model_checking_mode global did not had the same value when compiling with or without optimizations. Maybe I had a sort of race condition on model_checking_mode during initialization, or maybe the config element of the replay path was either called before or after the initialization of the library, thus replacing the model_checking_mode to REPLAY even if it was supposed to be APP_SIDE in my case. It's fixed now, but I'm not completely sure of which of these change was the right one (probably the replay path). Both seem legit, so commit both. --- diff --git a/src/kernel/EngineImpl.cpp b/src/kernel/EngineImpl.cpp index a5b2d5718e..2404648864 100644 --- a/src/kernel/EngineImpl.cpp +++ b/src/kernel/EngineImpl.cpp @@ -14,6 +14,7 @@ #include "src/kernel/resource/profile/Profile.hpp" #include "src/kernel/xml/platf.hpp" #include "src/mc/mc.h" +#include "src/mc/mc_config.hpp" #include "src/mc/mc_record.hpp" #include "src/mc/mc_replay.hpp" #include "src/simgrid/math_utils.h" @@ -604,6 +605,9 @@ void EngineImpl::run(double max_date) { seal_platform(); + XBT_DEBUG("Running the main loop until t=%.3f in mode %s", max_date, + to_c_str(simgrid::mc::get_model_checking_mode())); + if (MC_is_active()) { #if SIMGRID_HAVE_MC mc::AppSide::get()->main_loop(); diff --git a/src/mc/explo/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp index 700c4b9b58..5d973689af 100644 --- a/src/mc/explo/simgrid_mc.cpp +++ b/src/mc/explo/simgrid_mc.cpp @@ -21,7 +21,7 @@ int main(int argc, char** argv) xbt_assert(argc >= 2, "Missing arguments"); // Currently, we need this before sg_config_init: - simgrid::mc::model_checking_mode = simgrid::mc::ModelCheckingMode::CHECKER_SIDE; + simgrid::mc::set_model_checking_mode(simgrid::mc::ModelCheckingMode::CHECKER_SIDE); // The initialization function can touch argv. // We make a copy of argv before modifying it in order to pass the original value to the model-checked application: diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 8d8b66e985..6e4ecf107b 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -12,8 +12,6 @@ #include "src/mc/mc.h" #include "src/mc/mc_config.hpp" #include "src/mc/mc_replay.hpp" -/*#include "src/mc/api/RemoteApp.hpp" -#include "src/mc/remote/AppSide.hpp"*/ #if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/sosp/RemoteProcessMemory.hpp" @@ -53,7 +51,7 @@ void execute_actors() */ bool actor_is_enabled(kernel::actor::ActorImpl* actor) { - xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, + xbt_assert(get_model_checking_mode() != ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); // Now, we are in the client app, no need for remote memory reading. @@ -74,7 +72,7 @@ bool actor_is_enabled(kernel::actor::ActorImpl* actor) */ bool request_is_visible(const kernel::actor::Simcall* req) { - xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, + xbt_assert(get_model_checking_mode() != ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); if (req->observer_ == nullptr) diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp index 57e28cfb46..04967a426d 100644 --- a/src/mc/mc_client_api.cpp +++ b/src/mc/mc_client_api.cpp @@ -17,7 +17,7 @@ int MC_random(int min, int max) { - xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, + xbt_assert(simgrid::mc::get_model_checking_mode() != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); if (not MC_is_active() && not MC_record_replay_is_active()) { // no need to do a simcall in this case @@ -31,7 +31,7 @@ int MC_random(int min, int max) void MC_assert(int prop) { // Cannot used xbt_assert here, or it would be an infinite recursion. - xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, + xbt_assert(simgrid::mc::get_model_checking_mode() != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); #if SIMGRID_HAVE_MC if (not prop) { @@ -48,14 +48,14 @@ void MC_assert(int prop) int MC_is_active() { - return simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::APP_SIDE || - simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::CHECKER_SIDE; + return simgrid::mc::get_model_checking_mode() == simgrid::mc::ModelCheckingMode::APP_SIDE || + simgrid::mc::get_model_checking_mode() == simgrid::mc::ModelCheckingMode::CHECKER_SIDE; } void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value) { #if SIMGRID_HAVE_MC - xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, + xbt_assert(simgrid::mc::get_model_checking_mode() != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); simgrid::mc::AppSide::get()->declare_symbol(name, value); #endif @@ -64,7 +64,7 @@ void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value) void MC_ignore(void* addr, size_t size) { #if SIMGRID_HAVE_MC - xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, + xbt_assert(simgrid::mc::get_model_checking_mode() != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); simgrid::mc::AppSide::get()->ignore_memory(addr, size); #endif @@ -73,7 +73,7 @@ void MC_ignore(void* addr, size_t size) void MC_ignore_heap(void *address, size_t size) { #if SIMGRID_HAVE_MC - xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, + xbt_assert(simgrid::mc::get_model_checking_mode() != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); simgrid::mc::AppSide::get()->ignore_heap(address, size); #endif @@ -82,7 +82,7 @@ void MC_ignore_heap(void *address, size_t size) void MC_unignore_heap(void* address, size_t size) { #if SIMGRID_HAVE_MC - xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, + xbt_assert(simgrid::mc::get_model_checking_mode() != simgrid::mc::ModelCheckingMode::CHECKER_SIDE, "This should be called from the client side"); simgrid::mc::AppSide::get()->unignore_heap(address, size); #endif diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index a75b8b6778..e182f50540 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -14,7 +14,15 @@ XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(xbt_cfg); -simgrid::mc::ModelCheckingMode simgrid::mc::model_checking_mode = simgrid::mc::ModelCheckingMode::NONE; +static simgrid::mc::ModelCheckingMode model_checking_mode = simgrid::mc::ModelCheckingMode::NONE; +simgrid::mc::ModelCheckingMode simgrid::mc::get_model_checking_mode() +{ + return model_checking_mode; +} +void simgrid::mc::set_model_checking_mode(simgrid::mc::ModelCheckingMode mode) +{ + model_checking_mode = mode; +} static void _mc_cfg_cb_check(const char* spec, bool more_check = true) { @@ -28,12 +36,14 @@ static void _mc_cfg_cb_check(const char* spec, bool more_check = true) simgrid::config::Flag _sg_mc_record_path{ "model-check/replay", "Model-check path to replay (as reported by SimGrid when a violation is reported)", "", [](std::string_view value) { - xbt_assert(value.empty() || simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::NONE || - simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::REPLAY, + if (value.empty()) // Ignore default value + return; + xbt_assert(simgrid::mc::get_model_checking_mode() == simgrid::mc::ModelCheckingMode::NONE || + simgrid::mc::get_model_checking_mode() == simgrid::mc::ModelCheckingMode::REPLAY, "Specifying a MC replay path is not allowed when running the model-checker in mode %s. " "Either remove the model-check/replay parameter, or execute your code out of simgrid-mc.", - to_c_str(simgrid::mc::model_checking_mode)); - simgrid::mc::model_checking_mode = simgrid::mc::ModelCheckingMode::REPLAY; + to_c_str(simgrid::mc::get_model_checking_mode())); + simgrid::mc::set_model_checking_mode(simgrid::mc::ModelCheckingMode::REPLAY); MC_record_path() = value; }}; diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp index da11497178..64acccc142 100644 --- a/src/mc/mc_config.hpp +++ b/src/mc/mc_config.hpp @@ -12,7 +12,8 @@ namespace simgrid::mc { bool cfg_use_DPOR(); // "model-check/reduction" == "DPOR" XBT_DECLARE_ENUM_CLASS(ModelCheckingMode, NONE, APP_SIDE, CHECKER_SIDE, REPLAY); -extern XBT_PUBLIC ModelCheckingMode model_checking_mode; +XBT_PUBLIC ModelCheckingMode get_model_checking_mode(); +XBT_PUBLIC void set_model_checking_mode(ModelCheckingMode mode); }; extern XBT_PUBLIC simgrid::config::Flag _sg_mc_buffering; diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index 992df22477..3c5b688f19 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -43,13 +43,15 @@ std::unique_ptr AppSide::instance_; AppSide* AppSide::get() { // Only initialize the MC world once - if (instance_) + if (instance_ != nullptr) return instance_.get(); - if (not std::getenv(MC_ENV_SOCKET_FD)) // We are not in MC mode: don't initialize the MC world + if (std::getenv(MC_ENV_SOCKET_FD) == nullptr) // We are not in MC mode: don't initialize the MC world return nullptr; - simgrid::mc::model_checking_mode = ModelCheckingMode::APP_SIDE; + XBT_DEBUG("Initialize the MC world. MC_NEED_PTRACE=%s", std::getenv("MC_NEED_PTRACE")); + + simgrid::mc::set_model_checking_mode(ModelCheckingMode::APP_SIDE); setvbuf(stdout, nullptr, _IOLBF, 0); @@ -176,6 +178,8 @@ void AppSide::handle_fork(const s_mc_message_int_t* msg) answer.type = MessageType::FORK_REPLY; answer.value = getpid(); xbt_assert(channel_.send(answer) == 0, "Could not send response to WAIT_CHILD_REPLY: %s", strerror(errno)); + } else { + XBT_DEBUG("App %d forks subprocess %d.", getpid(), pid); } } void AppSide::handle_wait_child(const s_mc_message_int_t* msg) diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp index ee2f858ac6..0d5778af4b 100644 --- a/src/mc/remote/CheckerSide.cpp +++ b/src/mc/remote/CheckerSide.cpp @@ -176,6 +176,8 @@ void CheckerSide::setup_events(bool socket_only) /* When this constructor is called, no other checkerside exists */ CheckerSide::CheckerSide(const std::vector& args, bool need_memory_info) : running_(true) { + XBT_DEBUG("Create a CheckerSide. Needs_meminfo: %s", need_memory_info ? "YES" : "no"); + // Create an AF_LOCAL socketpair used for exchanging messages between the model-checker process (ancestor) // and the application process (child) int sockets[2]; @@ -438,7 +440,8 @@ void CheckerSide::handle_dead_child(int status) void CheckerSide::handle_waitpid() { - XBT_DEBUG("Check for wait event"); + XBT_DEBUG("%d checks for wait event. %s", getpid(), + child_checker_ == nullptr ? "Wait directly." : "Ask our proxy to wait for its child."); if (child_checker_ == nullptr) { // Wait directly int status;