mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

make sure we also detect mixed-size races that begin at different addresses

Browse Source
This commit is contained in:
Ralf Jung 2024-10-03 08:19:07 +02:00
parent 32d49680d6
commit 9b35886adf
3 changed files with 47 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/tools/miri/tests/fail/data_race/mixed_size_write_write.fst.stderr Normal file
View File

@ -0,0 +1,22 @@
error: Undefined Behavior: Race condition detected between (1) 2-byte atomic store on thread `unnamed-ID` and (2) 1-byte atomic store on thread `unnamed-ID` at ALLOC. (2) just happened here
--> tests/fail/data_race/mixed_size_write_write.rs:LL:CC
|
LL | a8[idx].store(1, Ordering::SeqCst);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 2-byte atomic store on thread `unnamed-ID` and (2) 1-byte atomic store on thread `unnamed-ID` at ALLOC. (2) just happened here
|
help: and (1) occurred earlier here
--> tests/fail/data_race/mixed_size_write_write.rs:LL:CC
|
LL | a16.store(1, Ordering::SeqCst);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= help: overlapping unsynchronized atomic accesses must use the same access size
= help: see https://doc.rust-lang.org/nightly/std/sync/atomic/index.html#memory-model-for-atomic-accesses for more information about the Rust memory model
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE (of the first span) on thread `unnamed-ID`:
= note: inside closure at tests/fail/data_race/mixed_size_write_write.rs:LL:CC
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
error: aborting due to 1 previous error

4
src/tools/miri/tests/fail/data_race/mixed_size_write_write.rs
View File

@ -1,6 +1,7 @@
//@compile-flags: -Zmiri-preemption-rate=0.0 -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
use std::sync::atomic::{AtomicU8, AtomicU16, Ordering};
use std::thread;
@ -21,7 +22,8 @@ fn main() {
a16.store(1, Ordering::SeqCst);
});
s.spawn(|| {
a8[0].store(1, Ordering::SeqCst);
let idx = if cfg!(fst) { 0 } else { 1 };
a8[idx].store(1, Ordering::SeqCst);
//~^ ERROR: Race condition detected between (1) 2-byte atomic store on thread `unnamed-1` and (2) 1-byte atomic store on thread `unnamed-2`
});
});

22
src/tools/miri/tests/fail/data_race/mixed_size_write_write.snd.stderr Normal file
View File

@ -0,0 +1,22 @@
error: Undefined Behavior: Race condition detected between (1) 2-byte atomic store on thread `unnamed-ID` and (2) 1-byte atomic store on thread `unnamed-ID` at ALLOC+0x1. (2) just happened here
--> tests/fail/data_race/mixed_size_write_write.rs:LL:CC
|
LL | a8[idx].store(1, Ordering::SeqCst);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Race condition detected between (1) 2-byte atomic store on thread `unnamed-ID` and (2) 1-byte atomic store on thread `unnamed-ID` at ALLOC+0x1. (2) just happened here
|
help: and (1) occurred earlier here
--> tests/fail/data_race/mixed_size_write_write.rs:LL:CC
|
LL | a16.store(1, Ordering::SeqCst);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= help: overlapping unsynchronized atomic accesses must use the same access size
= help: see https://doc.rust-lang.org/nightly/std/sync/atomic/index.html#memory-model-for-atomic-accesses for more information about the Rust memory model
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE (of the first span) on thread `unnamed-ID`:
= note: inside closure at tests/fail/data_race/mixed_size_write_write.rs:LL:CC
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
error: aborting due to 1 previous error