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 _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
