News for hackers. Stuff that matters.
Re:The SeL4 Microkernel: An Introduction [pdf] by nimish on Sunday March 23, 2025 @11:32AM (#43453594)
SeL4 is proof that microkernels are safe, efficient and scalable yet we are stuck with big honking Linux kernels in 2025. That said more and more drivers moving usermode anyway so it's a wash in the end.
Re:The SeL4 Microkernel: An Introduction [pdf] by pjmlp on Sunday March 23, 2025 @11:55AM (#43453744)
I feel like containers and Kubernetes are microkernels revenge.

They are for all practical purposes fulfilling the same role.

Re:The SeL4 Microkernel: An Introduction [pdf] by bri3d on Sunday March 23, 2025 @12:00PM (#43453778)
Not at all? If anything they’re filling the opposite role. Microkernels are about building interfaces which sandbox parts of the kernel. Namespaces are about giving sandboxed userlands full access to kernel interfaces.
Re:The SeL4 Microkernel: An Introduction [pdf] by pjmlp on Sunday March 23, 2025 @12:14PM (#43453876)
Namespaces is one form of capabilities.

Additionally a Linux kernel that exists for the sole purpose to keep KVM running, while everything that powers a cloud workload are Kubernetes pods, it is nothing more than a very fat microkernel, in terms of usefulness.

Re:The SeL4 Microkernel: An Introduction [pdf] by bigstrat2003 on Sunday March 23, 2025 @01:30PM (#43454375)
Microkernel does not mean it uses capabilities. And "very fat microkernel" is an oxymoron. The definition of a microkernel is that they do as little as possible in the kernel.
Re:The SeL4 Microkernel: An Introduction [pdf] by afiori on Sunday March 23, 2025 @03:16PM (#43455089)
Imo the microness is not about size but about the architecture of running drivers/services in fault-resistant separation from the kernel
Re:The SeL4 Microkernel: An Introduction [pdf] by pjmlp on Sunday March 23, 2025 @01:50PM (#43454515)
Of course it doesn't.

The point is how Linux is being tamed to provide some of the concepts, in spite of its monolithic design.

But naturally we can discuss minutiae instead.

Re:The SeL4 Microkernel: An Introduction [pdf] by bri3d on Sunday March 23, 2025 @06:13PM (#43456314)
It’s not “some of the concepts” nor minutae, though, it’s literally the difference between a microkernel and a monolithic kernel.

Presenting capabilities / namespaces to userland is a completely different and in the case of Linux, orthogonal thing to presenting capabilities/namespaces to kernel services. I guess you could argue that the concept of capabilities came from microkernels, but when it’s applied to only user space, it’s just not really related to a microkernel anymore at all.

That’s basically the whole problem with capabilities and especially their application in namespaces from a security standpoint in Linux: they try to firewall these little boxes from each other but the kernel they’re all talking to is still one big blob. And this difference is meaningful in a security sense, not just some theory hand waving. https://www.crowdstrike.com/en-us/blog/cve-2022-0185-kuberne... is just one good example, but entire classes of mitigations are rendered meaningless by the ability to unshare into a box that lets an attacker touch exploitable kernel surface area which is not further isolated.

Re:The SeL4 Microkernel: An Introduction [pdf] by indolering on Sunday March 23, 2025 @08:13PM (#43456882)
I don't think containers, namespaces, and the like failing to provide the same benefits of a true microkernel negate the OPs point. They are ways of segmenting userspace in a more finely grained manner and they do make attacks harder.

Linux security being a shit show and undermining these efforts is kinda besides the point: they are still attempts provide a runtime closer to what microkernels would naturally provide in a backwards compatible way. Indeed, these containers could be turned into fully fleged VMs if there were the resources to make it happen.

Re:The SeL4 Microkernel: An Introduction [pdf] by bri3d on Monday March 24, 2025 @11:50AM (#43462416)
I don't really get this argument: "you're saying that one thing, namespaces, isn't implemented in any way resembling a microkernel, but what if we replaced it with another completely different thing, a hypervisor? Then it would be similar!" Yes? Sure?

To me the word "microkernel" expresses how the kernel is structured, not what userspace interface it presents. A microkernel is built by separating kernel services into discrete processes which communicate using a defined IPC mechanism. Ideally, a microkernel offers memory boundary guarantees for each service, either by using hardware memory protection/MMU and running each service as a true "process" with its own address space, or by proving the memory safety of each kernel service using some form of ahead-of-time guarantee.

Of course, doing this lends itself to also segmenting user-space processes by offering a unique set of kernel service processes for each user-space segment (jail, namespace, etc.), but there's no reason this needs to be the case, and it's by and large orthogonal.

I do agree with what I eventually understand the grandparent poster was trying to express, which is that running a bunch of KVMs looks like a microkernel. Because then, you've moved the kernel services into a protected boundary and made them communicate across a common interface (hypercalls).

But that's not how Kubernetes works by default and in the case of containers and namespaces, I think this is entirely false and a dangerous thing to believe from a security standpoint.

> They are ways of segmenting userspace in a more finely grained manner and they do make attacks harder.

From a _kernel_ security standpoint (because we are talking about micro_kernels_ here), I actually think namespaces make attacks much easier and the surface area much greater. Which is basically the entire point I was trying to make: rather than exposing fragile kernel interfaces to exclusively system services with CAP_SYS_ADMIN, you now have provided an ability (unshare) for less-trusted runtimes to touch parts of the host kernel (firewall, filesystem drivers, etc.) which they would normally not have access to, and you have to go back and use fiddly rules engines (seccomp, apparmor, selinux) to fix the problem you created with namespaces.

To be clear, I think from a big picture standpoint, it's a tradeoff, and I'm nowhere near as anti-container/anti-namespace as it may seem. I just get annoyed when I see people express namespaces as a kernel security boundary when they are basically the exact opposite: they are a kernel security un-boundary, and Linux's monolithic nature makes this a problem.

Re:The SeL4 Microkernel: An Introduction [pdf] by indolering on Monday March 24, 2025 @10:01PM (#43467440)
That's fair!
Re:The SeL4 Microkernel: An Introduction [pdf] by pjmlp on Monday March 24, 2025 @03:44AM (#43458457)
A microkernel by the book, is just a bunch of processes doing stuff that would be on the kernel otherwise, if we are then discussing minutae.

Nothing else, critical set of OS services are no longer hosted in a single process space, rather required a distributed system of processes running on a single computer node.

The moment these processes are able to be hosted in a set of computing nodes, we enter the realm of distributed OSes, is is another discussion.

The amount of services that remain on the mikrokernel, versus what is hosted in each OS process, running outside of the kernel, depends on each microkernel, there is no rule for this division of labour and each one that was ever designed has chosen a different approach.

If you cannot see the parallel between this and a swarm of containers running on a node, doing the actual workload and only requiring the kernel services due to the way KVM is implemented, and rather focus on a security mechanism that is detail on how Linux works, well, it isn't on me to further break it down.

Re:The SeL4 Microkernel: An Introduction [pdf] by bri3d on Monday March 24, 2025 @11:38AM (#43462287)
OK, I get what you are saying now, and I agree if we are talking about KVM.

That's not how Kubernetes works by default, so I thought we were talking about container runtimes. I still disagree strongly from both a practical security and theory standpoint if we are talking about container runtimes implemented using namespaces and cgroups.

Re:The SeL4 Microkernel: An Introduction [pdf] by vacuity on Sunday March 23, 2025 @01:41PM (#43454444)
The dose makes the poison; we're still a long way from fulling embracing microkernels and capabilities. Security is a holistic property and encompasses finer details too. I want a small TCB. I want capabilities pervasively. And in pursuit of modularity and abstraction, I want to be able to choose the components I want and take those burdens myself. It's a bit silly seeing the nth SIGOPS-SOSP paper on how Linux can be improved by integrating userspace scheduling.
Re:The SeL4 Microkernel: An Introduction [pdf] by pjmlp on Sunday March 23, 2025 @01:56PM (#43454550)
It is the same in safer systems programming languages, we already have the concept since 1961, but apparently making the industry take the right decisions is a tenuous path until something finally makes good ideas stick and gain adoption.
Re:The SeL4 Microkernel: An Introduction [pdf] by cedws on Sunday March 23, 2025 @01:00PM (#43454148)
I heard a joke somewhere that sel4 is even more successful than Linux because it is running below ring 0 in every Intel chip shipped in the past N decades, plus probably many others.
Re:The SeL4 Microkernel: An Introduction [pdf] by CalChris on Sunday March 23, 2025 @01:13PM (#43454258)
Intel used a version of Minix rather than seL4 for its Intel Management Engine. [1] There was some controversy about this because they didn't give Andrew Tanenbaum proper credit. [2]

[1] https://www.zdnet.com/article/minix-intels-hidden-in-chip-op...

[2] https://www.cs.vu.nl/~ast/intel/

Re:The SeL4 Microkernel: An Introduction [pdf] by indolering on Sunday March 23, 2025 @07:42PM (#43456754)
Such a dumb technical choice driven by stupid managerial considerations. They do this ring -1 shit because hardware companies view this as a cheap way to add value. But they don't open source it or contribute back because they view it as secret sauce. Minix as a result didn't get the investments that GPL software receives. Now the project is in hard legacy mode.
Re:The SeL4 Microkernel: An Introduction [pdf] by ianburrell on Sunday March 23, 2025 @01:35PM (#43454405)
Intel Management Engine is a separate microcontroller integrated into the chipsets. Recent ones are Intel Quark x86 CPU and Minix 3 OS.
Re:The SeL4 Microkernel: An Introduction [pdf] by mrkeen on Sunday March 23, 2025 @01:15PM (#43454275)
That is Minix, not SeL4.
Re:The SeL4 Microkernel: An Introduction [pdf] by naasking on Monday March 24, 2025 @09:49AM (#43461052)
seL4 is used in a lot of cellular phone firmwares I believe.
Re:The SeL4 Microkernel: An Introduction [pdf] by ryao on Sunday March 23, 2025 @01:08PM (#43454221)
seL4 having a proof of correctness does not mean all microkernels do. In fact, seL4 is the only microkernel that has a proof of correctness. If you build on top of it in the microkernel way, you quickly find that it is not performant. That is why NT and XNU both abandoned their microkernel origins in favor of becoming monolithic kernels.
Re:The SeL4 Microkernel: An Introduction [pdf] by mastax on Sunday March 23, 2025 @01:27PM (#43454347)
I’ve seen this argument play out many times. I believe the next line is: “QNX proved that micro kernels can be fast given clever message passing syscall design.”

“I remember running the QNX demo disc: an entire graphical operating system on a single 1.44MB floppy! Whatever happened to them?”

“They got bought by blackberry, which ended as you’d expect. QNX had a lot of success in automotive though.”

“Nowadays Linux and Android are dominant in new cars, though, proving once and for all that worse is better.”

exeunt. End Scene

Re:The SeL4 Microkernel: An Introduction [pdf] by nine_k on Sunday March 23, 2025 @01:50PM (#43454506)
Also an illustration how an open-source solution, even if technically inferior, would displace a closed-source solution, even if technically superior, unless there is a huge moat. And huge moats usually exist only in relatively narrow niches.
Re:The SeL4 Microkernel: An Introduction [pdf] by vacuity on Sunday March 23, 2025 @02:03PM (#43454587)
It turns out that success is composed of 90% luck, 10% marketing, and 5% talent/technical advantage. A rhetorical question: how do you entice people to turn a movement into a revolution when it isn't likely the movement will succeed?
Re:The SeL4 Microkernel: An Introduction [pdf] by necovek on Sunday March 23, 2025 @03:44PM (#43455338)
Another rhetorical question: out of luck/marketing/technical advantage, which one is contributing the most to the extra 5% out of 105% of all the components success can be attributed to?
Re:The SeL4 Microkernel: An Introduction [pdf] by ryao on Sunday March 23, 2025 @01:39PM (#43454427)
Nice use of Latin. mihi placet.
Re:The SeL4 Microkernel: An Introduction [pdf] by netbsdusers on Sunday March 23, 2025 @02:24PM (#43454733)
NT and XNU never had microkernel origins - Cutler explicitly refuted this at a conference in the early 1990s (if anyone remembers which, kindly share) and NeXTSTEP forked Mach at version 2.5, which was not a microkernel (see https://cseweb.ucsd.edu/classes/wi11/cse221/papers/accetta86...). XNU retained this monolithic architecture (as did Tru64 and other systems that trace their heritage to Mach prior to its version 3).
Re:The SeL4 Microkernel: An Introduction [pdf] by danieldk on Sunday March 23, 2025 @04:20PM (#43455600)
NeXTSTEP forked Mach at version 2.5

Various sources state that they rebased to OSF Mach Kernel 7.3, which was based on Mach 3 and parts of Mach 4. The OSF MK ancestry of macOS XNU can still be seen in paths:

https://github.com/apple-oss-distributions/xnu/tree/main/osf...

Re:The SeL4 Microkernel: An Introduction [pdf] by netbsdusers on Sunday March 23, 2025 @06:13PM (#43456319)
As far as I can tell (this isn't gospel, just something I've inferred as the only reasonable explanation from comparing the codebases), Apple reconstructed a Mach 2.5 style kernel, like NeXTSTEP had, from fresh codebases (OSF Mach and 4.4BSD-Lite2), perhaps because 4.3BSD was still encumbered at the time.

The Darwin 0.1 and 0.3 releases contain the old kernel, derived directly from NeXTSTEP, and that's the direct derivative of Mach 2.5. The later XNU appears to be a reconstruction of that kernel with unencumbered code and that's also when IOKit replaced DriverKit.

Re:The SeL4 Microkernel: An Introduction [pdf] by rhet0rica on Sunday March 23, 2025 @04:27PM (#43455647)
This is quite a ship-of-Theseus problem. Steve Jobs hired Avi Tevanian to work at NeXT on the Mach kernel, and later brought Tevanian to Apple; he was still working on the Mach/Darwin kernel as late as the first iPhone release. There is a reasonable argument to be made that the OSF kernel is actually the derivative, by default.
Re:The SeL4 Microkernel: An Introduction [pdf] by p_ing on Sunday March 23, 2025 @04:33PM (#43455676)
There are a few references to the OSF Mach kernel from '98 in a few files, such as https://github.com/apple-oss-distributions/xnu/blob/main/osf...

EDIT: Apple calls out Mach 3.0.

https://developer.apple.com/library/archive/documentation/Da...

https://developer.apple.com/library/archive/documentation/Da...

Apple took Mach 3.0 and collapsed it into a single address space for performance purposes. Certainly reasonable.

Re:The SeL4 Microkernel: An Introduction [pdf] by rhet0rica on Sunday March 23, 2025 @04:35PM (#43455680)
In more recent interviews Cutler has been firm that the NT kernel was designed pragmatically, a view that Tevanian also evidently later adopted, as evident with the great wheel of incarnation that Darwin went through on the road to XNU, although I'm not sure Tevanian ever stated his perspectives on this matter publicly. Neither of these systems were ever true monolithic kernels in the Linux or Unix sense—at all times they both had some measure of sandboxing between e.g. driver code and the scheduler—rather sitting somewhere between.

True microkernels are, alas, more of an ideology than a practical reality, as the long-suffering GNU/HURD team discovered; Tanenbaum has been clear that the MINIX/NetBSD experiment was more about principles than performance. That said, certainly many hypervisors have attained success with configurations that coincidentally happen to be the same footprint as a microkernel.

Re:The SeL4 Microkernel: An Introduction [pdf] by vacuity on Sunday March 23, 2025 @06:36PM (#43456463)
The hypervisor/microkernel boundary has blurred, and commercial success for microkernels is more or less as hypervisors, e.g. OKL4 is widely used in mobile devices[0]. And Tanenbaum's Minix is used for the Intel Management Engine. I don't know the details with HURD, but I don't think it is mainly suffering from "inherent" or "nearly-inherent" (strongly associated) problems of microkernels. The main cost of microkernels is developer effort and likely performance overhead.

[0] https://vita.militaryembedded.com/5159-open-virtualization-a...

Re:The SeL4 Microkernel: An Introduction [pdf] by snvzz on Sunday March 23, 2025 @09:12PM (#43457126)
>the long-suffering GNU/HURD team discovered;

HURD is Mach-based; it is stuck in a pre-L4 world and thus irrelevant to this conversation.

Very 40 years ago technology. Still better than ~60yr ago UNIX, although they're trying to ultimately be UNIX-like.

It is sad Mach and HURD still keep coming up in microkernel discussion.

Re:The SeL4 Microkernel: An Introduction [pdf] by naasking on Monday March 24, 2025 @04:06PM (#43464892)
Maybe not that irrelevant, since another desktop and mobile operating system used around the world is also based on Mach.
Re:The SeL4 Microkernel: An Introduction [pdf] by snvzz on Monday March 24, 2025 @06:45PM (#43466185)
There's some hope now that Apple is a seL4 foundation member.
Re:The SeL4 Microkernel: An Introduction [pdf] by indolering on Monday March 24, 2025 @09:54PM (#43467389)
A Mach that is neutered WRT it's microkernel architecture.
Re:The SeL4 Microkernel: An Introduction [pdf] by p_l on Monday March 24, 2025 @09:12AM (#43460677)
From talking with some people who were witnesses to earliest days of Hurd (but not involved in the project), the real problems of Hurd were social not technical - if anything, OSF/1 & NeXTSTEP succeeding from similar code base (for some value of) points that it was possible to do it.

The story goes that the early days were dominated by some ridiculously bad project management that makes Cathedral and the Bazaar era "Cathedral" a nice and well maintained project.

Most importantly, GNU Hurd lacked the "ecological niche" to drive work towards it because it couldn't deliver enough, just like lack of information about 386BSD led to Linux (Linus explicitly said that if he had known about 386BSD, he would have worked on it and maybe forked it)

Re:The SeL4 Microkernel: An Introduction [pdf] by ryao on Sunday March 23, 2025 @05:05PM (#43455906)

  NT and XNU never had microkernel origins - Cutler explicitly refuted this at a conference in the early 1990s 
Interestingly, the Tanenbaum–Torvalds debate had Tanenbaum claim otherwise at the very start:

  The alternative is a microkernel-based system, in which most of the OS runs as separate processes, mostly outside the kernel. They communicate by message passing. The kernel's job is to handle the message passing, interrupt handling, low-level process management, and possibly the I/O. Examples of this design are the RC4000, Amoeba, Chorus, Mach, and the not-yet-released Windows/NT.
https://groups.google.com/g/comp.os.minix/c/wlhw16QWltI

That is why I thought Windows NT had originally been intended to be a microkernel.

Re:The SeL4 Microkernel: An Introduction [pdf] by p_ing on Monday March 24, 2025 @10:25PM (#43467568)
NT incorporates a client/server model, like a microkernel, but isn't a "pure" microkernel like Mach. This gives rise to the 'hybrid kernel' term, which Linus dislikes.

Wikipedia has a decent depiction of the hybrid structure, but quoting from the NT Design Workbook:

> This specification describes the kernel layer of the NT OS/2 operating system. The kernel is responsible for thread dispatching, multiprocessor synchronization, hardware exception handling, and the implementation of low-level machine dependent functions.

> The kernel is used by the executive layer of the system to synchronize its activities and to implement the higher levels of abstraction that are exported in user-level API's.

https://en.wikipedia.org/wiki/Windows_NT_3.1#Architecture

Re:The SeL4 Microkernel: An Introduction [pdf] by pjmlp on Sunday March 23, 2025 @02:05PM (#43454609)
NT in Windows 11 has very little to do with the monolithic kernel story that keeps being repeated.

Not only did the graphics stack moved again back into userspace, there is now a complete userspace drivers stack, and VBS (Virtualization-based security) for several kernel components that run on their mini Hyper-V island, talking via IPC with the rest of the kernel.

Likewise on XNU land, Apple has started a crusade already a few years ago, to move all kexts into userspace, no more drivers in the kernel beyond the ones Apple considers critical.

In both cases, they never were a pure monolithic kernel, due to the way walls were introduced with kernel level IPC to talk across modules, instead of straight function calls.

Re:The SeL4 Microkernel: An Introduction [pdf] by el_pollo_diablo on Monday March 24, 2025 @05:37AM (#43458954)
> seL4 is the only microkernel that has a proof of correctness

ProvenCore (https://provenrun.com/provencore/) has a proof that covers correctness (memory safety, and more generally absence of UB, termination, etc.), functional properties (e.g. the fork() system call is a refinement of an abstract "clone" operation of abstract machines), and security properties (memory isolation).

Re:The SeL4 Microkernel: An Introduction [pdf] by vacuity on Sunday March 23, 2025 @01:57PM (#43454556)
I will caution that IPC microbenchmarks should not be taken as confirmation that the "academic microkernel" is viable: OS services all in userspace and with fine granularity as is appropriate. Often microkernel-like designs like VMMs/hypervisors and exokernels make use of unikernels/library OSes on top, which reduces the burden of fast IPC somewhat. Or developers intentionally lump protection domains to reduce IPC burden. Of particular note: even seL4 did not evict its scheduler to userspace. Since the scheduler is the basis behind time management, it's quite a blow to performance if the scheduler eats up time constantly. My own thoughts there are that, with care, a userspace scheduler can efficiently communicate with the kernel with a shared memory scheme, but that is not ideal. But for desktop and mobile, a microkernel design would be delightful and the performance impact is negligible. We need far more investment on QoS there.

Edit: That being said, we should be building microkernel-based OSes, and if for some cases performance really is a restricting factor, they will be exceptions. The security, robustness, flexibility, etc. of microkernels is not to be understated.

Re:The SeL4 Microkernel: An Introduction [pdf] by indolering on Sunday March 23, 2025 @06:18PM (#43456344)
They verified that the scheduler doesn't interfere with the integrity, confidentiality, and authenticity requirements of the kernel so it's a moot point.
Re:The SeL4 Microkernel: An Introduction [pdf] by vacuity on Sunday March 23, 2025 @06:24PM (#43456381)
Rather, although I believe the seL4 scheduler is sufficiently general, I want a userspace scheduler to minimize policy. The seL4 team recognizes that a kernelspace scheduler violates Liedtke's minimality principle for microkernels, since the only motivating reason is performance. If an efficient userspace scheduler implementation exists, the minimality principle dictates no kernelspace scheduler. Otherwise there's pointless performance overhead and possibly policy inflexibility.
Re:The SeL4 Microkernel: An Introduction [pdf] by indolering on Sunday March 23, 2025 @07:18PM (#43456664)
I understand the minimality principle but one should not be afraid to violate layers of abstraction when justified. The whole point of the minimality principle is to improve modularity and remove the need to worry about the correctness of various OS components.

What would you be able to do in a userspace scheduler that couldn't be done safely in an in-kernel scheduler? Why couldn't it be configured or given a safe API to interact with userspace at runtime? But I guess your shared memory bit is an API to a userspace scheduler?

Re:The SeL4 Microkernel: An Introduction [pdf] by vacuity on Sunday March 23, 2025 @09:24PM (#43457182)
Well, one thing about adapting seL4 is that we shouldn't assume derivatives will be formally verified to the same degree. Ideally we would, but I don't expect this to happen in practice. And having a kernelspace scheduler that is minimal and requires a userspace scheduler to achieve full control of scheduling, where a userspace scheduler would do, is redundant overhead. If the kernelspace scheduler wasn't minimal, it would both be hard to verify and extend. This is all in line with seL4's design. So you're concerned about power where the question was always about performance. Hydra had userspace schedulers way back when, and it wasn't followed because it was prohibitive then. The minimality principle might be given various explanations, but I think the end result of what a system following it achieves speaks for itself.

> I understand the minimality principle but one should not be afraid to violate layers of abstraction when justified.

Rather, in a well-designed system, the justification necessarily is performance. Abstractions exist for the ease of the developer to write code that is correct. Performance (runtime, memory usage, etc.) is the concrete impact of code. For concerns like debugging or flexibility, those arise if the abstractions are lacking. Performance concerns arise because even good abstractions impose overhead. Note that conventional layered architectures are usually poor abstractions for implementation. Good for design but not coding.

> But I guess your shared memory bit is an API to a userspace scheduler?

Indeed. I would rather not, but shared memory probably is necessary to some degree for a userspace scheduler.

Re:The SeL4 Microkernel: An Introduction [pdf] by netbsdusers on Sunday March 23, 2025 @02:18PM (#43454700)
Drivers in userspace is not particularly microkernelly - most of the major monolithic kernels have supported this to some degree or another for years (it is easy in principle, just transmit I/O requests to userspace servers over some channel) while many historic microkernels (see e.g. Mach 3) did not do it. It hardly changes the architecture of the system at all.

It is moving the higher-level things into userland that is the harder problem, and the one that has been challenging for microkernels to do well.

Re:The SeL4 Microkernel: An Introduction [pdf] by vacuity on Sunday March 23, 2025 @02:47PM (#43454873)
People should stop bringing up Mach so much. It should never have been the poster child for microkernels. It's poisoned the discourse when there are plenty of alternative examples. Granted, Mach also did some good work in the space, but its shortcomings are emphasized as if they reflect the whole field.

More to the point, drivers in userspace is an important distinction between "pure" monolithic kernels and microkernels: the former is optimizing for performance and the latter is optimizing for robustness. It's not about ease of implementation for either. It's quite meaningful to shift on the axis nowadays: it represents a critical pragmatic decision (notice purity is irrelevant). You're right that "higher-level things" such as the networking stack or filesystem are also crucial to the discussion. I think here, too, ease of implementation is not relevant, though.

Re:The SeL4 Microkernel: An Introduction [pdf] by torginus on Sunday March 23, 2025 @04:22PM (#43455608)
Isn't it common to run OSes on desktop/server environment inside hypervisors? That means the OS itself can be transparently virtualized or preempted, and access to physical hardware can be transparently passed to the virtualized OSes. This can be accomplished today with minimal impact to performance on user experience.

The fact that this can be done with OS code not explicitly designed for this signals to me that there are no roadblocks to having a high-performing general purpose microkernel running our computers.

Re:The SeL4 Microkernel: An Introduction [pdf] by vacuity on Sunday March 23, 2025 @06:31PM (#43456431)
This leads to big units of code, namely multiple OSes, whereas the ideal is being able to use as finely granular units as developers are able to stomach. For example, Xen can work around the issue of device drivers by hosting a minimal OS instance that has drivers, but it is better to be able to run drivers as individual processes. This reduces code duplication and performance overhead.
Re:The SeL4 Microkernel: An Introduction [pdf] by torginus on Monday March 24, 2025 @03:06AM (#43458314)
You're absolutely right but I was making the point that there's demonstrably no significant downsides to running driver/kernel code in less privileged mode, rather than Ring 0.
Re:The SeL4 Microkernel: An Introduction [pdf] by phendrenad2 on Sunday March 23, 2025 @04:29PM (#43455657)
Yes and there's a very good reason: Linux is safe enough, more efficient, and more scalable.
Re:The SeL4 Microkernel: An Introduction [pdf] by vacuity on Sunday March 23, 2025 @06:46PM (#43456508)
I suppose I should ask the other side too, though I am biased to favor microkernels, and am better read on them, but how so?

"Safe enough" measured by the standards of this upside-down industry...I'll let everyone decide that for themselves.

"More efficient": while monolithic kernels have a higher ceiling, currently there's plenty of OS research papers and industry work demonstrating that more integration with userspace brings performance benefits, such as in the scheduler, storage, or memory management. Microkernels encourage/enforce userspace integration.

"More scalable": I think this has less to do with kernelspace scale and more with how nodes are connected. See Barrelfish[0] for eschewing shared memory in favor of message passing entirely, running separate kernels on each core. Meanwhile Linux has gradually discovered a "big lock" approach is not scalable and reduced coarse-grained locks, added RCU, etc.. So I think we will go moreso towards Barrelfish. But on a single core, for what goes into the kernel, that's covered by everything but scalability.

[0] https://people.inf.ethz.ch/troscoe/pubs/sosp09-barrelfish.pd...

Re:The SeL4 Microkernel: An Introduction [pdf] by naasking on Monday March 24, 2025 @09:49AM (#43461064)
"Safe enough" means "actually unsafe".
Re:The SeL4 Microkernel: An Introduction [pdf] by phendrenad2 on Wednesday March 26, 2025 @01:54AM (#43479229)
Yes, and bank vaults have doors.
Re:The SeL4 Microkernel: An Introduction [pdf] by sparkie on Sunday March 23, 2025 @05:00PM (#43455882)
To the best of my knowledge, seL4 is not AVX-512 aware. The AVX-512 state is not saved or restored on a context switch, which is clearly going to impact efficiency.

At present there's 16x64-bits of register state saved (128B), but if we were to have full support for the vectors, you need to potentially add 32x512-bits to the state (plus another 16 GP registers when APX arrives). Total state that needs moving from registers to memory/cache would jump to 2304B - a 1800% increase.

Give that memory is still the bottleneck, and cache is of limited size, a full context switch is going to have a big hit - and the main issue with microkernels is that a service you want to communicate with lives in another thread and address space. You have: app->kernel->service->kernel->app for a round-trip. If both app and service use the AVX-512 registers then you're going to have to save/restore more than half a page of CPU state up to 4 times, compared with up to 2 on the monolithic kernel which just does app->kernel->app.

The amount of CPU state only seems to be growing, and microkernels pay twice the cost.

Re:The SeL4 Microkernel: An Introduction [pdf] by Veserv on Sunday March 23, 2025 @05:39PM (#43456116)
The cost of moving 4 KB is miniscule. Assume a anemic basic desktop with a 2 GHz clock and 2 instructions per clock. You would be able to issue 4 billion 8-byte stores per second resulting 32 GB/s or 32 bytes per nanosecond. Memory bandwidth is going to be on the order of 40-60 GB/s for a basic desktop, so you will not run into memory bandwidth bottlenecks with the aforementioned instruction sequence. So, 4 KB of extra stores is a grand total of 128 additional nanoseconds.

In comparison, the average context switch time of Linux is already on the order of ~1,000 nanoseconds [1]. We can also see additional confirmation of the store overhead I computed as that page measures ~3 us for a 64 KB memcpy (load + store) which would be ~187 nanoseconds for 4 KB (load + store) where as the context saving operation is a 2 KB register -> store and a 2 KB load -> register.

So, your system call overhead only increases by 10 percentage points. Assuming you have a reasonably designed system that does not kill itself with system call overhead, spending the majority of the time actually handling the service request, then it constitutes a miniscule performance cost. For example, if you spend 90% of the time executing the service code, with only 10% in the actual overhead, then you only incur a 1% performance hit.

[1] https://eli.thegreenplace.net/2018/measuring-context-switchi...

Re:The SeL4 Microkernel: An Introduction [pdf] by vacuity on Sunday March 23, 2025 @07:11PM (#43456628)
I agree that a well-designed system for most use cases won't have performance issues, since we should not just be optimizing context switches but also things like kernel bypass mechanisms, mechanisms like io_uring, and various application-guided policies that will reduce context switches. Context switches are always a problem (the essential complexity of having granular protection), and moving an extra 4KB is not negligible depending on the workload, but we are not out of options. It will take more programmer effort, is all.
Re:The SeL4 Microkernel: An Introduction [pdf] by vacuity on Sunday March 23, 2025 @07:13PM (#43456636)
I appreciate your criticism; it is reasonable and relevant in the present and the future. I wrote a reply nearby in the thread[0]. I think it's mostly solveable, but I agree it's not trivial.

[0] https://news.ycombinator.com/item?id=43456628

Re:The SeL4 Microkernel: An Introduction [pdf] by arakageeta on Sunday March 23, 2025 @05:42PM (#43456128)
I’m not sure that seL4 even supports NUMA, so there are other tradeoffs to consider.
Re:The SeL4 Microkernel: An Introduction [pdf] by vacuity on Sunday March 23, 2025 @06:58PM (#43456571)
I think NUMA management is high level enough that in a microkernel it would be comfortably managed in userspace, unlike things relevant to performance-critical context switches. And seL4 is currently intended only for individual cores anyways.
Re:The SeL4 Microkernel: An Introduction [pdf] by nickpsecurity on Sunday March 23, 2025 @05:11PM (#43455941)
High-assurance security requires kernels clear or overwrite all shared state. That could become a covert, storage channel if one partition can write it and another read it. If so, it should be overwritten.
Re:The SeL4 Microkernel: An Introduction [pdf] by snvzz on Sunday March 23, 2025 @09:04PM (#43457083)
>AVX-512 and other x86 warts

While seL4 runs on x86, it is not recommended.

Effort seems to be focused on ARM and RISC-V, particularly the latter.

An argument could be made that x86's baggage makes it a particularly bad fit for offering the sort of guarantees seL4 does.