From: Gabriel Corona Date: Mon, 28 Sep 2015 10:20:51 +0000 (+0200) Subject: [mc] Bring back KSM (MADV_MERGEABLE) support X-Git-Tag: v3_12~62^2~5 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/4801057254232c8283c0d392783eea07ecdd874f [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 5052281354..dc05335355 100644 --- 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 634aadc85b..c59f1909fc 100644 --- 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 bd3578d41c..02ce10dac3 100644 --- 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 04554824e9..f1fae08e3a 100644 --- 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.",