4 ms·

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

by ryao 2y ago

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.

mastax 2y ago
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
- ryao 2y ago
  Nice use of Latin. mihi placet.
- nine_k 2y ago
  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.
  - vacuity 2y ago
    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?
    - necovek 2y ago
      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?
pjmlp 2y ago
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.
netbsdusers 2y ago
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.pdf 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).
- microtonal 2y ago
  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/osfmk https://github.com/apple-oss-distributions/xnu/tree/main/osf...
  - rhet0rica 2y ago
    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.
    - p_ing 2y ago
      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/osfmk/ipc/ipc_init.h https://github.com/apple-oss-distributions/xnu/blob/main/osf... EDIT: Apple calls out Mach 3.0. https://developer.apple.com/library/archive/documentation/Darwin/Conceptual/KernelProgramming/Architecture/Architecture.html https://developer.apple.com/library/archive/documentation/Da... https://developer.apple.com/library/archive/documentation/Darwin/Conceptual/KernelProgramming/Mach/Mach.html#//apple_ref/doc/uid/TP30000905-CH209-TPXREF101 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.
el_pollo_diablo 2y ago
> seL4 is the only microkernel that has a proof of correctness ProvenCore (https://provenrun.com/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).

by ryao 2y ago

mastax 2y ago

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

ryao 2y ago
Nice use of Latin. mihi placet.
nine_k 2y ago
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.
- vacuity 2y ago
  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?
  - necovek 2y ago
    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?

pjmlp 2y ago

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.

netbsdusers 2y ago

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

microtonal 2y ago
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/osfmk https://github.com/apple-oss-distributions/xnu/tree/main/osf...
- rhet0rica 2y ago
  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.
  - p_ing 2y ago
    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/osfmk/ipc/ipc_init.h https://github.com/apple-oss-distributions/xnu/blob/main/osf... EDIT: Apple calls out Mach 3.0. https://developer.apple.com/library/archive/documentation/Darwin/Conceptual/KernelProgramming/Architecture/Architecture.html https://developer.apple.com/library/archive/documentation/Da... https://developer.apple.com/library/archive/documentation/Darwin/Conceptual/KernelProgramming/Mach/Mach.html#//apple_ref/doc/uid/TP30000905-CH209-TPXREF101 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.

el_pollo_diablo 2y ago

> seL4 is the only microkernel that has a proof of correctness ProvenCore (https://provenrun.com/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).