Message-Id: <D7ZDF8NZGPS3.3QBMAVC1NTUDM@maslowski.xyz>
Date: Sun, 23 Feb 2025 00:42:06 +0100
From: Piotr Masłowski <piotr@...lowski.xyz>
To: "Martin Uecker" <uecker@...raz.at>
Cc: "Greg KH" <gregkh@...uxfoundation.org>, "Boqun Feng"
 <boqun.feng@...il.com>, "H. Peter Anvin" <hpa@...or.com>, "Miguel Ojeda"
 <miguel.ojeda.sandonis@...il.com>, "Christoph Hellwig" <hch@...radead.org>,
 "rust-for-linux" <rust-for-linux@...r.kernel.org>, "Linus Torvalds"
 <torvalds@...ux-foundation.org>, "David Airlie" <airlied@...il.com>,
 <linux-kernel@...r.kernel.org>, <ksummit@...ts.linux.dev>
Subject: Re: Rust kernel policy

On Thu Feb 20, 2025 at 9:57 AM CET, Martin Uecker wrote:
>
> For example, there is an effort to remove cases of UB.  There are about
> 87 cases of UB in the core language (exlcuding preprocessor and library)
> as of C23, and we have removed 17 already for C2Y (accepted by WG14 into
> the working draft) and we have concrete propsoals for 12 more.  This
> currently focusses on low-hanging fruits, and I hope we get most of the
> simple cases removed this year to be able to focus on the harder issues.
>
> In particulary, I have a relatively concrete plan to have a memory safe
> mode for C that can be toggled for some region of code and would make
> sure there is no UB or memory safety issues left (I am experimenting with
> this in the GCC FE).  So the idea is that one could start to activate this
> for certain critical regions of code to make sure there is no signed
> integer overflow or OOB access in it.   This is still in early stages, but
> seems promising. Temporal memory safety is harder and it is less clear
> how to do this ergonomically, but Rust shows that this can be done.
>

I'm sure you already know this, but the idea of safety in Rust isn't
just about making elementary language constructs safe. Rather, it is
primarily about designing types and code in such a way one can't "use
them wrong". As far as I understand it, anything that can blow up from
misuse (i.e. violate invariants or otherwise cause some internal state
corruption) should be marked `unsafe`, even if it does not relate to
memory safety and even if the consequences are fully defined.


In programming language theory there's this concept of total vs partial
functions. While the strict mathematical definition is simply concerned
with all possible inputs being assigned some output value, in practice
it's pretty useless unless you also make the said output meaningful.
This is quite abstract, so here's an (extremely cliché) example:

Let's say we're working with key-value maps `Dict : Type×Type -> Type`.
A naive way to look up a value behind some key would be
`get : Dict<k,v> × k -> v`. But what should the result be when a given
key isn't there? Well, you can change the return type to clearly reflect
that this is a possibility: `get : Dict<k,v> × k -> Optional<v>`. On the
other hand, if you have some special value `null : a` (for any `a`), you
can technically make the first way total as well. But this is precisely
why it's not really useful – it's some special case you need to keep in
mind and be careful to always handle. As someone here has said already,
besides undefined behavior we also need to avoid "unexpected behavior".

(Another way to make such function total is to show a given key will
always be there. You can achieve it by requiring a proof of this in
order to call the function:
`get : (dict : Dict<k,v>) × (key : k) × IsElem<dict,key> -> v`.)


Overall, making a codebase safe in this sense requires an entirely
different approach to writing code and not just some annotations
(like some other people here seem to suggest).


And while I'm at it, let me also point out that the concept of ownership
is really not about memory safety. Memory allocations are just the most
obvious use case for it. One could say that it is rather about something
like "resource safety". But instead of trying (and miserably failing) to
explain it, I'll link to this excellent blog post which talks about how
it works under the hood and what awesome things one can achieve with it:
<https://borretti.me/article/introducing-austral#linear>

Oh, and once again: I am sure you knew all of this. It's just that a lot
of people reading these threads think adding a few annotations here and
there will be enough to achieve a similar level of safety | robustness
as what newly-designed languages can offer.

Best regards,
Piotr Masłowski

Powered by blists - more mailing lists