Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
a flag for udpor in the simgrid config
authoreazimi <azimi.ehsan@outlook.com>
Mon, 8 Feb 2021 11:45:39 +0000 (12:45 +0100)
committereazimi <azimi.ehsan@outlook.com>
Mon, 8 Feb 2021 11:45:39 +0000 (12:45 +0100)
src/mc/checker/simgrid_mc.cpp
src/mc/mc_config.cpp
src/mc/mc_config.hpp

index 015fb3d..455290e 100644 (file)
@@ -33,6 +33,8 @@ static std::unique_ptr<simgrid::mc::Checker> create_checker()
 {
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
     return std::unique_ptr<simgrid::mc::Checker>(simgrid::mc::createCommunicationDeterminismChecker());
+  else if (_sg_mc_unfolding_checker)
+    return std::unique_ptr<simgrid::mc::Checker>(simgrid::mc::createUdporChecker());
   else if (_sg_mc_property_file.get().empty())
     return std::unique_ptr<simgrid::mc::Checker>(simgrid::mc::createSafetyChecker());
   else
index cfe3511..39c3491 100644 (file)
@@ -72,6 +72,13 @@ simgrid::config::Flag<bool> _sg_mc_send_determinism{
       _mc_cfg_cb_check("value to enable/disable the detection of send-determinism in the communications schemes");
     }};
 
+simgrid::config::Flag<bool> _sg_mc_unfolding_checker{
+    "model-check/unfolding-checker", "Whether to enable the unfolding-based dynamic partial order reduction to MPI programs",     
+    false,
+    [](bool) {
+      _mc_cfg_cb_check("value to to enable/disable the unfolding-based dynamic partial order reduction to MPI programs");
+    }};
+
 simgrid::config::Flag<std::string> _sg_mc_buffering{
     "smpi/buffering",
     "Buffering semantic to use for MPI (only used in MC)",
index f249c75..467a2b7 100644 (file)
@@ -15,6 +15,7 @@ extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_checkpoint;
 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;
+extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_unfolding_checker;
 extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_timeout;
 extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_max_depth;
 extern "C" XBT_PUBLIC int _sg_mc_max_visited_states;