3 ms·
SeL4 is a capability based operating system toolkit, entirely implemented in C. The core operating system is just a few thousand lines of code. Its even mathema
by josephg 1y ago
SeL4 is a capability based operating system toolkit, entirely implemented in C. The core operating system is just a few thousand lines of code. Its even mathematically proven to be bug free - which is totally insane.
It even uses a capability to allocate (assign) memory. So you typically have a microservice (userland process) in charge of memory on the whole system. Other processes get heap memory allocated to them by asking that service for it. (Though typically you'll allocate large blocks, and divide it up using a normal allocator).
- nmgycombinator 1y agoI think Apple uses an L4 variant for their SEP co-processor, though I'm not sure if it's that specific one. Sounds like another OS I'll probably have to do a deep dive into at some point.
- SSLy 1y agoThey also run L4 variants below and besides XNU, on same cores as the rest https://randomaugustine.medium.com/on-apple-exclaves-d683a2c37194 https://randomaugustine.medium.com/on-apple-exclaves-d683a2c...
- nmgycombinator 1y agoOoh! Thanks for the links!