[mc] Initial support MC record/replay

[simgrid.git] / src / simgrid / sg_config.c

diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index f857766..89a7959 100644 (file)
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -20,6 +20,7 @@
 #include "simgrid/sg_config.h"
 #include "smpi/smpi_interface.h"
 #include "mc/mc.h"
+#include "mc/mc_record.h"
 #include "instr/instr.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(surf_config, surf,
@@ -368,10 +369,17 @@ static void _sg_cfg_cb__surf_path(const char *name, int pos)
 
 /* callback to decide if we want to use the model-checking */
 #include "xbt_modinter.h"
+
 #ifdef HAVE_MC
 extern int _sg_do_model_check;   /* this variable lives in xbt_main until I find a right location for it */
+extern int _sg_do_model_check_record;
 #endif
 
+static void _sg_cfg_cb_model_check_replay(const char *name, int pos)
+{
+  MC_record_path = xbt_cfg_get_string(_sg_cfg_set, name);
+}
+
 static void _sg_cfg_cb_model_check(const char *name, int pos)
 {
 #ifdef HAVE_MC
@@ -383,6 +391,17 @@ static void _sg_cfg_cb_model_check(const char *name, int pos)
 #endif
 }
 
+static void _sg_cfg_cb_model_check_record(const char *name, int pos)
+{
+#ifdef HAVE_MC
+  _sg_do_model_check_record = xbt_cfg_get_boolean(_sg_cfg_set, name);
+#else
+  if (xbt_cfg_get_boolean(_sg_cfg_set, name)) {
+    xbt_die("You tried to activate the model-checking record from the command line, but it was not compiled in. Change your settings in cmake, recompile and try again");
+  }
+#endif
+}
+
 extern int _sg_do_verbose_exit;
 
 static void _sg_cfg_cb_verbose_exit(const char *name, int pos)
@@ -603,6 +622,11 @@ void sg_config_init(int *argc, char **argv)
                      xbt_cfgelm_boolean, 1, 1, NULL, NULL);
     xbt_cfg_setdefault_boolean(_sg_cfg_set, "network/maxmin_selective_update", "no");
 
+    /* Replay (this part is enabled event if MC it disabled) */
+    xbt_cfg_register(&_sg_cfg_set, "model-check/replay",
+      "Uenable replay mode with the given path",
+      xbt_cfgelm_string, 0, 1, _sg_cfg_cb_model_check_replay, NULL);
+
 #ifdef HAVE_MC
     /* do model-checking */
     xbt_cfg_register(&_sg_cfg_set, "model-check",
@@ -610,6 +634,12 @@ void sg_config_init(int *argc, char **argv)
                      xbt_cfgelm_boolean, 1, 1, _sg_cfg_cb_model_check, NULL);
     xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check", "no");
 
+    /* do model-checking-record */
+    xbt_cfg_register(&_sg_cfg_set, "model-check/record",
+                     "Record the model-checking paths",
+                     xbt_cfgelm_boolean, 1, 1, _sg_cfg_cb_model_check_record, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/record", "no");
+
     /* do stateful model-checking */
     xbt_cfg_register(&_sg_cfg_set, "model-check/checkpoint",
                      "Specify the amount of steps between checkpoints during stateful model-checking (default: 0 => stateless verification). "