6 ms·

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

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.
  - mananaysiempre 3y ago
    IIRC the KeyKOS/EROS/CapROS tradition used capabilities for everything including the scheduler. Of course, pervasive persistence makes those systems somewhat esoteric (barring fresh builds, they never shut down or boot up, only go to sleep and wake up in new bodies; compare Smalltalk, etc.).
    - vacuity 3y ago
      Guess I'm too ignorant. I need to read up on these. I did know about the persistence feature. I think it's not terrible but also not great, and systems should be designed for being shut down and apps being closed.
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

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.
- mananaysiempre 3y ago
  IIRC the KeyKOS/EROS/CapROS tradition used capabilities for everything including the scheduler. Of course, pervasive persistence makes those systems somewhat esoteric (barring fresh builds, they never shut down or boot up, only go to sleep and wake up in new bodies; compare Smalltalk, etc.).
  - vacuity 3y ago
    Guess I'm too ignorant. I need to read up on these. I did know about the persistence feature. I think it's not terrible but also not great, and systems should be designed for being shut down and apps being closed.

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