" We took a substantially different approach with seL4; its model for managing kernel memory is seL4’s main contribution to OS design. Motivated by the desire to reason about resource usage and isolation, we subject all kernel memory to authority conveyed by capabili- ties (except for the fixed amount used by the kernel to boot up, including its strictly bounded stack). "
I guess I should've said seL4 took capabilities to the extreme.
L4's contribution was speed. It was assumed that microkernels, and especially capability-based microkernels were fundamentally slower than monolithic kernels. This is why Linux (1991) is monolithic. Yet L4 (1994) was the fastest operating system in existence at the time, despite being a microkernel and capability based. It's too bad those dates aren't reversed, or we might have had a fast, capability-based, microkernel Linux :(
The problem with shutdowns and restarts is the secure bootstrapping problem. The boot process must be within the trusted computing base, so how do you minimize the chance of introducing vulnerabilities? With checkpointing, if you start in a secure state, you're guaranteed to have a secure state after a reboot. This is not the case with other any other form of reboot, particularly ones that are highly configurable and so easy for the user to introduce an insecure configuration.
In any case, many apps are now designed to restore their state on restart, so they are effectively checkpointing themselves, so there's clearly value to checkpointing. In systems with OS-provided checkpointing it's a central shared service and doesn't have to be replicated in every program. That's a significant reduction in overall system code that can go wrong.
That's not true actually. These capability systems have the principle of least privilege right down to their core. The checkpointing code is in the kernel which only calls out to the disk driver in user space. The checkpointing code itself is basically just "flush these cached pages to their corresponding locations on disk, then update a boot sector pointer to the new checkpoint", and booting a system is "read these pages pointed to by this disk pointer sequentially into memory and resume".
The attack surface in this system is incomparably small compared to the boot process of a typical OS, which run user-defined scripts and scripts written by completely unknown people from software you downloaded from the internet, often with root or other broad sets of privileges.
I really don't think you can appreciate how this system works without digging into it a little. EROS was built from the design of KeyKOS that ran transactional bank systems back in the 80s. KeyKOS pioneered this kind of checkpointing system, so it saw real industry use in secure systems for years. I recommend at least reading an overview:
https://flint.cs.yale.edu/cs428/doc/eros-ieee.pdf
EROS is kind of like what you'd get it if you took Smalltalk and tried to push it into the hardware as an operating system, while removing all sources of ambient authority. It lives on as CapROS:
Oh, and anytime as needed the OS could serialize out your process, pipe it across the network to another machine, and resume. Useful for load balancing, or relocating a program to be near the data it is accessing. Unless your program pays special attention to the clock, it wouldn't notice.
I still think about Amoeba from time to time, and imagine what could have been if we had gone down that route instead.
E.g. You spawn a process on another computer and then the connection drops.
In practice it might not be an issue. The reason you'd typically do something like move processes across a WAN is because you want it to operate next to data it is making heavy use of. The copy that booted up local to the data would continue operating, while the copy at the point of origin would suddenly see the data source go offline.
Now of course more complex schemes can be devised, like if the data source is replicated and so both copies continue operating. Maybe a metric could be devised for detecting these instances when the partition is healed, and one or both processes are suspended for manual resolution? Or maybe programs just have to be written with the expectation that their capabilities might suddenly become invalid at any time, because the capability sides with the partition that includes the resource? Or maybe go down the route of making the entire system transactional, so that partition healing can occur, and only throw away transaction deltas once receipts are received for all nodes ratcheting state forward?
It'd be an interesting research area for sure.
seL4 is now a healthy non-profit, seL4 foundation[1].
0. https://microkerneldude.org/2022/02/17/a-story-of-betrayal-c...
1. https://microkerneldude.org/2022/03/22/ts-in-2022-were-back/
With that out of the way, you're right in that the microkernel doesn't present a posix interface.
But, like QNX, there are libraries for that, seL4 foundation itself maintains some.
They have a major ongoing effort on system servers, driver APIs and ways to deploy system scenarios. Some of them were talked about in a recent seL4 conference.
And then there's third party efforts like the amazing Genode[0], which supports dynamic scenarios with the same drivers and userspace binaries across multiple microkernels.
They even have a modern webbrowser, 3d acceleration as well as providing a virtualbox box that runs inside Genode, so the dogfooding developers are be able to run e.g. Linux inside a virtualbox to bridge the gap.
I'm not bothered by the kernel bloat. There's a lot of dev time being invested in Linux and while the desktop is not as much of a priority as say the server space a performant kernel on handhelds and other such devices and the dev work to get it there will benefit the desktop users like myself.
A bunch of similar embedded systems. And blackberry, if anyone's still using them.
In the end, all I could practically use it for was as a bluetooth audio connector.
So much like a well structured main method in a C program or other C like language where main just orchestrates the calling of other functions and such. In this case main might initialize different things where the QNX kernel doesn't but the idea or general concept remains.
I'm no kernel dev but this sounds good to me. Keeps things simple.
The process of serving an HTTP request is broken into a large number of fine grained stages and plugin modules may hook into any or all of these to modify the input and output to each stage.
The same basic idea makes it easy to turn any application concept into a modules-and-core architecture. From the day I read (skimmed) that book a decade or two ago this pattern has been burned into my brain
Pretty much everywhere there is some undercurrent of "use this ultra-small generic interface for everything and life will be easier". With games and ECS, microkernels and IPC-for-everything, with frontend frameworks and components that only communicate between themselves via props and events, with event sourcing and CQRS backends, Actors in Erlang, with microservices only communicating via the network to enforce encapsulation... Perhaps even Haskell's functional-core-imperative-shell could count as that?
I feel like OOP _tried_ to get to this point, with dependency injection and interface segregation, but didn't quite get there due to bad ergonomics, verbosity and because it was still too easy to break the rules. But it was definitely an attempt at improving things.
~90% of those are device drivers, which you'd still need with a microkernel if you want it to run or arbitrary hardware.
The only downside of course, is that you don't get the isolation benefits of the microkernel for anything depending on the Linux kernel process.
The QNX kernel doesn't do anything with strings. No parsing, no formatting, no messages.
Linux suffers from being too bloated for real time. Millions of lines of kernel, all of which have to be made preemptable. It's the wrong architecture for real time. So it took two decades to try to fix this.