26 ms·
>They can use most L4-based microkernels, mostly their own, or NOVA or Fiasco. Correct, Genode supports several kernels, including but not limited to those. >
by snvzz 9mo ago
>They can use most L4-based microkernels, mostly their own, or NOVA or Fiasco.
Correct, Genode supports several kernels, including but not limited to those.
>Secure capabilities are a feature of all L4 kernels.
Not accurate. Liedtke's L4 does not do capabilities.
It would be more accurate to say that most modern L4-like kernels do.
The highlight is seL4, specifically because it offers those formal guarantees while also being the fastest.
- rurban 9mo agoWho cares about formal guarantees when the other kernels are much better and provide a much better infrastructure. The kernel itself is minimal. Fiasco can be real-time.
- snvzz 9mo ago>Who cares about formal guarantees Projection. You might not care, but extrapolating is a mistake. Public as well as private sector with high assurance needs have gathered around seL4 foundation due to its proofs and technical excellence. >are much better Subjective. What is your criteria? >Fiasco can be real-time. Depends on your definition of real-time. Hard realtime requires guarantees that the deadlines will always be met. The only non-toy kernel that offers proof of WCET is seL4. If soft realtime is all you need, then Linux with PREEMPT_RT suffices.