On 1 Jan 2022, at 00:14, 刘跃 Jeff Liu jeffliuyue@didiglobal.com wrote:
Hi; As we know, seL4 is a non preemptive kernel. Is it because the kernel of seL4 is an event based model?
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: https://trustworthy.systems/publications/nictaabstracts/Klein_AEMSKH_14.abst... https://trustworthy.systems/publications/nictaabstracts/Heiser_Elphinstone_1...
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 in performance.
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 https://trustworthy.systems/publications/csiroabstracts/Sewell_KH_17.abstrac...
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 https://trustworthy.systems/publications/nictaabstracts/Blackham_SH_12.abstr...
Gernot