Skip to content

Detect non-perfectly-overlapping unordered atomic accesses as UB? #2303

Closed
@RalfJung

Description

@RalfJung

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-data-raceArea: data race detectorC-bugCategory: This is a bug.I-misses-UBImpact: makes Miri miss UB, i.e., a false negative (with default settings)

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions