Merge pull request #4583 from Patrick-6/miri-genmc-estimation

Add GenMC estimation mode.

3 files changed, 37 insertions, 8 deletions

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<MiriGenmcShim>;
 
     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 <cmath>
 #include <cstdint>
+#include <limits>
 
 auto MiriGenmcShim::schedule_next(
     const int curr_thread_id,
@@ -40,3 +42,15 @@ auto MiriGenmcShim::handle_execution_end() -> std::unique_ptr<std::string> {
     GenMCDriver::handleExecutionEnd();
     return {};
 }
+
+/**** Estimation mode result ****/
+
+auto MiriGenmcShim::get_estimation_results() const -> EstimationResult {
+    const auto& res = getResult();
+    return EstimationResult {
+        .mean = static_cast<double>(res.estimationMean),
+        .sd = static_cast<double>(std::sqrt(res.estimationVariance)),
+        .explored_execs = static_cast<uint64_t>(res.explored),
+        .blocked_execs = static_cast<uint64_t>(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<MiriGenmcShim> {
     auto conf = std::make_shared<Config>();
 
@@ -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