rust-for-linux.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
From: Alice Ryhl <aliceryhl@google.com>
To: Ventura Jack <venturajack85@gmail.com>
Cc: Linus Torvalds <torvalds@linux-foundation.org>,
	 Kent Overstreet <kent.overstreet@linux.dev>,
	Gary Guo <gary@garyguo.net>,
	airlied@gmail.com,  boqun.feng@gmail.com,
	david.laight.linux@gmail.com, ej@inai.de,
	 gregkh@linuxfoundation.org, hch@infradead.org, hpa@zytor.com,
	 ksummit@lists.linux.dev, linux-kernel@vger.kernel.org,
	 miguel.ojeda.sandonis@gmail.com, rust-for-linux@vger.kernel.org
Subject: Re: C aggregate passing (Rust kernel policy)
Date: Tue, 25 Feb 2025 18:36:07 +0100	[thread overview]
Message-ID: <CAH5fLghEMtT663SNogAGad-qk7umefGeBKbm+QjKKzoskjOubw@mail.gmail.com> (raw)
In-Reply-To: <CAFJgqgREAj-eP-d244WpqO-9H48ajZh83AxE31GqoONZ=DJe-g@mail.gmail.com>

On Tue, Feb 25, 2025 at 6:21 PM Ventura Jack <venturajack85@gmail.com> wrote:
>
> On Tue, Feb 25, 2025 at 9:12 AM Alice Ryhl <aliceryhl@google.com> wrote:
> >
> > On Sun, Feb 23, 2025 at 4:30 PM Ventura Jack <venturajack85@gmail.com> wrote:
> > >
> > > Just to be clear and avoid confusion, I would
> > > like to clarify some aspects of aliasing.
> > > In case that you do not already know about this,
> > > I suspect that you may find it very valuable.
> > >
> > > I am not an expert at Rust, so for any Rust experts
> > > out there, please feel free to point out any errors
> > > or mistakes that I make in the following.
> > >
> > > The Rustonomicon is (as I gather) the semi-official
> > > documentation site for unsafe Rust.
> > >
> > > Aliasing in C and Rust:
> > >
> > > C "strict aliasing":
> > > - Is not a keyword.
> > > - Based on "type compatibility".
> > > - Is turned off by default in the kernel by using
> > >     a compiler flag.
> > >
> > > C "restrict":
> > > - Is a keyword, applied to pointers.
> > > - Is opt-in to a kind of aliasing.
> > > - Is seldom used in practice, since many find
> > >     it difficult to use correctly and avoid
> > >     undefined behavior.
> > >
> > > Rust aliasing:
> > > - Is not a keyword.
> > > - Applies to certain pointer kinds in Rust, namely
> > >     Rust "references".
> > >     Rust pointer kinds:
> > >     https://doc.rust-lang.org/reference/types/pointer.html
> > > - Aliasing in Rust is not opt-in or opt-out,
> > >     it is always on.
> > >     https://doc.rust-lang.org/nomicon/aliasing.html
> > > - Rust has not defined its aliasing model.
> > >     https://doc.rust-lang.org/nomicon/references.html
> > >         "Unfortunately, Rust hasn't actually
> > >         defined its aliasing model.
> > >         While we wait for the Rust devs to specify
> > >         the semantics of their language, let's use
> > >         the next section to discuss what aliasing is
> > >         in general, and why it matters."
> > >     There is active experimental research on
> > >     defining the aliasing model, including tree borrows
> > >     and stacked borrows.
> > > - The aliasing model not being defined makes
> > >     it harder to reason about and work with
> > >     unsafe Rust, and therefore harder to avoid
> > >     undefined behavior/memory safety bugs.
> >
> > I think all of this worrying about Rust not having defined its
> > aliasing model is way overblown. Ultimately, the status quo is that
> > each unsafe operation that has to do with aliasing falls into one of
> > three categories:
> >
> > * This is definitely allowed.
> > * This is definitely UB.
> > * We don't know whether we want to allow this yet.
> >
> > The full aliasing model that they want would eliminate the third
> > category. But for practical purposes you just stay within the first
> > subset and you will be happy.
> >
> > Alice
>
> Is there a specification for aliasing that defines your first bullet
> point, that people can read and use, as a kind of partial
> specification? Or maybe a subset of your first bullet point, as a
> conservative partial specification? I am guessing that stacked
> borrows or tree borrows might be useful for such a purpose.
> But I do not know whether either of stacked borrows or tree
> borrows have only false positives, only false negatives, or both.

In general I would say read the standard library docs. But I don't
know of a single resource with everything in one place.

Stacked borrows and tree borrows are attempts at creating a full model
that puts everything in the two first categories. They are not
conservative partial specifications.

> For Rust documentation, I have heard of the official
> documentation websites at
>
>     https://doc.rust-lang.org/book/
>     https://doc.rust-lang.org/nomicon/
>
> And various blogs, forums and research papers.
>
> If there is no such conservative partial specification for
> aliasing yet, I wonder if such a conservative partial
> specification could be made with relative ease, especially if
> it is very conservative, at least in its first draft. Though there
> is currently no specification of the Rust language and just
> one major compiler.
>
> I know that Java defines an additional conservative reasoning
> model for its memory model that is easier to reason about
> than the full memory model, namely happens-before
> relationship. That conservative reasoning model is taught in
> official Java documentation and in books.

On the topic of conservative partial specifications, I like the blog
post "Tower of weakenings" from back when the strict provenance APIs
were started, which I will share together with a quote from it:

> Instead, we should have a tower of Memory Models, with the ones at the top being “what users should think about and try to write their code against”. As you descend the tower, the memory models become increasingly complex or vague but critically always more permissive than the ones above it. At the bottom of the tower is “whatever the compiler actually does” (and arguably “whatever the hardware actually does” in the basement, if you care about that).
> https://faultlore.com/blah/tower-of-weakenings/

You can also read the docs for the ptr module:
https://doc.rust-lang.org/stable/std/ptr/index.html

> On the topic of difficulty, even if there was a full specification,
> it might still be difficult to work with aliasing in unsafe Rust.
> For C "restrict", I assume that "restrict" is fully specified, and
> C developers still typically avoid "restrict". And for unsafe
> Rust, the Rust community helpfully encourages people to
> avoid unsafe Rust when possible due to its difficulty.

This I will not object to :)

Alice

  reply	other threads:[~2025-02-25 17:36 UTC|newest]

Thread overview: 194+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2025-02-22 10:06 C aggregate passing (Rust kernel policy) Ventura Jack
2025-02-22 14:15 ` Gary Guo
2025-02-22 15:03   ` Ventura Jack
2025-02-22 18:54     ` Kent Overstreet
2025-02-22 19:18       ` Linus Torvalds
2025-02-22 20:00         ` Kent Overstreet
2025-02-22 20:54           ` H. Peter Anvin
2025-02-22 21:22             ` Kent Overstreet
2025-02-22 21:46               ` Linus Torvalds
2025-02-22 22:34                 ` Kent Overstreet
2025-02-22 23:56                   ` Jan Engelhardt
2025-02-22 22:12               ` David Laight
2025-02-22 22:46                 ` Kent Overstreet
2025-02-22 23:50               ` H. Peter Anvin
2025-02-23  0:06                 ` Kent Overstreet
2025-02-22 21:22             ` Linus Torvalds
2025-02-23 15:30         ` Ventura Jack
2025-02-23 16:28           ` David Laight
2025-02-24  0:27           ` Gary Guo
2025-02-24  9:57             ` Ventura Jack
2025-02-24 10:31               ` Benno Lossin
2025-02-24 12:21                 ` Ventura Jack
2025-02-24 12:47                   ` Benno Lossin
2025-02-24 16:57                     ` Ventura Jack
2025-02-24 22:03                       ` Benno Lossin
2025-02-24 23:04                         ` Ventura Jack
2025-02-25 22:38                           ` Benno Lossin
2025-02-25 22:47                             ` Miguel Ojeda
2025-02-25 23:03                               ` Benno Lossin
2025-02-24 12:58           ` Theodore Ts'o
2025-02-24 14:47             ` Miguel Ojeda
2025-02-24 14:54               ` Miguel Ojeda
2025-02-24 16:42                 ` Philip Herron
2025-02-25 15:55                   ` Ventura Jack
2025-02-25 17:30                     ` Arthur Cohen
2025-02-26 11:38               ` Ralf Jung
2025-02-24 15:43             ` Miguel Ojeda
2025-02-24 17:24               ` Kent Overstreet
2025-02-25 16:12           ` Alice Ryhl
2025-02-25 17:21             ` Ventura Jack
2025-02-25 17:36               ` Alice Ryhl [this message]
2025-02-25 18:16                 ` H. Peter Anvin
2025-02-25 20:21                   ` Kent Overstreet
2025-02-25 20:37                     ` H. Peter Anvin
2025-02-26 13:03                     ` Ventura Jack
2025-02-26 13:53                       ` Miguel Ojeda
2025-02-26 14:07                         ` Ralf Jung
2025-02-26 14:26                         ` James Bottomley
2025-02-26 14:37                           ` Ralf Jung
2025-02-26 14:39                           ` Greg KH
2025-02-26 14:45                             ` James Bottomley
2025-02-26 16:00                               ` Steven Rostedt
2025-02-26 16:42                                 ` James Bottomley
2025-02-26 16:47                                   ` Kent Overstreet
2025-02-26 16:57                                     ` Steven Rostedt
2025-02-26 17:41                                       ` Kent Overstreet
2025-02-26 17:47                                         ` Steven Rostedt
2025-02-26 22:07                                           ` Josh Poimboeuf
2025-03-02 12:19                                           ` David Laight
2025-02-26 17:11                           ` Miguel Ojeda
2025-02-26 17:42                             ` Kent Overstreet
2025-02-26 12:36                 ` Ventura Jack
2025-02-26 13:52                   ` Miguel Ojeda
2025-02-26 15:21                     ` Ventura Jack
2025-02-26 16:06                       ` Ralf Jung
2025-02-26 17:49                       ` Miguel Ojeda
2025-02-26 18:36                         ` Ventura Jack
2025-02-26 14:14                   ` Ralf Jung
2025-02-26 15:40                     ` Ventura Jack
2025-02-26 16:10                       ` Ralf Jung
2025-02-26 16:50                         ` Ventura Jack
2025-02-26 21:39                           ` Ralf Jung
2025-02-27 15:11                             ` Ventura Jack
2025-02-27 15:32                               ` Ralf Jung
2025-02-25 18:54             ` Linus Torvalds
2025-02-25 19:47               ` Kent Overstreet
2025-02-25 20:25                 ` Linus Torvalds
2025-02-25 20:55                   ` Kent Overstreet
2025-02-25 21:24                     ` Linus Torvalds
2025-02-25 23:34                       ` Kent Overstreet
2025-02-26 11:57                         ` Gary Guo
2025-02-27 14:43                           ` Ventura Jack
2025-02-26 14:26                         ` Ventura Jack
2025-02-25 22:45                   ` Miguel Ojeda
2025-02-26  0:05                     ` Miguel Ojeda
2025-02-25 22:42                 ` Miguel Ojeda
2025-02-26 14:01                   ` Ralf Jung
2025-02-26 13:54               ` Ralf Jung
2025-02-26 17:59                 ` Linus Torvalds
2025-02-26 19:01                   ` Paul E. McKenney
2025-02-26 20:00                   ` Martin Uecker
2025-02-26 21:14                     ` Linus Torvalds
2025-02-26 21:21                       ` Linus Torvalds
2025-02-26 22:54                         ` David Laight
2025-02-27  0:35                           ` Paul E. McKenney
2025-02-26 21:26                       ` Steven Rostedt
2025-02-26 21:37                         ` Steven Rostedt
2025-02-26 21:42                         ` Linus Torvalds
2025-02-26 21:56                           ` Steven Rostedt
2025-02-26 22:13                             ` Steven Rostedt
2025-02-26 22:22                               ` Linus Torvalds
2025-02-26 22:35                                 ` Steven Rostedt
2025-02-26 23:18                                   ` Linus Torvalds
2025-02-26 23:28                                     ` Steven Rostedt
2025-02-27  0:04                                       ` Linus Torvalds
2025-02-27 20:47                                   ` David Laight
2025-02-27 21:33                                     ` Steven Rostedt
2025-02-28 21:29                                       ` Paul E. McKenney
2025-02-27 21:41                                     ` Paul E. McKenney
2025-02-27 22:20                                       ` David Laight
2025-02-27 22:40                                         ` Paul E. McKenney
2025-02-28  7:44                                     ` Ralf Jung
2025-02-28 15:41                                       ` Kent Overstreet
2025-02-28 15:46                                         ` Boqun Feng
2025-02-28 16:04                                           ` Kent Overstreet
2025-02-28 16:13                                             ` Boqun Feng
2025-02-28 16:21                                               ` Kent Overstreet
2025-02-28 16:40                                                 ` Boqun Feng
2025-03-04 18:12                                         ` Ralf Jung
2025-02-26 22:27                       ` Kent Overstreet
2025-02-26 23:16                         ` Linus Torvalds
2025-02-27  0:17                           ` Kent Overstreet
2025-02-27  0:26                           ` comex
2025-02-27 18:33                           ` Ralf Jung
2025-02-27 19:15                             ` Linus Torvalds
2025-02-27 19:55                               ` Kent Overstreet
2025-02-27 20:28                                 ` Linus Torvalds
2025-02-28  7:53                               ` Ralf Jung
2025-03-06 19:16                           ` Ventura Jack
2025-02-27  4:18                       ` Martin Uecker
2025-02-27  5:52                         ` Linus Torvalds
2025-02-27  6:56                           ` Martin Uecker
2025-02-27 14:29                             ` Steven Rostedt
2025-02-27 17:35                               ` Paul E. McKenney
2025-02-27 18:13                                 ` Kent Overstreet
2025-02-27 19:10                                   ` Paul E. McKenney
2025-02-27 18:00                           ` Ventura Jack
2025-02-27 18:44                           ` Ralf Jung
2025-02-27 14:21                     ` Ventura Jack
2025-02-27 15:27                       ` H. Peter Anvin
2025-02-28  8:08                     ` Ralf Jung
2025-02-28  8:32                       ` Martin Uecker
2025-02-26 20:25                   ` Kent Overstreet
2025-02-26 20:34                     ` Andy Lutomirski
2025-02-26 22:45                   ` David Laight
2025-02-22 19:41       ` Miguel Ojeda
2025-02-22 20:49         ` Kent Overstreet
2025-02-26 11:34           ` Ralf Jung
2025-02-26 14:57             ` Ventura Jack
2025-02-26 16:32               ` Ralf Jung
2025-02-26 18:09                 ` Ventura Jack
2025-02-26 22:28                   ` Ralf Jung
2025-02-26 23:08                     ` David Laight
2025-02-27 13:55                       ` Ralf Jung
2025-02-27 17:33                     ` Ventura Jack
2025-02-27 17:58                       ` Ralf Jung
2025-02-27 19:06                         ` Ventura Jack
2025-02-27 19:45                           ` Ralf Jung
2025-02-27 20:22                             ` Kent Overstreet
2025-02-27 22:18                               ` David Laight
2025-02-27 23:18                                 ` Kent Overstreet
2025-02-28  7:38                                   ` Ralf Jung
2025-02-28 20:48                                   ` Ventura Jack
2025-02-28 20:41                             ` Ventura Jack
2025-02-28 22:13                               ` Geoffrey Thomas
2025-03-01 14:19                                 ` Ventura Jack
2025-03-04 18:24                               ` Ralf Jung
2025-03-06 18:49                                 ` Ventura Jack
2025-02-27 17:58                       ` Miguel Ojeda
2025-02-27 19:25                         ` Ventura Jack
2025-02-26 19:07                 ` Martin Uecker
2025-02-26 19:23                   ` Ralf Jung
2025-02-26 20:22                     ` Martin Uecker
     [not found] <CAFJgqgRZ1w0ONj2wbcczx2=boXYHoLOd=-ke7tHGBAcifSfPUw@mail.gmail.com>
2025-02-25 15:42 ` H. Peter Anvin
2025-02-25 16:45   ` Ventura Jack
  -- strict thread matches above, loose matches on Subject: below --
2025-02-09 20:56 Rust kernel policy Miguel Ojeda
2025-02-18 16:08 ` Christoph Hellwig
2025-02-18 18:46   ` Miguel Ojeda
2025-02-18 21:49     ` H. Peter Anvin
2025-02-18 22:54       ` Miguel Ojeda
2025-02-19  0:58         ` H. Peter Anvin
2025-02-19  3:04           ` Boqun Feng
2025-02-19  5:39             ` Greg KH
2025-02-20 12:28               ` Jan Engelhardt
2025-02-20 12:37                 ` Greg KH
2025-02-20 13:23                   ` H. Peter Anvin
2025-02-20 15:17                     ` C aggregate passing (Rust kernel policy) Jan Engelhardt
2025-02-20 16:46                       ` Linus Torvalds
2025-02-20 20:34                       ` H. Peter Anvin
2025-02-21  8:31                       ` HUANG Zhaobin
2025-02-21 18:34                       ` David Laight
2025-02-21 19:12                         ` Linus Torvalds
2025-02-21 20:07                           ` comex
2025-02-21 21:45                           ` David Laight
2025-02-22  6:32                             ` Willy Tarreau
2025-02-22  6:37                               ` Willy Tarreau
2025-02-22  8:41                                 ` David Laight
2025-02-22  9:11                                   ` Willy Tarreau
2025-02-21 20:06                         ` Jan Engelhardt
2025-02-21 20:23                           ` Laurent Pinchart
2025-02-21 20:24                             ` Laurent Pinchart
2025-02-21 22:02                             ` David Laight
2025-02-21 22:13                               ` Bart Van Assche
2025-02-22  5:56                                 ` comex
2025-02-21 20:26                           ` Linus Torvalds

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=CAH5fLghEMtT663SNogAGad-qk7umefGeBKbm+QjKKzoskjOubw@mail.gmail.com \
    --to=aliceryhl@google.com \
    --cc=airlied@gmail.com \
    --cc=boqun.feng@gmail.com \
    --cc=david.laight.linux@gmail.com \
    --cc=ej@inai.de \
    --cc=gary@garyguo.net \
    --cc=gregkh@linuxfoundation.org \
    --cc=hch@infradead.org \
    --cc=hpa@zytor.com \
    --cc=kent.overstreet@linux.dev \
    --cc=ksummit@lists.linux.dev \
    --cc=linux-kernel@vger.kernel.org \
    --cc=miguel.ojeda.sandonis@gmail.com \
    --cc=rust-for-linux@vger.kernel.org \
    --cc=torvalds@linux-foundation.org \
    --cc=venturajack85@gmail.com \
    /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;
as well as URLs for NNTP newsgroup(s).