Re: [PATCH 2/2] rust: page: add method to copy data between safe pages

[Andreas Hindborg <a.hindborg@kernel.org>]

"Miguel Ojeda" <miguel.ojeda.sandonis@gmail.com> writes:

> On Mon, Feb 16, 2026 at 12:42 AM Andreas Hindborg <a.hindborg@kernel.org> wrote:
>>
>> Why?
>
> If you mean why we don't do it everywhere, then it is because for many
> functions it wouldn't add much value, but it would add substantial
> verbosity, which has a cost for both readers and writers.
>
> Originally, we picked the standard library style, because it seemed
> like a good balance that both had shown good results (especially for
> this language, where we have rich, strong types in signatures which
> help reduce the need) and that would get others to write docs easily.
>
> Sometimes it may be needed, e.g. there are many parameters with
> details to explain that wouldn't read well otherwise, or there are
> primitive integers parameters with constraints on them (instead of a
> newtype that enforces them) and so on.
>
> i.e. why do you think you need it here? When a reader sees the list,
> they will need to pause to read it, thinking there is something
> important/subtle there -- is there?
>
> (I say this as someone that generally likes structured, "exhaustive"
> documentation such as, say, the classic Win32 docs...)

I would rather not get into an argument about things that are subjective,
but if we picked a style, I should for sure follow that.

If we picked a style for documenting argument lists, perhaps we should
add it to Documentation/rust/coding-guidelines.rst?

>
>> Writes require a mutable reference. There cannot be a mutable reference
>> while we have a shared reference.
>
> Ok, but I am trying to map what you wrote with what the callee
> requires. In the second bullet point, you justify there are no races
> for the read side, and the third one for the write side. But you refer
> to the type invariant in the second one, for some reason, and that
> type invariant already promises no data races for `SafePage`, and all
> we have here are `SafePage`s on both sides, no?
>
> So to me it sounds like either you could justify everything just by
> invoking the type invariant (that is why I mentioned circular
> reasoning, because the type invariant doesn't seem justified itself in
> `// INVARIANT:`) or the type invariant is actually a different, weaker
> one (which would explain why you need extra explanations in `//
> SAFETY:` on top of the type invariant).
>
> (By the way, if we use bullet points, then I think we should map each
> to the callee's one, i.e. #2 and #3 would be together since #2 is the
> one in the callee about data races).

Others called out that the type invariant on `SafePage` is mushy. I will
try to tighten that up. I want it to convey the information that the
data of this page follows standard Rust aliasing rules. If you have a
shared reference to a `SafePage`, there can be no writes to the data. If
you have an exclusive reference, you are the only writer, and there are
no other readers.

I disagree that the bullets should be swapped. The second bullet at the
call site:

  // - By type invariant and existence of shared reference, there are no other writes to
  //   `src` during this call.

Maps to the second bullet in the callee safety requirements:

  /// * Callers must ensure that there are no concurrent writes to the source memory region.

The third bullet at the call site:

  // - By exclusive ownership of `dst`, there are no other writes to `dst` during this
  //   call.

Maps to the third bullet of the callee safety requirements:


  /// * Callers must ensure that this call does not race with a read or write to the same page
  ///   that overlaps with this write.

I think it checks out? `self` becomes `src` at the call site.

But now that I look, I think it should say:

  // - By type invariant and existence of shared reference, there are no writes to
  //   `src` during this call.

That is, the word "other" is misleading. There are no writers, not us -
not others. We are doing a read of `src`.

Best regards,
Andreas Hindborg