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_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);
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);
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;
_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) {
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.",