From: Miguel Ojeda <miguel.ojeda.sandonis@gmail.com>
To: Andreas Hindborg <a.hindborg@kernel.org>
Cc: "Alice Ryhl" <aliceryhl@google.com>,
"Lorenzo Stoakes" <lorenzo.stoakes@oracle.com>,
"Liam R. Howlett" <Liam.Howlett@oracle.com>,
"Miguel Ojeda" <ojeda@kernel.org>,
"Boqun Feng" <boqun.feng@gmail.com>,
"Gary Guo" <gary@garyguo.net>,
"Björn Roy Baron" <bjorn3_gh@protonmail.com>,
"Benno Lossin" <lossin@kernel.org>,
"Trevor Gross" <tmgross@umich.edu>,
"Danilo Krummrich" <dakr@kernel.org>,
linux-mm@kvack.org, rust-for-linux@vger.kernel.org,
linux-kernel@vger.kernel.org
Subject: Re: [PATCH 2/2] rust: page: add method to copy data between safe pages
Date: Tue, 17 Feb 2026 22:35:39 +0100 [thread overview]
Message-ID: <CANiq72kZQiu9DbQgkHXDDjHORwUdTm7oOhZOE4Tr8eHiyW7RbQ@mail.gmail.com> (raw)
In-Reply-To: <87ldgteftm.fsf@t14s.mail-host-address-is-not-set>
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...)
> 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).
Cheers,
Miguel
next prev parent reply other threads:[~2026-02-17 21:35 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2026-02-15 20:03 [PATCH 0/2] rust: pages that cannot be racy Andreas Hindborg
2026-02-15 20:03 ` [PATCH 1/2] rust: page: add `SafePage` for race-free page access Andreas Hindborg
2026-02-16 8:52 ` Alice Ryhl
2026-02-15 20:03 ` [PATCH 2/2] rust: page: add method to copy data between safe pages Andreas Hindborg
2026-02-15 22:33 ` Miguel Ojeda
2026-02-15 23:40 ` Andreas Hindborg
2026-02-17 21:35 ` Miguel Ojeda [this message]
2026-02-18 9:37 ` Andreas Hindborg
2026-02-18 11:41 ` Miguel Ojeda
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=CANiq72kZQiu9DbQgkHXDDjHORwUdTm7oOhZOE4Tr8eHiyW7RbQ@mail.gmail.com \
--to=miguel.ojeda.sandonis@gmail.com \
--cc=Liam.Howlett@oracle.com \
--cc=a.hindborg@kernel.org \
--cc=aliceryhl@google.com \
--cc=bjorn3_gh@protonmail.com \
--cc=boqun.feng@gmail.com \
--cc=dakr@kernel.org \
--cc=gary@garyguo.net \
--cc=linux-kernel@vger.kernel.org \
--cc=linux-mm@kvack.org \
--cc=lorenzo.stoakes@oracle.com \
--cc=lossin@kernel.org \
--cc=ojeda@kernel.org \
--cc=rust-for-linux@vger.kernel.org \
--cc=tmgross@umich.edu \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox