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

64 files changed, 386 insertions, 170 deletions

diff --git a/src/tools/miri/doc/genmc.md b/src/tools/miri/doc/genmc.md
index 8af697be34a..44e11dcbec4 100644
--- a/src/tools/miri/doc/genmc.md
+++ b/src/tools/miri/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
 
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
diff --git a/src/tools/miri/genmc-sys/src/lib.rs b/src/tools/miri/genmc-sys/src/lib.rs
index 31bc2606adc..733b3d780b1 100644
--- a/src/tools/miri/genmc-sys/src/lib.rs
+++ b/src/tools/miri/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,
@@ -167,6 +186,19 @@ mod ffi {
 
     #[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 {
         /// If not null, contains the error encountered during the handling of the load.
         error: UniquePtr<CxxString>,
@@ -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;
     }
 }
diff --git a/src/tools/miri/src/bin/miri.rs b/src/tools/miri/src/bin/miri.rs
index 731fe283a21..8b15a786347 100644
--- a/src/tools/miri/src/bin/miri.rs
+++ b/src/tools/miri/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);
         };
 
diff --git a/src/tools/miri/src/concurrency/genmc/config.rs b/src/tools/miri/src/concurrency/genmc/config.rs
index 34933d423f0..c7cfa6012b8 100644
--- a/src/tools/miri/src/concurrency/genmc/config.rs
+++ b/src/tools/miri/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}\""));
         }
diff --git a/src/tools/miri/src/concurrency/genmc/dummy.rs b/src/tools/miri/src/concurrency/genmc/dummy.rs
index 92b34b83ee0..c28984cef35 100644
--- a/src/tools/miri/src/concurrency/genmc/dummy.rs
+++ b/src/tools/miri/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) {
diff --git a/src/tools/miri/src/concurrency/genmc/mod.rs b/src/tools/miri/src/concurrency/genmc/mod.rs
index 7270c668106..0086d3f2bf0 100644
--- a/src/tools/miri/src/concurrency/genmc/mod.rs
+++ b/src/tools/miri/src/concurrency/genmc/mod.rs
@@ -2,8 +2,8 @@ use std::cell::{Cell, RefCell};
 use std::sync::Arc;
 
 use genmc_sys::{
-    GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, MemOrdering, MiriGenmcShim, RMWBinOp, UniquePtr,
-    create_genmc_driver_handle,
+    EstimationResult, GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, MemOrdering, MiriGenmcShim,
+    RMWBinOp, UniquePtr, create_genmc_driver_handle,
 };
 use rustc_abi::{Align, Size};
 use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult, interp_ok};
@@ -16,6 +16,7 @@ use self::helper::{
     MAX_ACCESS_SIZE, Warnings, emit_warning, genmc_scalar_to_scalar,
     maybe_upgrade_compare_exchange_success_orderings, scalar_to_genmc_scalar, to_genmc_rmw_op,
 };
+use self::run::GenmcMode;
 use self::thread_id_map::ThreadIdMap;
 use crate::concurrency::genmc::helper::split_access;
 use crate::intrinsics::AtomicRmwOp;
@@ -37,6 +38,16 @@ pub use genmc_sys::GenmcParams;
 pub use self::config::GenmcConfig;
 pub use self::run::run_genmc_mode;
 
+#[derive(Debug)]
+pub enum ExecutionEndResult {
+    /// An error occurred at the end of the execution.
+    Error(String),
+    /// No errors occurred, and there are more executions to explore.
+    Continue,
+    /// No errors occurred and we are finished.
+    Stop,
+}
+
 #[derive(Clone, Copy, Debug)]
 pub enum ExitType {
     MainThreadFinish,
@@ -128,26 +139,33 @@ pub struct GenmcCtx {
 /// GenMC Context creation and administrative / query actions
 impl GenmcCtx {
     /// Create a new `GenmcCtx` from a given config.
-    fn new(miri_config: &MiriConfig, global_state: Arc<GlobalState>) -> Self {
+    fn new(miri_config: &MiriConfig, global_state: Arc<GlobalState>, mode: GenmcMode) -> Self {
         let genmc_config = miri_config.genmc_config.as_ref().unwrap();
-        let handle =
-            RefCell::new(create_genmc_driver_handle(&genmc_config.params, genmc_config.log_level));
+        let handle = RefCell::new(create_genmc_driver_handle(
+            &genmc_config.params,
+            genmc_config.log_level,
+            /* do_estimation: */ mode == GenmcMode::Estimation,
+        ));
         Self { handle, exec_state: Default::default(), global_state }
     }
 
+    fn get_estimation_results(&self) -> EstimationResult {
+        self.handle.borrow().get_estimation_results()
+    }
+
     /// Get the number of blocked executions encountered by GenMC.
-    pub fn get_blocked_execution_count(&self) -> u64 {
+    fn get_blocked_execution_count(&self) -> u64 {
         self.handle.borrow().get_blocked_execution_count()
     }
 
     /// Get the number of explored executions encountered by GenMC.
-    pub fn get_explored_execution_count(&self) -> u64 {
+    fn get_explored_execution_count(&self) -> u64 {
         self.handle.borrow().get_explored_execution_count()
     }
 
     /// Check if GenMC encountered an error that wasn't immediately returned during execution.
     /// Returns a string representation of the error if one occurred.
-    pub fn try_get_error(&self) -> Option<String> {
+    fn try_get_error(&self) -> Option<String> {
         self.handle
             .borrow()
             .get_error_string()
@@ -157,7 +175,7 @@ impl GenmcCtx {
 
     /// Check if GenMC encountered an error that wasn't immediately returned during execution.
     /// Returns a string representation of the error if one occurred.
-    pub fn get_result_message(&self) -> String {
+    fn get_result_message(&self) -> String {
         self.handle
             .borrow()
             .get_result_message()
@@ -166,13 +184,6 @@ impl GenmcCtx {
             .expect("there should always be a message")
     }
 
-    /// This function determines if we should continue exploring executions or if we are done.
-    ///
-    /// In GenMC mode, the input program should be repeatedly executed until this function returns `true` or an error is found.
-    pub fn is_exploration_done(&self) -> bool {
-        self.handle.borrow_mut().pin_mut().is_exploration_done()
-    }
-
     /// Select whether data race free actions should be allowed. This function should be used carefully!
     ///
     /// If `true` is passed, allow for data races to happen without triggering an error, until this function is called again with argument `false`.
@@ -218,13 +229,25 @@ impl GenmcCtx {
     /// This function will also check for those, and return their error description.
     ///
     /// To get the all messages (warnings, errors) that GenMC produces, use the `get_result_message` method.
-    fn handle_execution_end(&self) -> Option<String> {
+    fn handle_execution_end(&self) -> ExecutionEndResult {
         let result = self.handle.borrow_mut().pin_mut().handle_execution_end();
-        result.as_ref().map(|msg| msg.to_string_lossy().to_string())?;
+        if let Some(error) = result.as_ref() {
+            return ExecutionEndResult::Error(error.to_string_lossy().to_string());
+        }
+
+        // GenMC decides if there is more to explore:
+        let exploration_done = self.handle.borrow_mut().pin_mut().is_exploration_done();
 
         // GenMC currently does not return an error value immediately in all cases.
+        // Both `handle_execution_end` and `is_exploration_done` can produce such errors.
         // We manually query for any errors here to ensure we don't miss any.
-        self.try_get_error()
+        if let Some(error) = self.try_get_error() {
+            ExecutionEndResult::Error(error)
+        } else if exploration_done {
+            ExecutionEndResult::Stop
+        } else {
+            ExecutionEndResult::Continue
+        }
     }
 
     /**** Memory access handling ****/
diff --git a/src/tools/miri/src/concurrency/genmc/run.rs b/src/tools/miri/src/concurrency/genmc/run.rs
index 7e4ed816a76..bc2f5f7b79e 100644
--- a/src/tools/miri/src/concurrency/genmc/run.rs
+++ b/src/tools/miri/src/concurrency/genmc/run.rs
@@ -1,32 +1,65 @@
 use std::rc::Rc;
 use std::sync::Arc;
+use std::time::Instant;
 
+use genmc_sys::EstimationResult;
 use rustc_middle::ty::TyCtxt;
 
 use super::GlobalState;
+use crate::concurrency::genmc::ExecutionEndResult;
 use crate::rustc_const_eval::interpret::PointerArithmetic;
-use crate::{GenmcCtx, MiriConfig};
+use crate::{GenmcConfig, GenmcCtx, MiriConfig};
+
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub(super) enum GenmcMode {
+    Estimation,
+    Verification,
+}
+
+impl GenmcMode {
+    /// Return whether warnings on unsupported features should be printed in this mode.
+    fn print_unsupported_warnings(self) -> bool {
+        self == GenmcMode::Verification
+    }
+}
 
 /// Do a complete run of the program in GenMC mode.
 /// This will call `eval_entry` multiple times, until either:
 /// - An error is detected (indicated by a `None` return value)
 /// - All possible executions are explored.
 ///
-/// FIXME(genmc): add estimation mode setting.
+/// Returns `None` is an error is detected, or `Some(return_value)` with the return value of the last run of the program.
 pub fn run_genmc_mode<'tcx>(
     config: &MiriConfig,
     eval_entry: impl Fn(Rc<GenmcCtx>) -> Option<i32>,
     tcx: TyCtxt<'tcx>,
 ) -> Option<i32> {
     let genmc_config = config.genmc_config.as_ref().unwrap();
+    // Run in Estimation mode if requested.
+    if genmc_config.do_estimation {
+        eprintln!("Estimating GenMC verification time...");
+        run_genmc_mode_impl(config, &eval_entry, tcx, GenmcMode::Estimation)?;
+    }
+    // Run in Verification mode.
+    eprintln!("Running GenMC Verification...");
+    run_genmc_mode_impl(config, &eval_entry, tcx, GenmcMode::Verification)
+}
+
+fn run_genmc_mode_impl<'tcx>(
+    config: &MiriConfig,
+    eval_entry: &impl Fn(Rc<GenmcCtx>) -> Option<i32>,
+    tcx: TyCtxt<'tcx>,
+    mode: GenmcMode,
+) -> Option<i32> {
+    let time_start = Instant::now();
+    let genmc_config = config.genmc_config.as_ref().unwrap();
 
     // There exists only one `global_state` per full run in GenMC mode.
     // It is shared by all `GenmcCtx` in this run.
     // FIXME(genmc): implement multithreading once GenMC supports it.
-    // FIXME(genmc): disable warnings in estimation mode once it is added.
     let global_state =
-        Arc::new(GlobalState::new(tcx.target_usize_max(), /* print_warnings */ true));
-    let genmc_ctx = Rc::new(GenmcCtx::new(config, global_state));
+        Arc::new(GlobalState::new(tcx.target_usize_max(), mode.print_unsupported_warnings()));
+    let genmc_ctx = Rc::new(GenmcCtx::new(config, global_state, mode));
 
     // `rep` is used to report the progress, Miri will panic on wrap-around.
     for rep in 0u64.. {
@@ -37,46 +70,97 @@ pub fn run_genmc_mode<'tcx>(
 
         // Execute the program until completion to get the return value, or return if an error happens:
         let Some(return_code) = eval_entry(genmc_ctx.clone()) else {
-            // If requested, print the output GenMC produced:
-            if genmc_config.print_genmc_output {
-                eprintln!("== raw GenMC output =========================");
-                eprintln!("{}", genmc_ctx.get_result_message());
-                eprintln!("== end of raw GenMC output ==================");
-            }
+            genmc_ctx.print_genmc_output(genmc_config);
             return None;
         };
 
-        // We inform GenMC that the execution is complete. If there was an error, we print it.
-        if let Some(error) = genmc_ctx.handle_execution_end() {
-            // This can be reached for errors that affect the entire execution, not just a specific event.
-            // For instance, linearizability checking and liveness checking report their errors this way.
-            // Neither are supported by Miri-GenMC at the moment though. However, GenMC also
-            // treats races on deallocation as global errors, so this code path is still reachable.
-            // Since we don't have any span information for the error at this point,
-            // we just print GenMC's error message.
-            eprintln!("(GenMC) Error detected: {error}");
-            eprintln!();
-            eprintln!("{}", genmc_ctx.get_result_message());
-            return None;
+        // We inform GenMC that the execution is complete.
+        // If there was an error, we print it.
+        match genmc_ctx.handle_execution_end() {
+            ExecutionEndResult::Continue => continue,
+            ExecutionEndResult::Stop => {
+                let elapsed_time_sec = Instant::now().duration_since(time_start).as_secs_f64();
+                // Print the output for the current mode.
+                if mode == GenmcMode::Estimation {
+                    genmc_ctx.print_estimation_output(genmc_config, elapsed_time_sec);
+                } else {
+                    genmc_ctx.print_verification_output(genmc_config, elapsed_time_sec);
+                }
+                // Return the return code of the last execution.
+                return Some(return_code);
+            }
+            ExecutionEndResult::Error(error) => {
+                // This can be reached for errors that affect the entire execution, not just a specific event.
+                // For instance, linearizability checking and liveness checking report their errors this way.
+                // Neither are supported by Miri-GenMC at the moment though. However, GenMC also
+                // treats races on deallocation as global errors, so this code path is still reachable.
+                // Since we don't have any span information for the error at this point,
+                // we just print GenMC's error string, and the full GenMC output if requested.
+                eprintln!("(GenMC) Error detected: {error}");
+                genmc_ctx.print_genmc_output(genmc_config);
+                return None;
+            }
         }
+    }
+    unreachable!()
+}
 
-        // Check if we've explored enough executions:
-        if !genmc_ctx.is_exploration_done() {
-            continue;
+impl GenmcCtx {
+    /// Print the full output message produced by GenMC if requested, or a hint on how to enable it.
+    ///
+    /// This message can be very verbose and is likely not useful for the average user.
+    /// This function should be called *after* Miri has printed all of its output.
+    fn print_genmc_output(&self, genmc_config: &GenmcConfig) {
+        if genmc_config.print_genmc_output {
+            eprintln!("GenMC error report:");
+            eprintln!("{}", self.get_result_message());
+        } else {
+            eprintln!(
+                "(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)"
+            );
         }
+    }
 
-        eprintln!("(GenMC) Verification complete. No errors were detected.");
-
-        let explored_execution_count = genmc_ctx.get_explored_execution_count();
-        let blocked_execution_count = genmc_ctx.get_blocked_execution_count();
+    /// Given the time taken for the estimation mode run, print the expected time range for verification.
+    /// Verbose output also includes information about the expected number of executions and how many estimation rounds were explored or got blocked.
+    fn print_estimation_output(&self, genmc_config: &GenmcConfig, elapsed_time_sec: f64) {
+        let EstimationResult { mean, sd, explored_execs, blocked_execs } =
+            self.get_estimation_results();
+        #[allow(clippy::as_conversions)]
+        let time_per_exec_sec = elapsed_time_sec / (explored_execs as f64 + blocked_execs as f64);
+        let estimated_mean_sec = time_per_exec_sec * mean;
+        let estimated_sd_sec = time_per_exec_sec * sd;
 
-        eprintln!("Number of complete executions explored: {explored_execution_count}");
-        if blocked_execution_count > 0 {
-            eprintln!("Number of blocked executions seen: {blocked_execution_count}");
+        if genmc_config.verbose_output {
+            eprintln!("Finished estimation in {elapsed_time_sec:.2?}s");
+            if blocked_execs != 0 {
+                eprintln!("  Explored executions: {explored_execs}");
+                eprintln!("  Blocked  executions: {blocked_execs}");
+            }
+            eprintln!("Expected number of executions: {mean:.0} ± {sd:.0}");
+        }
+        // The estimation can be out-of-bounds of an `f64`.
+        if !(mean.is_finite() && mean >= 0.0 && sd.is_finite() && sd >= 0.0) {
+            eprintln!("WARNING: Estimation gave weird results, there may have been an overflow.");
         }
+        eprintln!("Expected verification time: {estimated_mean_sec:.2}s ± {estimated_sd_sec:.2}s");
+    }
 
-        // Return the return code of the last execution.
-        return Some(return_code);
+    /// Given the time taken for the verification mode run, print the expected time range for verification.
+    /// Verbose output also includes information about the expected number of executions and how many estimation rounds were explored or got blocked.
+    fn print_verification_output(&self, genmc_config: &GenmcConfig, elapsed_time_sec: f64) {
+        let explored_execution_count = self.get_explored_execution_count();
+        let blocked_execution_count = self.get_blocked_execution_count();
+        eprintln!(
+            "Verification complete with {} executions. No errors found.",
+            explored_execution_count + blocked_execution_count
+        );
+        if genmc_config.verbose_output {
+            if blocked_execution_count > 0 {
+                eprintln!("Number of complete executions explored: {explored_execution_count}");
+                eprintln!("Number of blocked executions seen: {blocked_execution_count}");
+            }
+            eprintln!("Verification took {elapsed_time_sec:.2?}s.");
+        }
     }
-    unreachable!()
 }
diff --git a/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr
index 946d9a2124b..00de74009d9 100644
--- a/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr
+++ b/src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: Undefined Behavior: Non-atomic race
   --> tests/genmc/fail/data_race/mpu2_rels_rlx.rs:LL:CC
    |
@@ -15,5 +16,6 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
 LL |         f();
    |         ^^^
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr
index 121ded2a181..501957a90d3 100644
--- a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr
+++ b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: Undefined Behavior: Non-atomic race
   --> tests/genmc/fail/data_race/weak_orderings.rs:LL:CC
    |
@@ -15,5 +16,6 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
 LL |         f();
    |         ^^^
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr
index 121ded2a181..501957a90d3 100644
--- a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr
+++ b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: Undefined Behavior: Non-atomic race
   --> tests/genmc/fail/data_race/weak_orderings.rs:LL:CC
    |
@@ -15,5 +16,6 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
 LL |         f();
    |         ^^^
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr
index 121ded2a181..501957a90d3 100644
--- a/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr
+++ b/src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: Undefined Behavior: Non-atomic race
   --> tests/genmc/fail/data_race/weak_orderings.rs:LL:CC
    |
@@ -15,5 +16,6 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
 LL |         f();
    |         ^^^
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr
index 5a8948ff9b4..9c3ba1d4c59 100644
--- a/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr
+++ b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/loom/buggy_inc.rs:LL:CC
    |
@@ -9,5 +10,6 @@ LL |             std::process::abort();
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr b/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr
index a6c3ed7055e..db92d0573fa 100644
--- a/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr
+++ b/src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/loom/store_buffering.rs:LL:CC
    |
@@ -9,5 +10,6 @@ LL |             std::process::abort();
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr
index cbfb6ec833e..773f86a9759 100644
--- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr
+++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/simple/2w2w_weak.rs:LL:CC
    |
@@ -9,5 +10,6 @@ LL |             std::process::abort();
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr
index cbfb6ec833e..773f86a9759 100644
--- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr
+++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/simple/2w2w_weak.rs:LL:CC
    |
@@ -9,5 +10,6 @@ LL |             std::process::abort();
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr
index cbfb6ec833e..773f86a9759 100644
--- a/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr
+++ b/src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 error: abnormal termination: the program aborted execution
   --> tests/genmc/fail/simple/2w2w_weak.rs:LL:CC
    |
@@ -9,5 +10,6 @@ LL |             std::process::abort();
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
 
+(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
 error: aborting due to 1 previous error
 
diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr b/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr
index d97b8b3d92f..31438f9352f 100644
--- a/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr
+++ b/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 warning: GenMC currently does not model the failure ordering for `compare_exchange`. Success ordering 'Release' was upgraded to 'AcqRel' to match failure ordering 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
   --> tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC
    |
@@ -18,5 +19,4 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/p
 LL |         f();
    |         ^^^
 
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 2
+Verification complete with 2 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr
index 3b22247ee44..7867be2dbe8 100644
--- a/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr
+++ b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 1
+Running GenMC Verification...
+Verification complete with 1 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr
index 3b22247ee44..7867be2dbe8 100644
--- a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr
+++ b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 1
+Running GenMC Verification...
+Verification complete with 1 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2cowr.stderr b/src/tools/miri/tests/genmc/pass/litmus/2cowr.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2cowr.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2cowr.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_2sc_scf.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release1.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release1.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release1.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release1.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release2.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release2.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release2.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_3sc_1rel.release2.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.sc.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4rel.weak.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4sc.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/2w2w_4sc.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/2w2w_4sc.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.stderr
index c760b446051..d6ec73a8c66 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 16
+Running GenMC Verification...
+Verification complete with 16 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr
index 4fc77b63f38..7ea2dd50851 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 [1, 1, 1, 1, 1]
 [1, 1, 1, 0, 1]
 [1, 1, 1, 0, 0]
@@ -26,5 +27,4 @@
 [0, 0, 0, 0, 0]
 [0, 0, 0, 0, 1]
 [0, 0, 0, 0, 0]
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 28
+Verification complete with 28 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/LB.stderr b/src/tools/miri/tests/genmc/pass/litmus/LB.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/LB.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/LB.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr b/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr
index c879e95a170..e414cd5e064 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/LB_incMPs.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 15
+Running GenMC Verification...
+Verification complete with 15 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP.stderr b/src/tools/miri/tests/genmc/pass/litmus/MP.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/MP.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/MP.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr b/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr
index 4551c00b057..29b59ce3bc1 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 X=1, Y=2, a=Err(1), b=Ok(1), c=2
 X=1, Y=2, a=Err(1), b=Ok(1), c=1
 X=1, Y=2, a=Err(1), b=Ok(1), c=0
@@ -34,5 +35,4 @@ X=1, Y=1, a=Err(0), b=Err(0), c=0
 X=1, Y=1, a=Err(0), b=Err(0), c=1
 X=1, Y=1, a=Err(0), b=Err(0), c=0
 X=1, Y=1, a=Err(0), b=Err(0), c=0
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 36
+Verification complete with 36 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr b/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr
index c5e34b00642..423ee6dc399 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 13
+Running GenMC Verification...
+Verification complete with 13 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr b/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr
index 2be9a6c7fbd..f527b612023 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/MP_incMPs.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 7
+Running GenMC Verification...
+Verification complete with 7 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr b/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/SB.stderr b/src/tools/miri/tests/genmc/pass/litmus/SB.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/SB.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/SB.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr b/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/SB_2sc_scf.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr
index 8dd2fbe1b97..c8fbb8951a3 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.sc.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 a=2, b=1, X=1, Y=3
 a=4, b=1, X=1, Y=4
 a=3, b=1, X=1, Y=3
@@ -16,5 +17,4 @@ a=3, b=0, X=1, Y=1
 a=1, b=1, X=1, Y=3
 a=1, b=1, X=1, Y=1
 a=1, b=0, X=1, Y=1
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 18
+Verification complete with 18 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr
index 65622575de2..72c59d33f77 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.weak.stderr
@@ -1,3 +1,4 @@
+Running GenMC Verification...
 a=2, b=1, X=1, Y=3
 a=4, b=1, X=1, Y=4
 a=4, b=0, X=1, Y=4
@@ -20,5 +21,4 @@ a=1, b=1, X=1, Y=3
 a=1, b=0, X=1, Y=3
 a=1, b=1, X=1, Y=1
 a=1, b=0, X=1, Y=1
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 22
+Verification complete with 22 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr b/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr
index 2be9a6c7fbd..f527b612023 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_acq.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 7
+Running GenMC Verification...
+Verification complete with 7 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr b/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/atomicpo.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr b/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr
index 01701dfe691..bde951866d0 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/casdep.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 2
+Running GenMC Verification...
+Verification complete with 2 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr b/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr
index 01701dfe691..bde951866d0 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/ccr.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 2
+Running GenMC Verification...
+Verification complete with 2 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/cii.stderr b/src/tools/miri/tests/genmc/pass/litmus/cii.stderr
index be75e68fde7..b9bdf2245ae 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/cii.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/cii.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 6
+Running GenMC Verification...
+Verification complete with 6 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr.stderr b/src/tools/miri/tests/genmc/pass/litmus/corr.stderr
index be75e68fde7..b9bdf2245ae 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/corr.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/corr.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 6
+Running GenMC Verification...
+Verification complete with 6 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr0.stderr b/src/tools/miri/tests/genmc/pass/litmus/corr0.stderr
index 0667962f99c..a67635dee1b 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/corr0.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/corr0.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 4
+Running GenMC Verification...
+Verification complete with 4 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr1.stderr b/src/tools/miri/tests/genmc/pass/litmus/corr1.stderr
index f6d07e9c77b..384425fc43c 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/corr1.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/corr1.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 36
+Running GenMC Verification...
+Verification complete with 36 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr2.stderr b/src/tools/miri/tests/genmc/pass/litmus/corr2.stderr
index 78a90b63fea..07fd2d4de18 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/corr2.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/corr2.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 72
+Running GenMC Verification...
+Verification complete with 72 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/corw.stderr b/src/tools/miri/tests/genmc/pass/litmus/corw.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/corw.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/corw.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/cowr.stderr b/src/tools/miri/tests/genmc/pass/litmus/cowr.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/cowr.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/cowr.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr b/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr
index 00394048ec5..a031dfc8977 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/cumul-release.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 8
+Running GenMC Verification...
+Verification complete with 8 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/default.stderr b/src/tools/miri/tests/genmc/pass/litmus/default.stderr
index e0313930282..87d38d25041 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/default.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/default.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 12
+Running GenMC Verification...
+Verification complete with 12 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/detour.join.stderr b/src/tools/miri/tests/genmc/pass/litmus/detour.join.stderr
index 15017249dc3..5006f11fefb 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/detour.join.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/detour.join.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 9
+Running GenMC Verification...
+Verification complete with 9 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/detour.no_join.stderr b/src/tools/miri/tests/genmc/pass/litmus/detour.no_join.stderr
index 15017249dc3..5006f11fefb 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/detour.no_join.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/detour.no_join.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 9
+Running GenMC Verification...
+Verification complete with 9 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.stderr b/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.stderr
index 3b6ba238f53..c09b50e282f 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 210
+Running GenMC Verification...
+Verification complete with 210 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr b/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr
index be75e68fde7..b9bdf2245ae 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/inc2w.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 6
+Running GenMC Verification...
+Verification complete with 6 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr b/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr
index b5f8cd15b68..770fb7ef880 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/inc_inc_RR_W_RR.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 600
+Running GenMC Verification...
+Verification complete with 600 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr b/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr
index 115b1986ce5..485142e945a 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/riwi.stderr
@@ -1,2 +1,2 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 3
+Running GenMC Verification...
+Verification complete with 3 executions. No errors found.
diff --git a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs
index a193dcf0683..3256c9f4211 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs
+++ b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.rs
@@ -1,6 +1,8 @@
-//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows -Zmiri-genmc-estimate
 
 // Translated from GenMC's "litmus/viktor-relseq" test.
+//
+// This test also checks that we can run the GenMC estimation mode.
 
 #![no_main]
 
diff --git a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr
index d63ac5199d5..c53d5c569b9 100644
--- a/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr
+++ b/src/tools/miri/tests/genmc/pass/litmus/viktor-relseq.stderr
@@ -1,2 +1,4 @@
-(GenMC) Verification complete. No errors were detected.
-Number of complete executions explored: 180
+Estimating GenMC verification time...
+Expected verification time: [MEAN] ± [SD]
+Running GenMC Verification...
+Verification complete with 180 executions. No errors found.
diff --git a/src/tools/miri/tests/ui.rs b/src/tools/miri/tests/ui.rs
index b7286d9a367..efaaf9fc841 100644
--- a/src/tools/miri/tests/ui.rs
+++ b/src/tools/miri/tests/ui.rs
@@ -277,6 +277,8 @@ regexes! {
     r"\bsys/([a-z_]+)/[a-z]+\b"     => "sys/$1/PLATFORM",
     // erase paths into the crate registry
     r"[^ ]*/\.?cargo/registry/.*/(.*\.rs)"  => "CARGO_REGISTRY/.../$1",
+    // remove time print from GenMC estimation mode output.
+    "\nExpected verification time: .* ± .*" => "\nExpected verification time: [MEAN] ± [SD]",
 }
 
 enum Dependencies {