[mc] Bring back KSM (MADV_MERGEABLE) support

For KSM support, we allocate the memory for the snapshot regions
directly with mmap() instead of using malloc(). This way we can safely
mark them as MERGEABLE without impacting the heap at all.

Another solution would be to use posix_memalign() (now that we are
using a full-featured malloc) to allocate page-aligned buffers and
remove MADV_UNMERGEABLE when deallocating.

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 5052281..dc05335 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -37,6 +37,7 @@
 SG_BEGIN_DECL()
 
 /********************************** Configuration of MC **************************************/        
+
 extern XBT_PUBLIC(int) _sg_do_model_check;
 extern XBT_PRIVATE int _sg_do_model_check_record;
 extern XBT_PRIVATE int _sg_mc_checkpoint;
@@ -58,6 +59,7 @@ extern XBT_PRIVATE xbt_dynar_t mc_heap_comparison_ignore;
 extern XBT_PRIVATE xbt_dynar_t stacks_areas;
 
 /********************************* Global *************************************/
+
 XBT_PRIVATE void _mc_cfg_cb_reduce(const char *name, int pos);
 XBT_PRIVATE void _mc_cfg_cb_checkpoint(const char *name, int pos);
 XBT_PRIVATE void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos);

diff --git a/src/mc/RegionSnapshot.cpp b/src/mc/RegionSnapshot.cpp
index 634aadc..c59f190 100644 (file)
--- a/src/mc/RegionSnapshot.cpp
+++ b/src/mc/RegionSnapshot.cpp
@@ -51,10 +51,24 @@ RegionSnapshot dense_region(
   RegionType region_type,
   void *start_addr, void* permanent_addr, size_t size)
 {
-  simgrid::mc::RegionSnapshot::flat_data_ptr data((char*) malloc(size));
+  simgrid::mc::RegionSnapshot::flat_data_ptr data;
+  if (!_sg_mc_ksm)
+    data = simgrid::mc::RegionSnapshot::flat_data_ptr((char*) malloc(size));
+  else {
+    char* ptr = (char*) mmap(nullptr, size, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS|MAP_POPULATE, -1, 0);
+    if (ptr == MAP_FAILED)
+      throw std::bad_alloc();
+    simgrid::mc::data_deleter deleter(
+      simgrid::mc::data_deleter::Munmap, size);
+    data = simgrid::mc::RegionSnapshot::flat_data_ptr(ptr, deleter);
+  }
   mc_model_checker->process().read_bytes(data.get(), size,
     remote(permanent_addr),
     simgrid::mc::ProcessIndexDisabled);
+  if (_sg_mc_ksm)
+    // Mark the region as mergeable *after* we have written into it.
+    // There no point to let KSM do the hard work before that.
+    madvise(data.get(), size, MADV_MERGEABLE);
 
   simgrid::mc::RegionSnapshot region(
     region_type, start_addr, permanent_addr, size);

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index bd3578d..02ce10d 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -50,6 +50,7 @@ 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;
 char *_sg_mc_property_file = NULL;
 int _sg_mc_hash = 0;
 int _sg_mc_max_depth = 1000;
@@ -95,6 +96,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_ksm(const char *name, int pos)
+{
+  if (_sg_cfg_init_status && !_sg_do_model_check)
+    xbt_die("You are specifying a KSM 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_ksm = 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/simgrid/sg_config.c b/src/simgrid/sg_config.c
index 0455482..f1fae08 100644 (file)
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -625,6 +625,11 @@ 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");
 
+    xbt_cfg_register(&_sg_cfg_set, "model-check/ksm",
+                     "Kernel same-page merging",
+                     xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_ksm, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/ksm", "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.",