user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

genmc: suppress compare_exchange warnings from dependencies

Browse source
This commit is contained in:
Ralf Jung 2025-12-07 12:10:38 +01:00
parent 673b3b186d
commit 8a99d48f84
15 changed files with 62 additions and 655 deletions
Download patch file Download diff file Expand all files Collapse all files

47
src/tools/miri/doc/genmc.md
View file

@ -1,7 +1,6 @@
# **(WIP)** Documentation for Miri-GenMC
**NOTE: GenMC mode is not yet fully implemented, and has [several correctness issues](https://github.com/rust-lang/miri/issues/4572). Using GenMC mode currently requires manually compiling Miri, see [Usage](#usage).**
**NOTE: GenMC mode is not yet fully implemented, and has [several correctness issues](https://github.com/rust-lang/miri/issues/4572) and [other limitations](#limitations). Using GenMC mode currently requires manually compiling Miri, see [Usage](#usage).**
[GenMC](https://github.com/MPI-SWS/genmc) is a stateless model checker for exploring concurrent executions of a program.
Miri-GenMC integrates that model checker into Miri.
@ -12,11 +11,14 @@ This includes all possible thread interleavings and all allowed return values fo
It is hence still possible to have latent bugs in a test case even if they passed GenMC.)
GenMC requires the input program to be bounded, i.e., have finitely many possible executions, otherwise it will not terminate.
Any loops that may run infinitely must be replaced or bounded (see below).
Any loops that may run infinitely must be replaced or bounded (see [below](#eliminating-unbounded-loops)).
GenMC makes use of Dynamic Partial Order Reduction (DPOR) to reduce the number of executions that must be explored, but the runtime can still be super-exponential in the size of the input program (number of threads and amount of interaction between threads).
Large programs may not be verifiable in a reasonable amount of time.
GenMC currently only supports Linux hosts.
Both the host and the target must be 64-bit little-endian.
## Usage
For testing/developing Miri-GenMC:
@ -50,16 +52,24 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
- `debug2`: Print the execution graph after every memory access.
- `debug3`: Print reads-from values considered by GenMC.
- `-Zmiri-genmc-verbose`: Show more information, such as estimated number of executions, and time taken for verification.
#### Regular Miri parameters useful for GenMC mode
- `-Zmiri-disable-weak-memory-emulation`: Disable any weak memory effects (effectively upgrading all atomic orderings in the program to `SeqCst`). This option may reduce the number of explored program executions, but any bugs related to weak memory effects will be missed. This option can help determine if an error is caused by weak memory effects (i.e., if it disappears with this option enabled).
<!-- FIXME(genmc): explain Miri-GenMC specific functions. -->
## Tips
## Limitations
<!-- FIXME(genmc): add tips for using Miri-GenMC more efficiently. -->
There are several limitations which can make GenMC miss bugs:
- GenMC does not support re-using freed memory for new allocations, so any bugs related to that will be missed.
- GenMC does not support `compare_exchange_weak`, so the consequences of spurious failures are not explored.
A warning will be emitted if this affects code you wrote (but not if it happens inside your dependencies).
- GenMC does not support the separate failure ordering of `compare_exchange`. Miri will take the maximum of the success and failure ordering and use that for the access; outcomes that rely on the real ordering being weaker will not be explored.
A warning will be emitted if this affects code you wrote (but not if it happens inside your dependencies).
- GenMC is incompatible with borrow tracking (Stacked/Tree Borrows). You need to set `-Zmiri-disable-stacked-borrows` to use GenMC.
- Like all C++ memory model verification tools, GenMC has to solve the [out-of-thin-air problem](https://www.cl.cam.ac.uk/~pes20/cpp/notes42.html).
It takes the [usual approach](https://plv.mpi-sws.org/scfix/paper.pdf) of requiring the union of "program-order" and "reads-from" to be acyclic.
This means it excludes certain behaviors allowed by the C++ memory model, some of which can occur on hardware that performs load buffering.
## Tips
### Eliminating unbounded loops
@ -121,24 +131,11 @@ fn count_until_true_genmc(flag: &AtomicBool) -> u64 {
<!-- FIXME: update the code above once Miri supports a loop bounding features like GenMC's `--unroll=N`. -->
<!-- FIXME: update this section once Miri-GenMC supports automatic program transformations (like spinloop-assume replacement). -->
## Limitations
Some or all of these limitations might get removed in the future:
- Borrow tracking is currently incompatible (stacked/tree borrows).
- Only Linux is supported for now.
- No support for 32-bit or big-endian targets.
- No cross-target interpretation.
<!-- FIXME(genmc): document remaining limitations -->
## Development
GenMC is written in C++, which complicates development a bit.
The prerequisites for building Miri-GenMC are:
- A compiler with C++23 support.
- LLVM developments headers and clang.
<!-- FIXME(genmc,llvm): remove once LLVM dependency is no longer required. -->
- A compiler with sufficient C++20 support (we are testing GCC 13).
The actual code for GenMC is not contained in the Miri repo itself, but in a [separate GenMC repo](https://github.com/MPI-SWS/genmc) (with its own maintainers).
These sources need to be available to build Miri-GenMC.
@ -149,6 +146,8 @@ The process for obtaining them is as follows:
If you place this directory inside the Miri folder, it is recommended to call it `genmc-src` as that tells `./miri fmt` to avoid
formatting the Rust files inside that folder.
<!-- FIXME(genmc): explain how submitting code to GenMC should be handled. -->
### Formatting the C++ code
For formatting the C++ code we provide a `.clang-format` file in the `genmc-sys` directory.
@ -157,7 +156,3 @@ With `clang-format` installed, run this command to format the c++ files (replace
find ./genmc-sys/cpp/ -name "*.cpp" -o -name "*.hpp" | xargs clang-format --style=file:"./genmc-sys/.clang-format" -i
```
NOTE: this is currently not done automatically on pull requests to Miri.
<!-- FIXME(genmc): explain how submitting code to GenMC should be handled. -->
<!-- FIXME(genmc): explain development. -->

7
src/tools/miri/src/concurrency/genmc/helper.rs
View file

@ -171,11 +171,8 @@ impl AtomicRwOrd {
(AtomicReadOrd::Acquire, AtomicWriteOrd::Relaxed) => AtomicRwOrd::Acquire,
(AtomicReadOrd::Relaxed, AtomicWriteOrd::Release) => AtomicRwOrd::Release,
(AtomicReadOrd::Acquire, AtomicWriteOrd::Release) => AtomicRwOrd::AcqRel,
(AtomicReadOrd::SeqCst, AtomicWriteOrd::SeqCst) => AtomicRwOrd::SeqCst,
_ =>
panic!(
"Unsupported memory ordering combination ({read_ordering:?}, {write_ordering:?})"
),
(AtomicReadOrd::SeqCst, _) => AtomicRwOrd::SeqCst,
(_, AtomicWriteOrd::SeqCst) => AtomicRwOrd::SeqCst,
}
}

18
src/tools/miri/src/concurrency/genmc/mod.rs
View file

@ -402,8 +402,20 @@ impl GenmcCtx {
// FIXME(genmc): remove once GenMC supports failure memory ordering in `compare_exchange`.
let (effective_failure_ordering, _) = upgraded_success_ordering.split_memory_orderings();
// Return a warning if the actual orderings don't match the upgraded ones.
if success != upgraded_success_ordering || effective_failure_ordering != fail {
// Return a warning if we cannot explore all behaviors of this operation.
// Only emit this if the operation is "in user code": walk up across `#[track_caller]`
// frames, then check if the next frame is local.
let show_warning = || {
ecx.active_thread_stack()
.iter()
.rev()
.find(|f| !f.instance().def.requires_caller_location(*ecx.tcx))
.is_none_or(|f| ecx.machine.is_local(f.instance()))
};
if (success != upgraded_success_ordering || effective_failure_ordering != fail)
&& show_warning()
{
static DEDUP: SpanDedupDiagnostic = SpanDedupDiagnostic::new();
ecx.dedup_diagnostic(&DEDUP, |_first| {
NonHaltingDiagnostic::GenmcCompareExchangeOrderingMismatch {
@ -415,7 +427,7 @@ impl GenmcCtx {
});
}
// FIXME(genmc): remove once GenMC implements spurious failures for `compare_exchange_weak`.
if can_fail_spuriously {
if can_fail_spuriously && show_warning() {
static DEDUP: SpanDedupDiagnostic = SpanDedupDiagnostic::new();
ecx.dedup_diagnostic(&DEDUP, |_first| NonHaltingDiagnostic::GenmcCompareExchangeWeak);
}

62
src/tools/miri/tests/genmc/fail/shims/mutex_diff_thread_unlock.stderr
View file

@ -1,64 +1,4 @@
Running GenMC Verification...
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC
note: inside `miri_start`
--> tests/genmc/fail/shims/mutex_diff_thread_unlock.rs:LL:CC
|
LL | let handle = std::thread::spawn(move || {
| __________________^
LL | | let guard = guard; // avoid field capturing
LL | | drop(guard);
LL | | });
| |______^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC
note: inside `miri_start`
--> tests/genmc/fail/shims/mutex_diff_thread_unlock.rs:LL:CC
|
LL | let handle = std::thread::spawn(move || {
| __________________^
LL | | let guard = guard; // avoid field capturing
LL | | drop(guard);
LL | | });
| |______^
error: Undefined Behavior: Invalid unlock() operation
--> RUSTLIB/std/src/sync/poison/mutex.rs:LL:CC
|
@ -82,5 +22,5 @@ note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
error: aborting due to 1 previous error; 2 warnings emitted
error: aborting due to 1 previous error

5
src/tools/miri/tests/genmc/pass/atomics/cas_simple.rs
View file

@ -30,5 +30,10 @@ fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
if 2 != VALUE.load(SeqCst) {
std::process::abort()
}
// Check that we emit warnings for cases that are not fully supported.
let _ = VALUE.compare_exchange(99, 99, SeqCst, Relaxed);
let _ = VALUE.compare_exchange_weak(99, 99, Relaxed, SeqCst);
0
}

18
src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr
View file

@ -1,2 +1,20 @@
Running GenMC Verification...
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'SeqCst', the failure ordering 'Relaxed' is treated like 'SeqCst'. Miri with GenMC might miss bugs related to this memory access.
--> tests/genmc/pass/atomics/cas_simple.rs:LL:CC
|
LL | let _ = VALUE.compare_exchange(99, 99, SeqCst, Relaxed);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Success ordering 'Relaxed' was upgraded to 'SeqCst' to match failure ordering 'SeqCst'. Miri with GenMC might miss bugs related to this memory access.
--> tests/genmc/pass/atomics/cas_simple.rs:LL:CC
|
LL | let _ = VALUE.compare_exchange_weak(99, 99, Relaxed, SeqCst);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> tests/genmc/pass/atomics/cas_simple.rs:LL:CC
|
LL | let _ = VALUE.compare_exchange_weak(99, 99, Relaxed, SeqCst);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
Verification complete with 1 executions. No errors found.

124
src/tools/miri/tests/genmc/pass/std/arc.check_count.stderr
View file

@ -1,126 +1,2 @@
Running GenMC Verification...
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/thread/id.rs:LL:CC
|
LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let weak = Arc::downgrade(&data_clone);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let weak = Arc::downgrade(&data_clone);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let handle = std::thread::spawn(move || {
| __________________^
... |
LL | | });
| |______^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let handle = std::thread::spawn(move || {
| __________________^
... |
LL | | });
| |______^
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | handle.join().unwrap();
| ^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/rt.rs:LL:CC
|
LL | / CLEANUP.call_once(|| unsafe {
LL | | // Flush stdout and disable buffering.
LL | | crate::io::cleanup();
... |
LL | | });
| |______^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sync/once.rs:LL:CC
|
LL | self.inner.call(true, &mut |p| f.take().unwrap()(p));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sync/once.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
|
LL | match EXITING_THREAD_ID.compare_exchange(ptr::null_mut(), this_thread_id, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
Verification complete with 4 executions. No errors found.

1
src/tools/miri/tests/genmc/pass/std/arc.rs
View file

@ -1,6 +1,5 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
//@revisions: check_count try_upgrade
//@normalize-stderr-test: "\n *= note: inside `std::.*" -> ""
// Check that various operations on `std::sync::Arc` are handled properly in GenMC mode.
//

150
src/tools/miri/tests/genmc/pass/std/arc.try_upgrade.stderr
View file

@ -1,152 +1,2 @@
Running GenMC Verification...
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/thread/id.rs:LL:CC
|
LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let weak = Arc::downgrade(&data_clone);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let weak = Arc::downgrade(&data_clone);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let handle = std::thread::spawn(move || {
| __________________^
... |
LL | | });
| |______^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let handle = std::thread::spawn(move || {
| __________________^
... |
LL | | });
| |______^
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | handle.join().unwrap();
| ^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/rt.rs:LL:CC
|
LL | / CLEANUP.call_once(|| unsafe {
LL | | // Flush stdout and disable buffering.
LL | | crate::io::cleanup();
... |
LL | | });
| |______^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sync/once.rs:LL:CC
|
LL | self.inner.call(true, &mut |p| f.take().unwrap()(p));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sync/once.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
|
LL | match EXITING_THREAD_ID.compare_exchange(ptr::null_mut(), this_thread_id, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | if self.inner()?.strong.fetch_update(Acquire, Relaxed, checked_increment).is_ok() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE on thread `unnamed-ID`:
note: inside closure
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | if let Some(strong) = weak_.upgrade() {
| ^^^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | if self.inner()?.strong.fetch_update(Acquire, Relaxed, checked_increment).is_ok() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE on thread `unnamed-ID`:
note: inside closure
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | if let Some(strong) = weak_.upgrade() {
| ^^^^^^^^^^^^^^^
Verification complete with 7 executions. No errors found.

1
src/tools/miri/tests/genmc/pass/std/empty_main.rs
View file

@ -1,5 +1,4 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
//@normalize-stderr-test: "\n *= note: inside `std::.*" -> ""
// A lot of code runs before main, which we should be able to handle in GenMC mode.

43
src/tools/miri/tests/genmc/pass/std/empty_main.stderr
View file

@ -1,45 +1,2 @@
Running GenMC Verification...
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/thread/id.rs:LL:CC
|
LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/rt.rs:LL:CC
|
LL | / CLEANUP.call_once(|| unsafe {
LL | | // Flush stdout and disable buffering.
LL | | crate::io::cleanup();
... |
LL | | });
| |______^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sync/once.rs:LL:CC
|
LL | self.inner.call(true, &mut |p| f.take().unwrap()(p));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sync/once.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
|
LL | match EXITING_THREAD_ID.compare_exchange(ptr::null_mut(), this_thread_id, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
Verification complete with 1 executions. No errors found.

1
src/tools/miri/tests/genmc/pass/std/spawn_std_threads.rs
View file

@ -1,5 +1,4 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
//@normalize-stderr-test: "\n *= note: inside `std::.*" -> ""
// We should be able to spawn and join standard library threads in GenMC mode.
// Since these threads do nothing, we should only explore 1 program execution.

128
src/tools/miri/tests/genmc/pass/std/spawn_std_threads.stderr
View file

@ -1,130 +1,2 @@
Running GenMC Verification...
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/thread/id.rs:LL:CC
|
LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC
note: inside closure
--> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC
|
LL | let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= note: inside closure at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC
= note: inside `<std::ops::Range<usize> as std::iter::Iterator>::fold::<(), {closure@std::iter::adapters::map::map_fold<usize, std::thread::JoinHandle<()>, (), {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}, {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@std::vec::Vec<std::thread::JoinHandle<()>>::extend_trusted<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
= note: inside `<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@std::vec::Vec<std::thread::JoinHandle<()>>::extend_trusted<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC
= note: inside `<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::for_each::<{closure@std::vec::Vec<std::thread::JoinHandle<()>>::extend_trusted<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::vec::spec_extend::SpecExtend<std::thread::JoinHandle<()>, std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::spec_extend` at RUSTLIB/alloc/src/vec/spec_extend.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::vec::spec_from_iter_nested::SpecFromIterNested<std::thread::JoinHandle<()>, std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::from_iter` at RUSTLIB/alloc/src/vec/spec_from_iter_nested.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::vec::spec_from_iter::SpecFromIter<std::thread::JoinHandle<()>, std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::from_iter` at RUSTLIB/alloc/src/vec/spec_from_iter.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::iter::FromIterator<std::thread::JoinHandle<()>>>::from_iter::<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
= note: inside `<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::collect::<std::vec::Vec<std::thread::JoinHandle<()>>>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC
|
LL | let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC
note: inside closure
--> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC
|
LL | let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= note: inside closure at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC
= note: inside `<std::ops::Range<usize> as std::iter::Iterator>::fold::<(), {closure@std::iter::adapters::map::map_fold<usize, std::thread::JoinHandle<()>, (), {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}, {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@std::vec::Vec<std::thread::JoinHandle<()>>::extend_trusted<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
= note: inside `<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@std::vec::Vec<std::thread::JoinHandle<()>>::extend_trusted<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC
= note: inside `<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::for_each::<{closure@std::vec::Vec<std::thread::JoinHandle<()>>::extend_trusted<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::vec::spec_extend::SpecExtend<std::thread::JoinHandle<()>, std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::spec_extend` at RUSTLIB/alloc/src/vec/spec_extend.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::vec::spec_from_iter_nested::SpecFromIterNested<std::thread::JoinHandle<()>, std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::from_iter` at RUSTLIB/alloc/src/vec/spec_from_iter_nested.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::vec::spec_from_iter::SpecFromIter<std::thread::JoinHandle<()>, std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::from_iter` at RUSTLIB/alloc/src/vec/spec_from_iter.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::iter::FromIterator<std::thread::JoinHandle<()>>>::from_iter::<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
= note: inside `<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::collect::<std::vec::Vec<std::thread::JoinHandle<()>>>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC
|
LL | let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
note: inside closure
--> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC
|
LL | handles.into_iter().for_each(|handle| handle.join().unwrap());
| ^^^^^^^^^^^^^
= note: inside closure at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
= note: inside `<std::vec::IntoIter<std::thread::JoinHandle<()>> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>::{closure#0}}>` at RUSTLIB/alloc/src/vec/into_iter.rs:LL:CC
= note: inside `<std::vec::IntoIter<std::thread::JoinHandle<()>> as std::iter::Iterator>::for_each::<{closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC
|
LL | handles.into_iter().for_each(|handle| handle.join().unwrap());
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/rt.rs:LL:CC
|
LL | / CLEANUP.call_once(|| unsafe {
LL | | // Flush stdout and disable buffering.
LL | | crate::io::cleanup();
... |
LL | | });
| |______^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sync/once.rs:LL:CC
|
LL | self.inner.call(true, &mut |p| f.take().unwrap()(p));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sync/once.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
|
LL | match EXITING_THREAD_ID.compare_exchange(ptr::null_mut(), this_thread_id, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
Verification complete with 1 executions. No errors found.

1
src/tools/miri/tests/genmc/pass/std/thread_locals.rs
View file

@ -1,5 +1,4 @@
//@compile-flags: -Zmiri-ignore-leaks -Zmiri-genmc -Zmiri-disable-stacked-borrows
//@normalize-stderr-test: "\n *= note: inside `std::.*" -> ""
use std::alloc::{Layout, alloc};
use std::cell::Cell;

111
src/tools/miri/tests/genmc/pass/std/thread_locals.stderr
View file

@ -1,113 +1,2 @@
Running GenMC Verification...
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/thread/id.rs:LL:CC
|
LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/thread_locals.rs:LL:CC
|
LL | / std::thread::spawn(|| {
LL | | R.set(unsafe { malloc() });
LL | | let r_ptr = R.get();
LL | | let _ = X.compare_exchange(std::ptr::null_mut(), r_ptr, SeqCst, SeqCst);
LL | | }),
| |__________^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/thread_locals.rs:LL:CC
|
LL | / std::thread::spawn(|| {
LL | | R.set(unsafe { malloc() });
LL | | let r_ptr = R.get();
LL | | let _ = X.compare_exchange(std::ptr::null_mut(), r_ptr, SeqCst, SeqCst);
LL | | }),
| |__________^
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
note: inside closure
--> tests/genmc/pass/std/thread_locals.rs:LL:CC
|
LL | handles.into_iter().for_each(|handle| handle.join().unwrap());
| ^^^^^^^^^^^^^
= note: inside closure at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
= note: inside closure at RUSTLIB/core/src/ops/try_trait.rs:LL:CC
= note: inside closure at RUSTLIB/core/src/array/iter/iter_inner.rs:LL:CC
= note: inside `<std::ops::index_range::IndexRange as std::iter::Iterator>::try_fold::<(), {closure@std::array::iter::iter_inner::PolymorphicIter<[std::mem::MaybeUninit<std::thread::JoinHandle<()>>]>::try_fold<(), {closure@std::ops::try_trait::NeverShortCircuit<()>::wrap_mut_2<(), std::thread::JoinHandle<()>, {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@tests/genmc/pass/std/thread_locals.rs:LL:CC}>::{closure#0}}>::{closure#0}}, std::ops::try_trait::NeverShortCircuit<()>>::{closure#0}}, std::ops::try_trait::NeverShortCircuit<()>>` at RUSTLIB/core/src/ops/index_range.rs:LL:CC
= note: inside `<std::array::IntoIter<std::thread::JoinHandle<()>, 3> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@tests/genmc/pass/std/thread_locals.rs:LL:CC}>::{closure#0}}>` at RUSTLIB/core/src/array/iter.rs:LL:CC
= note: inside `<std::array::IntoIter<std::thread::JoinHandle<()>, 3> as std::iter::Iterator>::for_each::<{closure@tests/genmc/pass/std/thread_locals.rs:LL:CC}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/thread_locals.rs:LL:CC
|
LL | handles.into_iter().for_each(|handle| handle.join().unwrap());
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/rt.rs:LL:CC
|
LL | / CLEANUP.call_once(|| unsafe {
LL | | // Flush stdout and disable buffering.
LL | | crate::io::cleanup();
... |
LL | | });
| |______^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sync/once.rs:LL:CC
|
LL | self.inner.call(true, &mut |p| f.take().unwrap()(p));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sync/once.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
|
LL | match EXITING_THREAD_ID.compare_exchange(ptr::null_mut(), this_thread_id, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
Verification complete with 2 executions. No errors found.