4 ms·

I suspect one of the "toy" operating systems being written in Rust (or some other safe/modern systems language) will end up being the Linux of 20 years from now

I suspect one of the "toy" operating systems being written in Rust (or some other safe/modern systems language) will end up being the Linux of 20 years from now. So, it seems relevant to see how this particular holy war plays out (once again). Linus nixed the idea of a microkernel for the dominant operating system for building the web while it was still a toy...I don't know that he was wrong to do so, but it might be interesting to try a different path for the next generation.

cvwright 11y ago
Wouldn't that be cool? Another neat idea would be to build on an existing microkernel like seL4, but write the userspace -- all the drivers, memory manager, filesystems, etc -- in Rust. The NICTA team already has proofs of correctness for the microkernel itself, so why reinvent the wheel? But at the same time, those proofs were super expensive and difficult to make. It would be awesome if we could get a reliable userland more easily by using a better language. I wonder what it would take to get Rust compiling for seL4?
- nanolith 11y ago
  Not much, really. The main thing needed is to port the language runtime to seL4. This should be a relatively small effort, and a great project to both learn some of the underbelly of Rust's ABI and seL4.
  - cmrx64 11y ago
    Already done :)
    - nanolith 11y ago
      I saw a sibling reply posted shortly before mine outlining your work. Nice job. :-)
- vitno 11y ago
  I've helped work some on a project doing that right now, although it's mostly been the awesome cmr. https://gitlab.com/robigalia/sel4-sys https://gitlab.com/robigalia/sel4-sys
- serge2k 11y ago
  > why reinvent the wheel Why not.
  - cmrx64 11y ago
    It's /only/ 30 man years of effort from experienced engineers. http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A... page 56.
- cmrx64 11y ago
  You can already use Rust on seL4, today! It's not ready for public consumption yet since there are no docs, but I've been working on it a lot recently and hope to have a release of the foundational libraries sometime in the next two weeks. There's a mailing list, if you want to watch: https://lists.robigalia.org/listinfo/robigalia-dev https://lists.robigalia.org/listinfo/robigalia-dev And the (still in-progress) source code: http://gitlab.com/robigalia/sel4-sys http://gitlab.com/robigalia/sel4-sys. I have some ideas about encoding RPC protocols as DFAs in Rust's type system, and then doing verification of the protocols in a more abstract setting (perhaps NuSMV or a similar checker). This is somewhat similar to the (ancient at this point) "protocol compiler" that used to be in Rust, doing a similar thing for channels. I'm interning at Data61 (née NICTA) on the verification team starting Jan 18, and I'm hoping to transfer some of that experience and knowledge into verifying Rust.
  - nanolith 11y ago
    I would love to see some blog posts regarding your experience during this internship. I am working on some formal verification myself for some commercial projects, and I enjoy reading about stuff like this.
  - xj9 11y ago
    Dream come true!
  - cvwright 11y ago
    Excellent! Thank you for your work on this. I'll be very excited to see where it goes.
jerf 11y ago
It has crossed my mind to wonder if one could obtain many benefits of microkernels while somehow leaning on something like the Rust type system to prove isolation. It seems to me one of the big practical things about microkernels is forcing you to isolate off the modules. In practice, when you do not force isolation, developers will always find reasons to violate the boundaries. Even very well meaning and very experienced ones will still tend to poke holes in, and this is one of those things where once you poke even tiny holes, the flood tends to come in. Thirty years ago, that level of isolation required OS-level enforcement if it was going to happen. But today, that's not the only way to guarantee isolation. We may also be able to do it via type systems. If we could create things statically guaranteed to be isolated but not requiring actual context switches, it should be theoretically possible to create things that are structurally microkernels, but do not need internal context switches because isolation has been proved at a higher level. Or, arguably, in some sense this would be something that transcends both microkernels and monolithic kernels to become something not properly called either. I'm sure there's many an i to be dotted and ts to be crossed before this would work, and you'd still probably want to work out a run-time loadable module which would probably make things interesting, you need a story for how a device driver can individually crash without bringing the whole process down (though since Linux can do it, presumably it is possible anyhow), and a whole bunch of things. But it does seem like an interesting opportunity for someone to make a kernel that is, well, not the same basic kernel the C type system naturally affords.
- nostrademons 11y ago
  That idea is generally termed a neokernel: http://c2.com/cgi/wiki?NeoKernel http://c2.com/cgi/wiki?NeoKernel It's basically relying on the type system & safety mechanisms of the underlying programming language to enforce some of the isolation properties that an operating system is normally used for. The Lisp Machine was probably the most commercially successful example. Since neokernels typically require tight integration between the programming language and the kernel, there are also opportunities for efficiency gains, eg. in Lisp Machines the garbage collector was tightly integrated with virtual memory to prevent page thrashing on collection, or in modern languages you could replace the OS scheduler with promises or green threads. The biggest downside of it is that it requires tight coupling between the programming language and OS, such that you can only use a single programming language (or a family of related ones that all share a type system) for all programs on the box. Few programming languages are flexible enough for that. With the move to cloud computing and virtualization, this becomes more practical, but then that same trend is also driving interest in the unikernel/exokernel pairing. If you only run a single application on a virtualized box, why not program directly to the hardware?

cvwright 11y ago

Wouldn't that be cool? Another neat idea would be to build on an existing microkernel like seL4, but write the userspace -- all the drivers, memory manager, filesystems, etc -- in Rust. The NICTA team already has proofs of correctness for the microkernel itself, so why reinvent the wheel? But at the same time, those proofs were super expensive and difficult to make. It would be awesome if we could get a reliable userland more easily by using a better language. I wonder what it would take to get Rust compiling for seL4?

nanolith 11y ago
Not much, really. The main thing needed is to port the language runtime to seL4. This should be a relatively small effort, and a great project to both learn some of the underbelly of Rust's ABI and seL4.
- cmrx64 11y ago
  Already done :)
  - nanolith 11y ago
    I saw a sibling reply posted shortly before mine outlining your work. Nice job. :-)
vitno 11y ago
I've helped work some on a project doing that right now, although it's mostly been the awesome cmr. https://gitlab.com/robigalia/sel4-sys https://gitlab.com/robigalia/sel4-sys
serge2k 11y ago
> why reinvent the wheel Why not.
- cmrx64 11y ago
  It's /only/ 30 man years of effort from experienced engineers. http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A... page 56.
cmrx64 11y ago
You can already use Rust on seL4, today! It's not ready for public consumption yet since there are no docs, but I've been working on it a lot recently and hope to have a release of the foundational libraries sometime in the next two weeks. There's a mailing list, if you want to watch: https://lists.robigalia.org/listinfo/robigalia-dev https://lists.robigalia.org/listinfo/robigalia-dev And the (still in-progress) source code: http://gitlab.com/robigalia/sel4-sys http://gitlab.com/robigalia/sel4-sys. I have some ideas about encoding RPC protocols as DFAs in Rust's type system, and then doing verification of the protocols in a more abstract setting (perhaps NuSMV or a similar checker). This is somewhat similar to the (ancient at this point) "protocol compiler" that used to be in Rust, doing a similar thing for channels. I'm interning at Data61 (née NICTA) on the verification team starting Jan 18, and I'm hoping to transfer some of that experience and knowledge into verifying Rust.
- nanolith 11y ago
  I would love to see some blog posts regarding your experience during this internship. I am working on some formal verification myself for some commercial projects, and I enjoy reading about stuff like this.
- xj9 11y ago
  Dream come true!
- cvwright 11y ago
  Excellent! Thank you for your work on this. I'll be very excited to see where it goes.

jerf 11y ago

It has crossed my mind to wonder if one could obtain many benefits of microkernels while somehow leaning on something like the Rust type system to prove isolation. It seems to me one of the big practical things about microkernels is forcing you to isolate off the modules. In practice, when you do not force isolation, developers will always find reasons to violate the boundaries. Even very well meaning and very experienced ones will still tend to poke holes in, and this is one of those things where once you poke even tiny holes, the flood tends to come in. Thirty years ago, that level of isolation required OS-level enforcement if it was going to happen. But today, that's not the only way to guarantee isolation. We may also be able to do it via type systems. If we could create things statically guaranteed to be isolated but not requiring actual context switches, it should be theoretically possible to create things that are structurally microkernels, but do not need internal context switches because isolation has been proved at a higher level. Or, arguably, in some sense this would be something that transcends both microkernels and monolithic kernels to become something not properly called either. I'm sure there's many an i to be dotted and ts to be crossed before this would work, and you'd still probably want to work out a run-time loadable module which would probably make things interesting, you need a story for how a device driver can individually crash without bringing the whole process down (though since Linux can do it, presumably it is possible anyhow), and a whole bunch of things. But it does seem like an interesting opportunity for someone to make a kernel that is, well, not the same basic kernel the C type system naturally affords.

nostrademons 11y ago
That idea is generally termed a neokernel: http://c2.com/cgi/wiki?NeoKernel http://c2.com/cgi/wiki?NeoKernel It's basically relying on the type system & safety mechanisms of the underlying programming language to enforce some of the isolation properties that an operating system is normally used for. The Lisp Machine was probably the most commercially successful example. Since neokernels typically require tight integration between the programming language and the kernel, there are also opportunities for efficiency gains, eg. in Lisp Machines the garbage collector was tightly integrated with virtual memory to prevent page thrashing on collection, or in modern languages you could replace the OS scheduler with promises or green threads. The biggest downside of it is that it requires tight coupling between the programming language and OS, such that you can only use a single programming language (or a family of related ones that all share a type system) for all programs on the box. Few programming languages are flexible enough for that. With the move to cloud computing and virtualization, this becomes more practical, but then that same trend is also driving interest in the unikernel/exokernel pairing. If you only run a single application on a virtualized box, why not program directly to the hardware?