-
Notifications
You must be signed in to change notification settings - Fork 402
Closed
Labels
A-concurrencyArea: affects our concurrency (multi-thread) supportArea: affects our concurrency (multi-thread) supportA-weak-memoryArea: emulation of weak memory effects (store buffers)Area: emulation of weak memory effects (store buffers)C-bugCategory: This is a bug.Category: This is a bug.I-false-UBImpact: makes Miri falsely report UB, i.e., a false positive (with default settings)Impact: makes Miri falsely report UB, i.e., a false positive (with default settings)
Description
Miri reports UB in this program (even with -Zmiri-fixed-schedule):
use std::sync::atomic::{AtomicUsize, Ordering};
use std::{ptr, thread};
const SIZE: usize = 256;
static mut ARRAY: [u8; SIZE] = [0; _];
// Everything strictly less than this has been initialized by the sender.
static POS: AtomicUsize = AtomicUsize::new(0);
fn main() {
// Sender
let th = std::thread::spawn(|| {
for i in 0..SIZE {
unsafe { ptr::write(&raw mut ARRAY[i], 1) };
POS.store(i + 1, Ordering::Release);
thread::yield_now();
// We are the only writer, so we can do non-atomic reads as well.
unsafe { (&raw const POS).cast::<usize>().read() };
}
});
// Receiver
loop {
let i = POS.load(Ordering::Acquire);
if i > 0 {
unsafe { ptr::read(&raw const ARRAY[i - 1]) };
}
if i == SIZE {
break;
}
thread::yield_now();
}
th.join().unwrap();
}This is related to the non-atomic read; if we remove that, the program is fine.
Mixed atomic and non-atomic accesses are a Rust extension to the C++ memory model. Does our extension allow this code? I would think so; the non-atomic load is fully ordered wrt all writes to that location. Tokio certainly would like this to be allowed (tokio-rs/tokio#7712). But apparently our extension to the data race checker disallows this...
Cc @cbeuw
Metadata
Metadata
Assignees
Labels
A-concurrencyArea: affects our concurrency (multi-thread) supportArea: affects our concurrency (multi-thread) supportA-weak-memoryArea: emulation of weak memory effects (store buffers)Area: emulation of weak memory effects (store buffers)C-bugCategory: This is a bug.Category: This is a bug.I-false-UBImpact: makes Miri falsely report UB, i.e., a false positive (with default settings)Impact: makes Miri falsely report UB, i.e., a false positive (with default settings)