Hacker News Reader

Physical-like prices?

msjyooon 10 Years SeL4: Still the Best, Still Getting Better

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

msjyooon 10 Years SeL4: Still the Best, Still Getting Better

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.

msjyooon Please do not attempt to simplify this code

Wow, that site is beautiful beyond words.