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 a5b2d57..2404648 100644 (file)
--- 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 700c4b9..5d97368 100644 (file)
--- 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 8d8b66e..6e4ecf1 100644 (file)
--- 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 57e28cf..04967a4 100644 (file)
--- 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 a75b8b6..e182f50 100644 (file)
--- 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<std::string> _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 da11497..64acccc 100644 (file)
--- 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<std::string> _sg_mc_buffering;

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 992df22..3c5b688 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -43,13 +43,15 @@ std::unique_ptr<AppSide> 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 ee2f858..0d5778a 100644 (file)
--- 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<char*>& 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;