Merge pull request #4272 from geetanshjuneja/scheduling
Make thread scheduling fully random
This commit is contained in:
commit
f521fa0c54
76 changed files with 111 additions and 92 deletions
|
|
@ -573,6 +573,8 @@ fn main() {
|
|||
miri_config.mute_stdout_stderr = true;
|
||||
} else if arg == "-Zmiri-retag-fields" {
|
||||
miri_config.retag_fields = RetagFields::Yes;
|
||||
} else if arg == "-Zmiri-fixed-schedule" {
|
||||
miri_config.fixed_scheduling = true;
|
||||
} else if let Some(retag_fields) = arg.strip_prefix("-Zmiri-retag-fields=") {
|
||||
miri_config.retag_fields = match retag_fields {
|
||||
"all" => RetagFields::Yes,
|
||||
|
|
|
|||
|
|
@ -6,6 +6,8 @@ use std::task::Poll;
|
|||
use std::time::{Duration, SystemTime};
|
||||
|
||||
use either::Either;
|
||||
use rand::rngs::StdRng;
|
||||
use rand::seq::IteratorRandom;
|
||||
use rustc_abi::ExternAbi;
|
||||
use rustc_const_eval::CTRL_C_RECEIVED;
|
||||
use rustc_data_structures::fx::FxHashMap;
|
||||
|
|
@ -401,6 +403,8 @@ pub struct ThreadManager<'tcx> {
|
|||
thread_local_allocs: FxHashMap<(DefId, ThreadId), StrictPointer>,
|
||||
/// A flag that indicates that we should change the active thread.
|
||||
yield_active_thread: bool,
|
||||
/// A flag that indicates that we should do round robin scheduling of threads else randomized scheduling is used.
|
||||
fixed_scheduling: bool,
|
||||
}
|
||||
|
||||
impl VisitProvenance for ThreadManager<'_> {
|
||||
|
|
@ -410,6 +414,7 @@ impl VisitProvenance for ThreadManager<'_> {
|
|||
thread_local_allocs,
|
||||
active_thread: _,
|
||||
yield_active_thread: _,
|
||||
fixed_scheduling: _,
|
||||
} = self;
|
||||
|
||||
for thread in threads {
|
||||
|
|
@ -421,8 +426,8 @@ impl VisitProvenance for ThreadManager<'_> {
|
|||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Default for ThreadManager<'tcx> {
|
||||
fn default() -> Self {
|
||||
impl<'tcx> ThreadManager<'tcx> {
|
||||
pub(crate) fn new(config: &MiriConfig) -> Self {
|
||||
let mut threads = IndexVec::new();
|
||||
// Create the main thread and add it to the list of threads.
|
||||
threads.push(Thread::new(Some("main"), None));
|
||||
|
|
@ -431,11 +436,10 @@ impl<'tcx> Default for ThreadManager<'tcx> {
|
|||
threads,
|
||||
thread_local_allocs: Default::default(),
|
||||
yield_active_thread: false,
|
||||
fixed_scheduling: config.fixed_scheduling,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> ThreadManager<'tcx> {
|
||||
pub(crate) fn init(
|
||||
ecx: &mut MiriInterpCx<'tcx>,
|
||||
on_main_stack_empty: StackEmptyCallback<'tcx>,
|
||||
|
|
@ -702,7 +706,11 @@ impl<'tcx> ThreadManager<'tcx> {
|
|||
/// used in stateless model checkers such as Loom: run the active thread as
|
||||
/// long as we can and switch only when we have to (the active thread was
|
||||
/// blocked, terminated, or has explicitly asked to be preempted).
|
||||
fn schedule(&mut self, clock: &MonotonicClock) -> InterpResult<'tcx, SchedulingAction> {
|
||||
fn schedule(
|
||||
&mut self,
|
||||
clock: &MonotonicClock,
|
||||
rng: &mut StdRng,
|
||||
) -> InterpResult<'tcx, SchedulingAction> {
|
||||
// This thread and the program can keep going.
|
||||
if self.threads[self.active_thread].state.is_enabled() && !self.yield_active_thread {
|
||||
// The currently active thread is still enabled, just continue with it.
|
||||
|
|
@ -720,30 +728,33 @@ impl<'tcx> ThreadManager<'tcx> {
|
|||
}
|
||||
// No callbacks immediately scheduled, pick a regular thread to execute.
|
||||
// The active thread blocked or yielded. So we go search for another enabled thread.
|
||||
// Crucially, we start searching at the current active thread ID, rather than at 0, since we
|
||||
// want to avoid always scheduling threads 0 and 1 without ever making progress in thread 2.
|
||||
//
|
||||
// `skip(N)` means we start iterating at thread N, so we skip 1 more to start just *after*
|
||||
// the active thread. Then after that we look at `take(N)`, i.e., the threads *before* the
|
||||
// active thread.
|
||||
let threads = self
|
||||
// We build the list of threads by starting with the threads after the current one, followed by
|
||||
// the threads before the current one and then the current thread itself (i.e., this iterator acts
|
||||
// like `threads.rotate_left(self.active_thread.index() + 1)`. This ensures that if we pick the first
|
||||
// eligible thread, we do regular round-robin scheduling, and all threads get a chance to take a step.
|
||||
let mut threads_iter = self
|
||||
.threads
|
||||
.iter_enumerated()
|
||||
.skip(self.active_thread.index() + 1)
|
||||
.chain(self.threads.iter_enumerated().take(self.active_thread.index()));
|
||||
for (id, thread) in threads {
|
||||
debug_assert_ne!(self.active_thread, id);
|
||||
if thread.state.is_enabled() {
|
||||
.chain(self.threads.iter_enumerated().take(self.active_thread.index() + 1))
|
||||
.filter(|(_id, thread)| thread.state.is_enabled());
|
||||
// Pick a new thread, and switch to it.
|
||||
let new_thread =
|
||||
if self.fixed_scheduling { threads_iter.next() } else { threads_iter.choose(rng) };
|
||||
|
||||
if let Some((id, _thread)) = new_thread {
|
||||
if self.active_thread != id {
|
||||
info!(
|
||||
"---------- Now executing on thread `{}` (previous: `{}`) ----------------------------------------",
|
||||
self.get_thread_display_name(id),
|
||||
self.get_thread_display_name(self.active_thread)
|
||||
);
|
||||
self.active_thread = id;
|
||||
break;
|
||||
}
|
||||
}
|
||||
// This completes the `yield`, if any was requested.
|
||||
self.yield_active_thread = false;
|
||||
|
||||
if self.threads[self.active_thread].state.is_enabled() {
|
||||
return interp_ok(SchedulingAction::ExecuteStep);
|
||||
}
|
||||
|
|
@ -1138,7 +1149,9 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
|
|||
use rand::Rng as _;
|
||||
|
||||
let this = self.eval_context_mut();
|
||||
if this.machine.rng.get_mut().random_bool(this.machine.preemption_rate) {
|
||||
if !this.machine.threads.fixed_scheduling
|
||||
&& this.machine.rng.get_mut().random_bool(this.machine.preemption_rate)
|
||||
{
|
||||
this.yield_active_thread();
|
||||
}
|
||||
}
|
||||
|
|
@ -1152,7 +1165,8 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
|
|||
this.machine.handle_abnormal_termination();
|
||||
throw_machine_stop!(TerminationInfo::Interrupted);
|
||||
}
|
||||
match this.machine.threads.schedule(&this.machine.monotonic_clock)? {
|
||||
let rng = this.machine.rng.get_mut();
|
||||
match this.machine.threads.schedule(&this.machine.monotonic_clock, rng)? {
|
||||
SchedulingAction::ExecuteStep => {
|
||||
if !this.step()? {
|
||||
// See if this thread can do something else.
|
||||
|
|
|
|||
|
|
@ -163,6 +163,8 @@ pub struct MiriConfig {
|
|||
pub address_reuse_rate: f64,
|
||||
/// Probability for address reuse across threads.
|
||||
pub address_reuse_cross_thread_rate: f64,
|
||||
/// Round Robin scheduling with no preemption.
|
||||
pub fixed_scheduling: bool,
|
||||
}
|
||||
|
||||
impl Default for MiriConfig {
|
||||
|
|
@ -200,6 +202,7 @@ impl Default for MiriConfig {
|
|||
collect_leak_backtraces: true,
|
||||
address_reuse_rate: 0.5,
|
||||
address_reuse_cross_thread_rate: 0.1,
|
||||
fixed_scheduling: false,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -669,7 +669,7 @@ impl<'tcx> MiriMachine<'tcx> {
|
|||
cpu_affinity::MAX_CPUS,
|
||||
config.num_cpus
|
||||
);
|
||||
let threads = ThreadManager::default();
|
||||
let threads = ThreadManager::new(config);
|
||||
let mut thread_cpu_affinity = FxHashMap::default();
|
||||
if matches!(&*tcx.sess.target.os, "linux" | "freebsd" | "android") {
|
||||
thread_cpu_affinity
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@ignore-target: windows # No pthreads on Windows
|
||||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
|
||||
// Joining itself is undefined behavior.
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@only-target: windows # Uses win32 api functions
|
||||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@error-in-other-file: deadlock
|
||||
|
||||
// On windows, joining main is not UB, but it will block a thread forever.
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@only-target: windows # Uses win32 api functions
|
||||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@error-in-other-file: deadlock
|
||||
|
||||
// On windows, a thread joining itself is not UB, but it will deadlock.
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-isolation -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-disable-isolation -Zmiri-fixed-schedule
|
||||
//@ignore-target: windows # No libc env support on Windows
|
||||
|
||||
use std::{env, thread};
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
//@only-target: linux android illumos
|
||||
//~^ERROR: deadlocked
|
||||
//~^^ERROR: deadlocked
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@error-in-other-file: deadlock
|
||||
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
//@only-target: linux android illumos
|
||||
//~^ERROR: deadlocked
|
||||
//~^^ERROR: deadlocked
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@error-in-other-file: deadlock
|
||||
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
//! to be considered synchronized.
|
||||
//@only-target: linux android illumos
|
||||
// ensure deterministic schedule
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
|
||||
use std::convert::TryInto;
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//~^ERROR: deadlocked
|
||||
//~^^ERROR: deadlocked
|
||||
//@only-target: linux android illumos
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
//! faulty logic around `release_clock` that led to this code not reporting a data race.
|
||||
//~^^ERROR: deadlock
|
||||
//@ignore-target: windows # no libc socketpair on Windows
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-address-reuse-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-address-reuse-rate=0
|
||||
//@error-in-other-file: deadlock
|
||||
use std::thread;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
//! This is a regression test for <https://github.com/rust-lang/miri/issues/3947>: we had some
|
||||
//! faulty logic around `release_clock` that led to this code not reporting a data race.
|
||||
//@ignore-target: windows # no libc socketpair on Windows
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-address-reuse-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-address-reuse-rate=0
|
||||
use std::thread;
|
||||
|
||||
fn main() {
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
//~^ERROR: deadlocked
|
||||
//~^^ERROR: deadlocked
|
||||
// test_race depends on a deterministic schedule.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@error-in-other-file: deadlock
|
||||
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
//~^ERROR: deadlocked
|
||||
//~^^ERROR: deadlocked
|
||||
// test_race depends on a deterministic schedule.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@error-in-other-file: deadlock
|
||||
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//! Make sure that a retag acts like a write for the data race model.
|
||||
//@revisions: stack tree
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
//@[tree]compile-flags: -Zmiri-tree-borrows
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation
|
||||
//@compile-flags:-Zmiri-fixed-schedule -Zmiri-disable-weak-memory-emulation
|
||||
#![feature(core_intrinsics)]
|
||||
#![feature(custom_mir)]
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation
|
||||
//@compile-flags:-Zmiri-fixed-schedule -Zmiri-disable-weak-memory-emulation
|
||||
use std::sync::atomic::Ordering::*;
|
||||
use std::sync::atomic::*;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation
|
||||
//@compile-flags:-Zmiri-fixed-schedule -Zmiri-disable-weak-memory-emulation
|
||||
use std::sync::atomic::Ordering::*;
|
||||
use std::sync::atomic::*;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation
|
||||
//@compile-flags:-Zmiri-fixed-schedule -Zmiri-disable-weak-memory-emulation
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
// Two variants: the atomic store matches the size of the first or second atomic load.
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation
|
||||
//@compile-flags:-Zmiri-fixed-schedule -Zmiri-disable-weak-memory-emulation
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
// Two revisions, depending on which access goes first.
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation
|
||||
//@compile-flags:-Zmiri-fixed-schedule -Zmiri-disable-weak-memory-emulation
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
//@revisions: fst snd
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We want to control preemption here.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
|
||||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// Avoid accidental synchronization via address reuse.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-address-reuse-cross-thread-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-address-reuse-cross-thread-rate=0
|
||||
use std::thread;
|
||||
|
||||
#[derive(Copy, Clone)]
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//! Make sure that a retag acts like a read for the data race model.
|
||||
// Avoid accidental synchronization via address reuse.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-address-reuse-cross-thread-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-address-reuse-cross-thread-rate=0
|
||||
#[derive(Copy, Clone)]
|
||||
struct SendPtr(*mut u8);
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Illustrating a problematic interaction between Reserved, interior mutability,
|
||||
// and protectors, that makes spurious writes fail in the previous model of Tree Borrows.
|
||||
// As for all similar tests, we disable preemption so that the error message is deterministic.
|
||||
//@compile-flags: -Zmiri-tree-borrows -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-tree-borrows -Zmiri-fixed-schedule
|
||||
//
|
||||
// One revision without spurious read (default source code) and one with spurious read.
|
||||
// Both are expected to be UB. Both revisions are expected to have the *same* error
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
// Note that we are *also* using barriers: the barriers enforce the
|
||||
// specific interleaving of operations that we want, but only the preemption
|
||||
// rate guarantees that the error message is also deterministic.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@compile-flags: -Zmiri-tree-borrows
|
||||
|
||||
use std::sync::{Arc, Barrier};
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-ignore-leaks -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-ignore-leaks -Zmiri-fixed-schedule
|
||||
|
||||
// Tests showing weak memory behaviours are exhibited. All tests
|
||||
// return true when the desired behaviour is seen.
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
//@only-target: darwin
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
|
||||
use std::time::{Duration, Instant};
|
||||
use std::{io, ptr, thread};
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-isolation -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-disable-isolation -Zmiri-fixed-schedule
|
||||
//@ignore-target: windows # No libc env support on Windows
|
||||
|
||||
use std::ffi::CStr;
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
//@only-target: freebsd
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-isolation
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-isolation
|
||||
|
||||
use std::mem::{self, MaybeUninit};
|
||||
use std::ptr::{self, addr_of};
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@only-target: windows # Uses win32 api functions
|
||||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
|
||||
use std::os::windows::io::IntoRawHandle;
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@only-target: windows # Uses win32 api functions
|
||||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
|
||||
use std::ptr::null_mut;
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@only-target: windows # Uses win32 api functions
|
||||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
|
||||
use std::os::windows::io::IntoRawHandle;
|
||||
use std::sync::atomic::{AtomicBool, Ordering};
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@only-target: linux android illumos
|
||||
// test_epoll_block_then_unblock and test_epoll_race depend on a deterministic schedule.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
|
||||
use std::convert::TryInto;
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@only-target: linux android illumos
|
||||
// test_race, test_blocking_read and test_blocking_write depend on a deterministic schedule.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
|
||||
// FIXME(static_mut_refs): Do not allow `static_mut_refs` lint
|
||||
#![allow(static_mut_refs)]
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@ignore-target: windows # No libc pipe on Windows
|
||||
// test_race depends on a deterministic schedule.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
use std::thread;
|
||||
fn main() {
|
||||
test_pipe();
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@ignore-target: windows # No libc socketpair on Windows
|
||||
// test_race depends on a deterministic schedule.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
|
||||
// FIXME(static_mut_refs): Do not allow `static_mut_refs` lint
|
||||
#![allow(static_mut_refs)]
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@ignore-target: windows # No pthreads on Windows
|
||||
// We use `yield` to test specific interleavings, so disable automatic preemption.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
#![feature(sync_unsafe_cell)]
|
||||
|
||||
use std::cell::SyncUnsafeCell;
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-fixed-schedule
|
||||
|
||||
use std::sync::atomic::*;
|
||||
use std::thread::{self, spawn};
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@compile-flags: -Zmiri-disable-data-race-detector
|
||||
// Avoid non-determinism
|
||||
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-address-reuse-cross-thread-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-address-reuse-cross-thread-rate=0
|
||||
|
||||
use std::thread::spawn;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// This specifically tests behavior *without* preemption.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
|
||||
use std::cell::Cell;
|
||||
use std::sync::atomic::{AtomicBool, AtomicUsize, Ordering};
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
//@revisions: stack tree
|
||||
//@[tree]compile-flags: -Zmiri-tree-borrows
|
||||
// We use `yield` to test specific interleavings, so disable automatic preemption.
|
||||
//@compile-flags: -Zmiri-disable-isolation -Zmiri-strict-provenance -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-disable-isolation -Zmiri-strict-provenance -Zmiri-fixed-schedule
|
||||
|
||||
use std::sync::{Arc, Barrier, Condvar, Mutex, Once, RwLock};
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-strict-provenance -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-strict-provenance -Zmiri-fixed-schedule
|
||||
|
||||
use std::sync::{Arc, Condvar, Mutex, RwLock};
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
|
||||
//! Cause a panic in one thread while another thread is unwinding. This checks
|
||||
//! that separate threads have their own panicking state.
|
||||
|
|
|
|||
2
src/tools/miri/tests/pass/shims/env/var.rs
vendored
2
src/tools/miri/tests/pass/shims/env/var.rs
vendored
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
use std::{env, thread};
|
||||
|
||||
fn main() {
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
// This test relies on a specific interleaving that cannot be enforced
|
||||
// with just barriers. We must remove preemption so that the execution and the
|
||||
// error messages are deterministic.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
use std::ptr::addr_of_mut;
|
||||
use std::sync::{Arc, Barrier};
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
// Note that we are *also* using barriers: the barriers enforce the
|
||||
// specific interleaving of operations that we want, but only the preemption
|
||||
// rate guarantees that the error message is also deterministic.
|
||||
//@compile-flags: -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@compile-flags: -Zmiri-tree-borrows
|
||||
|
||||
use std::sync::{Arc, Barrier};
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-ignore-leaks -Zmiri-preemption-rate=0
|
||||
//@compile-flags: -Zmiri-ignore-leaks -Zmiri-fixed-schedule
|
||||
|
||||
// Tests showing weak memory behaviours are exhibited. All tests
|
||||
// return true when the desired behaviour is seen.
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue