Message-Id: <DBDENRP6Z2L7.1BU1I3ZTJ21ZY@kernel.org>
Date: Wed, 16 Jul 2025 12:25:30 +0200
From: "Benno Lossin" <lossin@...nel.org>
To: "Boqun Feng" <boqun.feng@...il.com>
Cc: <linux-kernel@...r.kernel.org>, <rust-for-linux@...r.kernel.org>,
 <lkmm@...ts.linux.dev>, <linux-arch@...r.kernel.org>, "Miguel Ojeda"
 <ojeda@...nel.org>, "Alex Gaynor" <alex.gaynor@...il.com>, "Gary Guo"
 <gary@...yguo.net>, Björn Roy Baron
 <bjorn3_gh@...tonmail.com>, "Andreas Hindborg" <a.hindborg@...nel.org>,
 "Alice Ryhl" <aliceryhl@...gle.com>, "Trevor Gross" <tmgross@...ch.edu>,
 "Danilo Krummrich" <dakr@...nel.org>, "Will Deacon" <will@...nel.org>,
 "Peter Zijlstra" <peterz@...radead.org>, "Mark Rutland"
 <mark.rutland@....com>, "Wedson Almeida Filho" <wedsonaf@...il.com>,
 "Viresh Kumar" <viresh.kumar@...aro.org>, "Lyude Paul" <lyude@...hat.com>,
 "Ingo Molnar" <mingo@...nel.org>, "Mitchell Levy"
 <levymitchell0@...il.com>, "Paul E. McKenney" <paulmck@...nel.org>, "Greg
 Kroah-Hartman" <gregkh@...uxfoundation.org>, "Linus Torvalds"
 <torvalds@...ux-foundation.org>, "Thomas Gleixner" <tglx@...utronix.de>,
 "Alan Stern" <stern@...land.harvard.edu>
Subject: Re: [PATCH v7 6/9] rust: sync: atomic: Add the framework of
 arithmetic operations

On Tue Jul 15, 2025 at 10:13 PM CEST, Boqun Feng wrote:
> On Tue, Jul 15, 2025 at 08:39:04PM +0200, Benno Lossin wrote:
> [...]
>> >> > Hmm.. the CAST comment should explain why a pointer of `T` can be a
>> >> > valid pointer of `T::Repr` because the atomic_add() below is going to
>> >> > read through the pointer and write value back. The comment starting with
>> >> > "`*self`" explains the value written is a valid `T`, therefore
>> >> > conceptually atomic_add() below writes a valid `T` in form of `T::Repr`
>> >> > into `a`.
>> >> 
>> >> I see, my interpretation was that if we put it on the cast, then the
>> >> operation that `atomic_add` does also is valid.
>> >> 
>> >> But I think this comment should either be part of the `CAST` or the
>> >> `SAFETY` comment. Going by your interpretation, it would make more sense
>> >> in the SAFETY one, since there you justify that you're actually writing
>> >> a value of type `T`.
>> >> 
>> >
>> > Hmm.. you're probably right. There are two safety things about
>> > atomic_add():
>> >
>> > - Whether calling it is safe
>> > - Whether the operation on `a` (a pointer to `T` essentially) is safe.
>> 
>> Well part of calling `T::Repr::atomic_add` is that the pointer is valid.
>
> Here by saying "calling `T::Repr::atomic_add`", I think you mean the
> whole operation, so yeah, we have to consider the validy for `T` of the
> result.

I meant just the call to `atomic_add`.

> But what I'm trying to do is reasoning this in 2 steps:
>
> First, let's treat it as an `atomic_add(*mut i32, i32)`, then as long as
> we provide a valid `*mut i32`, it's safe to call. 

But the thing is, we're not supplying a valid `*mut i32`. Because the
pointer points to a value that is not actually an `i32`. You're only
allowed to write certain values and so you basically have to treat it as
a transmute + write. And so you need to include a justification for this
transmute in the write itself. 

For example, if we had `bool: AllowAtomic`, then writing a `2` in store
would be insta-UB, since we then have a `&UnsafeCell<bool>` pointing at
`2`.

This is part of library vs language UB, writing `2` into a bool and
having a reference is language-UB (ie instant UB) and writing a `2` into
a variable of type `i32` that is somewhere cast to `bool` is library-UB
(since it will lead to language-UB later). 

The safety comments become simpler when you use `UnsafeCell<T::Repr>`
instead :) since that changes this language-UB into library-UB. (the
only safety comment that is more complex then is `get_mut`, but that's
only a single one)

If you don't want that, then we can solve this in two ways:

(1) add a guarantee on `atomic_add` (and all other operations) that it
    will write `*a + v` to `a` and nothing else.
(2) make the safety requirement only require writes of the addition to
    be valid.

My preference precedence is: use `T::Repr`, (2) and finally (1). (2)
will be very wordy on all operations & the safety comments in this file,
but it's clean from a formal perspective. (1) works by saying "what
we're supplying is actually not a valid `*mut i32`, but since the
guarantee of the function ensures that only specific things are written,
it's fine" which isn't very clean. And the `T::Repr` approach avoids all
this by just storing value of `T::Repr` circumventing the whole issue.
Then we only need to justify why we can point a `&mut T` at it and that
we can do by having an invariant that should be simple to keep.

We probably should talk about this in our meeting :)

---
Cheers,
Benno

> And second assume we call it with a valid pointer to `T::Repr`, and a
> delta from `rhs_into_delta()`, then per the safety guarantee of
> `AllowAtomicAdd`, the value written at the pointer is a valid `T`.
>
> Based on these, we can prove the whole operation is safe for the given
> input.
>
>> But it actually isn't valid for all operations, only for the specific
>> one you have here. If we want to be 100% correct, we actually need to
>> change the safety comment of `atomic_add` to say that it only requires
>> the result of `*a + v` to be writable... But that is most likely very
>> annoying... (note that we also have this issue for `store`)
>> 
>> I'm not too sure on what the right way to do this is. The formal answer
>> is to "just do it right", but then safety comments really just devolve
>> into formally proving the correctness of the program. I think -- for now
>> at least :) -- that we shouldn't do this here & now (since we also have
>> a lot of other code that isn't using normal good safety comments, let
>> alone formally correct ones).
>> 
>> > How about the following:
>> >
>> >         let v = T::rhs_into_delta(v);
>> >         // CAST: Per the safety requirement of `AllowAtomic`, a valid pointer of `T` is a valid
>> >         // pointer of `T::Repr` for reads and valid for writes of values transmutable to `T`.
>> >         let a = self.as_ptr().cast::<T::Repr>();
>> >
>> >         // `*self` remains valid after `atomic_add()` because of the safety requirement of
>> >         // `AllowAtomicAdd`.
>> >         //
>> >         // SAFETY:
>> >         // - For calling `atomic_add()`:
>> >         //   - `a` is aligned to `align_of::<T::Repr>()` because of the safety requirement of
>> >         //   `AllowAtomic` and the guarantee of `Atomic::as_ptr()`.
>> >         //   - `a` is a valid pointer per the CAST justification above.
>> >         // - For accessing `*a`: the value written is transmutable to `T`
>> >         //   due to the safety requirement of `AllowAtomicAdd`.
>> >         unsafe { T::Repr::atomic_add(a, v) };

Powered by blists - more mailing lists