Centralize definitions for the name of environment variables used by the MC.

diff --git a/MANIFEST.in b/MANIFEST.in
index 85f70a9..be98527 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2226,6 +2226,7 @@ include src/mc/mc_base.hpp
 include src/mc/mc_client_api.cpp
 include src/mc/mc_config.cpp
 include src/mc/mc_config.hpp
+include src/mc/mc_environ.h
 include src/mc/mc_exit.hpp
 include src/mc/mc_forward.hpp
 include src/mc/mc_global.cpp

diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp
index ceac33e..124c413 100644 (file)
--- a/src/mc/explo/Exploration.cpp
+++ b/src/mc/explo/Exploration.cpp
@@ -5,6 +5,7 @@
 
 #include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_config.hpp"
+#include "src/mc/mc_environ.h"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
 
@@ -62,7 +63,7 @@ void Exploration::log_state()
     dot_output("}\n");
     fclose(dot_output_);
   }
-  if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")) {
+  if (getenv(MC_ENV_SYSTEM_STATISTICS)) {
     int ret = system("free");
     if (ret != 0)
       XBT_WARN("Call to system(free) did not return 0, but %d", ret);

diff --git a/src/mc/mc_environ.h b/src/mc/mc_environ.h
new file mode 100644 (file)
index 0000000..f285d65
--- /dev/null
+++ b/src/mc/mc_environ.h
@@ -0,0 +1,27 @@
+/* Copyright (c) 2023. 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. */
+
+#ifndef MC_ENVIRON_H
+#define MC_ENVIRON_H
+
+/* Define macros for the name of environment variables used by the MC.  Keep them in a separate file without any other
+ * includes, since it's also loaded from mmalloc.
+ */
+
+/** Environment variable name used to pass the communication socket.
+ *
+ * It is set by `simgrid-mc` to enable MC support in the children processes.
+ */
+#define MC_ENV_SOCKET_FD "SIMGRID_MC_SOCKET_FD"
+
+/** Environment variable name defined when ptrace(2) is used to control the MCed process.
+ */
+#define MC_ENV_NEED_PTRACE "MC_NEED_PTRACE"
+
+/** Environment variable used to request additional system statistics.
+ */
+#define MC_ENV_SYSTEM_STATISTICS "SIMGRID_MC_SYSTEM_STATISTICS"
+
+#endif

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 71d8414..18315d3 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -11,6 +11,7 @@
 #include "src/kernel/actor/SimcallObserver.hpp"
 #include "src/mc/mc_base.hpp"
 #include "src/mc/mc_config.hpp"
+#include "src/mc/mc_environ.h"
 #if SIMGRID_HAVE_STATEFUL_MC
 #include "src/mc/sosp/RemoteProcessMemory.hpp"
 #endif
@@ -49,7 +50,7 @@ AppSide* AppSide::get()
   if (std::getenv(MC_ENV_SOCKET_FD) == nullptr) // We are not in MC mode: don't initialize the MC world
     return nullptr;
 
-  XBT_DEBUG("Initialize the MC world. MC_NEED_PTRACE=%s", std::getenv("MC_NEED_PTRACE"));
+  XBT_DEBUG("Initialize the MC world. %s=%s", MC_ENV_NEED_PTRACE, std::getenv(MC_ENV_NEED_PTRACE));
 
   simgrid::mc::set_model_checking_mode(ModelCheckingMode::APP_SIDE);
 
@@ -63,7 +64,7 @@ AppSide* AppSide::get()
   instance_ = std::make_unique<simgrid::mc::AppSide>(fd);
 
   // Wait for the model-checker:
-  if (getenv("MC_NEED_PTRACE") != nullptr) {
+  if (getenv(MC_ENV_NEED_PTRACE) != nullptr) {
     errno = 0;
 #if defined __linux__
     ptrace(PTRACE_TRACEME, 0, nullptr, nullptr);

diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp
index dd29fc9..71850ec 100644 (file)
--- a/src/mc/remote/CheckerSide.cpp
+++ b/src/mc/remote/CheckerSide.cpp
@@ -5,6 +5,7 @@
 
 #include "src/mc/remote/CheckerSide.hpp"
 #include "src/mc/explo/Exploration.hpp"
+#include "src/mc/mc_environ.h"
 #include "xbt/config.hpp"
 #include "xbt/system_error.hpp"
 
@@ -56,7 +57,7 @@ XBT_ATTRIB_NORETURN static void run_child_process(int socket, const std::vector<
 
   setenv(MC_ENV_SOCKET_FD, std::to_string(socket).c_str(), 1);
   if (need_ptrace)
-    setenv("MC_NEED_PTRACE", "1", 1);
+    setenv(MC_ENV_NEED_PTRACE, "1", 1);
 
   /* Setup the tokenizer that parses the cfg:model-check/setenv parameter */
   using Tokenizer = boost::tokenizer<boost::char_separator<char>>;

diff --git a/src/xbt/mmalloc/mm_legacy.c b/src/xbt/mmalloc/mm_legacy.c
index 5cd89d5..fb22a59 100644 (file)
--- a/src/xbt/mmalloc/mm_legacy.c
+++ b/src/xbt/mmalloc/mm_legacy.c
@@ -7,7 +7,7 @@
 #define _GNU_SOURCE
 
 #include "mmprivate.h"
-
+#include "src/mc/mc_environ.h" // MC_ENV_SOCKET_FD
 #include <dlfcn.h>
 #include <math.h>
 #include <stdlib.h>

diff --git a/src/xbt/mmalloc/mmalloc.h b/src/xbt/mmalloc/mmalloc.h
index d3cdc24..7dff4e7 100644 (file)
--- a/src/xbt/mmalloc/mmalloc.h
+++ b/src/xbt/mmalloc/mmalloc.h
@@ -11,14 +11,6 @@
 
 #include "src/internal_config.h"
 
-/** Environment variable name used to pass the communication socket.
- *
- * It is set by `simgrid-mc` to enable MC support in the children processes.
- *
- * It is placed in this file so that it's visible from mmalloc and MC without sharing anythin of xbt in mmalloc
- */
-#define MC_ENV_SOCKET_FD "SIMGRID_MC_SOCKET_FD"
-
 #include <stdio.h>     /* for NULL */
 #include <sys/types.h> /* for size_t */
 

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 01e6e54..17b6a41 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -613,6 +613,7 @@ set(MC_SRC_STATEFUL
   src/mc/VisitedState.cpp
   src/mc/VisitedState.hpp
   src/mc/compare.cpp
+  src/mc/mc_environ.h
   src/mc/mc_exit.hpp
   src/mc/mc_forward.hpp
   src/mc/mc_private.hpp