Expand GenMC mode:

- Implement support for 'assume' statements.
- Improve scheduling and next instruction type determination.
- Improve GenMC mode documentation.

Co-authored-by: Ralf Jung <[email protected]>

Author: Patrick-6

doc/genmc.md

@@ -1,15 +1,26 @@
 # **(WIP)** Documentation for Miri-GenMC
 
+**NOTE: GenMC mode is not yet fully implemented, and has [several correctness issues](https://github.com/rust-lang/miri/issues/4572). Using GenMC mode currently requires manually compiling Miri, see [Usage](#usage).**
+
+
 [GenMC](https://github.com/MPI-SWS/genmc) is a stateless model checker for exploring concurrent executions of a program.
 Miri-GenMC integrates that model checker into Miri.
 
-**NOTE: Currently, no actual GenMC functionality is part of Miri, this is still WIP.**
+Miri in GenMC mode takes a program as input like regular Miri, but instead of running it once, the program is executed repeatedly, until all possible executions allowed by the Rust memory model are explored.
+This includes all possible thread interleavings and all allowed return values for atomic operations, including cases that are very rare to encounter on actual hardware.
+(However, this does not include other sources of non-determinism, such as the absolute addresses of allocations.
+It is hence still possible to have latent bugs in a test case even if they passed GenMC.)
 
-<!-- FIXME(genmc): add explanation. -->
+GenMC requires the input program to be bounded, i.e., have finitely many possible executions, otherwise it will not terminate.
+Any loops that may run infinitely must be replaced or bounded (see below).
+
+GenMC makes use of Dynamic Partial Order Reduction (DPOR) to reduce the number of executions that must be explored, but the runtime can still be super-exponential in the size of the input program (number of threads and amount of interaction between threads).
+Large programs may not be verifiable in a reasonable amount of time.
 
 ## Usage
 
 For testing/developing Miri-GenMC:
+- install all [dependencies required by GenMC](https://github.com/MPI-SWS/genmc?tab=readme-ov-file#dependencies)
 - clone the Miri repo.
 - build Miri-GenMC with `./miri build --features=genmc`.
 - OR: install Miri-GenMC in the current system with `./miri install --features=genmc`
@@ -50,6 +61,68 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
 
 <!-- FIXME(genmc): add tips for using Miri-GenMC more efficiently. -->
 
+### Eliminating unbounded loops
+
+#### Limiting the number of explored executions
+
+The number of explored executions in a concurrent program can increase super-exponentially in the size of the program.
+Reducing the number of explored executions is the most impactful way to improve verification times.
+Some programs also contain possibly infinite loops, which are not supported by GenMC.
+
+One way to drastically improve verification performance is by bounding spinloops.
+A spinloop may loop a many times before it can finally make progress.
+If such a loop doesn't have any visible side effects, meaning it does not matter to the outcome of the program whether the loop ran once or a million time, then the loop can be limited to one iteration.
+
+The following code gives an example for how to replace a loop that waits for a boolean to be true.
+Since there are no side effects, replacing the loop with one iteration is safe.
+
+```rust
+#[cfg(miri)]
+unsafe extern "Rust" {
+  // This is a special function that Miri provides.
+  // It blocks the thread calling this function if the condition is false.
+  pub unsafe fn miri_genmc_assume(condition: bool);
+}
+
+/// This functions loads an atomic boolean in a loop until it is true.
+/// GenMC will explore all executions where this does 1, 2, ..., ∞ loads, which means the verification will never terminate.
+fn spin_until_true(flag: &AtomicBool) {
+  while (!flag.load(Relaxed)) {
+    std::hint::spin_loop();
+  }
+}
+
+/// By replacing this loop with an assume statement, the only executions that will be explored are those with exactly 1 load.
+/// Incorrect use of assume statements can lead GenMC to miss important executions, so it is marked `unsafe`.
+fn spin_until_true_genmc(flag: &AtomicBool) {
+  unsafe { miri_genmc_assume(flag.load(Relaxed)); }
+}
+```
+
+Some loops do contain side effects, meaning the number of explored iterations affects the rest of the program.
+Replacing the loop with one iteration like we did above would mean we miss all those possible executions.
+
+In such a case, the loop can be limited to a fixed number of iterations instead.
+The choice of iteration limit trades off verification time for possibly missing bugs requiring more iterations.
+
+```rust
+/// The loop in this function has a side effect, which is to increment the counter for the number of iterations.
+/// Instead of replacing the loop entirely (which would miss all executions with `count > 0`), we limit the loop to at most 3 iterations.
+fn count_until_true_genmc(flag: &AtomicBool) -> u64 {
+  let mut count = 0;
+  while (!flag.load(Relaxed)) {
+    // Any execution that takes more than 3 iterations will not be explored.
+    unsafe { miri_genmc_assume(count < 3); }
+    count += 1;
+    std::hint::spin_loop();
+  }
+  count
+}
+```
+
+<!-- FIXME: update the code above once Miri supports a loop bounding features like GenMC's `--unroll=N`. -->
+<!-- FIXME: update this section once Miri-GenMC supports automatic program transformations (like spinloop-assume replacement). -->
+
 ## Limitations
 
 Some or all of these limitations might get removed in the future:

genmc-sys/cpp/include/MiriInterface.hpp

@@ -134,6 +134,13 @@ struct MiriGenmcShim : private GenMCDriver {
     void handle_thread_finish(ThreadId thread_id, uint64_t ret_val);
     void handle_thread_kill(ThreadId thread_id);
 
+    /**** Blocking instructions ****/
+    /// Inform GenMC that the thread should be blocked.
+    /// Note: this function is currently hardcoded for `AssumeType::User`, corresponding to user
+    /// supplied assume statements. This can become a parameter once more types of assumes are
+    /// added.
+    void handle_assume_block(ThreadId thread_id);
+
     /***** Exploration related functionality *****/
 
     /** Ask the GenMC scheduler for a new thread to schedule and return whether the execution is

genmc-sys/cpp/src/MiriInterface/EventHandling.cpp

@@ -30,6 +30,12 @@
 #include <memory>
 #include <utility>
 
+/**** Blocking instructions ****/
+
+void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {
+    GenMCDriver::handleAssume(inc_pos(thread_id), AssumeType::User);
+}
+
 /**** Memory access handling ****/
 
 [[nodiscard]] auto MiriGenmcShim::handle_load(

genmc-sys/src/lib.rs

@@ -258,9 +258,11 @@ mod ffi {
     /// Corresponds to GenMC's type with the same name.
     /// Should only be modified if changed by GenMC.
     enum ActionKind {
-        /// Any Mir terminator that's atomic and has load semantics.
+        /// Any MIR terminator that's atomic and that may have load semantics.
+        /// This includes functions with atomic properties, such as `pthread_create`.
+        /// If the exact type of the terminator cannot be determined, load is a safe default `Load`.
         Load,
-        /// Anything that's not a `Load`.
+        /// Anything that's definitely not a `Load`.
         NonLoad,
     }
 
@@ -412,6 +414,12 @@ mod ffi {
         fn handle_thread_finish(self: Pin<&mut MiriGenmcShim>, thread_id: i32, ret_val: u64);
         fn handle_thread_kill(self: Pin<&mut MiriGenmcShim>, thread_id: i32);
 
+        /**** Blocking instructions ****/
+        /// Inform GenMC that the thread should be blocked.
+        /// Note: this function is currently hardcoded for `AssumeType::User`, corresponding to user supplied assume statements.
+        /// This can become a parameter once more types of assumes are added.
+        fn handle_assume_block(self: Pin<&mut MiriGenmcShim>, thread_id: i32);
+
         /***** Exploration related functionality *****/
 
         /// Ask the GenMC scheduler for a new thread to schedule and

src/concurrency/genmc/dummy.rs

@@ -1,11 +1,12 @@
 use rustc_abi::{Align, Size};
 use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult};
 
+pub use self::intercept::EvalContextExt as GenmcEvalContextExt;
 pub use self::run::run_genmc_mode;
 use crate::intrinsics::AtomicRmwOp;
 use crate::{
-    AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MemoryKind, MiriMachine, Scalar,
-    ThreadId, ThreadManager, VisitProvenance, VisitWith,
+    AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MemoryKind, MiriMachine, OpTy,
+    Scalar, ThreadId, ThreadManager, VisitProvenance, VisitWith,
 };
 
 #[derive(Clone, Copy, Debug)]
@@ -36,9 +37,27 @@ mod run {
     }
 }
 
+mod intercept {
+    use super::*;
+
+    impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
+    pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
+        fn handle_genmc_verifier_assume(&mut self, _condition: &OpTy<'tcx>) -> InterpResult<'tcx> {
+            unreachable!();
+        }
+    }
+}
+
 impl GenmcCtx {
     // We don't provide the `new` function in the dummy module.
 
+    pub(crate) fn schedule_thread<'tcx>(
+        &self,
+        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
+    ) -> InterpResult<'tcx, Option<ThreadId>> {
+        unreachable!()
+    }
+
     /**** Memory access handling ****/
 
     pub(super) fn set_ongoing_action_data_race_free(&self, _enable: bool) {
@@ -191,26 +210,6 @@ impl GenmcCtx {
     ) -> InterpResult<'tcx> {
         unreachable!()
     }
-
-    /**** Scheduling functionality ****/
-
-    pub fn schedule_thread<'tcx>(
-        &self,
-        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
-    ) -> InterpResult<'tcx, ThreadId> {
-        unreachable!()
-    }
-
-    /**** Blocking instructions ****/
-
-    #[allow(unused)]
-    pub(crate) fn handle_verifier_assume<'tcx>(
-        &self,
-        _machine: &MiriMachine<'tcx>,
-        _condition: bool,
-    ) -> InterpResult<'tcx, ()> {
-        unreachable!()
-    }
 }
 
 impl VisitProvenance for GenmcCtx {

src/concurrency/genmc/intercept.rs

@@ -0,0 +1,38 @@
+use tracing::debug;
+
+use crate::concurrency::thread::EvalContextExt as _;
+use crate::{
+    BlockReason, InterpResult, MachineCallback, MiriInterpCx, OpTy, UnblockKind, VisitProvenance,
+    VisitWith, callback, interp_ok,
+};
+
+// Handling of code intercepted by Miri in GenMC mode, such as assume statement or `std::sync::Mutex`.
+
+/// Other functionality not directly related to event handling
+impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
+pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
+    /// Handle an `assume` statement. This will tell GenMC to block the current thread if the `condition` is false.
+    /// Returns `true` if the current thread should be blocked in Miri too.
+    fn handle_genmc_verifier_assume(&mut self, condition: &OpTy<'tcx>) -> InterpResult<'tcx> {
+        let this = self.eval_context_mut();
+        let condition_bool = this.read_scalar(condition)?.to_bool()?;
+        debug!("GenMC: handle_genmc_verifier_assume, condition: {condition:?} = {condition_bool}");
+        if condition_bool {
+            return interp_ok(());
+        }
+        let genmc_ctx = this.machine.data_race.as_genmc_ref().unwrap();
+        genmc_ctx.handle_assume_block(&this.machine)?;
+        this.block_thread(
+            BlockReason::Genmc,
+            None,
+            callback!(
+                @capture<'tcx> {}
+                |_this, unblock: UnblockKind| {
+                    assert_eq!(unblock, UnblockKind::Ready);
+                    unreachable!("GenMC should never unblock a thread blocked by an `assume`.");
+                }
+            ),
+        );
+        interp_ok(())
+    }
+}

src/concurrency/genmc/mod.rs

@@ -29,13 +29,15 @@ use crate::{
 mod config;
 mod global_allocations;
 mod helper;
+mod intercept;
 mod run;
 pub(crate) mod scheduling;
 mod thread_id_map;
 
 pub use genmc_sys::GenmcParams;
 
 pub use self::config::GenmcConfig;
+pub use self::intercept::EvalContextExt as GenmcEvalContextExt;
 pub use self::run::run_genmc_mode;
 
 #[derive(Debug)]
@@ -732,17 +734,6 @@ impl GenmcCtx {
         self.exec_state.exit_status.set(Some(exit_status));
         interp_ok(())
     }
-
-    /**** Blocking instructions ****/
-
-    #[allow(unused)]
-    pub(crate) fn handle_verifier_assume<'tcx>(
-        &self,
-        machine: &MiriMachine<'tcx>,
-        condition: bool,
-    ) -> InterpResult<'tcx, ()> {
-        if condition { interp_ok(()) } else { self.handle_user_block(machine) }
-    }
 }
 
 impl GenmcCtx {
@@ -903,8 +894,13 @@ impl GenmcCtx {
     /// Handle a user thread getting blocked.
     /// This may happen due to an manual `assume` statement added by a user
     /// or added by some automated program transformation, e.g., for spinloops.
-    fn handle_user_block<'tcx>(&self, _machine: &MiriMachine<'tcx>) -> InterpResult<'tcx> {
-        todo!()
+    fn handle_assume_block<'tcx>(&self, machine: &MiriMachine<'tcx>) -> InterpResult<'tcx> {
+        let curr_thread = machine.threads.active_thread();
+        let genmc_curr_thread =
+            self.exec_state.thread_id_manager.borrow().get_genmc_tid(curr_thread);
+        debug!("GenMC: assume statement, blocking thread {curr_thread:?} ({genmc_curr_thread:?})");
+        self.handle.borrow_mut().pin_mut().handle_assume_block(genmc_curr_thread);
+        interp_ok(())
     }
 }