Message-Id: <DBDL9KI7VNO2.1QZBWS222KQGP@kernel.org>
Date: Wed, 16 Jul 2025 17:36:05 +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 Wed Jul 16, 2025 at 4:13 PM CEST, Boqun Feng wrote:
> 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.

There is no UB here and the public API surface is sound.

The problem is the internal safe <-> unsafe code interaction & the
safety documentation.

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

That's true, but not analogous to this case. This is a better analogy:

You have a lemma that proves P given that x == 10. Now you want to use
this lemma, but you are only able to prove that x >= 10. You argue that
this is fine, because the proof of the lemma only uses the fact that
x >= 10.
    But in this situation you're not following the exact rules of the
formal system. To do that you would have to reformulate the lemma to
only ask for x >= 10.

The last part is what relaxing the safety requirements would be
(approach (2) given below).

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

Hmm what does the additional indirection give you?

Otherwise this looks like the `T::Repr` approach that I detailed above,
so I like it :)

---
Cheers,
Benno

Powered by blists - more mailing lists