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.
SG_BEGIN_DECL()
/********************************** Configuration of MC **************************************/
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;
extern XBT_PUBLIC(int) _sg_do_model_check;
extern XBT_PRIVATE int _sg_do_model_check_record;
extern XBT_PRIVATE int _sg_mc_checkpoint;
extern XBT_PRIVATE xbt_dynar_t stacks_areas;
/********************************* Global *************************************/
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);
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);
RegionType region_type,
void *start_addr, void* permanent_addr, size_t size)
{
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);
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);
simgrid::mc::RegionSnapshot region(
region_type, start_addr, permanent_addr, size);
int _sg_do_model_check_record = 0;
int _sg_mc_checkpoint = 0;
int _sg_mc_sparse_checkpoint = 0;
int _sg_do_model_check_record = 0;
int _sg_mc_checkpoint = 0;
int _sg_mc_sparse_checkpoint = 0;
char *_sg_mc_property_file = NULL;
int _sg_mc_hash = 0;
int _sg_mc_max_depth = 1000;
char *_sg_mc_property_file = NULL;
int _sg_mc_hash = 0;
int _sg_mc_max_depth = 1000;
_sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
}
_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) {
void _mc_cfg_cb_property(const char *name, int pos)
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_sparse_checkpoint, NULL);
xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/sparse-checkpoint", "no");
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.",
/* 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.",