From: Benno Lossin <benno.lossin@proton.me>
To: Boqun Feng <boqun.feng@gmail.com>
Cc: "Jonathan Corbet" <corbet@lwn.net>,
"Miguel Ojeda" <ojeda@kernel.org>,
"Alex Gaynor" <alex.gaynor@gmail.com>,
"Wedson Almeida Filho" <wedsonaf@gmail.com>,
"Gary Guo" <gary@garyguo.net>,
"Björn Roy Baron" <bjorn3_gh@protonmail.com>,
"Andreas Hindborg" <a.hindborg@samsung.com>,
"Alice Ryhl" <aliceryhl@google.com>,
linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org,
rust-for-linux@vger.kernel.org, lkmm@lists.linux.dev
Subject: Re: [RFC PATCH 1/5] doc: rust: create safety standard
Date: Wed, 24 Jul 2024 22:01:50 +0000 [thread overview]
Message-ID: <289d66fb-a698-4d3b-b809-0e3305199a2c@proton.me> (raw)
In-Reply-To: <Zprkf4FrBXgYmtgg@boqun-archlinux>
On 20.07.24 00:11, Boqun Feng wrote:
> Hi Benno,
>
> On Wed, Jul 17, 2024 at 10:12:29PM +0000, Benno Lossin wrote:
> [...]
>> @@ -0,0 +1,246 @@
>> +.. SPDX-License-Identifier: GPL-2.0
>> +.. highlight:: rust
>> +
>> +====================
>> +Rust Safety Standard
>> +====================
>> +
>> +Safe Rust code cannot have memory related bugs. This is a guarantee by the Rust compiler. Of course
>> +it is not without caveats: no compiler bugs, no bugs in the specification etc. But the possibly most
>> +important caveat is that of ``unsafe`` code. ``unsafe`` code needs to follow certain rules in order
>> +for safe code to enjoy the no-memory-bugs privilege. A simple example of such a rule is that
>> +references must be valid for the duration of their lifetime. If any rule is violated, it can lead
>> +to undefined behavior even in safe code! The term undefined behavior in Rust has a lot stricter
>> +meaning than in C or C++: UB in Rust is totally forbidden. In C one might rely on the compiler
>> +implementation to ensure correct code generation, but that is not the case for Rust. You can read
>
> I don't disagree with your intention here (i.e. we should seek for
> UB-free program), however, during the discussion on memory model, I got
> response like in [1]:
>
> ... they are technically wrong (violating the C standard), but
> practically well-tested. (and then above I added that there's
> good reasons for why they don't go wrong: volatile compilation
> strategies and reordering constraints relating volatile, inline
> asm, and non-atomics make it so that this almost 'has to' work,
> I think.)
>
> which suggests that we should rely on the compiler implementation to
> ensure the "correct" code generation.
I disagree, why can't we get the specification to specify what we need?
I would rather have a compiler and standard that are in sync and give us
what we need, than have a standard that says we aren't allowed to do X,
but compilers still allow you to do X. I don't understand why this is
the case for C (I would bet this is is because of history/legacy).
> Basically, since LKMM relies on a few things that C standard dosen't
> say, e.g. votatile accesses on certain types are atomic, behaviors of
> asm blocks, dependencies. Let alone we have data_race() where for
> example, the diagnostic code accesses the shared variable out of the
> core synchronization design.
>
> All of the above is difficult to implement purely UB-free in Rust IIUC.
> Of course you could argue the ideal way is to teach Rust how to model
> these useful operations/patterns as non-UBs, but that's a relatively
> high task:
>
> Or do we want to go well beyond what happens in C, and actually
> define a memory model that both has the performance
> characteristics required by Linux, and can be defined precisely
> as a language-level graph-based (or ideally operational)
> concurrency memory model? This is a monumental task and a large
> open problem, and should not be on the list of blocking issues
> for anything that needs to get done in the next 5 years. ;)
>
> from Ralf [2].
>
> Again, I don't want to rely on compiler's behaviors on UBs, it's just
> the langauge is not ready for some jobs and programmers have to be
> "creative".
I think this is something that we need to very carefully evaluate on a
case-by-case basis. I think that with Rust we have a clean slate and can
try from the beginning to ensure that there is no
compiler-but-not-specification behavior that we rely upon. AFAIK the
Rust standard moves quicker than the C standard, so we might be able to
influence it more easily.
So what I am trying to say is: let UB be an actually useful term of
forbidden behavior. If you want to convince me otherwise, I think we
should talk specifics and not in this general way, since "sometimes UB
is actually ok" is something that I don't want to accept in Rust as a
general statement. If we have an exception, it should have a damn good
reason to be an exception and then still I don't like it one bit. Can't
we just ask the Rust folks to implement some compiler magic for us that
achieves what we need without relying one some weird compiler quirk?
---
Cheers,
Benno
> Regards,
> Boqun
>
> [1]: https://rust-lang.zulipchat.com/#narrow/stream/136281-t-opsem/topic/.E2.9C.94.20Rust.20and.20the.20Linux.20Kernel.20Memory.20Model/near/422193212
> [2]: https://github.com/rust-lang/unsafe-code-guidelines/issues/348#issuecomment-1221376388
>
>> +more about UB in Rust
>> +`here <https://doc.rust-lang.org/reference/behavior-considered-undefined.html>`_.
>> +
> [...]
next prev parent reply other threads:[~2024-07-24 22:01 UTC|newest]
Thread overview: 32+ messages / expand[flat|nested] mbox.gz Atom feed top
2024-07-17 22:12 [RFC PATCH 0/5] Introduce the Rust Safety Standard Benno Lossin
2024-07-17 22:12 ` [RFC PATCH 1/5] doc: rust: create safety standard Benno Lossin
2024-07-18 4:45 ` Greg KH
2024-07-24 19:13 ` Benno Lossin
2024-07-25 4:57 ` Greg KH
2024-07-18 12:20 ` Alice Ryhl
2024-07-24 19:36 ` Benno Lossin
2024-07-19 16:24 ` Daniel Almeida
2024-07-19 16:46 ` Alice Ryhl
2024-07-19 17:10 ` Danilo Krummrich
2024-07-19 18:09 ` Daniel Almeida
2024-07-19 19:20 ` Danilo Krummrich
2024-07-19 17:28 ` Miguel Ojeda
2024-07-19 18:18 ` Daniel Almeida
2024-07-19 17:56 ` Miguel Ojeda
2024-07-24 20:31 ` Benno Lossin
2024-07-24 21:20 ` Miguel Ojeda
2024-07-24 21:28 ` Benno Lossin
2024-08-08 13:01 ` Daniel Almeida
2024-08-08 13:08 ` Miguel Ojeda
2024-07-19 22:11 ` Boqun Feng
2024-07-24 22:01 ` Benno Lossin [this message]
2024-07-20 7:45 ` Dirk Behme
2024-07-17 22:12 ` [RFC PATCH 2/5] doc: rust: safety standard: add examples Benno Lossin
2024-07-19 16:28 ` Daniel Almeida
2024-07-19 16:36 ` Daniel Almeida
2024-07-25 7:47 ` Benno Lossin
2024-08-08 13:10 ` Daniel Almeida
2024-08-08 14:33 ` Benno Lossin
2024-07-17 22:12 ` [RFC PATCH 3/5] doc: rust: safety standard: add guarantees and type invariants Benno Lossin
2024-07-17 22:12 ` [RFC PATCH 4/5] doc: rust: safety standard: add safety requirements Benno Lossin
2024-07-17 22:13 ` [RFC PATCH 5/5] doc: rust: safety standard: add justifications Benno Lossin
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=289d66fb-a698-4d3b-b809-0e3305199a2c@proton.me \
--to=benno.lossin@proton.me \
--cc=a.hindborg@samsung.com \
--cc=alex.gaynor@gmail.com \
--cc=aliceryhl@google.com \
--cc=bjorn3_gh@protonmail.com \
--cc=boqun.feng@gmail.com \
--cc=corbet@lwn.net \
--cc=gary@garyguo.net \
--cc=linux-doc@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=lkmm@lists.linux.dev \
--cc=ojeda@kernel.org \
--cc=rust-for-linux@vger.kernel.org \
--cc=wedsonaf@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).