make scheduler preemptive, with configurable preemption rate

Author: RalfJung

README.md

@@ -288,14 +288,16 @@ environment variable. We first document the most relevant and most commonly used
   `-Zmiri-disable-isolation` is set.
 * `-Zmiri-ignore-leaks` disables the memory leak checker, and also allows some
   remaining threads to exist when the main thread exits.
-* `-Zmiri-seed=<hex>` configures the seed of the RNG that Miri uses to resolve
-  non-determinism. This RNG is used to pick base addresses for allocations. When
-  isolation is enabled (the default), this is also used to emulate system
-  entropy. The default seed is 0. You can increase test coverage by running Miri
-  multiple times with different seeds.
-  **NOTE**: This entropy is not good enough for cryptographic use! Do not
-  generate secret keys in Miri or perform other kinds of cryptographic
-  operations that rely on proper random numbers.
+* `-Zmiri-preemption-rate` configures the probability that at the end of a basic block, the active
+  thread will be preempted. The default is `0.01` (i.e., 1%). Setting this to `0` disables
+  preemption.
+* `-Zmiri-seed=<hex>` configures the seed of the RNG that Miri uses to resolve non-determinism. This
+  RNG is used to pick base addresses for allocations, to determine preemption and failure of
+  `compare_exchange_weak`, and to control store buffering for weak memory emulation. When isolation
+  is enabled (the default), this is also used to emulate system entropy. The default seed is 0. You
+  can increase test coverage by running Miri multiple times with different seeds. **NOTE**: This
+  entropy is not good enough for cryptographic use! Do not generate secret keys in Miri or perform
+  other kinds of cryptographic operations that rely on proper random numbers.
 * `-Zmiri-strict-provenance` enables [strict
   provenance](https://github.com/rust-lang/rust/issues/95228) checking in Miri. This means that
   casting an integer to a pointer yields a result with 'invalid' provenance, i.e., with provenance

src/bin/miri.rs

@@ -449,6 +449,17 @@ fn main() {
                     ),
             };
             miri_config.cmpxchg_weak_failure_rate = rate;
+        } else if let Some(param) = arg.strip_prefix("-Zmiri-preemption-rate=") {
+            let rate = match param.parse::<f64>() {
+                Ok(rate) if rate >= 0.0 && rate <= 1.0 => rate,
+                Ok(_) => panic!("-Zmiri-preemption-rate must be between `0.0` and `1.0`"),
+                Err(err) =>
+                    panic!(
+                        "-Zmiri-preemption-rate requires a `f64` between `0.0` and `1.0`: {}",
+                        err
+                    ),
+            };
+            miri_config.preemption_rate = rate;
         } else if let Some(param) = arg.strip_prefix("-Zmiri-measureme=") {
             miri_config.measureme_out = Some(param.to_string());
         } else if let Some(param) = arg.strip_prefix("-Zmiri-backtrace=") {

src/eval.rs

@@ -122,6 +122,8 @@ pub struct MiriConfig {
     /// Whether to ignore any output by the program. This is helpful when debugging miri
     /// as its messages don't get intermingled with the program messages.
     pub mute_stdout_stderr: bool,
+    /// The probability of the active thread being preempted at the end of each basic block.
+    pub preemption_rate: f64,
 }
 
 impl Default for MiriConfig {
@@ -145,12 +147,13 @@ impl Default for MiriConfig {
             tag_raw: false,
             data_race_detector: true,
             weak_memory_emulation: true,
-            cmpxchg_weak_failure_rate: 0.8,
+            cmpxchg_weak_failure_rate: 0.8, // 80%
             measureme_out: None,
             panic_on_unsupported: false,
             backtrace_style: BacktraceStyle::Short,
             provenance_mode: ProvenanceMode::Legacy,
             mute_stdout_stderr: false,
+            preemption_rate: 0.01, // 1%
         }
     }
 }

src/machine.rs

@@ -333,6 +333,9 @@ pub struct Evaluator<'mir, 'tcx> {
 
     /// Whether weak memory emulation is enabled
     pub(crate) weak_memory: bool,
+
+    /// The probability of the active thread being preempted at the end of each basic block.
+    pub(crate) preemption_rate: f64,
 }
 
 impl<'mir, 'tcx> Evaluator<'mir, 'tcx> {
@@ -389,6 +392,7 @@ impl<'mir, 'tcx> Evaluator<'mir, 'tcx> {
             cmpxchg_weak_failure_rate: config.cmpxchg_weak_failure_rate,
             mute_stdout_stderr: config.mute_stdout_stderr,
             weak_memory: config.weak_memory_emulation,
+            preemption_rate: config.preemption_rate,
         }
     }
 
@@ -846,6 +850,11 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for Evaluator<'mir, 'tcx> {
         ecx.active_thread_stack_mut()
     }
 
+    fn before_terminator(ecx: &mut InterpCx<'mir, 'tcx, Self>) -> InterpResult<'tcx> {
+        ecx.maybe_preempt_active_thread();
+        Ok(())
+    }
+
     #[inline(always)]
     fn after_stack_push(ecx: &mut InterpCx<'mir, 'tcx, Self>) -> InterpResult<'tcx> {
         if ecx.machine.stacked_borrows.is_some() { ecx.retag_return_place() } else { Ok(()) }

src/thread.rs

@@ -717,6 +717,16 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
         this.machine.threads.yield_active_thread();
     }
 
+    #[inline]
+    fn maybe_preempt_active_thread(&mut self) {
+        use rand::Rng as _;
+
+        let this = self.eval_context_mut();
+        if this.machine.rng.get_mut().gen_bool(this.machine.preemption_rate) {
+            this.yield_active_thread();
+        }
+    }
+
     #[inline]
     fn register_timeout_callback(
         &mut self,

tests/fail/concurrency/libc_pthread_join_self.rs

@@ -1,4 +1,6 @@
 // ignore-windows: No libc on Windows
+// We are making scheduler assumptions here.
+// compile-flags: -Zmiri-preemption-rate=0
 
 // Joining itself is undefined behavior.
 

tests/fail/data_race/alloc_read_race.rs

@@ -1,5 +1,5 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
-// compile-flags: -Zmiri-disable-weak-memory-emulation
+// compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
 #![feature(new_uninit)]
 
 use std::thread::spawn;

tests/fail/data_race/alloc_write_race.rs

@@ -1,5 +1,5 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
-// compile-flags: -Zmiri-disable-weak-memory-emulation
+// compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
 #![feature(new_uninit)]
 
 use std::thread::spawn;

tests/fail/data_race/dealloc_read_race_stack.rs

@@ -1,5 +1,5 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
-// compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation
+// compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
 
 use std::thread::{spawn, sleep};
 use std::ptr::null_mut;

tests/fail/data_race/dealloc_write_race_stack.rs

@@ -1,5 +1,5 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
-// compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation
+// compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
 
 use std::thread::{spawn, sleep};
 use std::ptr::null_mut;

tests/fail/data_race/read_write_race_stack.rs

@@ -1,5 +1,5 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
-// compile-flags: -Zmiri-disable-isolation -Zmir-opt-level=0 -Zmiri-disable-weak-memory-emulation
+// compile-flags: -Zmiri-disable-isolation -Zmir-opt-level=0 -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
 
 // Note: mir-opt-level set to 0 to prevent the read of stack_var in thread 1
 // from being optimized away and preventing the detection of the data-race.

tests/fail/data_race/relax_acquire_race.rs

@@ -1,5 +1,5 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
-// compile-flags: -Zmiri-disable-weak-memory-emulation
+// compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
 
 use std::thread::spawn;
 use std::sync::atomic::{AtomicUsize, Ordering};

tests/fail/data_race/release_seq_race.rs

@@ -1,5 +1,5 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
-// compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation
+// compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
 
 use std::thread::{spawn, sleep};
 use std::sync::atomic::{AtomicUsize, Ordering};

tests/fail/data_race/release_seq_race_same_thread.rs

@@ -1,5 +1,5 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
-// compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation
+// compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
 
 use std::thread::spawn;
 use std::sync::atomic::{AtomicUsize, Ordering};

tests/fail/data_race/rmw_race.rs

@@ -1,5 +1,5 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
-// compile-flags: -Zmiri-disable-weak-memory-emulation
+// compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
 
 use std::thread::spawn;
 use std::sync::atomic::{AtomicUsize, Ordering};

tests/fail/data_race/write_write_race_stack.rs

@@ -1,5 +1,5 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
-// compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation
+// compile-flags: -Zmiri-disable-isolation -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
 
 use std::thread::{spawn, sleep};
 use std::ptr::null_mut;

tests/pass/concurrency/spin_loop.rs

@@ -0,0 +1,42 @@
+use std::thread;
+use std::sync::atomic::{AtomicUsize, Ordering};
+
+static FLAG: AtomicUsize = AtomicUsize::new(0);
+
+fn spin() {
+    let j = thread::spawn(|| {
+        while FLAG.load(Ordering::Acquire) == 0 {
+            // We do *not* yield, and yet this should terminate eventually.
+        }
+    });
+    thread::yield_now(); // schedule the other thread
+    FLAG.store(1, Ordering::Release);
+    j.join().unwrap();
+}
+
+fn two_player_ping_pong() {
+    static FLAG: AtomicUsize = AtomicUsize::new(0);
+
+    let waiter1 = thread::spawn(|| {
+        while FLAG.load(Ordering::Acquire) == 0 {
+            // We do *not* yield, and yet this should terminate eventually.
+        }
+    });
+    let waiter2 = thread::spawn(|| {
+        while FLAG.load(Ordering::Acquire) == 0 {
+            // We do *not* yield, and yet this should terminate eventually.
+        }
+    });
+    let progress = thread::spawn(|| {
+        FLAG.store(1, Ordering::Release);
+    });
+    // The first `join` blocks the main thread and thus takes it out of the equation.
+    waiter1.join().unwrap();
+    waiter2.join().unwrap();
+    progress.join().unwrap();
+}
+
+fn main() {
+    spin();
+    two_player_ping_pong();
+}

tests/pass/concurrency/spin_loop.stderr

@@ -0,0 +1,3 @@
+warning: thread support is experimental: the scheduler is not preemptive, and can get stuck in spin loops.
+         (see https://github.com/rust-lang/miri/issues/1388)
+

tests/pass/concurrency/spin_loops.rs renamed to tests/pass/concurrency/spin_loops_nopreempt.rs

@@ -1,4 +1,6 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
+// This specifically tests behavior *without* preemption.
+// compile-flags: -Zmiri-preemption-rate=0
 
 use std::thread;
 use std::sync::atomic::{AtomicBool, AtomicUsize, Ordering};

tests/pass/concurrency/spin_loops_nopreempt.stderr

@@ -0,0 +1,3 @@
+warning: thread support is experimental: the scheduler is not preemptive, and can get stuck in spin loops.
+         (see https://github.com/rust-lang/miri/issues/1388)
+

tests/pass/concurrency/sync.rs

@@ -1,5 +1,6 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
-// compile-flags: -Zmiri-disable-isolation -Zmiri-strict-provenance
+// We are making scheduler assumptions here.
+// compile-flags: -Zmiri-disable-isolation -Zmiri-strict-provenance -Zmiri-preemption-rate=0
 
 use std::sync::{Arc, Barrier, Condvar, Mutex, Once, RwLock};
 use std::thread;

tests/pass/panic/concurrent-panic.rs

@@ -1,4 +1,6 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
+// We are making scheduler assumptions here.
+// compile-flags: -Zmiri-preemption-rate=0
 
 //! Cause a panic in one thread while another thread is unwinding. This checks
 //! that separate threads have their own panicking state.

tests/pass/weak_memory/weak.rs

@@ -1,5 +1,5 @@
 // ignore-windows: Concurrency on Windows is not supported yet.
-// compile-flags: -Zmiri-ignore-leaks
+// compile-flags: -Zmiri-ignore-leaks -Zmiri-preemption-rate=0
 
 // Tests showing weak memory behaviours are exhibited. All tests
 // return true when the desired behaviour is seen.