Re: [PATCH] rust: revocable: clarify invariants in safety documentation

["Benno Lossin" <lossin@kernel.org>]

On Thu May 1, 2025 at 12:18 PM CEST, Miguel Ojeda wrote:
> On Thu, May 1, 2025 at 2:57 AM Marcelo Moreira
> <marcelomoreira1905@gmail.com> wrote:
>>
>> This is part of issue #1160 ("correct safety comments and documentation
>> in revocable.rs"), reported by Miguel Ojeda and Benno Lossin.
>>
>> Reported-by: Miguel Ojeda <ojeda@kernel.org>
>> Closes: https://github.com/Rust-for-Linux/linux/issues/1160
>
> I think it was just Benno. :)
>
>> Tested-by: Marcelo Moreira <marcelomoreira1905@gmail.com>
>
> Normally one is supposed to test a patch before submitting it, i.e. it
> is implicit.
>
>> +/// # Invariants
>
> We also place `// INVARIANT: ...` comments in the places that need to
> ensure the type invariants hold, e.g. in constructors.
>
> Given the issue, I think Benno may have also wanted that you then
> refer to the type invariants to justify some of the comments, e.g. in
> the "Since `self.is_available` is true, ..." ones.

Indeed, we also need the comments that establish/make use of the
invariant. For example in the `try_access_with_guard` function.

There also is a missing invariant on `RevocableGuard` that the
`data_ref` pointer is valid.

>> +/// - Access to `data` must occur only while holding the RCU read-side lock (e.g., vi
>
> The "must occur" wording seems a bit strange for a type invariant, but
> maybe Benno had something in mind here?

Yeah, I don't think that using RCU is even a hard requirement. One could
also call `revoke_nosync`, since one knows the revocable is only used by
a single kernel thread. I also don't think that it's needed for memory
correctness, but I could be wrong there.

The most important invariant is that `data` is valid while
`is_available` is true. That's what's needed by the different functions
accessing it.

---
Cheers,
Benno