Convert MC config parameters to C++ API, and move their definitions to mc_config...

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 1d19d06..3ca696b 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -96,7 +96,7 @@ void ModelChecker::start()
 
   process_->init();
 
-  if (not _sg_mc_dot_output_file.empty())
+  if (not _sg_mc_dot_output_file.get().empty())
     MC_init_dot_output();
 
   setup_ignore();

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 0553d89..2190ad0 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -122,7 +122,7 @@ void Session::logState()
 {
   mc_model_checker->getChecker()->logState();
 
-  if (not _sg_mc_dot_output_file.empty()) {
+  if (not _sg_mc_dot_output_file.get().empty()) {
     fprintf(dot_output, "}\n");
     fclose(dot_output);
   }

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index c1afd7a..ee00b66 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -345,8 +345,8 @@ void LivenessChecker::backtrack()
 
 void LivenessChecker::run()
 {
-  XBT_INFO("Check the liveness property %s", _sg_mc_property_file.c_str());
-  MC_automaton_load(_sg_mc_property_file.c_str());
+  XBT_INFO("Check the liveness property %s", _sg_mc_property_file.get().c_str());
+  MC_automaton_load(_sg_mc_property_file.get().c_str());
 
   XBT_DEBUG("Starting the liveness algorithm");
   simgrid::mc::session->initialize();

diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp
index 13431d3..a6e3159 100644 (file)
--- a/src/mc/checker/simgrid_mc.cpp
+++ b/src/mc/checker/simgrid_mc.cpp
@@ -43,7 +43,7 @@ static std::unique_ptr<simgrid::mc::Checker> createChecker(simgrid::mc::Session&
 {
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
     return std::unique_ptr<simgrid::mc::Checker>(simgrid::mc::createCommunicationDeterminismChecker(session));
-  else if (_sg_mc_property_file.empty())
+  else if (_sg_mc_property_file.get().empty())
     return std::unique_ptr<simgrid::mc::Checker>(simgrid::mc::createSafetyChecker(session));
   else
     return std::unique_ptr<simgrid::mc::Checker>(simgrid::mc::createLivenessChecker(session));

diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp
index 11ef27c..bd1a8d7 100644 (file)
--- a/src/mc/mc_checkpoint.cpp
+++ b/src/mc/mc_checkpoint.cpp
@@ -519,7 +519,7 @@ static std::vector<s_fd_infos_t> get_current_fds(pid_t pid)
     // If dot_output enabled, do not handle the corresponding file
     if (dot_output != nullptr) {
       std::string link_basename = simgrid::xbt::Path(link).getBasename();
-      if (link_basename == _sg_mc_dot_output_file)
+      if (link_basename == _sg_mc_dot_output_file.get())
         continue;
     }
 
@@ -561,7 +561,7 @@ std::shared_ptr<simgrid::mc::Snapshot> take_snapshot(int num_state)
 
   snapshot->to_ignore = mc_model_checker->process().ignored_heap();
 
-  if (_sg_mc_max_visited_states > 0 || not _sg_mc_property_file.empty()) {
+  if (_sg_mc_max_visited_states > 0 || not _sg_mc_property_file.get().empty()) {
     snapshot->stacks = take_snapshot_stacks(snapshot.get());
     if (_sg_mc_hash)
       snapshot->hash = simgrid::mc::hash(*snapshot);

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index 5acdd2b..fbe4312 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -34,8 +34,6 @@ simgrid::mc::ReductionMode reduction_mode = simgrid::mc::ReductionMode::unset;
 #define _sg_do_model_check 0
 #endif
 
-int _sg_mc_timeout = 0;
-
 static void _mc_cfg_cb_check(const char* spec, bool more_check = true)
 {
   if (_sg_cfg_init_status && not _sg_do_model_check && more_check)
@@ -44,123 +42,103 @@ static void _mc_cfg_cb_check(const char* spec, bool more_check = true)
             spec);
 }
 
-void _mc_cfg_cb_timeout(const char *name)
-{
-  _mc_cfg_cb_check("value to enable/disable timeout for wait requests", MC_record_path.empty());
+/* Replay (this part is enabled even if MC it disabled) */
+static 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)", "",
+    [](const std::string& value) { MC_record_path = value; }};
 
-  _sg_mc_timeout = xbt_cfg_get_boolean(name);
-}
+simgrid::config::Flag<bool> _sg_mc_timeout{
+    "model-check/timeout", "Whether to enable timeouts for wait requests", false,
+    [](bool) { _mc_cfg_cb_check("value to enable/disable timeout for wait requests", MC_record_path.empty()); }};
 
 #if SIMGRID_HAVE_MC
 int _sg_do_model_check = 0;
-int _sg_do_model_check_record = 0;
-int _sg_mc_checkpoint = 0;
-int _sg_mc_sparse_checkpoint = 0;
-int _sg_mc_ksm = 0;
-std::string _sg_mc_property_file;
-int _sg_mc_hash = 0;
-int _sg_mc_max_depth = 1000;
 int _sg_mc_max_visited_states = 0;
-std::string _sg_mc_dot_output_file;
-int _sg_mc_comms_determinism = 0;
-int _sg_mc_send_determinism = 0;
-int _sg_mc_snapshot_fds = 0;
-int _sg_mc_termination = 0;
-
-void _mc_cfg_cb_reduce(const char *name)
-{
-  _mc_cfg_cb_check("reduction strategy");
-
-  std::string val = xbt_cfg_get_string(name);
-  if (val == "none")
-    simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
-  else if (val == "dpor")
-    simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor;
-  else
-    xbt_die("configuration option %s can only take 'none' or 'dpor' as a value", name);
-}
-
-void _mc_cfg_cb_checkpoint(const char *name)
-{
-  _mc_cfg_cb_check("checkpointing value");
-
-  _sg_mc_checkpoint = xbt_cfg_get_int(name);
-}
-
-void _mc_cfg_cb_sparse_checkpoint(const char *name) {
-  _mc_cfg_cb_check("checkpointing value");
-
-  _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(name);
-}
-
-void _mc_cfg_cb_ksm(const char *name)
-{
-  _mc_cfg_cb_check("KSM value");
-
-  _sg_mc_ksm = xbt_cfg_get_boolean(name);
-}
-
-void _mc_cfg_cb_property(const char *name)
-{
-  _mc_cfg_cb_check("property");
-
-  _sg_mc_property_file = xbt_cfg_get_string(name);
-}
-
-void _mc_cfg_cb_hash(const char *name)
-{
-  _mc_cfg_cb_check("value to enable/disable the use of global hash to speedup state comparaison");
-
-  _sg_mc_hash = xbt_cfg_get_boolean(name);
-}
-
-void _mc_cfg_cb_snapshot_fds(const char *name)
-{
-  _mc_cfg_cb_check("value to enable/disable the use of FD snapshotting");
-
-  _sg_mc_snapshot_fds = xbt_cfg_get_boolean(name);
-}
-
-void _mc_cfg_cb_max_depth(const char *name)
-{
-  _mc_cfg_cb_check("max depth value");
-
-  _sg_mc_max_depth = xbt_cfg_get_int(name);
-}
-
-void _mc_cfg_cb_visited(const char *name)
-{
-  _mc_cfg_cb_check("number of stored visited states");
-
-  _sg_mc_max_visited_states = xbt_cfg_get_int(name);
-}
-
-void _mc_cfg_cb_dot_output(const char *name)
-{
-  _mc_cfg_cb_check("file name for a dot output of graph state");
 
-  _sg_mc_dot_output_file = xbt_cfg_get_string(name);
-}
-
-void _mc_cfg_cb_comms_determinism(const char *name)
-{
-  _mc_cfg_cb_check("value to enable/disable the detection of determinism in the communications schemes");
-
-  _sg_mc_comms_determinism = xbt_cfg_get_boolean(name);
-}
-
-void _mc_cfg_cb_send_determinism(const char *name)
-{
-  _mc_cfg_cb_check("value to enable/disable the detection of send-determinism in the communications schemes");
-
-  _sg_mc_send_determinism = xbt_cfg_get_boolean(name);
-}
-
-void _mc_cfg_cb_termination(const char *name)
-{
-  _mc_cfg_cb_check("value to enable/disable the detection of non progressive cycles");
-
-  _sg_mc_termination = xbt_cfg_get_boolean(name);
-}
+simgrid::config::Flag<bool> _sg_do_model_check_record{"model-check/record", "Record the model-checking paths", false};
+
+simgrid::config::Flag<int> _sg_mc_checkpoint{
+    "model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking "
+                              "(default: 0 => stateless verification). If value=1, one checkpoint is saved for each "
+                              "step => faster verification, but huge memory consumption; higher values are good "
+                              "compromises between speed and memory consumption.",
+    0, [](int) { _mc_cfg_cb_check("checkpointing value"); }};
+
+simgrid::config::Flag<bool> _sg_mc_sparse_checkpoint{"model-check/sparse-checkpoint", "Use sparse per-page snapshots.",
+                                                     false, [](bool) { _mc_cfg_cb_check("checkpointing value"); }};
+
+simgrid::config::Flag<bool> _sg_mc_ksm{"model-check/ksm", "Kernel same-page merging", false,
+                                       [](bool) { _mc_cfg_cb_check("KSM value"); }};
+
+simgrid::config::Flag<std::string> _sg_mc_property_file{
+    "model-check/property", "Name of the file containing the property, as formatted by the ltl2ba program.", "",
+    [](const std::string&) { _mc_cfg_cb_check("property"); }};
+
+simgrid::config::Flag<bool> _sg_mc_comms_determinism{
+    "model-check/communications-determinism",
+    {"model-check/communications_determinism"},
+    "Whether to enable the detection of communication determinism",
+    false,
+    [](bool) {
+      _mc_cfg_cb_check("value to enable/disable the detection of determinism in the communications schemes");
+    }};
+
+simgrid::config::Flag<bool> _sg_mc_send_determinism{
+    "model-check/send-determinism",
+    {"model-check/send_determinism"},
+    "Enable/disable the detection of send-determinism in the communications schemes",
+    false,
+    [](bool) {
+      _mc_cfg_cb_check("value to enable/disable the detection of send-determinism in the communications schemes");
+    }};
+
+static simgrid::config::Flag<std::string> _sg_mc_reduce{
+    "model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", "dpor",
+    [](const std::string& value) {
+      _mc_cfg_cb_check("reduction strategy");
+
+      if (value == "none")
+        simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
+      else if (value == "dpor")
+        simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor;
+      else
+        xbt_die("configuration option model-check/reduction can only take 'none' or 'dpor' as a value");
+    }};
+
+simgrid::config::Flag<bool> _sg_mc_hash{
+    "model-check/hash", "Whether to enable state hash for state comparison (experimental)", false,
+    [](bool) { _mc_cfg_cb_check("value to enable/disable the use of global hash to speedup state comparaison"); }};
+
+simgrid::config::Flag<bool> _sg_mc_snapshot_fds{
+    "model-check/snapshot-fds",
+    {"model-check/snapshot_fds"},
+    "Whether file descriptors must be snapshoted (currently unusable)",
+    false,
+    [](bool) { _mc_cfg_cb_check("value to enable/disable the use of FD snapshotting"); }};
+
+simgrid::config::Flag<int> _sg_mc_max_depth{"model-check/max-depth",
+                                            {"model-check/max_depth"},
+                                            "Maximal exploration depth (default: 1000)",
+                                            1000,
+                                            [](int) { _mc_cfg_cb_check("max depth value"); }};
+
+static simgrid::config::Flag<int> _sg_mc_max_visited_states__{
+    "model-check/visited", "Specify the number of visited state stored for state comparison reduction. If value=5, the "
+                           "last 5 visited states are stored. If value=0 (the default), all states are stored.",
+    0, [](int value) {
+      _mc_cfg_cb_check("number of stored visited states");
+      _sg_mc_max_visited_states = value;
+    }};
+
+simgrid::config::Flag<std::string> _sg_mc_dot_output_file{
+    "model-check/dot-output",
+    {"model-check/dot_output"},
+    "Name of dot output file corresponding to graph state",
+    "",
+    [](const std::string&) { _mc_cfg_cb_check("file name for a dot output of graph state"); }};
+
+simgrid::config::Flag<bool> _sg_mc_termination{
+    "model-check/termination", "Whether to enable non progressive cycle detection", false,
+    [](bool) { _mc_cfg_cb_check("value to enable/disable the detection of non progressive cycles"); }};
 
 #endif

diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp
index 8f88805..0068a2c 100644 (file)
--- a/src/mc/mc_config.hpp
+++ b/src/mc/mc_config.hpp
@@ -6,38 +6,23 @@
 #ifndef MC_CONFIG_HPP
 #define MC_CONFIG_HPP
 
-#include <string>
+#include <xbt/config.hpp>
 
 /********************************** Configuration of MC **************************************/
 extern "C" XBT_PUBLIC int _sg_do_model_check;
-extern XBT_PRIVATE int _sg_do_model_check_record;
-extern XBT_PRIVATE int _sg_mc_checkpoint;
-extern XBT_PUBLIC int _sg_mc_sparse_checkpoint;
-extern XBT_PUBLIC int _sg_mc_ksm;
-extern XBT_PUBLIC std::string _sg_mc_property_file;
-extern XBT_PRIVATE int _sg_mc_timeout;
-extern XBT_PRIVATE int _sg_mc_hash;
-extern XBT_PRIVATE int _sg_mc_max_depth;
+extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_do_model_check_record;
+extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_checkpoint;
+extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_sparse_checkpoint;
+extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_ksm;
+extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_property_file;
+extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_comms_determinism;
+extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_send_determinism;
+extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_timeout;
+extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_hash;
+extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_snapshot_fds;
+extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_max_depth;
 extern "C" XBT_PUBLIC int _sg_mc_max_visited_states;
-extern XBT_PRIVATE std::string _sg_mc_dot_output_file;
-extern XBT_PUBLIC int _sg_mc_comms_determinism;
-extern XBT_PUBLIC int _sg_mc_send_determinism;
-extern XBT_PRIVATE int _sg_mc_snapshot_fds;
-extern XBT_PRIVATE int _sg_mc_termination;
-
-XBT_PRIVATE void _mc_cfg_cb_reduce(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_checkpoint(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_sparse_checkpoint(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_ksm(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_property(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_timeout(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_snapshot_fds(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_hash(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_max_depth(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_visited(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_dot_output(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_comms_determinism(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_send_determinism(const char* name);
-XBT_PRIVATE void _mc_cfg_cb_termination(const char* name);
+extern XBT_PRIVATE simgrid::config::Flag<std::string> _sg_mc_dot_output_file;
+extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_termination;
 
 #endif

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index c0fbaa3..ac4ccd4 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -76,7 +76,7 @@ FILE *dot_output = nullptr;
 
 void MC_init_dot_output()
 {
-  dot_output = fopen(_sg_mc_dot_output_file.c_str(), "w");
+  dot_output = fopen(_sg_mc_dot_output_file.get().c_str(), "w");
 
   if (dot_output == nullptr) {
     perror("Error open dot output file");

diff --git a/src/simgrid/sg_config.cpp b/src/simgrid/sg_config.cpp
index 5999898..afb483b 100644 (file)
--- a/src/simgrid/sg_config.cpp
+++ b/src/simgrid/sg_config.cpp
@@ -187,12 +187,6 @@ static void _sg_cfg_cb__network_model(const std::string& value)
   find_model_description(surf_network_model_description, value);
 }
 
-#if SIMGRID_HAVE_MC
-static void _sg_cfg_cb_model_check_record(const char *name) {
-  _sg_do_model_check_record = xbt_cfg_get_boolean(name);
-}
-#endif
-
 static void _sg_cfg_cb_contexts_parallel_mode(const std::string& mode_name)
 {
   if (mode_name == "posix") {
@@ -299,59 +293,6 @@ void sg_config_init(int *argc, char **argv)
                                                                         "default unless optim is set to lazy)",
                                      "no");
   simgrid::config::alias("network/maxmin-selective-update", {"network/maxmin_selective_update"});
-  /* Replay (this part is enabled even if MC it disabled) */
-  simgrid::config::bindFlag(MC_record_path, "model-check/replay",
-                            "Model-check path to replay (as reported by SimGrid when a violation is reported)");
-
-#if SIMGRID_HAVE_MC
-  /* do model-checking-record */
-  xbt_cfg_register_boolean("model-check/record", "no", _sg_cfg_cb_model_check_record,
-                           "Record the model-checking paths");
-
-  xbt_cfg_register_int("model-check/checkpoint", 0, _mc_cfg_cb_checkpoint,
-                       "Specify the amount of steps between checkpoints during stateful model-checking (default: 0 => "
-                       "stateless verification). "
-                       "If value=1, one checkpoint is saved for each step => faster verification, but huge memory "
-                       "consumption; higher values are good compromises between speed and memory consumption.");
-
-  xbt_cfg_register_boolean("model-check/sparse-checkpoint", "no", _mc_cfg_cb_sparse_checkpoint,
-                           "Use sparse per-page snapshots.");
-  xbt_cfg_register_boolean("model-check/ksm", "no", _mc_cfg_cb_ksm, "Kernel same-page merging");
-
-  xbt_cfg_register_string("model-check/property", "", _mc_cfg_cb_property,
-                          "Name of the file containing the property, as formatted by the ltl2ba program.");
-  xbt_cfg_register_boolean("model-check/communications-determinism", "no", _mc_cfg_cb_comms_determinism,
-                           "Whether to enable the detection of communication determinism");
-  simgrid::config::alias("model-check/communications-determinism", {"model-check/communications_determinism"});
-
-  xbt_cfg_register_boolean("model-check/send-determinism", "no", _mc_cfg_cb_send_determinism,
-                           "Enable/disable the detection of send-determinism in the communications schemes");
-  simgrid::config::alias("model-check/send-determinism", {"model-check/send_determinism"});
-
-  /* Specify the kind of model-checking reduction */
-  xbt_cfg_register_string("model-check/reduction", "dpor", _mc_cfg_cb_reduce,
-                          "Specify the kind of exploration reduction (either none or DPOR)");
-  xbt_cfg_register_boolean("model-check/timeout", "no", _mc_cfg_cb_timeout,
-                           "Whether to enable timeouts for wait requests");
-
-  xbt_cfg_register_boolean("model-check/hash", "no", _mc_cfg_cb_hash,
-                           "Whether to enable state hash for state comparison (experimental)");
-  xbt_cfg_register_boolean("model-check/snapshot-fds", "no", _mc_cfg_cb_snapshot_fds,
-                           "Whether file descriptors must be snapshoted (currently unusable)");
-  simgrid::config::alias("model-check/snapshot-fds", {"model-check/snapshot_fds"});
-  xbt_cfg_register_int("model-check/max-depth", 1000, _mc_cfg_cb_max_depth,
-                       "Maximal exploration depth (default: 1000)");
-  simgrid::config::alias("model-check/max-depth", {"model-check/max_depth"});
-  xbt_cfg_register_int("model-check/visited", 0, _mc_cfg_cb_visited,
-                       "Specify the number of visited state stored for state comparison reduction. If value=5, the "
-                       "last 5 visited states are stored. If value=0 (the default), all states are stored.");
-
-  xbt_cfg_register_string("model-check/dot-output", "", _mc_cfg_cb_dot_output,
-                          "Name of dot output file corresponding to graph state");
-  simgrid::config::alias("model-check/dot-output", {"model-check/dot_output"});
-  xbt_cfg_register_boolean("model-check/termination", "no", _mc_cfg_cb_termination,
-                           "Whether to enable non progressive cycle detection");
-#endif
 
   extern bool _sg_do_verbose_exit;
   simgrid::config::bindFlag(_sg_do_verbose_exit, "verbose-exit", "Activate the \"do nothing\" mode in Ctrl-C");