Hi; As we know, seL4 is a non preemptive kernel. Is it because the kernel of seL4 is an event based model? Then why not use the thread based kernel? As far as I know, VxWorks and QNX are thread based. SeL4's view is that for non preemptive kernel, real-time performance focuses on WCET, and the faster kernel does not guarantee the real-time performance of the system. I partially agree with this view. I want to know if there are real-time comparison data?, The comparison test with VxWorks or QNX is about the real-time performance of the system. the worst case interrupt latency is the sum of both the longest region with interrupts disabled, and the time to dispatch an interrupt to a user thread. How are these two parts of time calculated? Is it the method of WCET static analysis? And Then how to improve the interrupt response time, What is the specific method to reduce interrupt latency? I think most users of seL4 are more concerned about this. I look forward to communicating and discussing with you, experts. Thanks;