Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
RalfJung opened this issue Jul 2, 2022 · 4 comments · Fixed by #3137
Closed

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

RalfJung opened this issue Jul 2, 2022 · 4 comments · Fixed by #3137
Labels
A-data-race Area: data race detector C-bug Category: This is a bug. I-misses-UB Impact: makes Miri miss UB, i.e., a false negative (with default settings)

Comments

@RalfJung
Copy link
Member

RalfJung commented Jul 2, 2022

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

@RalfJung RalfJung added A-data-race Area: data race detector C-bug Category: This is a bug. I-misses-UB Impact: makes Miri miss UB, i.e., a false negative (with default settings) labels Jul 2, 2022
@RalfJung
Copy link
Member Author

RalfJung commented Jul 2, 2022

A concern here is that this would have to duplicate a bunch of logic from weak_memory_emulation in data_race, which would not be great. Or maybe they could somehow share that logic.

Alternatively, we would have to rephrase the documentation of -Zmiri-disable-weak-memory-emulation (and maybe rename the flag?) to indicate that setting this flag could miss some UB.

Or can we run just enough of weak memory emulation to detect this UB, but do no outdated reads and also mitigate most of the performance cost of weak memory emulation?

@RalfJung
Copy link
Member Author

We should also detect racing atomic and non-atomic accesses, even if both are reads -- C++ does not allow them so Rust should conservatively also not allow them. Here is a test:

use std::sync::atomic::{AtomicU16, Ordering};
use std::thread;

fn main() {
    let a = AtomicU16::new(0);
    
    thread::scope(|s| {
        s.spawn(|| {
            let ptr = &a as *const AtomicU16 as *mut u16;
            unsafe { ptr.read(); }
        });
        s.spawn(|| {
            a.load(Ordering::SeqCst);
        });
    });
}

@taiki-e
Copy link
Member

taiki-e commented Oct 22, 2023

even if both are reads

If the atomic load is lock-free and read-only, there should be no problem. (Otherwise, It will not be possible to make code like rust-lang/rust#115577 (comment) safe.)

@RalfJung
Copy link
Member Author

If the atomic load is lock-free and read-only, there should be no problem.

In rust-lang/rust#115719 we documented this as UB, since it's not possible to write such code in C++ and we are using the C++ memory model.

I personally think read-read "races" between atomic and non-atomic accesses are fine, but if we want to allow them we'd have to extend the C++ memory model and that is something I think we should avoid. In this case the extension is already covered by extensive academic literature, so maybe it can be justified, but it should still go through a careful and explicit process.

bors added a commit that referenced this issue Oct 24, 2023
Detect mixed-size and mixed-atomicity non-synchronized accesses

Fixes #2303
@bors bors closed this as completed in d7278f9 Oct 24, 2023
RalfJung pushed a commit to RalfJung/rust that referenced this issue Oct 25, 2023
Detect mixed-size and mixed-atomicity non-synchronized accesses

Fixes rust-lang/miri#2303
lnicola pushed a commit to lnicola/rust-analyzer that referenced this issue Apr 7, 2024
Detect mixed-size and mixed-atomicity non-synchronized accesses

Fixes rust-lang/miri#2303
RalfJung pushed a commit to RalfJung/rust-analyzer that referenced this issue Apr 27, 2024
Detect mixed-size and mixed-atomicity non-synchronized accesses

Fixes rust-lang/miri#2303
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-data-race Area: data race detector C-bug Category: This is a bug. I-misses-UB Impact: makes Miri miss UB, i.e., a false negative (with default settings)
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants