[seL4] Re: getKernelWcetUs: where does the 10us return value come from?

On 3 Dec 2021, at 19:56, Jack Chen via Devel <devel@sel4.systems> wrote:

Hope someone will answer my second question (Rephrasing my question: is checkBudget part of the implementation of temporal partitioning, with +WCET for padding?)

It’s to ensure there’s enough time left for handling the system call without violating budget constraints. Else you could help yourself to extra budget by a syscall just before budget expiry. Gernot