From 4899abbee2485469b99df371168310b5e6ad2d87 Mon Sep 17 00:00:00 2001 From: eazimi Date: Mon, 8 Feb 2021 12:45:39 +0100 Subject: [PATCH] a flag for udpor in the simgrid config --- src/mc/checker/simgrid_mc.cpp | 2 ++ src/mc/mc_config.cpp | 7 +++++++ src/mc/mc_config.hpp | 1 + 3 files changed, 10 insertions(+) diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp index 015fb3d250..455290e6a7 100644 --- a/src/mc/checker/simgrid_mc.cpp +++ b/src/mc/checker/simgrid_mc.cpp @@ -33,6 +33,8 @@ static std::unique_ptr create_checker() { if (_sg_mc_comms_determinism || _sg_mc_send_determinism) return std::unique_ptr(simgrid::mc::createCommunicationDeterminismChecker()); + else if (_sg_mc_unfolding_checker) + return std::unique_ptr(simgrid::mc::createUdporChecker()); else if (_sg_mc_property_file.get().empty()) return std::unique_ptr(simgrid::mc::createSafetyChecker()); else diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index cfe3511b25..39c3491dee 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -72,6 +72,13 @@ simgrid::config::Flag _sg_mc_send_determinism{ _mc_cfg_cb_check("value to enable/disable the detection of send-determinism in the communications schemes"); }}; +simgrid::config::Flag _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 _sg_mc_buffering{ "smpi/buffering", "Buffering semantic to use for MPI (only used in MC)", diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp index f249c753e8..467a2b7b3a 100644 --- a/src/mc/mc_config.hpp +++ b/src/mc/mc_config.hpp @@ -15,6 +15,7 @@ extern XBT_PRIVATE simgrid::config::Flag _sg_mc_checkpoint; extern XBT_PUBLIC simgrid::config::Flag _sg_mc_property_file; extern XBT_PUBLIC simgrid::config::Flag _sg_mc_comms_determinism; extern XBT_PUBLIC simgrid::config::Flag _sg_mc_send_determinism; +extern XBT_PUBLIC simgrid::config::Flag _sg_mc_unfolding_checker; extern XBT_PRIVATE simgrid::config::Flag _sg_mc_timeout; extern XBT_PRIVATE simgrid::config::Flag _sg_mc_max_depth; extern "C" XBT_PUBLIC int _sg_mc_max_visited_states; -- 2.20.1