4 ms·

seL4 at the moment doesn't have kernel interrupts. The kernel relies on run-to-completion and "incremental consistency" partly because IPC in seL4 is already sh

by msjyoo 7y ago

seL4 at the moment doesn't have kernel interrupts. The kernel relies on run-to-completion and "incremental consistency" partly because IPC in seL4 is already short so the time window for a kernel interrupt to be needed is also correspondingly small, and because it makes proofs easier. Of course, this means there's possibilities of long tail latency for interrupts to be delivered to userspace if the kernel needs to run a long operation.

repolfx 7y ago
My understanding of seL4 is that the kernel never really needs to run a long operation because it does so very little. For instance filesystems would be a usermode process, along with nearly all drivers. Isn't that why the MCS stuff works - the kernel may not be able to interrupt itself but that doesn't matter because it can interrupt userspace, which is where 99% of traditional kernel code ends up?
- msjyoo 7y ago
  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.pdf 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 http://ts.csiro.au/publications/nicta_full_text/5859.pdf
  - repolfx 7y ago
    Thanks, that's super helpful.
    - snvzz 7y ago
      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.
      - repolfx 7y ago
        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.

by msjyoo 7y ago

repolfx 7y ago

My understanding of seL4 is that the kernel never really needs to run a long operation because it does so very little. For instance filesystems would be a usermode process, along with nearly all drivers. Isn't that why the MCS stuff works - the kernel may not be able to interrupt itself but that doesn't matter because it can interrupt userspace, which is where 99% of traditional kernel code ends up?

msjyoo 7y ago
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.pdf 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 http://ts.csiro.au/publications/nicta_full_text/5859.pdf
- repolfx 7y ago
  Thanks, that's super helpful.
  - snvzz 7y ago
    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.
    - repolfx 7y ago
      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.