4 ms·
And unfortunately had its funding dumped because it wasn’t shiny AI.
by _kb 3y ago
And unfortunately had its funding dumped because it wasn’t shiny AI.
- snvzz 3y agoIts old source of funding. And it was much more complex[0] than that. seL4 is now a healthy non-profit, seL4 foundation[1]. 0. https://microkerneldude.org/2022/02/17/a-story-of-betrayal-csiros-war-on-ts/ https://microkerneldude.org/2022/02/17/a-story-of-betrayal-c... 1. https://microkerneldude.org/2022/03/22/ts-in-2022-were-back/ https://microkerneldude.org/2022/03/22/ts-in-2022-were-back/
- Animats 3y agoThe trouble with L4 is that it's so low-level you have to put another OS on top of it to do anything Which usually means a bloated Linux. QNX offers a basic POSIX interface, implemented mostly as libraries.
- snvzz 3y agoNote that L4 and seL4 are very different kernels. They represent the 2nd generation and 3rd generation of microkernels respectively. 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. 0. https://www.genode.org/ https://www.genode.org/