6 ms·

Since rust is a true systems programming language, without a mandatory GC, I wonder if there will be any serious attempt to build a kernel entirely in Rust? It

by Hypx 12y ago

Since rust is a true systems programming language, without a mandatory GC, I wonder if there will be any serious attempt to build a kernel entirely in Rust? It certainly sounds possible, and I suspect it would quickly be better than any FOSS kernel currently available, given the fact that Rust is so well designed against bad or sloppy code. Perhaps I'm just talking out of my ass here, but it sounds like a good idea.

imanaccount247 12y ago
There's already a high performance, formally verified, "FLOSS" microkernel: http://sel4.systems/ http://sel4.systems/ As it turns out, very few people are interested in having software that works.
- Hypx 12y ago
  I've only briefly heard of that kernel, and I suspect the same is true for many people at HN. It's also been open sourced pretty recently so maybe it needs more time for people to become aware of it. It may catch on if we give it more time. But even so, it's still mostly written in C and likely have many of the same pitfalls that all kernels written in C will have. I was thinking of a kernel written entirely in Rust, and that would be not only much more reliable, because it would have far fewer segfaults and the like, plus be more immune to the types of highly publicized security flaws lately (Heartbleed, etc.). Of course, the whole OS might have to be written in Rust + memory safe languages. So we might be a ways off from the ideal goal, but clear I was thinking that we can start with a Rust kernel and build on top of that.
  - nullc 12y ago
    SEL4 is provably free of segfaults, without any runtime overhead at all. Unlike Rust. Though it took considerable development time overhead to achieve that. (Moreover, rust itself may have bugs, or there could be bugs in unsafe code in the standard library. The amount of trusted infrastructure is much smaller for SEL4, I suppose if you compile it with compcert, I imagine it's quite small) The worst case latency is also part of the proof for SEL4-- which is a kind of correctness you cannot achieve via rust (even ignoring overhead). There are many elements of program correctness beyond memory safety. The developers of rust generally eschewed concerns about other kinds of correctness. For example, your integer types may overflow and your algorithms could fail to work as a result. SEL4's proofs show the operation of the software match its specifications completely (given some assumptions), it's really far far beyond the memory safety promises of rust.
    - TheHydroImpulse 12y ago
      > there could be bugs in unsafe code in the standard library For any embedded work or kernels, you wouldn't be pulling in the standard library via a `#![no_std]` attribute. But you're right that bugs in the compiler could produce safety issues.
      - nullc 12y ago
        > any embedded work or kernels Perhaps not, but in a kernel you'd have plenty of your own unsafe code. SEL4 doesn't. There are, of course, people thinking about bridging the worlds of formally provable correctness and Rust, e.g. https://github.com/rust-lang/rust/issues/18496 https://github.com/rust-lang/rust/issues/18496 though extraction based is likely to not produce the most elegant or efficient code... and I assume the along-the-side proofs like SEL4 uses would be harder for Rust because the language is more complex than C.
    - Havvy 12y ago
      Rust is able to be almost (unsafe blocks) free of segfaults without runtime overhead. That's the core feature that Rust provides with lifetimes. The Rust compiler can (and does) have bugs, but they get weeded out over time. But so can whatever proof system or proof checker is used on SEL4. As for integer overflow, yeah...that's a hard problem with Rust, and unfortunately, unlikely to be fixed.
      - MichaelGG 12y ago
        Aren't bounds checks and unwinding examples of non-free safety code in Rust?
        kibwen 12y ago
        Unwinding is only potentially unsafe if you're already using `unsafe` blocks. If you're sticking to safe Rust, unwinding can't cause memory unsafety.
        steveklabnik 12y ago
  - tptacek 12y ago
    Hasn't code for L4 been available for, like, a very long time? SEL4 is a variant of L4, and not (IIRC) the best-known. L4 is fantastic, by the way.
  - imanaccount247 12y ago
    >But even so, it's still mostly written in C and likely have many of the same pitfalls that all kernels written in C will have No it won't, that's the point. It is a much stronger guarantee of being without those bugs than using rust would provide. >because it would have far fewer segfaults and the like SEL4 can not segfault, that's the point. It isn't fewer, it is zero. >but clear I was thinking that we can start with a Rust kernel and build on top of that. Yes, and I am saying if people actually wanted that, they could start with a formally verified kernel that already exists and build on top of that. But they don't.
- nullc 12y ago
  Or perhaps very few people are in a position to use a very recently Open Sourced OS that has no file system or network stack, or write these things for it? Presumably you'd want formally verified versions of at least the network device driver... otherwise process isolation might be violated.
  - imanaccount247 12y ago
    Tons of people use L4 for their systems, there's billions of devices running some L4 kernel. The question is why are they not switching to SEL4 given that it provides the same thing they are already using, but faster and proven correct.
- coldtea 12y ago
  I call BS. The reason very few people care is that "works" is not a binary, but obviously a continium -- and people inherently understand diminishing returns... Especially when the "works" they care about is getting shit done, by having access to software (including proprietary), drivers, a community, vendors, etc. The "is formally verified" they could not care less, and rightly so, if their other demands are not satisfied...
  - Animats 12y ago
    That L4 kernel is in the air link CPU of most cell phones.
    - coldtea 12y ago
      Nice that it found a niche there. That's however orthogonal to what I wrote, I think. It's not like it has a software ecosystem, community, drivers, etc, to be adopted over any major OSes as something that "all others being equal" is also "formally verified".
  - imanaccount247 12y ago
    >I call BS. And yet your post can be summarized as "I am not aware of the usage of L4 microkernels". >The "is formally verified" they could not care less, and rightly so, if their other demands are not satisfied... Except their "other demands" are satisfied. It implements L4, just like every other L4 implementation does. It also happens to be the fastest L4 implementation ever tested. So rather than vague dismissive "calling BS", how about you point out the specific fault in SEL4 that causes people to need to use other L4 implementations instead?
    - coldtea 12y ago
      >how about you point out the specific fault in SEL4 that causes people to need to use other L4 implementations instead? I'm talking about people in general, prefaring their mainstream OS of choice over some platform based on L4. Not about L4 users opting for this or that implementation. The parent talked about people in general not caring for software quality, while those L4 users are highly specialized enteprises and businesses making a choice.
acomjean 12y ago
I think Rust would be a interesting (probably safer) language to write an os, embeded code in . I asked the question a few months ago in the "lets write a Kernel" https://news.ycombinator.com/item?id=7588205 https://news.ycombinator.com/item?id=7588205. It takes a while to write a stable OS, because a lot of things that we use in our helpful libs can't be used in Kernel space. I'm thinking of taking some time and trying to help a Rust OS project. http://src3.org/#RHEL6-2.6.32+220.el6/lib/ http://src3.org/#RHEL6-2.6.32+220.el6/lib/ or for example Linux Kernel "string.h" (with fun ifdef) http://src3.org/#RHEL6-2.6.32+220.el6/include/linux/string.h http://src3.org/#RHEL6-2.6.32+220.el6/include/linux/string.h I'm sure reaching Rust 1.0 will speed things up. Someone posted their Rust kernel https://github.com/lexs/rust-os https://github.com/lexs/rust-os
rdc12 12y ago
"I suspect it would quickly be better than any FOSS kernel currently available" It would take a very long time for that to be even possible. The hardest part of writing an OS today is more about the amount of hardware out there to support and getting users. There are a couple of approachs to mitagate this thou. 1) Work well in a niche, this has worked well for L4, QNX, VxWorks etc, but doesn't make the OS very visable to most people. 2) Run on top of an existing virtulisation plaform to minimise the hardware support needed, butby doing that you also reduce the impact of working in a safer language. I guess you could argue that "better" doesn't have to mean relevent to end users/devs, a bit of an ivory tower approach thou. Otherwise you are looking at several years of work

by Hypx 12y ago

imanaccount247 12y ago

There's already a high performance, formally verified, "FLOSS" microkernel: http://sel4.systems/ http://sel4.systems/ As it turns out, very few people are interested in having software that works.

Hypx 12y ago
I've only briefly heard of that kernel, and I suspect the same is true for many people at HN. It's also been open sourced pretty recently so maybe it needs more time for people to become aware of it. It may catch on if we give it more time. But even so, it's still mostly written in C and likely have many of the same pitfalls that all kernels written in C will have. I was thinking of a kernel written entirely in Rust, and that would be not only much more reliable, because it would have far fewer segfaults and the like, plus be more immune to the types of highly publicized security flaws lately (Heartbleed, etc.). Of course, the whole OS might have to be written in Rust + memory safe languages. So we might be a ways off from the ideal goal, but clear I was thinking that we can start with a Rust kernel and build on top of that.
- nullc 12y ago
  SEL4 is provably free of segfaults, without any runtime overhead at all. Unlike Rust. Though it took considerable development time overhead to achieve that. (Moreover, rust itself may have bugs, or there could be bugs in unsafe code in the standard library. The amount of trusted infrastructure is much smaller for SEL4, I suppose if you compile it with compcert, I imagine it's quite small) The worst case latency is also part of the proof for SEL4-- which is a kind of correctness you cannot achieve via rust (even ignoring overhead). There are many elements of program correctness beyond memory safety. The developers of rust generally eschewed concerns about other kinds of correctness. For example, your integer types may overflow and your algorithms could fail to work as a result. SEL4's proofs show the operation of the software match its specifications completely (given some assumptions), it's really far far beyond the memory safety promises of rust.
  - TheHydroImpulse 12y ago
    > there could be bugs in unsafe code in the standard library For any embedded work or kernels, you wouldn't be pulling in the standard library via a `#![no_std]` attribute. But you're right that bugs in the compiler could produce safety issues.
    - nullc 12y ago
      > any embedded work or kernels Perhaps not, but in a kernel you'd have plenty of your own unsafe code. SEL4 doesn't. There are, of course, people thinking about bridging the worlds of formally provable correctness and Rust, e.g. https://github.com/rust-lang/rust/issues/18496 https://github.com/rust-lang/rust/issues/18496 though extraction based is likely to not produce the most elegant or efficient code... and I assume the along-the-side proofs like SEL4 uses would be harder for Rust because the language is more complex than C.
  - Havvy 12y ago
    Rust is able to be almost (unsafe blocks) free of segfaults without runtime overhead. That's the core feature that Rust provides with lifetimes. The Rust compiler can (and does) have bugs, but they get weeded out over time. But so can whatever proof system or proof checker is used on SEL4. As for integer overflow, yeah...that's a hard problem with Rust, and unfortunately, unlikely to be fixed.
    - MichaelGG 12y ago
      Aren't bounds checks and unwinding examples of non-free safety code in Rust?
      - kibwen 12y ago
        Unwinding is only potentially unsafe if you're already using `unsafe` blocks. If you're sticking to safe Rust, unwinding can't cause memory unsafety.
      - steveklabnik 12y ago
- tptacek 12y ago
  Hasn't code for L4 been available for, like, a very long time? SEL4 is a variant of L4, and not (IIRC) the best-known. L4 is fantastic, by the way.
- imanaccount247 12y ago
  >But even so, it's still mostly written in C and likely have many of the same pitfalls that all kernels written in C will have No it won't, that's the point. It is a much stronger guarantee of being without those bugs than using rust would provide. >because it would have far fewer segfaults and the like SEL4 can not segfault, that's the point. It isn't fewer, it is zero. >but clear I was thinking that we can start with a Rust kernel and build on top of that. Yes, and I am saying if people actually wanted that, they could start with a formally verified kernel that already exists and build on top of that. But they don't.
nullc 12y ago
Or perhaps very few people are in a position to use a very recently Open Sourced OS that has no file system or network stack, or write these things for it? Presumably you'd want formally verified versions of at least the network device driver... otherwise process isolation might be violated.
- imanaccount247 12y ago
  Tons of people use L4 for their systems, there's billions of devices running some L4 kernel. The question is why are they not switching to SEL4 given that it provides the same thing they are already using, but faster and proven correct.
coldtea 12y ago
I call BS. The reason very few people care is that "works" is not a binary, but obviously a continium -- and people inherently understand diminishing returns... Especially when the "works" they care about is getting shit done, by having access to software (including proprietary), drivers, a community, vendors, etc. The "is formally verified" they could not care less, and rightly so, if their other demands are not satisfied...
- Animats 12y ago
  That L4 kernel is in the air link CPU of most cell phones.
  - coldtea 12y ago
    Nice that it found a niche there. That's however orthogonal to what I wrote, I think. It's not like it has a software ecosystem, community, drivers, etc, to be adopted over any major OSes as something that "all others being equal" is also "formally verified".
- imanaccount247 12y ago
  >I call BS. And yet your post can be summarized as "I am not aware of the usage of L4 microkernels". >The "is formally verified" they could not care less, and rightly so, if their other demands are not satisfied... Except their "other demands" are satisfied. It implements L4, just like every other L4 implementation does. It also happens to be the fastest L4 implementation ever tested. So rather than vague dismissive "calling BS", how about you point out the specific fault in SEL4 that causes people to need to use other L4 implementations instead?
  - coldtea 12y ago
    >how about you point out the specific fault in SEL4 that causes people to need to use other L4 implementations instead? I'm talking about people in general, prefaring their mainstream OS of choice over some platform based on L4. Not about L4 users opting for this or that implementation. The parent talked about people in general not caring for software quality, while those L4 users are highly specialized enteprises and businesses making a choice.

acomjean 12y ago

I think Rust would be a interesting (probably safer) language to write an os, embeded code in . I asked the question a few months ago in the "lets write a Kernel" https://news.ycombinator.com/item?id=7588205 https://news.ycombinator.com/item?id=7588205. It takes a while to write a stable OS, because a lot of things that we use in our helpful libs can't be used in Kernel space. I'm thinking of taking some time and trying to help a Rust OS project. http://src3.org/#RHEL6-2.6.32+220.el6/lib/ http://src3.org/#RHEL6-2.6.32+220.el6/lib/ or for example Linux Kernel "string.h" (with fun ifdef) http://src3.org/#RHEL6-2.6.32+220.el6/include/linux/string.h http://src3.org/#RHEL6-2.6.32+220.el6/include/linux/string.h I'm sure reaching Rust 1.0 will speed things up. Someone posted their Rust kernel https://github.com/lexs/rust-os https://github.com/lexs/rust-os

rdc12 12y ago

"I suspect it would quickly be better than any FOSS kernel currently available" It would take a very long time for that to be even possible. The hardest part of writing an OS today is more about the amount of hardware out there to support and getting users. There are a couple of approachs to mitagate this thou. 1) Work well in a niche, this has worked well for L4, QNX, VxWorks etc, but doesn't make the OS very visable to most people. 2) Run on top of an existing virtulisation plaform to minimise the hardware support needed, butby doing that you also reduce the impact of working in a safer language. I guess you could argue that "better" doesn't have to mean relevent to end users/devs, a bit of an ivory tower approach thou. Otherwise you are looking at several years of work