Sanitize how we know the current MC mode

This can be either NONE, AppSide, CheckerSide or Replay.

Also, further reduce how often we use the mc_model_checker singleton

diff --git a/src/mc/explo/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp
index 00debdc..f1525fe 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::cfg_do_model_check = true;
+  simgrid::mc::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 c400422..c21dc14 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -9,6 +9,7 @@
 #include "src/kernel/activity/MutexImpl.hpp"
 #include "src/kernel/actor/SimcallObserver.hpp"
 #include "src/mc/mc.h"
+#include "src/mc/mc_config.hpp"
 #include "src/mc/mc_replay.hpp"
 
 #if SIMGRID_HAVE_MC
@@ -53,7 +54,8 @@ void execute_actors()
 bool actor_is_enabled(kernel::actor::ActorImpl* actor)
 {
 #if SIMGRID_HAVE_MC
-  xbt_assert(mc_model_checker == nullptr, "This should be called from the client side");
+  xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+             "This should be called from the client side");
 #endif
 
   // Now, we are in the client app, no need for remote memory reading.
@@ -75,7 +77,8 @@ bool actor_is_enabled(kernel::actor::ActorImpl* actor)
 bool request_is_visible(const kernel::actor::Simcall* req)
 {
 #if SIMGRID_HAVE_MC
-  xbt_assert(mc_model_checker == nullptr, "This should be called from the client side");
+  xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+             "This should be called from the client side");
 #endif
   if (req->observer_ == nullptr)
     return false;

diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp
index f75d35a..c257a76 100644 (file)
--- a/src/mc/mc_client_api.cpp
+++ b/src/mc/mc_client_api.cpp
@@ -18,7 +18,8 @@
 int MC_random(int min, int max)
 {
 #if SIMGRID_HAVE_MC
-  xbt_assert(mc_model_checker == nullptr);
+  xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+             "This should be called from the client side");
 #endif
   if (not MC_is_active() && not MC_record_replay_is_active()) { // no need to do a simcall in this case
     static simgrid::xbt::random::XbtRandom prng;
@@ -32,8 +33,8 @@ void MC_assert(int prop)
 {
   // Cannot used xbt_assert here, or it would be an infinite recursion.
 #if SIMGRID_HAVE_MC
-  if (mc_model_checker != nullptr)
-    xbt_die("This should be called from the client side");
+  xbt_assert(simgrid::mc::model_checking_mode != simgrid::mc::ModelCheckingMode::CHECKER_SIDE,
+             "This should be called from the client side");
   if (not prop) {
     if (MC_is_active())
       simgrid::mc::AppSide::get()->report_assertion_failure();
@@ -48,13 +49,15 @@ void MC_assert(int prop)
 
 int MC_is_active()
 {
-  return simgrid::mc::cfg_do_model_check;
+  return simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::APP_SIDE ||
+         simgrid::mc::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(mc_model_checker == nullptr);
+  xbt_assert(simgrid::mc::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
 }
@@ -62,7 +65,8 @@ 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(mc_model_checker == nullptr);
+  xbt_assert(simgrid::mc::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
 }
@@ -70,7 +74,8 @@ void MC_ignore(void* addr, size_t size)
 void MC_ignore_heap(void *address, size_t size)
 {
 #if SIMGRID_HAVE_MC
-  xbt_assert(mc_model_checker == nullptr);
+  xbt_assert(simgrid::mc::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
 }
@@ -78,7 +83,8 @@ void MC_ignore_heap(void *address, size_t size)
 void MC_unignore_heap(void* address, size_t size)
 {
 #if SIMGRID_HAVE_MC
-  xbt_assert(mc_model_checker == nullptr);
+  xbt_assert(simgrid::mc::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 ad0fe22..3416d5c 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -14,7 +14,7 @@
 
 XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(xbt_cfg);
 
-bool simgrid::mc::cfg_do_model_check = false;
+simgrid::mc::ModelCheckingMode simgrid::mc::model_checking_mode = simgrid::mc::ModelCheckingMode::NONE;
 
 static void _mc_cfg_cb_check(const char* spec, bool more_check = true)
 {
@@ -31,7 +31,15 @@ static void _mc_cfg_cb_check(const char* spec, bool more_check = true)
 /* Replay (this part is enabled even if MC it disabled) */
 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) { MC_record_path() = value; }};
+    [](std::string_view value) {
+      xbt_assert(simgrid::mc::model_checking_mode == simgrid::mc::ModelCheckingMode::NONE ||
+                     simgrid::mc::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;
+      MC_record_path()                 = value;
+    }};
 
 #if SIMGRID_HAVE_MC
 simgrid::config::Flag<bool> _sg_mc_timeout{

diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp
index eaf2e20..a900f7c 100644 (file)
--- a/src/mc/mc_config.hpp
+++ b/src/mc/mc_config.hpp
@@ -11,7 +11,8 @@
 /********************************** Configuration of MC **************************************/
 namespace simgrid::mc {
 bool cfg_use_DPOR(); // "model-check/reduction" == "DPOR"
-extern XBT_PUBLIC bool cfg_do_model_check;
+XBT_DECLARE_ENUM_CLASS(ModelCheckingMode, NONE, APP_SIDE, CHECKER_SIDE, REPLAY);
+extern XBT_PUBLIC ModelCheckingMode model_checking_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 036fd29..b62e060 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -45,7 +45,7 @@ AppSide* AppSide::initialize()
   if (instance_)
     return instance_.get();
 
-  simgrid::mc::cfg_do_model_check = true;
+  simgrid::mc::model_checking_mode = ModelCheckingMode::APP_SIDE;
 
   setvbuf(stdout, nullptr, _IOLBF, 0);