[geofft]

As one of the developers of this patchset, here is my simple answer: try it. I'd love to see it.

I know Rust; I don't know Frama-C or Idris or Ada. What little I know of Ada indicates that it doesn't actually solve the problem because it doesn't have safe dynamic memory allocation. Ada advocates have told me I'm wrong and there's some new thing (inspired by Rust) that does this. Maybe! I'm not sure there's any benefit to the world in arguing it; someone skilled in Ada should just write something and show how it would actually work.

Write a kernel module with any of those techniques, send in a patch, and see what people say. Any effective means of making the kernel less buggy is great. It doesn't have to be Rust.

I claim that Rust is effective because, well, those patches are there, and frankly I haven't been doing any work for this project in almost a year and we're getting so many enthusiastic contributors. So, apparently, a lot of other people also know or are willing to learn Rust. Maybe it's actually better than the alternatives you mention; maybe it just has better documentation. I don't know. I'm not claiming Rust is perfect, just that it's empirically likely to solve the problem.

If you can get together a community of folks who can do any of these other approaches, that would be fantastic. Try it!

[pjmlp]

> What little I know of Ada indicates that it doesn't actually solve the problem because it doesn't have safe dynamic memory allocation.

It does, just not the way most are used to it.

Surely if one wants to code like malloc()/free(), free() is unsafe in Ada and requires the Ada version of unsafe {}

However many type constructions in Ada do dynamic allocation by themselves, including on the stack.

If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path.

Ada also has RAII since Ada95 (controlled types), and yes SPARK formal specification now allows for ownership rules.

[tialaramex]

> If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path.

So, since we're talking about the Linux kernel, that's a red flag straight away. Notice a whole section of this new LKML post is about their implementation of Rust's alloc crate? Linus doesn't want useless exceptions here and has previously objected on that basis.

Meanwhile... Over in the C++ world they have this same behaviour. For them these exception handlers are a fiction, in reality popular standard libraries (never mind everything else you're using) will blow up in low memory and it's game over. Maybe Ada does a lot better. Maybe.

[pjmlp]

Linux kernel doesn't have clearance for high integrity computing, or being in control of machines responsible for human life's, Ada does.

Ada also has no exception allowed profiles and other mechanisms.

HN is not the place to hold a lecture on Ada features.

It is not a maybe, rather lack of knowledge.

[short_sells_poo]

You seem to be arguing as if this effort should have gone to Ada instead. So go ahead and do it. There's a group of people who are trying to get kernel support for Rust. This is not a statement about Rust being superior to Ada or Ada's (in)suitability for the same job. It's only a statement that this group of people likes rust for it's safety features. I'm sure they are all aware that there are other, even safer languages, but these people like Rust.

We can lead academic discussions about which language is safer/better/leaner/whatever-er, but the fact is that Rust has a larger and growing mindshare so this effort is unsurprising. For Ada, the solution isn't to try and prove to anonymous forum goers it would've been better choice if only people recognized the fact. The solution is to mobilize the Ada community to put the same amount of effort into the publicity and marketing (yes, the bad M word) of their ecosystem.

Ada clearly lives on in many safety critical systems, but judging by the admittedly biased topic frequency on HN and other technical sites, it has a tiny community who mostly keep to themselves. That's fine, but then don't be surprised when it's Hip Language X that gets the headlines and these sort of efforts.

[pjmlp]

That effort has been happening for production code in high integrity systems since Ada was released to the world in 1983.

My only point is how many in the Rust community advocate as if Rust would be the first language having features, that actually were already in Ada for the past decades.

As for Ada on Linux, naturally Linus would never go along it.

A C kernel guy liking a language with Pascal syntax, a community that worships a paper that hasn't been true in the Pascal world since early 80's, not even at gunpoint.

If you want to see a use case where Ada was chosen against Rust, check NVidia's project for self driving vehicles firmware.

[short_sells_poo]

I appreciate what you are saying, but it is again just repeating why Ada is better than Rust. I posit that's irrelevant to this discussion. Rust is a safety centered language that seems to have champions and a growing community around it. Can we not just be happy that finally a safety conscious language has a following? If you are convinced Ada is better, nobody is stopping you from being the champion and building the Ada ecosystem. Right now, Ada is for all intents and purposes invisible both in terms of libraries, mindshare and hype.

[grumblenum]

>the fact is that Rust has a larger and growing mindshare so this effort is unsurprising.

I think that is a false perception created by the dev-blogging community. Based on GitHub activity (https://madnight.github.io/githut/#/pull_requests/2021/2) Rust usage is declining (absolute numbers show little growth). Based on developer surveys (https://www.jetbrains.com/lp/devecosystem-2020/) very few people use rust outside of hobby development.

I think the concern is that the core argument that "I think Linux should adopt rust for safety" is a bit dishonest, given that there are a large number of well-vetted alternatives. "I think Linux should adopt rust because I like rust for social reasons" would probably be more correct. That Google staff seem to think rust is good for the Linux kernel but not, say, Zircon, would be surprising if those same people actually believed that any legal rust program is safe and inherently trustworthy. "Embrace, extend, extinguish" wasn't that long ago.

[short_sells_poo]

I don't use rust so I have no money in this game, but based on the two links you provided, Rust ranks the highest among the "safety minded" languages. It ranks the same level as Ruby, Swift, Matlab or R in the Jetbrains ranking. That's incredible for such a new language.

I mean, neither Ada nor Zircon are even on the lists, so in terms of mindshare, they are clearly blown out of the water by Rust (from the evidence you provide). To discount Rust based on usage when the alternatives being suggested don't even make the rankings is also a bit dishonest.

In fact, the argument "I think Linux should adopt rust for safety" makes perfect sense. Here's finally a safety conscious language that seems to be embraced by a larger community, and even the big tech players. Instead we get people suggesting arcane alternatives that may be technically better, but have a snowball's chance in hell to become commonplace any time soon.

[dexterlemmer]

Rust was considered for Zircon. The only reason it wasn't chosen was that at the time Rust wasn't yet sufficiently mature for embedded. And it really wasn't.

In the meantime, Google makes extensive use of Rust in new components of both Fuchsia and Android and even rewrites some legacy components where it makes sense.

[geofft]

Right. It is a lack of knowledge, and I know I've seen you argue that Ada has facilities for this before, and I don't know enough Ada to answer that one way or another.

I think you and 'grumblenum should team up and write a working kernel module in Ada/Spark and then we can have a fruitful discussion about it, instead of just theorizing about whether it could be done. I'm interested in seeing the problems solved, and I'm indifferent to technology. If you think Ada/Spark can solve them, that would be awesome!

(Editing to reply to a small claim in another subthread, "Linus would never go for it" - we believed the same thing when we started. We were originally thinking that we'd pitch this directly at Linux distros shipping out-of-tree modules that they didn't want to keep having to push security updates for. https://github.com/fishinabarrel/linux-kernel-module-rust was out-of-tree and we tried to keep compatibility with kernels 4.4 onwards. But it turned out Linus isn't opposed to it.)

[pjmlp]

Why should we waste time doing stuff already exists?

https://www.adacore.com/academia/projects/muen-project

https://www.adacore.com/company/partners/nvidia

https://genode.org/about/road-map

https://www.ptc.com/-/media/Files/PDFs/Developer-Tools/apexa... (ApexAda Exec)

https://www.ghs.com/products/safety_critical/integrity_178_e...

https://www.windriver.com/products/helix (Wind River Helix Bare Metal partitions)

[geofft]

Fascinatingly, the more you post, the less convinced I am that Ada could ever be suitable for this use case. I looked at all these links to see what's been done:

Muen: If I am reading the allocator in https://git.codelabs.ch/?p=muen.git;a=tree;f=tools/liballoc/... correctly, it simply has no deallocator function at all. It does have a "Clear" function, but there's no sign that it has any ability to statically check that calling it is safe. That is exactly what we're talking about.

Nvidia: No public source code, and it's not obvious what actually exists here, beyond a compiler to Nvidia hardware.

Genode: This project is mostly written in C++. There is a very tiny, experimental amount of Ada in it (< 400 lines of code). There's certainly nothing that speaks to the questions discussed in this thread (safe dynamic allocation/deallocation, security, etc.).

ApexAda: This is a marketing brochure. Also this marketing brochure talks about "significant deployments in satellite communications, avionics, weapons control systems, and a myriad of other mil/aero applications," all of which - as discussed elsewhere in these comment - are applications that neither need nor want dynamic allocation (and are generally not exposed to deeply-structured untrusted input, for that matter).

Green Hills: This looks interesting - there's a POSIX filesystem and a UDP socket implementation, both of which (probably) want dynamic memory allocation. That is, at last, an application that needs dynamic allocation. Is it actually written in Ada? I see that the RTOS itself supports development in C, C++, and Ada, and they claim to offer a BSD socket implementation, so they at least have C bindings. I don't see any claim about what language it's written in, and Green Hills seems to do a lot of C work (see e.g. https://www.ghs.com/products/micro_velosity.html). If it's in Ada, then I think this gets the closest to what would be needed for the Linux kernel - do you know how their filesystem and socket implementations handle dynamic allocation? (I'll also note that they lost their certification many years ago, so if the answer is that they have safe code because they spent a whole lot of time perfecting a single version of an OS, then that's a very different problem space from Linux, which is constantly changing.)

Wind River: This is a marketing page without much detail, but it looks like it's a hypervisor to run general-purpose OSes on top of, not a general-purpose OS itself, which means it probably does not need dynamic memory allocation, or that if it does, the safety of deallocation can be verified by hand.

---

No Ada developer has done what's being done in this patchset, and it's pretty insulting to the folks putting in the work to claim it's been done and Gish-gallop a bunch of random links and expect people to put in the time to figure out what exactly you're claiming already exists. Everyone knows it's possible to write code in Ada. Nobody is asking if Ada can be used for completely unrelated purposes. You may as well link to GORILLAS.BAS and ask why the Linux kernel isn't using QBasic, a memory-safe language if you use the subset without PEEK and POKE.

Write - or point to - a kernel driver for a UNIX-like operating system written in Ada, that safely handles dynamic allocation. That's the clear bright-line goal. If you think that's not the right goal, say why.

[grumblenum]

>I'm interested in seeing the problems solved, and I'm indifferent to technology.

I think the first problem is some kind of language specification. That it's not possible to know what behavior one should expect from rustc means that it isn't a solution. It's another problem. You should check out Ken Thompson's great speech on why this is an issue. https://www.cs.cmu.edu/~rdriley/487/papers/Thompson_1984_Ref...

Or do you think it's wrong to regard unauditable enhancements to free software paid for by Google with suspicion?

[geofft]

Ken Thompson's speech was made two years before the first draft specification of C was published, so I don't understand how it is connected to language specifications.

Here's a way to address the issue he brings up in that speech that does not involve language specifications: https://dwheeler.com/trusting-trust/

[grumblenum]

As one of the developers of this patchset, can you comment on how these contributions will be licensed? Can you also comment on how a third party can verify or audit the output of a compiler without a specification?

>just that it's empirically likely to solve the problem.

Can you comment on what empirical evidence you based this statement on?

[geofft]

> As one of the developers of this patchset, can you comment on how these contributions will be licensed?

Yes, I can comment on this. The licensing is the same as any other submission to the Linux kernel. See https://www.kernel.org/doc/html/latest/process/license-rules... for Linux kernel licensing in general and also https://www.kernel.org/doc/html/latest/process/submitting-pa... for the meaning of the Signed-off-by lines.

> Can you also comment on how a third party can verify or audit the output of a compiler without a specification?

I imagine it's pretty similar to how you verify or audit the output of a compiler with a specification. If you can show me an example of the sort of verification or audit you envision, I can perhaps give you a more helpful comment.

We do not make any claims about verified or audited compiler outputs or compliance with specifications, and to the best of my knowledge, the Linux kernel does not currently verify or audit any compiler outputs, so I'm not sure I follow why I would be particularly qualified to comment on it, but I could maybe point you at some interesting research.

> Can you comment on what empirical evidence you based this statement on?

Yes, I did comment on this, in the paragraph you quoted. If you'd like me to expand on something can you clarify?

[grumblenum]

>I imagine it's pretty similar to how you verify or audit the output of a compiler with a specification.

I must be missing the humor here. You can test against a specification to verify implementation. Testing an implementation against itself is meaningless. I would think that this is obvious. Also I don't typically use the word "empirical" to indicate purely qualitative assessments or intuition. You also provided a dead link.

[geofft]

Fixed the link, thanks.

There's no attempt at humor here - I'm just trying to get you to explain what, precisely, you mean by "test against a specification to verify implementation" so that we're in agreement on terms.

When I hear "test against a specification" and "verify implementation," I think about things like CompCert. But the Linux kernel does not use CompCert, it uses GCC or Clang. To the best of my knowledge, neither is tested against a specification and neither has a verified implementation.

Actually, when we first started discussing mainlining this, we had a bit of discussion about whether it was safe to allow rustc-compiled Rust code to link against GCC-compled C code. The specific worry was potential compiler bugs, of which the kernel has historically run into many. We eventually decided the risk was low, but the kernel has gone through periods where it insisted you use the exact same compiler for the kernel and for modules because of bugs. Those bugs have gone away through the normal human process of writing better code, not through formal verification. And when they existed, the kernel's response was not to reject those compilers, it was to work around the bugs.

Also, CompCert does not test against the C standard, which is written in English prose. It tests against the CompCert developers' attempt to re-express the C standard in terms of machine-checkable theorems. The C standard is confusing even to human readers, so it would be misleading to say that CompCert has verified their compiler against the standard as published by the standards committee. (Hence my claim that they're similar; you can verify a compiler of any language provided you write your own machine-checkable statements about what you expect it to do, and you still need other humans to read those theorems and convince themselves that they're the right ones.)

For those reasons, I'm trying to understand what your question is in a precise manner. Are you asking about things like CompCert? Because if so, I don't follow the relevance to our work, though again, I'm happy to point you at interesting research.

[grumblenum]

Just FYI, I didn’t read any of that wall, but it did make me laugh that you wrote it. You should go tell your rest friends to check the slack and down vote.