Hacker News Reader

Comment by nine_k | Hacker News Reader

C and C++ are the only languages used in widely deployed production OS kernels, so Fuchsia decides to only use them in its kernel, too.

Nobody seem to want to stand out and use e.g. Rust in the kernel, so the situation is perpetuated. (How old was C again when it was used to write the Unix kernel? Apparently Google's stakes here are higher.)

View on HN

I think that it's more that they already have a kernel, and their focus is moving as much as possible outside the kernel rather than adding to it.

And, FWIW, I can see a point where they have a kernel written in C or C++ that's formally verified (like sel4), at which point, what's the point of rewriting it in Rust? sel4's semantics are stronger than what Rust gives you out of the box.

I say this as someone who's written a handful of Rust kernels, and is quite bullish on Rust adoption.

Neat, I didn't know about seL4. Can you point me to how they define the proof for it?

They've done a really good job documenting it in their papers and online docs, but the general flow is to verify equivalence of the generated binary and the formal specification, then to prove properties like memory safety of the formal spec.

I'd start here if you want to learn more: https://sel4.systems/Info/FAQ/proof.pml

Let me know if you have any other questions.

FOSDEM speach video [1] about the status of seL4, I really enjoyed.

[1]: https://fosdem.org/2020/schedule/event/uk_sel4/

> what's the point of rewriting it in Rust

The fact that you don't have to write C and also that you can have different API semantics. E.g. you can pass user space code (say callbacks) to the kernel while maintaining safety.

I don't see a world where they allow "run this user code as ring 0".

I do. If it's a callback and all arguments are passed in, it's fine.

It can literally take control of the machine. Even if it's written in Rust, there's no "this binary used an unsafe block" on binaries. If they're signing and proving everything, then what's the purpose of sticking that code in user space to begin with?

There does exist a precedent in tha mainframe world of trusted compilers and mechanisms of verifying that a piece of code was produced by the blessed compiler.

I guess the embedded version of this would have to be an offline compiler & code signing based system, and the language would need to be much more sandboxy than Rust.

I know maybe you are writing a driver or smth.

Bad idea in the wake of Spectre and meltdown. You want user code in a different address space for those reasons these days.

Unless you mean more like using the user callback in the same way, say, a posix signal handler works, or Microsoft's SEH or APCs, then I would say it's already possible with a C ABI, citing those things as examples.

IIRC sel4 was initially specified in Haskell, formally verified, then formally translated to C.

> While the Haskell prototype is an executable model and implementation of the final design, it is not the final production kernel. We manually re-implement the model in the C programming language for several reasons. Firstly, the Haskell runtime is a significant body of code (much bigger than our kernel) which would be hard to verify for correctness. Secondly, the Haskell runtime relies on garbage collection which is unsuitable for real-time environments. Incidentally, the same arguments apply to other systems based on type-safe languages, such as SPIN [7] and Singularity [23]. Additionally, using C enables optimisation of the low-level implementation for performance. While an automated translation from Haskell to C would have simplified verification, we would have lost most opportunities to micro-optimise the kernel, which is required for adequate microkernel performance.

https://www.sigops.org/s/conferences/sosp/2009/papers/klein-...

> C and C++ are the only languages used in widely deployed production OS kernels, so Fuchsia decides to only use them in its kernel, too.

Frankly - who didn't see this coming. The widely touted network stack written in Go will be rewritten in something else.

> Nobody seem to want to stand out and use e.g. Rust in the kernel, so the situation is perpetuated

Redox does, but it's still early days there apparently. I tried to boot it in VirtualBox a few minutes ago, following some instructions on StackExchange[1] but it didn't boot.

> How old was C again when it was used to write the Unix kernel?

Very young, as C was developed between 72-73[2], and the first rewrite of UNIX in C from PDP assembly happened in 1973 for V4, although it wasn't really _portably_ rewritten until 1978[3]). The C rewrite was the first version to support multi-programming; before that it was single-tasking.

(maybe you know all this, but I post the info to clarify for other readers who might not, and to underscore your point).

Also don't forget that UNIX source was reasonably available in those days, and both C and UNIX developed alongside the much simpler hardware of the day, and evolved with them. Hitting modern hardware targets, trying to provide modern OS features out of the gate, and using a newly emerging language seems to be a feat which is an order of magnitude larger IMHO.

[1] https://unix.stackexchange.com/questions/463192/install-redo...

[2] https://en.wikipedia.org/wiki/C_(programming_language)

[3] https://en.wikipedia.org/wiki/Unix#History

> Redox does, but it's still early days there apparently. I tried to boot it in VirtualBox a few minutes ago, following some instructions on StackExchange[1] but it didn't boot.

Worth giving it another go. I've been playing around with it in QEMU lately, and it even booted on my laptop (but I had no working input since it seems USB HID isn't implemented). It's an impressive project.

Remember the kernel here is pretty small. A lot of stuff that's built-in to the kernel in e.g. Linux is implemented outside the kernel in Fuchsia, and a lot of that is implemented in Rust.

Might have more to do with them starting with a stable microkernel as a base. They picked LK.

Why aren't you writing a kernel in Rust?

Mostly because I'm not qualified to write serious close-to-metal code (I majored in embedded systems 25 years ago, but gravitated up the stack), and don't have enough time for that as a hobby.

The day is only 25 hours, or maybe even less.

Reply on news.ycombinator.com