From 2c1f1f0e9bb706d9adbb71e0bc33923c4478eb85 Mon Sep 17 00:00:00 2001 From: Patrick-6 Date: Mon, 8 Sep 2025 10:17:14 +0200 Subject: Add GenMC estimation mode. Improve error handling and output printing. --- .../miri/genmc-sys/cpp/include/MiriInterface.hpp | 8 +++++++- .../cpp/src/MiriInterface/Exploration.cpp | 14 +++++++++++++ .../miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp | 23 +++++++++++++++------- 3 files changed, 37 insertions(+), 8 deletions(-) (limited to 'src/tools/miri/genmc-sys/cpp') diff --git a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp index 662eb0e173c..444c9375319 100644 --- a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp +++ b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp @@ -31,6 +31,7 @@ enum class LogLevel : std::uint8_t; struct GenmcScalar; struct SchedulingResult; +struct EstimationResult; struct LoadResult; struct StoreResult; struct ReadModifyWriteResult; @@ -66,7 +67,7 @@ struct MiriGenmcShim : private GenMCDriver { /// `logLevel`, causing a data race. The safest way to use these functions is to call /// `set_log_level_raw` once, and only then start creating handles. There should not be any /// other (safe) way to create a `MiriGenmcShim`. - /* unsafe */ static auto create_handle(const GenmcParams& params) + /* unsafe */ static auto create_handle(const GenmcParams& params, bool estimation_mode) -> std::unique_ptr; virtual ~MiriGenmcShim() {} @@ -183,6 +184,11 @@ struct MiriGenmcShim : private GenMCDriver { return nullptr; } + /**** Printing and estimation mode functionality. ****/ + + /// Get the results of a run in estimation mode. + auto get_estimation_results() const -> EstimationResult; + private: /** Increment the event index in the given thread by 1 and return the new event. */ [[nodiscard]] inline auto inc_pos(ThreadId tid) -> Event { diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index c51b59e8651..5e7188f17e0 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -10,7 +10,9 @@ #include "Support/Verbosity.hpp" // C++ headers: +#include #include +#include auto MiriGenmcShim::schedule_next( const int curr_thread_id, @@ -40,3 +42,15 @@ auto MiriGenmcShim::handle_execution_end() -> std::unique_ptr { GenMCDriver::handleExecutionEnd(); return {}; } + +/**** Estimation mode result ****/ + +auto MiriGenmcShim::get_estimation_results() const -> EstimationResult { + const auto& res = getResult(); + return EstimationResult { + .mean = static_cast(res.estimationMean), + .sd = static_cast(std::sqrt(res.estimationVariance)), + .explored_execs = static_cast(res.explored), + .blocked_execs = static_cast(res.exploredBlocked), + }; +} diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp index a17a83aa06e..af13f0d0774 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp @@ -58,7 +58,7 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel logLevel = to_genmc_verbosity_level(log_level); } -/* unsafe */ auto MiriGenmcShim::create_handle(const GenmcParams& params) +/* unsafe */ auto MiriGenmcShim::create_handle(const GenmcParams& params, bool estimation_mode) -> std::unique_ptr { auto conf = std::make_shared(); @@ -82,7 +82,8 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel // Miri. conf->warnOnGraphSize = 1024 * 1024; - // We only support the `RC11` memory model for Rust, and `SC` when weak memory emulation is disabled. + // We only support the `RC11` memory model for Rust, and `SC` when weak memory emulation is + // disabled. conf->model = params.disable_weak_memory_emulation ? ModelType::SC : ModelType::RC11; // This prints the seed that GenMC picks for randomized scheduling during estimation mode. @@ -119,12 +120,20 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel ); conf->symmetryReduction = params.do_symmetry_reduction; - // FIXME(genmc): expose this setting to Miri (useful for testing Miri-GenMC). - conf->schedulePolicy = SchedulePolicy::WF; - + // Set the scheduling policy. GenMC uses `WFR` for estimation mode. + // For normal verification, `WF` has the best performance and is the GenMC default. + // Other scheduling policies are used by GenMC for testing and for modes currently + // unsupported with Miri such as bounding, which uses LTR. + conf->schedulePolicy = estimation_mode ? SchedulePolicy::WFR : SchedulePolicy::WF; + + // Set the min and max number of executions tested in estimation mode. + conf->estimationMin = 10; // default taken from GenMC + conf->estimationMax = params.estimation_max; + // Deviation threshold % under which estimation is deemed good enough. + conf->sdThreshold = 10; // default taken from GenMC // Set the mode used for this driver, either estimation or verification. - // FIXME(genmc): implement estimation mode. - const auto mode = GenMCDriver::Mode(GenMCDriver::VerificationMode {}); + const auto mode = estimation_mode ? GenMCDriver::Mode(GenMCDriver::EstimationMode {}) + : GenMCDriver::Mode(GenMCDriver::VerificationMode {}); // Running Miri-GenMC without race detection is not supported. // Disabling this option also changes the behavior of the replay scheduler to only schedule -- cgit 1.4.1-3-g733a5