[mc] Config to disable soft-dirty page tracking --cfg=model-check/soft-dirty:yes

It is here mostly to test the effect on soft-dirty page tracking on
the performance of the simulator. It might be removed in the future
once we will be certain that soft-dirty page tracking does not have a
significant negative impact on some workloads.

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index a49184d..c8a24f4 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -39,6 +39,7 @@ SG_BEGIN_DECL()
 extern int _sg_do_model_check;
 extern int _sg_mc_checkpoint;
 extern int _sg_mc_sparse_checkpoint;
+extern int _sg_mc_soft_dirty;
 extern char* _sg_mc_property_file;
 extern int _sg_mc_timeout;
 extern int _sg_mc_hash;
@@ -59,6 +60,7 @@ extern void *maestro_stack_end;
 void _mc_cfg_cb_reduce(const char *name, int pos);
 void _mc_cfg_cb_checkpoint(const char *name, int pos);
 void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos);
+void _mc_cfg_cb_soft_dirty(const char *name, int pos);
 void _mc_cfg_cb_property(const char *name, int pos);
 void _mc_cfg_cb_timeout(const char *name, int pos);
 void _mc_cfg_cb_hash(const char *name, int pos);

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 883f900..722e3d5 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -585,7 +585,7 @@ mc_snapshot_t MC_take_snapshot(int num_state)
 
   /* Save the std heap and the writable mapped pages of libsimgrid and binary */
   MC_get_memory_regions(snapshot);
-  if (_sg_mc_sparse_checkpoint) {
+  if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) {
     mc_softdirty_reset();
   }
 
@@ -631,7 +631,7 @@ void MC_restore_snapshot(mc_snapshot_t snapshot)
   }
 
   MC_snapshot_ignore_restore(snapshot);
-  if (_sg_mc_sparse_checkpoint) {
+  if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) {
     mc_softdirty_reset();
   }
   mc_model_checker->parent_snapshot = snapshot;

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index b22364d..1359cf3 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -30,6 +30,7 @@ e_mc_reduce_t mc_reduce_kind = e_mc_reduce_unset;
 int _sg_do_model_check = 0;
 int _sg_mc_checkpoint = 0;
 int _sg_mc_sparse_checkpoint = 0;
+int _sg_mc_soft_dirty = 1;
 char *_sg_mc_property_file = NULL;
 int _sg_mc_timeout = 0;
 int _sg_mc_hash = 0;
@@ -76,6 +77,13 @@ void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos) {
   _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
+void _mc_cfg_cb_soft_dirty(const char *name, int pos) {
+  if (_sg_cfg_init_status && !_sg_do_model_check) {
+    xbt_die("You are specifying a soft dirty value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+  }
+  _sg_mc_soft_dirty = xbt_cfg_get_boolean(_sg_cfg_set, name);
+}
+
 void _mc_cfg_cb_property(const char *name, int pos)
 {
   if (_sg_cfg_init_status && !_sg_do_model_check) {

diff --git a/src/mc/mc_page_snapshot.cpp b/src/mc/mc_page_snapshot.cpp
index c049b7d..4a964ac 100644 (file)
--- a/src/mc/mc_page_snapshot.cpp
+++ b/src/mc/mc_page_snapshot.cpp
@@ -151,7 +151,7 @@ mc_mem_region_t mc_region_new_sparse(int type, void *start_addr, size_t size, mc
   size_t page_count = mc_page_count(size);
 
   uint64_t* pagemap = NULL;
-  if (mc_model_checker->parent_snapshot) {
+  if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot) {
       pagemap = (uint64_t*) mmalloc_no_memset((xbt_mheap_t) mc_heap, sizeof(uint64_t) * page_count);
       mc_read_pagemap(pagemap, mc_page_number(NULL, start_addr), page_count);
   }
@@ -175,7 +175,7 @@ void mc_region_restore_sparse(mc_mem_region_t reg, mc_mem_region_t ref_reg)
   uint64_t* pagemap = NULL;
 
   // Read soft-dirty bits if necessary in order to know which pages have changed:
-  if (mc_model_checker->parent_snapshot) {
+  if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot) {
     pagemap = (uint64_t*) mmalloc_no_memset((xbt_mheap_t) mc_heap, sizeof(uint64_t) * page_count);
     mc_read_pagemap(pagemap, mc_page_number(NULL, reg->start_addr), page_count);
   }

diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index d9dea55..65878a0 100644 (file)
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -608,6 +608,12 @@ void sg_config_init(int *argc, char **argv)
                      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", "yes");
+
     /* 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.",