Message-ID: <aHezbbzk0FyBW9jS@Mac.home>
Date: Wed, 16 Jul 2025 07:13:01 -0700
From: Boqun Feng <boqun.feng@...il.com>
To: Benno Lossin <lossin@...nel.org>
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 Wed, Jul 16, 2025 at 12:25:30PM +0200, Benno Lossin wrote:
> 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). 
> 

But we are not writing `2` in this case, right? 

A) we have a pointer `*mut i32`, and the memory location is valid for
   writing an `i32`, so we can pass it to a function that may write
   an `i32` to it.

B) and at the same time, we prove that the value written was a valid
   `bool`.

There is no `2` written in the whole process, the proof contains two
parts, that is it. There is no language-UB or library-UB in the whole
process, and you're missing it.

It's like if you want to prove 3 < x < 5, you first prove that x > 3
and then x < 5. It's just that you don't prove it in one go.

> 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 :)
> 

I have a better solution:

in ops.rs

    pub struct AtomicRepr<T: AtomicImpl>(UnsafeCell<T>)

    impl AtomicArithmeticOps for i32 {
        // a *safe* function
        fn atomic_add(a: &AtomicRepr, v: i32) {
	    ...
	}
    }

in generic.rs

    pub struct Atomic<T>(AtoimcRepr<T::Repr>);

    impl<T: AtomicAdd> Atomic<T> {
        fn add(&self, v: .., ...) {
	    T::Repr::atomic_add(&self.0, ...);
	}
    }

see:

	https://git.kernel.org/pub/scm/linux/kernel/git/boqun/linux.git/log/?h=rust-atomic-impl

Regards,
Boqun

> ---
> 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