rust-for-linux.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
From: Miguel Ojeda <miguel.ojeda.sandonis@gmail.com>
To: "Paul E. McKenney" <paulmck@kernel.org>
Cc: Gary Guo <gary@garyguo.net>, Marco Elver <elver@google.com>,
	Boqun Feng <boqun.feng@gmail.com>,
	kasan-dev <kasan-dev@googlegroups.com>,
	rust-for-linux <rust-for-linux@vger.kernel.org>
Subject: Re: Can the Kernel Concurrency Sanitizer Own Rust Code?
Date: Sat, 9 Oct 2021 18:31:06 +0200	[thread overview]
Message-ID: <CANiq72nGX6bgwDuVMX3nGUfs_UQB1ikOBHE-Q74nEaJ2Stx_2w@mail.gmail.com> (raw)
In-Reply-To: <20211009000838.GV880162@paulmck-ThinkPad-P17-Gen-1>

On Sat, Oct 9, 2021 at 2:08 AM Paul E. McKenney <paulmck@kernel.org> wrote:
>
> If it complies with requirements, is it really a bug?  And while we are
> at it, I need to make an insignificant change to those requirements.  ;-)
>
> Hey, they have been using C for quite some time!  In at least some cases,
> with the assistance of formal verification tooling that takes the C code
> as input (cbmc, for example).

Indeed, for assurance levels that require that kind of verification,
there is a need for that kind of tooling for Rust.

> And how many of those boxes are ticked by the usual open-source processes?
> Nicholas Mc Guire talks about this from time to time.
>
> One challenge for use of Rust in my previous work with similar standards
> would be repeatability.  It would be necessary to carefully identify and
> archive the Rust compiler.

This may be open for interpretation, but I am aware of safety-critical
projects having used open-source compilers (e.g. GCC) and passing
certification (in at least some assurance levels).

Of course, in any case, companies looking to certify a system will not
jump right away into Rust because there are many other things to
consider: previous experience certifying, existence of tools, etc. and
all their implications in cost.

> So Rust is an attempt to let the compiler writers have their UB while
> inflicting at least somewhat less inconvenience on those of us poor
> fools using the resulting compilers?  If so, I predict that the compiler

You can see Rust as a way to "tame" C and C++, yes ;D

More seriously, users of Rust also take advantage of it, not just
compiler writers. For instance, unsafe code is used all the time to
implement all sorts of data structures in a performant way, while
still giving callers a safe interface.

There is also the angle about using `unsafe` even in "normal code" as
an escape hatch when you really need the performance (e.g. to avoid a
runtime check you can show it always holds).

The key idea is to encapsulate and minimize all that, and keep most of
the code (e.g. drivers) within the safe subset while still taking
advantage of the performance potentially-UB operations give us.

> writers will work hard to exploit additional UB until such time as Rust
> is at least as unsound as the C language currently is.

Rust has defined both the language and the compiler frontend so far,
thus it is also its own compiler writer here (ignoring here
alternative compilers which are very welcome). So it is in a good
position to argue with itself about what should be UB ;)

Now, of course, the Rust compiler writers have to ensure to abide by
LLVM's UB semantics when they lower code (and similarly for
alternative backends). But this is a different layer of UB, one that
frontend writers are responsible for, not the Rust one, which is the
one we care about for writing unsafe code.

Nevertheless, in the layer we care about, it would be nice to see the
unsafe Rust semantics defined as precisely as possible -- and there is
work to do there (as well as an opportunity).

(In any case, to be clear, this all is about unsafe Rust -- for safe
Rust, it has to show no UB modulo bugs in optimizers, libraries,
hardware, etc. -- see my other email about this. Furthermore, even if
there comes a time Rust has an standard, the safe Rust subset should
still not allow any UB).

> Sorry, but you did leave yourself wide open for that one!!!  ;-)

No worries :) I appreciate that you raise all these points, and I hope
it clarifies things for others with the same questions.

Cheers,
Miguel

  reply	other threads:[~2021-10-09 16:31 UTC|newest]

Thread overview: 39+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2021-10-07 13:01 Can the Kernel Concurrency Sanitizer Own Rust Code? Marco Elver
2021-10-07 14:15 ` Boqun Feng
2021-10-07 14:22   ` Marco Elver
2021-10-07 14:43     ` Boqun Feng
2021-10-07 17:44     ` Miguel Ojeda
2021-10-07 18:50       ` Paul E. McKenney
2021-10-07 21:42         ` Gary Guo
2021-10-07 22:30           ` Paul E. McKenney
2021-10-07 23:06             ` Gary Guo
2021-10-07 23:42               ` Paul E. McKenney
2021-10-07 23:59                 ` Gary Guo
2021-10-08  0:27                   ` comex
2021-10-08 17:40                   ` Paul E. McKenney
2021-10-08 21:32                     ` Miguel Ojeda
2021-10-09  0:08                       ` Paul E. McKenney
2021-10-09 16:31                         ` Miguel Ojeda [this message]
2021-10-09 23:59                           ` Paul E. McKenney
2021-10-11  1:24                             ` Miguel Ojeda
2021-10-11 19:01                               ` Paul E. McKenney
2021-10-13 11:48                                 ` Miguel Ojeda
2021-10-13 16:07                                   ` Paul E. McKenney
2021-10-13 17:50                                     ` Wedson Almeida Filho
2021-10-14  3:35                                       ` Paul E. McKenney
2021-10-14  8:03                                         ` Wedson Almeida Filho
2021-10-14 19:43                                           ` Paul E. McKenney
2021-10-15 15:06                                             ` Wedson Almeida Filho
2021-10-15 23:29                                               ` Paul E. McKenney
2021-10-08 19:53                 ` Miguel Ojeda
2021-10-08 23:57                   ` Paul E. McKenney
2021-10-09 16:30                     ` Miguel Ojeda
2021-10-09 23:48                       ` Paul E. McKenney
2021-10-11  0:59                         ` Miguel Ojeda
2021-10-11 18:52                           ` Paul E. McKenney
2021-10-13 11:47                             ` Miguel Ojeda
2021-10-13 23:29                               ` Paul E. McKenney
2021-10-22 19:17                                 ` Miguel Ojeda
2021-10-22 20:34                                   ` Paul E. McKenney
2021-10-07 16:30 ` Paul E. McKenney
2021-10-07 16:35   ` Marco Elver

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=CANiq72nGX6bgwDuVMX3nGUfs_UQB1ikOBHE-Q74nEaJ2Stx_2w@mail.gmail.com \
    --to=miguel.ojeda.sandonis@gmail.com \
    --cc=boqun.feng@gmail.com \
    --cc=elver@google.com \
    --cc=gary@garyguo.net \
    --cc=kasan-dev@googlegroups.com \
    --cc=paulmck@kernel.org \
    --cc=rust-for-linux@vger.kernel.org \
    /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).