Re: [PATCH v5 04/10] rust: sync: atomic: Add generic atomics

[Andreas Hindborg <a.hindborg@kernel.org>]

"Boqun Feng" <boqun.feng@gmail.com> writes:

> On Tue, Jul 01, 2025 at 10:54:09AM +0200, Andreas Hindborg wrote:
>> "Alan Stern" <stern@rowland.harvard.edu> writes:
>>
>> > On Mon, Jun 30, 2025 at 11:52:35AM +0200, Andreas Hindborg wrote:
>> >> "Boqun Feng" <boqun.feng@gmail.com> writes:
>> >> > Well, a non-atomic read vs an atomic read is not a data race (for both
>> >> > Rust memory model and LKMM), so your proposal is overly restricted.
>> >>
>> >> OK, my mistake then. I thought mixing marked and plain accesses would be
>> >> considered a race. I got hat from
>> >> `tools/memory-model/Documentation/explanation.txt`:
>> >>
>> >>     A "data race"
>> >>     occurs when there are two memory accesses such that:
>> >>
>> >>     1.	they access the same location,
>> >>
>> >>     2.	at least one of them is a store,
>> >>
>> >>     3.	at least one of them is plain,
>> >>
>> >>     4.	they occur on different CPUs (or in different threads on the
>> >>       same CPU), and
>> >>
>> >>     5.	they execute concurrently.
>> >>
>> >> I did not study all that documentation, so I might be missing a point or
>> >> two.
>> >
>> > You missed point 2 above: at least one of the accesses has to be a
>> > store.  When you're looking at a non-atomic read vs. an atomic read,
>> > both of them are loads and so it isn't a data race.
>>
>> Ah, right. I was missing the entire point made by Boqun. Thanks for
>> clarifying.
>>
>> Since what constitutes a race might not be immediately clear to users
>> (like me), can we include the section above in the safety comment,
>> rather than deferring to LKMM docs?
>>
>
> Still, I don't think it's a good idea. For a few reasons:
>
> 1) Maintaining multiple sources of truth is painful and risky, it's
>    going to be further confusing if users feel LKMM and the function
>    safety requirement conflict with each other.

I would agree.

>
> 2) Human language is not the best tool to describe memory model, that's
>    why we use herd to describe and use memory model. Trying to describe
>    the memory model in comments rather than referring to the formal
>    model is a way backwards.

I do not agree with this. I read human language much better than formal logic.

>
> 3) I believed the reason we got our discussion here is because you tried
>    to improve the comment of `from_ptr()`, and I do appreciate that
>    effort. And I think we should continue in that direction instead of
>    pulling the whole "what are data race conditions" into picture.

Yes, absolutely.

> So
>    how about we clearly call out that it'll be safe if other accesses
>    are atomic, which should be the most cases:
>
>    /// - For the duration of `'a`, other accesses to the object cannot cause data races
>    ///   (defined by [`LKMM`]) against atomic operations on the returned reference. Note
>    ///   that if all other accesses are atomic, then this safety requirement is trivially
>    ///   fulfilled.

Sounds good to me, thanks!


Best regards,
Andreas Hindborg