On 29 Nov 2023, at 17:49, chenpingyuan--- via Devel devel@sel4.systems wrote:

I'm reading the code of seL4 kernel, but I got confused how seL4 could help to avoid priority inversion. seL4 itself doesn't change the priority of TCB at the kernel level, does it mean that seL4 leaves the user level to handle priority inversion?

Preventing priority inversion isn’t the kernel’s job, that’s a question of design.

In general, priority inversion cannot be prevented if you have non-preemtible critical sections, but there are approaches to limit it, specifically protocols like PIP, OPCP, IPCP. The kernel’s job is to provide the mechanisms for implementing your protocol.

A properly configured passive server (using the MCS configuration of seL4) will automatically implement IPCP.

Gernot