Skip to content

Commit

Permalink
Auto merge of #2208 - RalfJung:preempt, r=RalfJung
Browse files Browse the repository at this point in the history
Make scheduler preemptive

This is actually fairly easy. :D I just roll the dice on each terminator to decide whether we want to yield the active thread. I think with this we are also justified to no longer show "experimental" warnings when a thread is spawned. :)

Closes #1388
  • Loading branch information
bors committed Jun 7, 2022
2 parents d98bd98 + 11a8b3a commit ad576d8
Show file tree
Hide file tree
Showing 88 changed files with 192 additions and 273 deletions.
18 changes: 10 additions & 8 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
11 changes: 11 additions & 0 deletions src/bin/miri.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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=") {
Expand Down
2 changes: 1 addition & 1 deletion src/concurrency/mod.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
mod allocation_map;
pub mod data_race;
mod range_object_map;
pub mod weak_memory;
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
//! Implements a map from allocation ranges to data.
//! This is somewhat similar to RangeMap, but the ranges
//! and data are discrete and non-splittable. An allocation in the
//! map will always have the same range until explicitly removed
//! Implements a map from allocation ranges to data. This is somewhat similar to RangeMap, but the
//! ranges and data are discrete and non-splittable -- they represent distinct "objects". An
//! allocation in the map will always have the same range until explicitly removed

use rustc_target::abi::Size;
use std::ops::{Index, IndexMut, Range};
Expand All @@ -20,7 +19,7 @@ struct Elem<T> {
type Position = usize;

#[derive(Clone, Debug)]
pub struct AllocationMap<T> {
pub struct RangeObjectMap<T> {
v: Vec<Elem<T>>,
}

Expand All @@ -34,7 +33,7 @@ pub enum AccessType {
ImperfectlyOverlapping(Range<Position>),
}

impl<T> AllocationMap<T> {
impl<T> RangeObjectMap<T> {
pub fn new() -> Self {
Self { v: Vec::new() }
}
Expand Down Expand Up @@ -135,15 +134,15 @@ impl<T> AllocationMap<T> {
}
}

impl<T> Index<Position> for AllocationMap<T> {
impl<T> Index<Position> for RangeObjectMap<T> {
type Output = T;

fn index(&self, pos: Position) -> &Self::Output {
&self.v[pos].data
}
}

impl<T> IndexMut<Position> for AllocationMap<T> {
impl<T> IndexMut<Position> for RangeObjectMap<T> {
fn index_mut(&mut self, pos: Position) -> &mut Self::Output {
&mut self.v[pos].data
}
Expand All @@ -159,7 +158,7 @@ mod tests {
fn empty_map() {
// FIXME: make Size::from_bytes const
let four = Size::from_bytes(4);
let map = AllocationMap::<()>::new();
let map = RangeObjectMap::<()>::new();

// Correctly tells where we should insert the first element (at position 0)
assert_eq!(map.find_offset(Size::from_bytes(3)), Err(0));
Expand All @@ -173,7 +172,7 @@ mod tests {
fn no_overlapping_inserts() {
let four = Size::from_bytes(4);

let mut map = AllocationMap::<&str>::new();
let mut map = RangeObjectMap::<&str>::new();

// |_|_|_|_|#|#|#|#|_|_|_|_|...
// 0 1 2 3 4 5 6 7 8 9 a b c d
Expand All @@ -187,7 +186,7 @@ mod tests {
fn boundaries() {
let four = Size::from_bytes(4);

let mut map = AllocationMap::<&str>::new();
let mut map = RangeObjectMap::<&str>::new();

// |#|#|#|#|_|_|...
// 0 1 2 3 4 5
Expand Down Expand Up @@ -215,7 +214,7 @@ mod tests {
fn perfectly_overlapping() {
let four = Size::from_bytes(4);

let mut map = AllocationMap::<&str>::new();
let mut map = RangeObjectMap::<&str>::new();

// |#|#|#|#|_|_|...
// 0 1 2 3 4 5
Expand All @@ -241,7 +240,7 @@ mod tests {
fn straddling() {
let four = Size::from_bytes(4);

let mut map = AllocationMap::<&str>::new();
let mut map = RangeObjectMap::<&str>::new();

// |_|_|_|_|#|#|#|#|_|_|_|_|...
// 0 1 2 3 4 5 6 7 8 9 a b c d
Expand Down
6 changes: 3 additions & 3 deletions src/concurrency/weak_memory.rs
Original file line number Diff line number Diff line change
Expand Up @@ -85,8 +85,8 @@ use rustc_data_structures::fx::FxHashMap;
use crate::{AtomicReadOp, AtomicRwOp, AtomicWriteOp, Tag, VClock, VTimestamp, VectorIdx};

use super::{
allocation_map::{AccessType, AllocationMap},
data_race::{GlobalState, ThreadClockSet},
range_object_map::{AccessType, RangeObjectMap},
};

pub type AllocExtra = StoreBufferAlloc;
Expand All @@ -101,7 +101,7 @@ const STORE_BUFFER_LIMIT: usize = 128;
pub struct StoreBufferAlloc {
/// Store buffer of each atomic object in this allocation
// Behind a RefCell because we need to allocate/remove on read access
store_buffers: RefCell<AllocationMap<StoreBuffer>>,
store_buffers: RefCell<RangeObjectMap<StoreBuffer>>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
Expand Down Expand Up @@ -134,7 +134,7 @@ struct StoreElement {

impl StoreBufferAlloc {
pub fn new_allocation() -> Self {
Self { store_buffers: RefCell::new(AllocationMap::new()) }
Self { store_buffers: RefCell::new(RangeObjectMap::new()) }
}

/// Checks if the range imperfectly overlaps with existing buffers
Expand Down
5 changes: 4 additions & 1 deletion src/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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%
}
}
}
Expand Down
9 changes: 9 additions & 0 deletions src/machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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> {
Expand Down Expand Up @@ -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,
}
}

Expand Down Expand Up @@ -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(()) }
Expand Down
4 changes: 0 additions & 4 deletions src/shims/unix/thread.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,6 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
) -> InterpResult<'tcx, i32> {
let this = self.eval_context_mut();

this.tcx.sess.warn(
"thread support is experimental: the scheduler is not preemptive, and can get stuck in spin loops.\n(see https://github.com/rust-lang/miri/issues/1388)",
);

// Create the new thread
let new_thread_id = this.create_thread();

Expand Down
10 changes: 10 additions & 0 deletions src/thread.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
Original file line number Diff line number Diff line change
@@ -1,9 +1,6 @@
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)

error: the main thread terminated without waiting for all remaining threads

note: pass `-Zmiri-ignore-leaks` to disable this check

error: aborting due to previous error; 1 warning emitted
error: aborting due to previous error

5 changes: 1 addition & 4 deletions tests/fail/concurrency/libc_pthread_join_detached.stderr
Original file line number Diff line number Diff line change
@@ -1,6 +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)

error: Undefined Behavior: trying to join a detached or already joined thread
--> $DIR/libc_pthread_join_detached.rs:LL:CC
|
Expand All @@ -14,5 +11,5 @@ LL | ... assert_eq!(libc::pthread_join(native, ptr::null_mut()), 0);

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to previous error; 1 warning emitted
error: aborting due to previous error

5 changes: 1 addition & 4 deletions tests/fail/concurrency/libc_pthread_join_joined.stderr
Original file line number Diff line number Diff line change
@@ -1,6 +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)

error: Undefined Behavior: trying to join a detached or already joined thread
--> $DIR/libc_pthread_join_joined.rs:LL:CC
|
Expand All @@ -14,5 +11,5 @@ LL | ... assert_eq!(libc::pthread_join(native, ptr::null_mut()), 0);

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to previous error; 1 warning emitted
error: aborting due to previous error

5 changes: 1 addition & 4 deletions tests/fail/concurrency/libc_pthread_join_main.stderr
Original file line number Diff line number Diff line change
@@ -1,6 +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)

error: Undefined Behavior: trying to join a detached or already joined thread
--> $DIR/libc_pthread_join_main.rs:LL:CC
|
Expand All @@ -14,5 +11,5 @@ LL | ... assert_eq!(libc::pthread_join(thread_id, ptr::null_mut()), 0);

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to previous error; 1 warning emitted
error: aborting due to previous error

5 changes: 1 addition & 4 deletions tests/fail/concurrency/libc_pthread_join_multiple.stderr
Original file line number Diff line number Diff line change
@@ -1,6 +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)

error: Undefined Behavior: trying to join a detached or already joined thread
--> $DIR/libc_pthread_join_multiple.rs:LL:CC
|
Expand All @@ -14,5 +11,5 @@ LL | ... assert_eq!(libc::pthread_join(native_copy, ptr::null_mut()), 0);

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to previous error; 1 warning emitted
error: aborting due to previous error

2 changes: 2 additions & 0 deletions tests/fail/concurrency/libc_pthread_join_self.rs
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
5 changes: 1 addition & 4 deletions tests/fail/concurrency/libc_pthread_join_self.stderr
Original file line number Diff line number Diff line change
@@ -1,6 +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)

error: Undefined Behavior: trying to join itself
--> $DIR/libc_pthread_join_self.rs:LL:CC
|
Expand All @@ -14,5 +11,5 @@ LL | assert_eq!(libc::pthread_join(native, ptr::null_mut()), 0);

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to previous error; 1 warning emitted
error: aborting due to previous error

5 changes: 1 addition & 4 deletions tests/fail/concurrency/thread_local_static_dealloc.stderr
Original file line number Diff line number Diff line change
@@ -1,6 +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)

error: Undefined Behavior: pointer to ALLOC was dereferenced after this allocation got freed
--> $DIR/thread_local_static_dealloc.rs:LL:CC
|
Expand All @@ -14,5 +11,5 @@ LL | let _val = *(dangling_ptr as *const u8);

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to previous error; 1 warning emitted
error: aborting due to previous error

5 changes: 1 addition & 4 deletions tests/fail/concurrency/too_few_args.stderr
Original file line number Diff line number Diff line change
@@ -1,6 +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)

error: Undefined Behavior: callee has fewer arguments than expected
--> $DIR/too_few_args.rs:LL:CC
|
Expand All @@ -13,5 +10,5 @@ LL | panic!()
= note: inside `thread_start` at RUSTLIB/std/src/panic.rs:LL:CC
= note: this error originates in the macro `$crate::panic::panic_2015` (in Nightly builds, run with -Z macro-backtrace for more info)

error: aborting due to previous error; 1 warning emitted
error: aborting due to previous error

5 changes: 1 addition & 4 deletions tests/fail/concurrency/too_many_args.stderr
Original file line number Diff line number Diff line change
@@ -1,6 +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)

error: Undefined Behavior: callee has more arguments than expected
--> $DIR/too_many_args.rs:LL:CC
|
Expand All @@ -13,5 +10,5 @@ LL | panic!()
= note: inside `thread_start` at RUSTLIB/std/src/panic.rs:LL:CC
= note: this error originates in the macro `$crate::panic::panic_2015` (in Nightly builds, run with -Z macro-backtrace for more info)

error: aborting due to previous error; 1 warning emitted
error: aborting due to previous error

5 changes: 1 addition & 4 deletions tests/fail/concurrency/unwind_top_of_stack.stderr
Original file line number Diff line number Diff line change
@@ -1,6 +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)

thread '<unnamed>' panicked at 'explicit panic', $DIR/unwind_top_of_stack.rs:LL:CC
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: Undefined Behavior: unwinding past the topmost frame of the stack
Expand All @@ -16,5 +13,5 @@ LL | | }

= note: inside `thread_start` at $DIR/unwind_top_of_stack.rs:LL:CC

error: aborting due to previous error; 1 warning emitted
error: aborting due to previous error

Loading

0 comments on commit ad576d8

Please sign in to comment.