On 1 Jan 2022, at 00:14, 刘跃 Jeff Liu <jeffliuyue(a)didiglobal.com> wrote:
As we know, seL4 is a non preemptive kernel. Is it because the kernel of seL4 is an event
There are multiple reasons for using an event-based approach in seL4 (note that its
predecessor L4 kernels were process-based). The main reason seL4 is event based is that
this makes it much easier to reason about correctness. It also reduces the kernel’s memory
footprint. It is performance neutral.
The design and implementation of seL4, and the rationale behind it, are discussed at
length in the relevant publications, specifically:
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.
First off, neither VxWorks nor QNX have any correctness proofs, unlike seL4 which has a
proof of implementation correctness, plus a lot of other formal verification.
However, despite seL4 having a degree of assurance that is completely out of reach for
those other systems, it is also much faster (in terms of average-case performance). Data I
have seen (which is quite dated) about QNX and other non-L4 microkernels show them
generally about a factor 10 slower in IPC performance.
In other words, those system are not in the same league as seL4, neither in assurance nor
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?
seL4 is, to my knowledge, still the only protected-mode OS kernel with a complete and
sound WCET analysis (based on static analysis, although on a by now pretty dated
processor). As such there is no comparison. I did (years ago) read a report form QNX about
their WCILs, and this was the usual unsound approach of loading the system up, measuring
latencies, adding a fudge factor, and calling that “WCIL”. I wouldn’t want my live to
depend on that.
For details about seL4’s WCET analysis, see
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.
Optimisation of seL4 WCIL is discussed in