[mc] Disable soft-dirty page tracking by default

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

diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index bd6c7e2..b5f11e3 100644 (file)
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -602,6 +602,18 @@ void sg_config_init(int *argc, char **argv)
                      xbt_cfgelm_int, 1, 1, _mc_cfg_cb_checkpoint, NULL);
     xbt_cfg_setdefault_int(_sg_cfg_set, "model-check/checkpoint", 0);
 
+    /* do stateful model-checking */
+    xbt_cfg_register(&_sg_cfg_set, "model-check/sparse-checkpoint",
+                     "Use sparse per-page snapshots.",
+                     xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_sparse_checkpoint, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/sparse-checkpoint", "no");
+
+    /* do stateful model-checking */
+    xbt_cfg_register(&_sg_cfg_set, "model-check/soft-dirty",
+                     "Use sparse per-page snapshots.",
+                     xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_soft_dirty, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/soft-dirty", "no");
+
     /* do liveness model-checking */
     xbt_cfg_register(&_sg_cfg_set, "model-check/property",
                      "Specify the name of the file containing the property. It must be the result of the ltl2ba program.",
@@ -765,6 +777,11 @@ void sg_config_init(int *argc, char **argv)
                      xbt_cfgelm_boolean, 1, 1, NULL, NULL);
     xbt_cfg_setdefault_boolean(_sg_cfg_set, "smpi/display_timing", "no");
 
+    xbt_cfg_register(&_sg_cfg_set, "smpi/simulate_computation",
+                     "Boolean indicating whether the computational part of the simulated application should be simulated.",
+                     xbt_cfgelm_boolean, 1, 1, NULL, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "smpi/simulate_computation", "yes");
+
     xbt_cfg_register(&_sg_cfg_set, "smpi/use_shared_malloc",
                      "Boolean indicating whether we should use shared memory when using SMPI_SHARED_MALLOC. Allows user to disable it for debug purposes.",
                      xbt_cfgelm_boolean, 1, 1, NULL, NULL);
@@ -819,10 +836,12 @@ void sg_config_init(int *argc, char **argv)
                      "Small messages timings (MPI_Recv minimum time for small messages)",
                      xbt_cfgelm_string, 1, 1, NULL, NULL);
     xbt_cfg_setdefault_string(_sg_cfg_set, "smpi/or", "1:0:0:0:0");
+
     xbt_cfg_register(&_sg_cfg_set, "smpi/iprobe",
                      "Minimum time to inject inside a call to MPI_Iprobe",
                      xbt_cfgelm_double, 1, 1, NULL, NULL);
     xbt_cfg_setdefault_double(_sg_cfg_set, "smpi/iprobe", 1e-4);
+
     xbt_cfg_register(&_sg_cfg_set, "smpi/coll_selector",
                      "Which collective selector to use",
                      xbt_cfgelm_string, 1, 1, NULL, NULL);