A Different Core
A couple of years ago, the HURD developers began to realize that, no matter how shiny their design was, it would always be held back by the fact that it used a first-generation microkernel at the core. An effort began to port the system to a much more modern microkernel—L4.
L4 is sometimes called a nanokernel because it tries to be as small as possible. It’s very fast, and delegates even more work to servers outside of kernelspace. One of the most interesting features of the L4 port of HURD is how it handles paging.
Flat memory space is my favorite example of a leaky abstraction. A lot of processes actually do care about whether their memory is on disk or in RAM, and would alter their behavior accordingly. A good example is something like Firefox, which fills up available RAM with page caches. Often, swapping these pages back in from disk can be slower than re-fetching from the Internet.
L4/HURD puts paging entirely within the application’s control. When memory is constrained, applications receive a message asking them to free some memory. Something like a web browser could discard some caches, while other apps might swap some pages to disk that they were unlikely to use in the near future.
Another option for a replacement kernel, and one which is receiving a lot more attention, is Coyotos. This is a capability-based system, which fits quite well with the HURD security model. The EROS kernel, of which Coyotos is an evolution, has performance comparable to that of L4. Coyotos is somewhat simpler than EROS, and has the interesting goal of being aimed at being formally verifiable. It’s written in BitC, a Lisp-like language with low-level semantics. With a formally verified microkernel and clean separation of system servers, a Coyotos/HURD system could be very secure and stable.