Yeah. That's why my preferred approach isn't to use Rust for the core TCB. It'd be mostly unsafe anyway, so what's the point? You can write in an all-unsafe language if you want. you can still prove it correct out of band, and seL4 has done that work for you.
Sure, you could just use unsafe Rust and prove it correct with Prusti or something, but why duplicate work?
It is true that hardware, by definition, is a big ball of globally mutable state with no guarantees about concurrency, data types, or anything else. However, one could take the view that it's the role of the OS to restrict & refine that raw power into a set of APIs that are safe, through a set of disciplines, such as reasoning through why an unsafe block might actually be sound.
unsafe means that the compiler can't provide any guarantees about what happens inside the unsafe block. However, it is possible to manually ensure those guarantees.
Thus as a matter of discipline every time an unsafe block is used there's a comment next to it recanting the mantra of safety: This `unsafe` is sound because ... all data types are representable, the region is aligned & initialized with valid data, the lifetime is static, we structurally guarantee only one owner at a time (no concurrency issues)...often times in writing that comment, I'll be like, "oh, right. I didn't actually think about concurrency, we're going to need an Atomic somewhere around this to guarantee that" - and that saves me a really hard-to-find concurrency bug down the road.
So while this is a very manual process, I have found the process of documenting safety to be pretty helpful in improving code quality.
Once you've established safety, then you do get some nice things in your life, like Mutexes, Refcells, Arcs, and the whole collections library to build an OS on top of, which saves us a lot of bugs. It is kind of nice to have a situation where if the code compiles, it often just works.
Because not ALL of it is unsafe. The point of using Rust in the kernel is to write abstractions over the unsafe bits and then utilize safe Rust for all the logic you build on top.
Yep. And that's a good place to be. Keep in mind that the "driver suite" in an seL4 system includes a bunch of things that others would put in the kernel: memory management and swap, networking, filesystems, linking and loading, and so on are all userspace. So, if you want, you still get to differentiate based on interesting low-level things.
Calling seL4 system guts a "driver suite" is like calling rustc "just a preprocessor for LLVM IR". True, but only in the most uselessly pedantic sense.
>It'd be mostly unsafe anyway, so what's the point?
The vast majority of the code that will be tagged "unsafe", will be done so because you're doing the equivalent of FFI, but implemented in hardware. If there was a way to automatically generate the binding from a register map, the only purpose of the unsafe keyword would be to warn you that the effect of the ffi call you are doing is unknown. In other words, the unsafe marker isn't some kind of admission of defeat. It marks the potentially unsafe sections of the code where additional care might be required.
This means you're throwing out the baby with the bathwater.
