Hacker News Reader

Comment by snvzz | Hacker News Reader

> foregoing the verified nature of seL4

If anything, seL4 is the fastest L4 out there, proving that they can be fast and proven at the same time.

So, why would anyone want to do that?

Because Redox's aim is to be as little non-Rust as possible. I agree it'd be ill-advised to rewrite seL4 rather than use it, even though it's been a while since a revision was verified, because it's been battle tested, is continually improved and small enough to trust.

We really need to have a mainstream desktop microkernel operating system because:

1. no need anymore for kernel bypass mechanisms (too many to name for linux, btw)

2. decoupling of drivers from the kernel

3. instead of waiting for a backport of a new syscall to an LTS kernel, something like that will be just part of your system's stdlib

4. extremely reduced need to reboot a machine

5. driver faults can be recovered from gracefully, just like in Erlang's supervisor scheme

6. seL4's capability system allows for a safer system overall, with less hacks

Seeing how even Intel is introducing a message passing network with growing number of cores in their mainstream CPU designs, we should be over the general objections regarding a message passing design. They call it QMD, and it's something they already have in their Xeon Phi line for some time for obvious reasons, just as countless other general purpose or special purpose chip designs have had for a long time.

I wonder if one could get funding for an effort like Robigalia to reach production quality and have Servo running on it. Given the feature set of Servo, it's a safe bet that the required features would provide a reasonably complete system to replace your Linux machine.

The bigger struggle would be getting hardware vendors to contribute to FreeBSD and Linux drivers to also provide some level of support for a non-C code base. Though, moving up to that abstraction and language level should make it easier to write working hardware drivers.

> I wonder if one could get funding for an effort like Robigalia to reach production quality and have Servo running on it. Given the feature set of Servo, it's a safe bet that the required features would provide a reasonably complete system to replace your Linux machine.

If I got funding, Robigalia would definitely progress at least 10x faster than it does currently :) If anyone is interested in that, email me: corey@octayn.net...

As an aside, Robigalia has been picking up steam. The first developer preview should be out by Robigalia 2017 (April 25). Design documents and prototypes should be out by December 26 (the project's anniversary).

Oh, and if you extend it with multi-kernel functionality, scaling to very large number of cores/chips will also be solved in a fundamentally cleaner way. I haven't looked into it but there's an seL4 branch that implements multi-kernel support. If you don't know what this is, it's simply a way to have one kernel instance per processor, making scalability easier. Fujitsu has a linux variant to achieve the same and I think it's a goal of Barrelfish as well. Similar solutions exist in certain linux and dragonflybsd subsystems where, say, the network stack uses one scheduler or queue per core, removing the need for synchronization in a coarse way. Then, of course, you have to be smarter about scheduling things, but if you bind certain hardware bits to cores long-term, it should avoid accidental overhead via random migration. Language runtime VMs do the same for green threads with job stealing designs and pinning schedulers to cores. None of it is bleeding edge research material, we just have to use what's been invented.

I'm not sure that you need a kernel per-core. However, it would be nice for the microkernel to provide reliably per-cpu data structures to userspace. For example, via per-cpu replicated receive capabilities. That way, a capability send request from a client program would get routed to the same CPU's capability in the server. That would provide some very cache-friendly superfast machine-local IPC.

Completely eliminating shared-memory multiprocessing in userspace seems like a non-starter to me. Message passing is great, but there are plenty of cases where it's slower by many orders of magnitude. A good example is sparse matrix solvers; there's no way to get any kind of acceptable performance if you can't share the underlying data.

Google is developing an open source microkernel based OS code named Fuchsia. It's for x86, ARM and ARM64.

https://en.wikipedia.org/wiki/Google_Fuchsia

https://fuchsia.googlesource.com/magenta/+/master/README.md

From the top of my head, a few differences:

* Fuchsia is C (for the actual microkernel) and C++ (for userspace) / Redox is Rust. * Fuchsia's main current target is smartphones & laptops / Redox' main current target is Rust. * Fuchsia is very much funded / Redox is pretty grassroot. * Fuchsia supports any language for app development but favors Dart / Redox supports any language for app developent but favors Rust.

Keep in mind that both projects are pretty young and that my points above involve some dose of mind-reading, so caveat lector.

Genode OS framework lets you use Linux drivers with L4 kernels, including seL4.

the master branch of sel4 is always passing verification, for the verified platform: armv7-a on a Sabre Lite.

the x86_64 verification is coming out soon according to the roadmap.

Reply on news.ycombinator.com