3 ms·
The other L4s before it showed that caps are useful and can be implemented efficiently.
by monocasa 3y ago
The other L4s before it showed that caps are useful and can be implemented efficiently.
- vacuity 3y agohttps://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 fixed 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 agoseL4 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.