10 Years SeL4: Still the Best, Still Getting Better

Re:10 Years SeL4: Still the Best, Still Getting Better by msjyoo on Wednesday August 07, 2019 @11:38AM (#20635689)

That's not quite true. It's not solely because seL4 does little. seL4 maintains low interrupt latency through "preemption points" - basically points where the kernel can and can only context-switch while maintaining global consistency.

Keeping in mind I'm not an expert on this, I dug up these papers when I was vaguely looking, they may be useful to you:

"Improving Interrupt Response Time in a Verifiable Protected Microkernel" https://ts.data61.csiro.au/publications/nicta_full_text/5391...

"To Preempt or Not To Preempt, That Is the Question" http://ts.csiro.au/publications/nicta_full_text/5859.pdf

[ Parent | on HN ]

Re:10 Years SeL4: Still the Best, Still Getting Better by repolfx on Wednesday August 07, 2019 @02:29PM (#20637450)

Thanks, that's super helpful.

[ Parent | on HN ]

Re:10 Years SeL4: Still the Best, Still Getting Better by snvzz on Thursday August 08, 2019 @02:34AM (#20642343)

AIUI there's only one such preemption point, in some resume-able operation to do with cleanup. Every other operation is short enough.

Thus interrupt latency is guaranteed to be very low, even if the interrupt happens while the microkernel is running.

It is my intuition that the "it's not a RTOS" has to come from something else, like some non-implemented API that's expected in an RTOS or the like. The required services might actually be implementable as non-privileged tasks.

[ Parent | on HN ]

Re:10 Years SeL4: Still the Best, Still Getting Better by repolfx on Thursday August 08, 2019 @02:00PM (#20646893)

Maybe it's just slight conservatism. If all existing RTOS' have pre-emptible kernels and yours doesn't, perhaps you'd rather let the market decide you've built an RTOS rather than stating you have and risking an argument over terminology.

[ Parent | on HN ]