Hacker News Reader

Comment by snvzz | Hacker News Reader

I applaud lessons taken from Liedtke/L4, a major step in the right direction. Now I can look at that project seriously, rather than consider it yet another pre-Liedtke mistake.

I'm not so sure, however, about concurrency in the kernel. The locks and added complexity certainly aren't going to help keep WCET low and bound.

NICTA's SSRG did study this: https://ts.data61.csiro.au/publications/nictaabstracts/Peter...

View on HN

I thinl the paper is a bit unclear about how one can come to that conclusion since concerning the Redis benchmark they state "The figure shows that throughput is independent of thekernel variant. Further investigation reveals that overall system throughput is limited by the network bandwidth, andthat the all cores have significant idle time."

If you are network limited you might not _really_ be testing in-kernel locking in the general case. But there might be something about the kernel that allow them to generalise even with low load, but I can't see anything obvious that would make a certain kernel immune to high load induced issues, but then I'm largely ignorant about L4 et al.

> I can't see anything obvious that would make a certain kernel immune to high load induced issues, but then I'm largely ignorant about L4 et al.

The typical system call in a modern microkernel costs on the order of hundreds of cycles. Fine-grained locking would by itself probably double this cost for almost no gain. Just waiting the hundreds of cycles is likely to be just as good as a fine-grained lock in such kernels, and the complexity savings are significant.

I was midly in shock when I looked in to L4 message passing times [1]. 250-300 cycles on x86_64 processors, and ~150-300 on ARM.

As somebody interested in concurrency what is being done internally to pull off this speed, but maintain extra-thread consistency in a SMT-type system? As far as I know even a x86_64 memory fence will require around >2,000 cycles.

I understand you create a notification object to pass a message, but don't you have to collect these notification objects at some point?

Edit 1:

I'm reading the manual [2], but I'm just becoming more confused. If you are passing register files, swapping stacks normally takes ~3ns even with small stacks. Or is the 300 cycles just the send time?

[1] https://ts.data61.csiro.au/publications/nictaabstracts/8988....

[2] https://sel4.systems/Info/Docs/seL4-manual-2.0.0.pdf

Notification objects are only for specific receive patterns IIRC. Simple message sends occur via endpoints, which I believe in seL4 you can think of sort of like a file descriptor, ie. each thread has a kernel-controlled address space of endpoints it can index to send messages.

The cycle count is for a one-way IPC. This roughly consists of entering kernel mode (~50-100 cycles), switch to kernel stack, finding the endpoint specified by system call (roughly: thread_control_block.endpoints[registerX], let's say ~10 cycles), switch to thread's address space (~100 cycles, maybe more for TLB flushes), switch to new thread's stack, return to user mode (~50-100 cycles). This is the fast path in which the whole message is passed in registers. The only memory that's touched are the original and target thread control blocks, so it's quite fast at ~300 cycles for x86_64.

These are all rough estimates of course, so don't quote me. Longer message sends require copying buffers which may also incur page mapping overheads and page faults. A page fault would abort the message send, notify the disk process to load the missing pages, and the send is retried once the page is mapped back into memory.

Edit: as noted in the L4 review paper you linked to, the majority of message sends are very small, and most simply pass all data in registers, so the fast path is the average cost.

Out of curiosity, do you have a reference to "lessons taken from Liedtke/L4"? Out of the blue, I have no clue what it means :)

I'm thinking mostly about the principle of minimality (what can be out of the kernel should be). But there's some more contributions from L4.

The ACM did a talk on those insights 20 years later: https://www.youtube.com/watch?v=RdoaFc5-1Rk

The associated NICTA SSRG paper: https://ts.data61.csiro.au/publications/nictaabstracts/Elphi...

A more recent NICTA SSRG paper: https://ts.data61.csiro.au/publications/nictaabstracts/Heise...

Yeah, I wish they had teamed up with Robigalia in order to build on seL4 or at least translated that 1:1 to Rust, foregoing the verified nature of seL4.

> 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.

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.

> 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).

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

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.

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.

I wrote on their forum about why they "shouldn't" use seL4, and definitely shouldn't port it to Rust:

https://discourse.redox-os.org/t/why-not-port-sel4-microkern...

If the goal is trusthworthy, reliable software, then you should use seL4. If the goal is to yell about how great Rust is, you could port seL4 to Rust.

Fully support your point of view.

What we always see on programming languages is that when shortcuts for arriving faster at our goals are taken, usually they give ammunition to remarks of the sort "language X cannot do Y".

Apparently most lack vision and need to be proven wrong.

So I hope they manage to just use Rust and Assembly.

EDIT: Improved the sentence

Reply on news.ycombinator.com