Closed
Description
See rust-lang/unsafe-code-guidelines#345 for the details. This issue is about actually detecting the UB described there in Miri. In particular, this should be UB:
use std::sync::atomic::{AtomicU8, AtomicU16, Ordering};
use std::thread;
fn convert(a: &AtomicU16) -> &[AtomicU8; 2] {
unsafe { std::mem::transmute(a) }
}
fn main() {
let a = AtomicU16::new(0);
let a16 = &a;
let a8 = convert(a16);
thread::scope(|s| {
s.spawn(|| {
a16.store(1, Ordering::SeqCst);
});
s.spawn(|| {
a8[0].load(Ordering::SeqCst);
});
});
}
So, I wonder can we make the Miri data race detector detect this?
@cbeuw and me discussed these things in detail for #1963, because the weak memory layer inevitably notices this. However I think we should detect this even with -Zmiri-disable-weak-memory-emulation
, since this is more of a data race thing than a weak memory thing. And in principle, the vector clocks should have enough information for that, shouldn't they?
Cc @JCTyblaidd