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;