4 ms·

For a modern example, there's seL4. I believe it does no dynamic memory allocation. It's also formally verified for various properties. (Arguably?) its biggest

For a modern example, there's seL4. I believe it does no dynamic memory allocation. It's also formally verified for various properties. (Arguably?) its biggest contribution to kernel design is the pervasive usage of capabilities to securely but flexibly export control to userspace.

adastra22 3y ago
Capabilities are important, but I don’t think that was introduced by seL4. Mach (which underlies macOS) has the same capability-based system.
- vacuity 3y ago
  I didn't say seL4 introduced capabilities. However, to my knowledge, seL4 was the first kernel to show that pervasive usage of capabilities is both feasible and beneficial.
  - monocasa 3y ago
    The other L4s before it showed that caps are useful and can be implemented efficiently.
    - vacuity 3y ago
      https://dl.acm.org/doi/pdf/10.1145/2517349.2522720 https://dl.acm.org/doi/pdf/10.1145/2517349.2522720 " 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 ﬁxed 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.
      - naasking 3y ago
        seL4 was heavily inspired by prior capability based operating systems like EROS (now CapROS) and Coyotos. Tying all storage to capabilities was core to those designs.
  - adastra22 3y ago
    There's quite a history of capabilities-based research OS's that culminated in, but did not start with L4 (of which seL4 is a later variant).
    - vacuity 3y ago
      Yes, but I believe seL4 took it to the max. I may be wrong on that count, but I think seL4 is unique in that it leverages capabilities for pretty much everything except the scheduler. (There was work in that area, but it's incomplete.)
      - adastra22 3y ago
        L4 was developed in the 90's. Operating Systems like Amoeba, which were fundamentally capability-based to a degree that even exceeds L4, were a hot research topic in the 80's. 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 :(
        josephg 3y ago
        How did it achieve its speed? My understanding was that microkernel architectures were fundamentally slower than monolithic kernels because context switching is slower than function calls. How did L4 manage to be the fastest?
        vacuity 3y ago
        Two factors are the small working set (fit the code and data in cache) and heavily optimized IPC. The IPC in L4 kernels is "a context switch with benefits": in the best case, the arguments are placed in registers and the context is switched. Under real workloads, microkernels probably will be slower, but not by much.
  - Animats 3y ago
    No, that was KeyKOS, which was way ahead of its time.[1] Norm Hardy was brilliant but had a terrible time getting his ideas across. [1] https://en.wikipedia.org/wiki/KeyKOS https://en.wikipedia.org/wiki/KeyKOS
_kb 3y ago
And unfortunately had its funding dumped because it wasn’t shiny AI.
- snvzz 3y ago
  Its 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 ago
    The 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 ago
      Note 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/

adastra22 3y ago

Capabilities are important, but I don’t think that was introduced by seL4. Mach (which underlies macOS) has the same capability-based system.

vacuity 3y ago
I didn't say seL4 introduced capabilities. However, to my knowledge, seL4 was the first kernel to show that pervasive usage of capabilities is both feasible and beneficial.
- monocasa 3y ago
  The other L4s before it showed that caps are useful and can be implemented efficiently.
  - vacuity 3y ago
    https://dl.acm.org/doi/pdf/10.1145/2517349.2522720 https://dl.acm.org/doi/pdf/10.1145/2517349.2522720 " 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 ﬁxed 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.
    - naasking 3y ago
      seL4 was heavily inspired by prior capability based operating systems like EROS (now CapROS) and Coyotos. Tying all storage to capabilities was core to those designs.
- adastra22 3y ago
  There's quite a history of capabilities-based research OS's that culminated in, but did not start with L4 (of which seL4 is a later variant).
  - vacuity 3y ago
    Yes, but I believe seL4 took it to the max. I may be wrong on that count, but I think seL4 is unique in that it leverages capabilities for pretty much everything except the scheduler. (There was work in that area, but it's incomplete.)
    - adastra22 3y ago
      L4 was developed in the 90's. Operating Systems like Amoeba, which were fundamentally capability-based to a degree that even exceeds L4, were a hot research topic in the 80's. 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 :(
      - josephg 3y ago
        How did it achieve its speed? My understanding was that microkernel architectures were fundamentally slower than monolithic kernels because context switching is slower than function calls. How did L4 manage to be the fastest?
        vacuity 3y ago
        Two factors are the small working set (fit the code and data in cache) and heavily optimized IPC. The IPC in L4 kernels is "a context switch with benefits": in the best case, the arguments are placed in registers and the context is switched. Under real workloads, microkernels probably will be slower, but not by much.
- Animats 3y ago
  No, that was KeyKOS, which was way ahead of its time.[1] Norm Hardy was brilliant but had a terrible time getting his ideas across. [1] https://en.wikipedia.org/wiki/KeyKOS https://en.wikipedia.org/wiki/KeyKOS

_kb 3y ago

And unfortunately had its funding dumped because it wasn’t shiny AI.

snvzz 3y ago
Its 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 ago
  The 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 ago
    Note 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/