Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
mc: kill model-check/ksm option. Was not activated because not very useful
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Wed, 15 May 2019 23:03:28 +0000 (01:03 +0200)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Thu, 16 May 2019 00:44:31 +0000 (02:44 +0200)
It's probably a pity, but I need to simplify this code to get the
grasp back.

src/mc/mc_config.cpp
src/mc/mc_config.hpp
src/mc/sosp/RegionSnapshot.cpp
src/mc/sosp/mc_checkpoint.cpp

index 584d0ba..b8de285 100644 (file)
@@ -64,9 +64,6 @@ simgrid::config::Flag<int> _sg_mc_checkpoint{
 simgrid::config::Flag<bool> _sg_mc_sparse_checkpoint{"model-check/sparse-checkpoint", "Use sparse per-page snapshots.",
                                                      false, [](bool) { _mc_cfg_cb_check("checkpointing value"); }};
 
-simgrid::config::Flag<bool> _sg_mc_ksm{"model-check/ksm", "Kernel same-page merging", false,
-                                       [](bool) { _mc_cfg_cb_check("KSM value"); }};
-
 simgrid::config::Flag<std::string> _sg_mc_property_file{
     "model-check/property", "Name of the file containing the property, as formatted by the ltl2ba program.", "",
     [](const std::string&) { _mc_cfg_cb_check("property"); }};
index ffc0c2e..3d74a3d 100644 (file)
@@ -13,7 +13,6 @@ extern "C" XBT_PUBLIC int _sg_do_model_check;
 extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_record_path;
 extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_checkpoint;
 extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_sparse_checkpoint;
-extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_ksm;
 extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_property_file;
 extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_comms_determinism;
 extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_send_determinism;
index ea2445f..6dea387 100644 (file)
@@ -76,24 +76,10 @@ void Buffer::clear() noexcept
 
 RegionSnapshot dense_region(RegionType region_type, void* start_addr, void* permanent_addr, size_t size)
 {
-  // When KSM support is enables, we allocate memory using mmap:
-  // * we don't want to advise bits of the heap as mergable
-  // * mmap gives data aligned on page boundaries which is merge friendly
-  simgrid::mc::Buffer data;
-  if (_sg_mc_ksm)
-    data = Buffer::mmap(size);
-  else
-    data = Buffer::malloc(size);
+  simgrid::mc::Buffer data = Buffer::malloc(size);
 
   mc_model_checker->process().read_bytes(data.get(), size, remote(permanent_addr), simgrid::mc::ProcessIndexDisabled);
 
-#ifdef __linux__
-  if (_sg_mc_ksm)
-    // Mark the region as mergeable *after* we have written into it.
-    // Trying to merge them before is useless/counterproductive.
-    madvise(data.get(), size, MADV_MERGEABLE);
-#endif
-
   simgrid::mc::RegionSnapshot region(region_type, start_addr, permanent_addr, size);
   region.flat_data(std::move(data));
 
index 0ae2a09..b222445 100644 (file)
@@ -92,12 +92,12 @@ RegionSnapshot privatized_region(RegionType region_type, void* start_addr, void*
   mc_model_checker->process().read_bytes(&privatization_regions, sizeof(privatization_regions),
                                          remote(remote_smpi_privatization_regions));
 
-  std::vector<simgrid::mc::RegionSnapshot> data;
+  std::vector<RegionSnapshot> data;
   data.reserve(process_count);
   for (size_t i = 0; i < process_count; i++)
-    data.push_back(simgrid::mc::region(region_type, start_addr, privatization_regions[i].address, size));
+    data.push_back(region(region_type, start_addr, privatization_regions[i].address, size));
 
-  simgrid::mc::RegionSnapshot region = simgrid::mc::RegionSnapshot(region_type, start_addr, permanent_addr, size);
+  RegionSnapshot region = RegionSnapshot(region_type, start_addr, permanent_addr, size);
   region.privatized_data(std::move(data));
   return region;
 }