4 ms·

Seeing these results touted as being pretty good makes me wonder why we haven't fully adopted microkernels yet. Their singular disadvantage, which is the need f

Seeing these results touted as being pretty good makes me wonder why we haven't fully adopted microkernels yet. Their singular disadvantage, which is the need for two IPC calls vs one for a monolithic kernel, is completely irrelevant in comparison to these numbers. The average IPC cost of an L4 IPC call is about 500 cycles, which is about half a microsecond on a 1ghz processor. Cache locality is a big deal, and L4, which can fit entirely within a core's l2 cache, is king when it comes to cache locality. And you don't have to worry about memory safety either. Memory safety has been formally proven as part of the SeL4 spec.

pa7ch 6y ago
I've also wondered why we haven't seen more industrial effort around using sel4. Seems like it'd be perfect for mission critical firmware in cars and such too. For replacing linux, I guess there is still a lot of effort that would be required, but it seems worth it from my admittedly surface viewpoint.
Matthias247 6y ago
> Seeing these results touted as being pretty good makes me wonder why we haven't fully adopted microkernels yet. Their singular disadvantage, which is the need for two IPC calls vs one for a monolithic kernel, is completely irrelevant in comparison to these numbers. And that's even the worst case of synchronous/blocking calls. With different API design - e.g. asynchronous interactions as done with io_uring or IOCP - the latency becomes less important as long as the overall efficiency and thereby throughput is high.
vlovich123 6y ago
Depends on who "we" is. Apple's OS is largely a microkernel design & that ships on billions of devices. Build services for that OS at Apple from a safety/security/performance/battery life perspective is a dream compared to other OSes. Granted outside of that it's a bit rarer.
- ksec 6y ago
  >Apple's OS is largely a microkernel design They are hybrid design, or some would even refer them to monolithic. Definitely not microkernel, although they are moving in that direction with DriverKit and other kit initiative.
  - vlovich123 6y ago
    True they are hybrid but most drivers lived in user space except for ultra critical performance stuff if I recall correctly (mainly graphics stuff if I recall correctly but I never took a complete inventory). IPC was a core part of how both drivers, system daemons, and apps communicated with each other (with thin shim APIs to make it friendlier). It was pretty great at how consistent a lot of it was.
sitkack 6y ago
Hypervisors are the microkernels that are socially acceptable.
knaq 6y ago
That is 500 cycles without mitigation for CPU bugs, and without considering the non-local performance effects. Non-local performance effects arise from TLB and other cache invalidation, which is required when changing from one task to another. You can't avoid that without putting everything in the same address space, which would make the system a fake microkernel. Fake microkernels have the less-readable code of microkernel design but without any benefits other than buzzword compliance. CPU bugs like Meltdown and Spectre mean that every IPC now needs to blow away all sorts of caches and prediction. For example, you wipe out branch history. The cycles spent during the IPC call are only a tiny portion of the cost. The loss of cache content (TLB, branch history, data cache, code cache, etc.) greatly slows down the CPU.
- mangamadaiyan 6y ago
  Oh, I wouldn't dismiss "fake microkernels" so completely. One of them used to power a rather popular (proprietary) NAS Filer. I don't have a reference -- I believe this little gem never found its way into a publication (though the file system that ran on top of it did: https://www.cs.princeton.edu/courses/archive/fall04/cos318/docs/netapp.pdf https://www.cs.princeton.edu/courses/archive/fall04/cos318/d...).
- pjmlp 6y ago
  That is the thing, when you put all mitigations in place, the supposed performance gain is already out of the window. And there is the whole point that many of the performance issues with microkernels have long been solved.
- darksaints 6y ago
  Well, for one, those bugs aren't an issue on non-shared devices, and anything else outside of x86. That is not insignificant...that is still the majority of devices. Two, the benchmarks for IPC usually include the cost of cache invalidation. This one [0] for SeL4 clearly shows the difference on Skylake for the kernels compiled with Meltdown mitigations. Still in the sub-microsecond range. [0] https://sel4.systems/About/Performance/home.pml https://sel4.systems/About/Performance/home.pml

pa7ch 6y ago

I've also wondered why we haven't seen more industrial effort around using sel4. Seems like it'd be perfect for mission critical firmware in cars and such too. For replacing linux, I guess there is still a lot of effort that would be required, but it seems worth it from my admittedly surface viewpoint.

Matthias247 6y ago

> Seeing these results touted as being pretty good makes me wonder why we haven't fully adopted microkernels yet. Their singular disadvantage, which is the need for two IPC calls vs one for a monolithic kernel, is completely irrelevant in comparison to these numbers. And that's even the worst case of synchronous/blocking calls. With different API design - e.g. asynchronous interactions as done with io_uring or IOCP - the latency becomes less important as long as the overall efficiency and thereby throughput is high.

vlovich123 6y ago

Depends on who "we" is. Apple's OS is largely a microkernel design & that ships on billions of devices. Build services for that OS at Apple from a safety/security/performance/battery life perspective is a dream compared to other OSes. Granted outside of that it's a bit rarer.

ksec 6y ago
>Apple's OS is largely a microkernel design They are hybrid design, or some would even refer them to monolithic. Definitely not microkernel, although they are moving in that direction with DriverKit and other kit initiative.
- vlovich123 6y ago
  True they are hybrid but most drivers lived in user space except for ultra critical performance stuff if I recall correctly (mainly graphics stuff if I recall correctly but I never took a complete inventory). IPC was a core part of how both drivers, system daemons, and apps communicated with each other (with thin shim APIs to make it friendlier). It was pretty great at how consistent a lot of it was.

sitkack 6y ago

Hypervisors are the microkernels that are socially acceptable.

knaq 6y ago

That is 500 cycles without mitigation for CPU bugs, and without considering the non-local performance effects. Non-local performance effects arise from TLB and other cache invalidation, which is required when changing from one task to another. You can't avoid that without putting everything in the same address space, which would make the system a fake microkernel. Fake microkernels have the less-readable code of microkernel design but without any benefits other than buzzword compliance. CPU bugs like Meltdown and Spectre mean that every IPC now needs to blow away all sorts of caches and prediction. For example, you wipe out branch history. The cycles spent during the IPC call are only a tiny portion of the cost. The loss of cache content (TLB, branch history, data cache, code cache, etc.) greatly slows down the CPU.

mangamadaiyan 6y ago
Oh, I wouldn't dismiss "fake microkernels" so completely. One of them used to power a rather popular (proprietary) NAS Filer. I don't have a reference -- I believe this little gem never found its way into a publication (though the file system that ran on top of it did: https://www.cs.princeton.edu/courses/archive/fall04/cos318/docs/netapp.pdf https://www.cs.princeton.edu/courses/archive/fall04/cos318/d...).
pjmlp 6y ago
That is the thing, when you put all mitigations in place, the supposed performance gain is already out of the window. And there is the whole point that many of the performance issues with microkernels have long been solved.
darksaints 6y ago
Well, for one, those bugs aren't an issue on non-shared devices, and anything else outside of x86. That is not insignificant...that is still the majority of devices. Two, the benchmarks for IPC usually include the cost of cache invalidation. This one [0] for SeL4 clearly shows the difference on Skylake for the kernels compiled with Meltdown mitigations. Still in the sub-microsecond range. [0] https://sel4.systems/About/Performance/home.pml https://sel4.systems/About/Performance/home.pml