add -Zmiri-deterministic-concurrency flag and use it for concurrency tests
This commit is contained in:
parent
f521fa0c54
commit
bbcc6a24cd
75 changed files with 129 additions and 156 deletions
|
|
@ -277,22 +277,15 @@ Try running `cargo miri clean`.
|
|||
Miri adds its own set of `-Z` flags, which are usually set via the `MIRIFLAGS`
|
||||
environment variable. We first document the most relevant and most commonly used flags:
|
||||
|
||||
* `-Zmiri-address-reuse-rate=<rate>` changes the probability that a freed *non-stack* allocation
|
||||
will be added to the pool for address reuse, and the probability that a new *non-stack* allocation
|
||||
will be taken from the pool. Stack allocations never get added to or taken from the pool. The
|
||||
default is `0.5`.
|
||||
* `-Zmiri-address-reuse-cross-thread-rate=<rate>` changes the probability that an allocation which
|
||||
attempts to reuse a previously freed block of memory will also consider blocks freed by *other
|
||||
threads*. The default is `0.1`, which means by default, in 90% of the cases where an address reuse
|
||||
attempt is made, only addresses from the same thread will be considered. Reusing an address from
|
||||
another thread induces synchronization between those threads, which can mask data races and weak
|
||||
memory bugs.
|
||||
* `-Zmiri-compare-exchange-weak-failure-rate=<rate>` changes the failure rate of
|
||||
`compare_exchange_weak` operations. The default is `0.8` (so 4 out of 5 weak ops will fail).
|
||||
You can change it to any value between `0.0` and `1.0`, where `1.0` means it
|
||||
will always fail and `0.0` means it will never fail. Note that setting it to
|
||||
`1.0` will likely cause hangs, since it means programs using
|
||||
`compare_exchange_weak` cannot make progress.
|
||||
* `-Zmiri-deterministic-concurrency` makes Miri's concurrency-related behavior fully deterministic.
|
||||
Strictly speaking, Miri is always fully deterministic when isolation is enabled (the default
|
||||
mode), but this determinism is achieved by using an RNG with a fixed seed. Seemingly harmless
|
||||
changes to the program, or just running it for a different target architecture, can thus lead to
|
||||
completely different program behavior down the line. This flag disables the use of an RNG for
|
||||
concurrency-related decisions. Therefore, Miri cannot find bugs that only occur under some
|
||||
specific circumstances, but Miri's behavior will also be more stable across versions and targets.
|
||||
This is equivalent to `-Zmiri-fixed-schedule -Zmiri-compare-exchange-weak-failure-rate=0.0
|
||||
-Zmiri-address-reuse-cross-thread-rate=0.0 -Zmiri-disable-weak-memory-emulation`.
|
||||
* `-Zmiri-disable-isolation` disables host isolation. As a consequence,
|
||||
the program has access to host resources such as environment variables, file
|
||||
systems, and randomness.
|
||||
|
|
@ -334,9 +327,6 @@ environment variable. We first document the most relevant and most commonly used
|
|||
This will necessarily miss some bugs as those operations are not efficiently and accurately
|
||||
implementable in a sanitizer, but it will only miss bugs that concern memory/pointers which is
|
||||
subject to these operations.
|
||||
* `-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-report-progress` makes Miri print the current stacktrace every now and then, so you can
|
||||
tell what it is doing when a program just keeps running. You can customize how frequently the
|
||||
report is printed via `-Zmiri-report-progress=<blocks>`, which prints the report every N basic
|
||||
|
|
@ -365,6 +355,22 @@ The remaining flags are for advanced use only, and more likely to change or be r
|
|||
Some of these are **unsound**, which means they can lead
|
||||
to Miri failing to detect cases of undefined behavior in a program.
|
||||
|
||||
* `-Zmiri-address-reuse-rate=<rate>` changes the probability that a freed *non-stack* allocation
|
||||
will be added to the pool for address reuse, and the probability that a new *non-stack* allocation
|
||||
will be taken from the pool. Stack allocations never get added to or taken from the pool. The
|
||||
default is `0.5`.
|
||||
* `-Zmiri-address-reuse-cross-thread-rate=<rate>` changes the probability that an allocation which
|
||||
attempts to reuse a previously freed block of memory will also consider blocks freed by *other
|
||||
threads*. The default is `0.1`, which means by default, in 90% of the cases where an address reuse
|
||||
attempt is made, only addresses from the same thread will be considered. Reusing an address from
|
||||
another thread induces synchronization between those threads, which can mask data races and weak
|
||||
memory bugs.
|
||||
* `-Zmiri-compare-exchange-weak-failure-rate=<rate>` changes the failure rate of
|
||||
`compare_exchange_weak` operations. The default is `0.8` (so 4 out of 5 weak ops will fail).
|
||||
You can change it to any value between `0.0` and `1.0`, where `1.0` means it
|
||||
will always fail and `0.0` means it will never fail. Note that setting it to
|
||||
`1.0` will likely cause hangs, since it means programs using
|
||||
`compare_exchange_weak` cannot make progress.
|
||||
* `-Zmiri-disable-alignment-check` disables checking pointer alignment, so you
|
||||
can focus on other failures, but it means Miri can miss bugs in your program.
|
||||
Using this flag is **unsound**.
|
||||
|
|
@ -383,6 +389,10 @@ to Miri failing to detect cases of undefined behavior in a program.
|
|||
this flag is **unsound**.
|
||||
* `-Zmiri-disable-weak-memory-emulation` disables the emulation of some C++11 weak
|
||||
memory effects.
|
||||
* `-Zmiri-fixed-schedule` disables preemption (like `-Zmiri-preemption-rate=0.0`) and furthermore
|
||||
disables the randomization of the next thread to be picked, instead fixing a round-robin schedule.
|
||||
Note however that other aspects of Miri's concurrency behavior are still randomize; use
|
||||
`-Zmiri-deterministic-concurrency` to disable them all.
|
||||
* `-Zmiri-native-lib=<path to a shared object file>` is an experimental flag for providing support
|
||||
for calling native functions from inside the interpreter via FFI. The flag is supported only on
|
||||
Unix systems. Functions not provided by that file are still executed via the usual Miri shims.
|
||||
|
|
@ -412,6 +422,10 @@ to Miri failing to detect cases of undefined behavior in a program.
|
|||
without an explicit value), `none` means it never recurses, `scalar` means it only recurses for
|
||||
types where we would also emit `noalias` annotations in the generated LLVM IR (types passed as
|
||||
individual scalars or pairs of scalars). Setting this to `none` is **unsound**.
|
||||
* `-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. Note that even without preemption, the schedule is still non-deterministic:
|
||||
if a thread blocks or yields, the next thread is chosen randomly.
|
||||
* `-Zmiri-provenance-gc=<blocks>` configures how often the pointer provenance garbage collector runs.
|
||||
The default is to search for and remove unreachable provenance once every `10000` basic blocks. Setting
|
||||
this to `0` disables the garbage collector, which causes some programs to have explosive memory
|
||||
|
|
|
|||
|
|
@ -575,6 +575,11 @@ fn main() {
|
|||
miri_config.retag_fields = RetagFields::Yes;
|
||||
} else if arg == "-Zmiri-fixed-schedule" {
|
||||
miri_config.fixed_scheduling = true;
|
||||
} else if arg == "-Zmiri-deterministic-concurrency" {
|
||||
miri_config.fixed_scheduling = true;
|
||||
miri_config.address_reuse_cross_thread_rate = 0.0;
|
||||
miri_config.cmpxchg_weak_failure_rate = 0.0;
|
||||
miri_config.weak_memory_emulation = false;
|
||||
} else if let Some(retag_fields) = arg.strip_prefix("-Zmiri-retag-fields=") {
|
||||
miri_config.retag_fields = match retag_fields {
|
||||
"all" => RetagFields::Yes,
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@ignore-target: windows # No pthreads on Windows
|
||||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
// Joining itself is undefined behavior.
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,7 @@
|
|||
//@ignore-target: windows # No pthreads on Windows
|
||||
//@error-in-other-file: deadlock
|
||||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
use std::cell::UnsafeCell;
|
||||
use std::sync::Arc;
|
||||
|
|
|
|||
|
|
@ -1,5 +1,7 @@
|
|||
//@ignore-target: windows # No pthreads on Windows
|
||||
//@error-in-other-file: deadlock
|
||||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
use std::cell::UnsafeCell;
|
||||
use std::sync::Arc;
|
||||
|
|
|
|||
|
|
@ -1,5 +1,7 @@
|
|||
//@ignore-target: windows # No pthreads on Windows
|
||||
//@error-in-other-file: deadlock
|
||||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
use std::cell::UnsafeCell;
|
||||
use std::sync::Arc;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
//@only-target: windows # Uses win32 api functions
|
||||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
//@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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
//@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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-disable-isolation -Zmiri-deterministic-concurrency
|
||||
//@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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
//@error-in-other-file: deadlock
|
||||
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
//@only-target: linux android illumos
|
||||
//~^ERROR: deadlocked
|
||||
//~^^ERROR: deadlocked
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
//@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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
use std::convert::TryInto;
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
//~^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-fixed-schedule -Zmiri-address-reuse-rate=0
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
//@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-fixed-schedule -Zmiri-address-reuse-rate=0
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
use std::thread;
|
||||
|
||||
fn main() {
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
//~^ERROR: deadlocked
|
||||
//~^^ERROR: deadlocked
|
||||
// test_race depends on a deterministic schedule.
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
//@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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
//@error-in-other-file: deadlock
|
||||
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -1,8 +1,6 @@
|
|||
//! Make sure that a retag acts like a write for the data race model.
|
||||
//@revisions: stack tree
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
//@[tree]compile-flags: -Zmiri-tree-borrows
|
||||
#[derive(Copy, Clone)]
|
||||
struct SendPtr(*mut u8);
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
//@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
|
||||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::mem::MaybeUninit;
|
||||
use std::ptr::null_mut;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
//@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
|
||||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::ptr::null_mut;
|
||||
use std::sync::atomic::{AtomicPtr, Ordering};
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
use std::thread::spawn;
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
use std::thread::spawn;
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
use std::thread::spawn;
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
use std::thread::spawn;
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
use std::thread::spawn;
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
use std::thread::spawn;
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::mem;
|
||||
use std::thread::{sleep, spawn};
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-stacked-borrows
|
||||
// Avoid accidental synchronization via address reuse.
|
||||
//@compile-flags: -Zmiri-address-reuse-cross-thread-rate=0
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::mem;
|
||||
use std::thread::{sleep, spawn};
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
#![feature(rustc_attrs)]
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
#![feature(rustc_attrs)]
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
//@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
|
||||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::ptr::null_mut;
|
||||
use std::sync::atomic::{AtomicPtr, Ordering};
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
#![feature(rustc_attrs)]
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
#![feature(rustc_attrs)]
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
//@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
|
||||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::ptr::null_mut;
|
||||
use std::sync::atomic::{AtomicPtr, Ordering};
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::thread::spawn;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::sync::Arc;
|
||||
use std::sync::atomic::{AtomicUsize, Ordering, fence};
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags:-Zmiri-fixed-schedule -Zmiri-disable-weak-memory-emulation
|
||||
//@compile-flags:-Zmiri-deterministic-concurrency
|
||||
#![feature(core_intrinsics)]
|
||||
#![feature(custom_mir)]
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags:-Zmiri-fixed-schedule -Zmiri-disable-weak-memory-emulation
|
||||
//@compile-flags:-Zmiri-deterministic-concurrency
|
||||
use std::sync::atomic::Ordering::*;
|
||||
use std::sync::atomic::*;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags:-Zmiri-fixed-schedule -Zmiri-disable-weak-memory-emulation
|
||||
//@compile-flags:-Zmiri-deterministic-concurrency
|
||||
use std::sync::atomic::Ordering::*;
|
||||
use std::sync::atomic::*;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,4 @@
|
|||
//@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
|
||||
//@compile-flags:-Zmiri-deterministic-concurrency
|
||||
// Two variants: the atomic store matches the size of the first or second atomic load.
|
||||
//@revisions: match_first_load match_second_load
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,4 @@
|
|||
//@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
|
||||
//@compile-flags:-Zmiri-deterministic-concurrency
|
||||
// Two revisions, depending on which access goes first.
|
||||
//@revisions: read_write write_read
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,4 @@
|
|||
//@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
|
||||
//@compile-flags:-Zmiri-deterministic-concurrency
|
||||
//@revisions: fst snd
|
||||
|
||||
use std::sync::atomic::{AtomicU8, AtomicU16, Ordering};
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@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
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::thread::spawn;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
//@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
|
||||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::ptr::null_mut;
|
||||
use std::sync::atomic::{AtomicPtr, Ordering};
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
//@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
|
||||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
use std::thread::spawn;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
//@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
|
||||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
use std::thread::{sleep, spawn};
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
//@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
|
||||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
use std::thread::spawn;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
//@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
|
||||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
use std::thread::spawn;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
//@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
|
||||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::thread;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
// We want to control preemption here.
|
||||
//@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
|
||||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::thread::spawn;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
//@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
|
||||
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -Zmiri-disable-stacked-borrows
|
||||
|
||||
use std::ptr::null_mut;
|
||||
use std::sync::atomic::{AtomicPtr, Ordering};
|
||||
|
|
|
|||
|
|
@ -1,5 +1,4 @@
|
|||
// Avoid accidental synchronization via address reuse.
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-address-reuse-cross-thread-rate=0
|
||||
//@compile-flags:-Zmiri-deterministic-concurrency
|
||||
use std::thread;
|
||||
|
||||
#[derive(Copy, Clone)]
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
//! Make sure that a retag acts like a read for the data race model.
|
||||
// Avoid accidental synchronization via address reuse.
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-address-reuse-cross-thread-rate=0
|
||||
//@compile-flags:-Zmiri-deterministic-concurrency
|
||||
#[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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-tree-borrows -Zmiri-deterministic-concurrency
|
||||
//
|
||||
// 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
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
// We ensure a deterministic execution.
|
||||
// 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-fixed-schedule
|
||||
// specific interleaving of operations that we want, but we need to disable
|
||||
// preemption to ensure that the error message is also deterministic.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
//@compile-flags: -Zmiri-tree-borrows
|
||||
|
||||
use std::sync::{Arc, Barrier};
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
//@only-target: darwin
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
use std::time::{Duration, Instant};
|
||||
use std::{io, ptr, thread};
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
//@compile-flags: -Zmiri-disable-isolation -Zmiri-fixed-schedule
|
||||
//@compile-flags: -Zmiri-disable-isolation -Zmiri-deterministic-concurrency
|
||||
//@ignore-target: windows # No libc env support on Windows
|
||||
|
||||
use std::ffi::CStr;
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
//@only-target: freebsd
|
||||
//@compile-flags: -Zmiri-fixed-schedule -Zmiri-disable-isolation
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency -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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
// 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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
// 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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
#![feature(sync_unsafe_cell)]
|
||||
|
||||
use std::cell::SyncUnsafeCell;
|
||||
|
|
|
|||
|
|
@ -1,4 +1,5 @@
|
|||
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-fixed-schedule
|
||||
// This tests carefully crafted schedules to ensure they are not considered races.
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
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-fixed-schedule -Zmiri-address-reuse-cross-thread-rate=0
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
use std::thread::spawn;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// This specifically tests behavior *without* preemption.
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-disable-isolation -Zmiri-deterministic-concurrency
|
||||
|
||||
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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
use std::sync::{Arc, Condvar, Mutex, RwLock};
|
||||
use std::thread;
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// We are making scheduler assumptions here.
|
||||
//@compile-flags: -Zmiri-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
|
||||
//! 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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
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-fixed-schedule
|
||||
//@compile-flags: -Zmiri-deterministic-concurrency
|
||||
//@compile-flags: -Zmiri-tree-borrows
|
||||
|
||||
use std::sync::{Arc, Barrier};
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue