Add GenMC estimation mode. Improve error handling and output printing.

Author: Patrick-6

doc/genmc.md

@@ -24,6 +24,8 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
 ### Supported Parameters
 
 - `-Zmiri-genmc`: Enable GenMC mode (not required if any other GenMC options are used).
+- `-Zmiri-genmc-estimate`: This enables estimation of the concurrent execution space and verification time, before running the full verification. This should help users detect when their program is too complex to fully verify in a reasonable time. This will explore enough executions to make a good estimation, but at least 10 and at most `estimation-max` executions.
+- `-Zmiri-genmc-estimation-max={MAX_ITERATIONS}`: Set the maximum number of executions that will be explored during estimation (default: 1000).
 - `-Zmiri-genmc-print-exec-graphs={none,explored,blocked,all}`: Make GenMC print the execution graph of the program after every explored, every blocked, or after every execution (default: None).
 - `-Zmiri-genmc-print-exec-graphs`: Shorthand for suffix `=explored`.
 - `-Zmiri-genmc-print-genmc-output`: Print the output that GenMC provides. NOTE: this output is quite verbose and the events in the printed execution graph are hard to map back to the Rust code location they originate from.
@@ -36,6 +38,7 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
     - `debug1`:   Print revisits considered by GenMC.
     - `debug2`:   Print the execution graph after every memory access.
     - `debug3`:   Print reads-from values considered by GenMC.
+- `-Zmiri-genmc-verbose`: Show more information, such as estimated number of executions, and time taken for verification.
 
 #### Regular Miri parameters useful for GenMC mode
 

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 {

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),
+    };
+}

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

genmc-sys/src/lib.rs

@@ -27,6 +27,7 @@ static GENMC_LOG_LEVEL: OnceLock<LogLevel> = OnceLock::new();
 pub fn create_genmc_driver_handle(
     params: &GenmcParams,
     genmc_log_level: LogLevel,
+    do_estimation: bool,
 ) -> UniquePtr<MiriGenmcShim> {
     // SAFETY: Only setting the GenMC log level once is guaranteed by the `OnceLock`.
     // No other place calls `set_log_level_raw`, so the `logLevel` value in GenMC will not change once we initialize it once.
@@ -40,7 +41,7 @@ pub fn create_genmc_driver_handle(
         }),
         "Attempt to change the GenMC log level after it was already set"
     );
-    unsafe { MiriGenmcShim::create_handle(params) }
+    unsafe { MiriGenmcShim::create_handle(params, do_estimation) }
 }
 
 impl GenmcScalar {
@@ -54,6 +55,7 @@ impl GenmcScalar {
 impl Default for GenmcParams {
     fn default() -> Self {
         Self {
+            estimation_max: 1000, // default taken from GenMC
             print_random_schedule_seed: false,
             do_symmetry_reduction: false,
             // GenMC graphs can be quite large since Miri produces a lot of (non-atomic) events.
@@ -70,6 +72,20 @@ impl Default for LogLevel {
     }
 }
 
+impl FromStr for SchedulePolicy {
+    type Err = &'static str;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        Ok(match s {
+            "wf" => SchedulePolicy::WF,
+            "wfr" => SchedulePolicy::WFR,
+            "arbitrary" | "random" => SchedulePolicy::Arbitrary,
+            "ltr" => SchedulePolicy::LTR,
+            _ => return Err("invalid scheduling policy"),
+        })
+    }
+}
+
 impl FromStr for LogLevel {
     type Err = &'static str;
 
@@ -92,9 +108,12 @@ mod ffi {
     /**** Types shared between Miri/Rust and Miri/C++ through cxx_bridge: ****/
 
     /// Parameters that will be given to GenMC for setting up the model checker.
-    /// (The fields of this struct are visible to both Rust and C++)
+    /// The fields of this struct are visible to both Rust and C++.
+    /// Note that this struct is #[repr(C)], so the order of fields matters.
     #[derive(Clone, Debug)]
     struct GenmcParams {
+        /// Maximum number of executions explored in estimation mode.
+        pub estimation_max: u32,
         pub print_random_schedule_seed: bool,
         pub do_symmetry_reduction: bool,
         pub print_execution_graphs: ExecutiongraphPrinting,
@@ -165,6 +184,19 @@ mod ffi {
         next_thread: i32,
     }
 
+    #[must_use]
+    #[derive(Debug)]
+    struct EstimationResult {
+        /// Expected number of total executions.
+        mean: f64,
+        /// Standard deviation of the total executions estimate.
+        sd: f64,
+        /// Number of explored executions during the estimation.
+        explored_execs: u64,
+        /// Number of encounteded blocked executions during the estimation.
+        blocked_execs: u64,
+    }
+
     #[must_use]
     #[derive(Debug)]
     struct LoadResult {
@@ -214,6 +246,14 @@ mod ffi {
     /**** These are GenMC types that we have to copy-paste here since cxx does not support
     "importing" externally defined C++ types. ****/
 
+    #[derive(Clone, Copy, Debug)]
+    enum SchedulePolicy {
+        LTR,
+        WF,
+        WFR,
+        Arbitrary,
+    }
+
     #[derive(Debug)]
     /// Corresponds to GenMC's type with the same name.
     /// Should only be modified if changed by GenMC.
@@ -272,6 +312,7 @@ mod ffi {
         type ActionKind;
         type MemOrdering;
         type RMWBinOp;
+        type SchedulePolicy;
 
         /// Set the log level for GenMC.
         ///
@@ -295,7 +336,10 @@ mod ffi {
         /// start creating handles.
         /// There should not be any other (safe) way to create a `MiriGenmcShim`.
         #[Self = "MiriGenmcShim"]
-        unsafe fn create_handle(params: &GenmcParams) -> UniquePtr<MiriGenmcShim>;
+        unsafe fn create_handle(
+            params: &GenmcParams,
+            estimation_mode: bool,
+        ) -> UniquePtr<MiriGenmcShim>;
         /// Get the bit mask that GenMC expects for global memory allocations.
         fn get_global_alloc_static_mask() -> u64;
 
@@ -403,5 +447,10 @@ mod ffi {
         fn get_result_message(self: &MiriGenmcShim) -> UniquePtr<CxxString>;
         /// If an error occurred, return a string describing the error, otherwise, return `nullptr`.
         fn get_error_string(self: &MiriGenmcShim) -> UniquePtr<CxxString>;
+
+        /**** Printing functionality. ****/
+
+        /// Get the results of a run in estimation mode.
+        fn get_estimation_results(self: &MiriGenmcShim) -> EstimationResult;
     }
 }

src/bin/miri.rs

@@ -186,18 +186,17 @@ impl rustc_driver::Callbacks for MiriCompilerCalls {
                     optimizations is usually marginal at best.");
         }
 
-        if let Some(_genmc_config) = &config.genmc_config {
+        // Run in GenMC mode if enabled.
+        if config.genmc_config.is_some() {
+            // This is the entry point used in GenMC mode.
+            // This closure will be called multiple times to explore the concurrent execution space of the program.
             let eval_entry_once = |genmc_ctx: Rc<GenmcCtx>| {
                 miri::eval_entry(tcx, entry_def_id, entry_type, &config, Some(genmc_ctx))
             };
-
-            // FIXME(genmc): add estimation mode here.
-
             let return_code = run_genmc_mode(&config, eval_entry_once, tcx).unwrap_or_else(|| {
                 tcx.dcx().abort_if_errors();
                 rustc_driver::EXIT_FAILURE
             });
-
             exit(return_code);
         };
 

src/concurrency/genmc/config.rs

@@ -10,11 +10,15 @@ use crate::{IsolatedOp, MiriConfig, RejectOpWith};
 pub struct GenmcConfig {
     /// Parameters sent to the C++ side to create a new handle to the GenMC model checker.
     pub(super) params: GenmcParams,
+    pub(super) do_estimation: bool,
     /// Print the output message that GenMC generates when an error occurs.
     /// This error message is currently hard to use, since there is no clear mapping between the events that GenMC sees and the Rust code location where this event was produced.
     pub(super) print_genmc_output: bool,
     /// The log level for GenMC.
     pub(super) log_level: LogLevel,
+    /// Enable more verbose output, such as number of executions estimate
+    /// and time to completion of verification step.
+    pub(super) verbose_output: bool,
 }
 
 impl GenmcConfig {
@@ -57,8 +61,21 @@ impl GenmcConfig {
                         "Invalid suffix to GenMC argument '-Zmiri-genmc-print-exec-graphs', expected '', '=none', '=explored', '=blocked' or '=all'"
                     )),
             }
+        } else if trimmed_arg == "estimate" {
+            // FIXME(genmc): should this be on by default (like for GenMC)?
+            // Enable estimating the execution space and require time before running the actual verification.
+            genmc_config.do_estimation = true;
+        } else if let Some(estimation_max_str) = trimmed_arg.strip_prefix("estimation-max=") {
+            // Set the maximum number of executions to explore during estimation.
+            genmc_config.params.estimation_max = estimation_max_str.parse().ok().filter(|estimation_max| *estimation_max > 0).ok_or_else(|| {
+                format!(
+                    "'-Zmiri-genmc-estimation-max=...' expects a positive integer argument, but got '{estimation_max_str}'"
+                )
+            })?;
         } else if trimmed_arg == "print-genmc-output" {
             genmc_config.print_genmc_output = true;
+        } else if trimmed_arg == "verbose" {
+            genmc_config.verbose_output = true;
         } else {
             return Err(format!("Invalid GenMC argument: \"-Zmiri-genmc-{trimmed_arg}\""));
         }

src/concurrency/genmc/dummy.rs

@@ -39,18 +39,6 @@ mod run {
 impl GenmcCtx {
     // We don't provide the `new` function in the dummy module.
 
-    pub fn get_blocked_execution_count(&self) -> usize {
-        unreachable!()
-    }
-
-    pub fn get_explored_execution_count(&self) -> usize {
-        unreachable!()
-    }
-
-    pub fn is_exploration_done(&self) -> bool {
-        unreachable!()
-    }
-
     /**** Memory access handling ****/
 
     pub(super) fn set_ongoing_action_data_race_free(&self, _enable: bool) {