Message-Id: <6149F5A9-D38A-4D28-8F97-3D672079AAB7@collabora.com>
Date: Wed, 10 Sep 2025 11:43:20 -0300
From: Daniel Almeida <daniel.almeida@...labora.com>
To: Alice Ryhl <aliceryhl@...gle.com>
Cc: Danilo Krummrich <dakr@...nel.org>,
 Miguel Ojeda <ojeda@...nel.org>,
 Alex Gaynor <alex.gaynor@...il.com>,
 Boqun Feng <boqun.feng@...il.com>,
 Gary Guo <gary@...yguo.net>,
 Björn Roy Baron <bjorn3_gh@...tonmail.com>,
 Benno Lossin <lossin@...nel.org>,
 Andreas Hindborg <a.hindborg@...nel.org>,
 Trevor Gross <tmgross@...ch.edu>,
 rust-for-linux@...r.kernel.org,
 linux-kernel@...r.kernel.org
Subject: Re: [PATCH] rust: irq: request: touch up the documentation

Hi Alice,

> On 10 Sep 2025, at 03:38, Alice Ryhl <aliceryhl@...gle.com> wrote:
> 
> On Tue, Sep 09, 2025 at 05:46:55PM -0300, Daniel Almeida wrote:
>> Parts of the documentation are either unclear or misplaced and can
>> otherwise be improved. This commit fixes them.
>> 
>> This is specially important in the context of the safety requirements of
>> functions or type invariants, as users have to uphold the former and may
>> rely on the latter, so we should avoid anything that may create
>> confusion.
>> 
>> Suggested-by: Andreas Hindborg <a.hindborg@...nel.org>
>> Signed-off-by: Daniel Almeida <daniel.almeida@...labora.com>
> 
>> /// A request for an IRQ line for a given device.
>> @@ -112,7 +117,7 @@ impl<'a> IrqRequest<'a> {
>>     ///
>>     /// - `irq` should be a valid IRQ number for `dev`.
>>     pub(crate) unsafe fn new(dev: &'a Device<Bound>, irq: u32) -> Self {
>> -        // INVARIANT: `irq` is a valid IRQ number for `dev`.
>> +        // By function safety requirement, irq` is a valid IRQ number for `dev`.
>>         IrqRequest { dev, irq }
> 
> When creating a value with an Invariants section, we usually have an
> INVARIANT comment. Why was this one removed?

This was requested by Andreas [0].

> 
>>     }
>> 
>> @@ -183,6 +188,8 @@ pub fn irq(&self) -> u32 {
>> /// * We own an irq handler whose cookie is a pointer to `Self`.
>> #[pin_data]
>> pub struct Registration<T: Handler + 'static> {
>> +    /// We need to drop inner before handler, as we must ensure that the handler
>> +    /// is valid until `free_irq` is called.
>>     #[pin]
>>     inner: Devres<RegistrationInner>,
>> 
>> @@ -196,7 +203,8 @@ pub struct Registration<T: Handler + 'static> {
>> }
>> 
>> impl<T: Handler + 'static> Registration<T> {
>> -    /// Registers the IRQ handler with the system for the given IRQ number.
>> +    /// Registers the IRQ handler with the system for the IRQ number represented
>> +    /// by `request`.
>>     pub fn new<'a>(
>>         request: IrqRequest<'a>,
>>         flags: Flags,
>> @@ -208,7 +216,11 @@ pub fn new<'a>(
>>             inner <- Devres::new(
>>                 request.dev,
>>                 try_pin_init!(RegistrationInner {
>> -                    // INVARIANT: `this` is a valid pointer to the `Registration` instance
>> +                    // INVARIANT: `this` is a valid pointer to the `Registration` instance.
>> +                    // INVARIANT: `cookie` is being passed to `request_irq` as
>> +                    // the cookie. It is guaranteed to be unique by the type
>> +                    // system, since each call to `new` will return a different
>> +                    // instance of `Registration`.
>>                     cookie: this.as_ptr().cast::<c_void>(),
> 
> I believe these comments address the invariants of RegistrationInner. In
> that case, we usually place them on the struct:
> 
> // INVARIANT: `this` is a valid pointer to the `Registration` instance.
> // INVARIANT: `cookie` is being passed to `request_irq` as
> // the cookie. It is guaranteed to be unique by the type
> // system, since each call to `new` will return a different
> // instance of `Registration`.
> try_pin_init!(RegistrationInner {
> 

Also requested by Andreas, i.e.:

> >>> +/// # Invariants
> >>> +///
> >>> +/// - `self.irq` is the same as the one passed to `request_{threaded}_irq`.
> >>> +/// - `cookie` was passed to `request_{threaded}_irq` as the cookie. It is guaranteed to be unique
> >>> +/// by the type system, since each call to `new` will return a different instance of
> >>> +/// `Registration`.
> >>
> >> This seems like a mix of invariant declaration and conformance. I don't
> >> think the following belongs here:
> >>
> >> It is guaranteed to be unique
> >> by the type system, since each call to `new` will return a different instance of
> >> `Registration`.
> >>
> >> You could replace it with a uniqueness requirement.
> >
> > WDYM? This invariant is indeed provided by the type system and we do rely on it
> > to make the abstraction work.
> 
> The invariant section of the type documentation should be a list of
> invariants, not reasoning about why the invariants hold. The reasoning
> goes in the code where we construct the type, where we momentarily
> break invariants, or where we change the value of the type.
> 
> In this case, I think the invariant is that `cookie` is unique. How we
> conform to this invariant does not belong in the list. When you
> construct the type, you should have an `// INVARIANT:` comment
> explaining why the newly constructed type upholds the invariant.
> 
> At least that is how I understand intended use of the framework.



> Also, I don't really understand these comments. The first invariant is:
> 
> `self.irq` is the same as the one passed to `request_{threaded}_irq`.
> 
> and the justification for that is that `this` is a valid pointer to the
> `Registration` instance. That doesn't make sense to me because this
> comment talks about `this`/`cookie` when it should talk about `irq`.
> 
>>                     irq: {
>>                         // SAFETY:
> 
> Alice

Is the order supposed to match? I wasn’t relating these two at this particular “// INVARIANT: "

[0]: https://lore.kernel.org/rust-for-linux/87zfblurtj.fsf@t14s.mail-host-address-is-not-set/

Powered by blists - more mailing lists