Data race detection with a shared slice pattern

[wyfo]

https://github.com/wyfo/swap-buffer-queue crate implement a shared slice pattern: distinct parts of a slice can be written concurrently. Of course, it uses UnsafeCell and a lot of unsafe code, but the algorithm use synchronization mechanism to prevent data races.

I've just tried to run tests with miri, and data races were spotted. However, it seems to me that Miri only report concurrent accesses to the UnsafeCell, not concurrent access to the individual bytes of the UnsafeCell – in my case, a thread is accessing the length of the slice while another thread is writing a part of the slice.

Adding UnsafeCell inside the slice seems to be a solution, as it would work for buffers like Box<[MaybeUninit<T>]>, but I have several types of buffer, and one of them is just a Box<[u8]> where I write with copy_from_slice, so I don't really see how I could copy_from_slice with Box<[UnsafeCell<u8>]> ...

Considering that this data race may be a false positive, would there be a way to make miri happy with my use case?
Reformulating: how to make miri accepting concurrent writes on distinct parts of &[u8]?

[RalfJung]

Why do you think this data race is a false positive? Miri does not have known false positives for data races, so I would expect this to be a true positive. It might be surprising though since data races can arise from aliasing model interactions.

That entire crate is a bit too much code for us to go through; can you extract the most important parts into a small example (ideally one that works on the playground)?

how to make miri accepting concurrent writes on distinct parts of &[u8]?

Note that writing to &[u8] is never allowed! This is a shared reference to a type without interior mutability, it must not be mutated. Concurrency isn't even relevant for that.

[wyfo]

Here is a minimal reproducible example: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=8f2b1d1e45328e1b999cb33b7d0da96c

Miri will report a data race for accessing the length of the buffer while writing the last bytes.
If you comment the first thread::spawn and uncomment the second thread::spawn, miri report an other error, while the written bytes don't overlap. Is it a true positive data race when bytes don't overlap?

Note that writing to &[u8] is never allowed! This is a shared reference to a type without interior mutability, it must not be mutated. Concurrency isn't even relevant for that.

I wanted to say UnsafeCell<Box<[u8]>>, or UnsafeCell<Box<[UnsafeCell<u8>]>>, actually I don't know what I can use to call copy_from_slice ...

[saethlin]

Is it a true positive data race when bytes don't overlap?

Miri's data race detection, aliasing tracking, and initialization tracking all have byte-level granularity. Miri's checks are precise and there isn't any static reasoning about the program that would normally lead to false positives in other tools.

This data race arises from an aliasing model interaction. This can be made much more clear by modifying the second thread to be this:

    thread::spawn(move || loop {
        unsafe {
            let ouch = &mut *buffer_clone.0.get();
            ouch[1] = 0;
        }   
    }); 

Stacked Borrows will report a data race on the &mut * part, and Tree Borrows delays the UB until the line following.

Our diagnostics should definitely be better here. These aliasing interactions with the data race model are relatively new, and also rather hard to hit, so the diagnostic should probably call them out when they happen and try to educate the user. For the time being, you can try to refer to this issue and the linked Zulip thread: #2648.

---

While Miri doesn't have false positives like some other tools, since all the rules in Unsafe Rust aren't specified yet we tend to default to implementing a more strict prototype version than will eventually be The Rules. So since Rust isn't specified yet, IMO it's best to treat these less as "I found a Miri bug" and more as "Is it possible to make this not be UB, because that is very confusing".

[wyfo]

Actually, I've found a way of making Miri happy using Box<Cell<[u8]>> and Cell::as_slice_of_cells: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=99bdf3bc287456a9bb2d7e4143a195de

I had to use UnsafeCell::raw_get because of the lack of Cell::from_slice_of_cells.

it's best to treat these less as "I found a Miri bug" and more as "Is it possible to make this not be UB, because that is very confusing"

Indeed, I did not consider this issue as a Miri bug, what mattered to me was to find a way to express my use case in a Miri-compatible way. Now I'm fine with the solution I've found, if you don't have remarks about it, I think the issue can be closed.

[saethlin]

Sure, I'll open a new issue for improving the diagnostic.

[RalfJung]

That code is intended to be UB: when a function has &[u8], it should be allowed to read from any part of that slice, so concurrent mutation of that slice is UB. The compiler is allowed to insert reads from that reference even if none currently exist.

Note that UnsafeCell is entirely a by-value construct: it does not apply recursively below pointer indirections. Thus, UnsafeCell<Box<[u8]>> does not allow shared mutating of the inner slice.

[wyfo]

That code is intended to be UB

Do you talk about my first exemple? Is the second one with Box<Cell<[u8]>> also UB?

[RalfJung]

Box<Cell> is fine, since it properly reflects the shares mutability where it happens.