Comment by mimd
3 days ago
Isn't this a bait and switch, that all the c kernel devs were complaining about? That it wouldn't be just drivers but also all new kernel code? The lack of candor over the goal of R4L and downplaying of other potential solutions should give any maintainer (including potential rust ones) pause.
Anyway, why just stop at rust? If we really care about safety, lets drop the act and go make everyone do formal methods. Frama-C is at least C, has a richer contract language, has heavy static analysis tools before having to go to proofs, is much more proven, and the list goes on. Or, why not add Spark to the codebase if we are okay with mixing langs in the codebase? Its very safe.
Frama-C doesn't actually prove memory safety and has a huge proof hole due to the nature of UB. It gives weaker guarantees than Rust in many cases. It's also far more of a pain to write. The Frama-C folks have been using the kernel as a testbed for years and contributing small patches back. The analysis just doesn't scale well enough to involve other people.
Spark doesn't have an active community willing to support its integration into the kernel and has actually been taking inspiration from Rust for access types. If you want to rustle up a community, go ahead I guess?
No, it can track pointer bounds and validity across functions. It also targets identifying cases of UB via eva. Both rust and frama-C rely on assertions to low level memory functions. Rust has the same gaping UB hole in unsafe that can cross into safe.
If we are talking about more than memory, such as what greg is talking about in encoding operational properties then no, rust is far behind both frama-C, Spark, and tons of others. They can prove functional correctness. Or do you think miri, kani, cruesot, and the rest of the FM tools for Rust are superfluous?
My mocking was that that the kernel devs have had options for years and have ignored them out of dislike (ada and spark) or lack of effort (frama-C). That other options provide better solutions to some of their intrests. And that this is more a project exercise in getting new kernel blood than technical merits.
For it to be bait and switch someone should've said "Rust will forever be only for drivers". Has anyone from the Linux leadership or R4L people done that? To my knowledge it has always been "for now".
"But for new code / drivers..." encompasses more than just "drivers" and refers to all new code. I doubt it's a mistake either due to the way the rest of the email is written. And Greg said "no one sane ever thought that (force anyone to learn rust)" just 5 months ago (https://lkml.org/lkml/2024/8/29/312). But he is now telling his C devs they will need to learn and code rust to make new code in the kernel.
> But he is now telling his C devs they will need to learn and code rust to make new code in the kernel.
I don't think this is accurate, Rust is still totally optional. Also, the Rust folks are supposed to fix Rust code whenever it breaks due to changes on the C side. If they fail to do this, the newly-broken Rust code is supposed to be excluded from the build - up to and including not building any Rust at all.
1 reply →
I'm no kernel dev, but I assume that DMA bindings (what this round of drama was originally all about) fall squarely into "stuff that drivers obviously need".