strange response time question

Gernot Heiser gernot at
Wed Aug 6 02:36:11 CEST 2014

MP as in multiprocessor seL4? There’s no released multiprocessor version of seL4.


On 6 Aug 2014, at 10:18 , Daniel Potts <danielp at> wrote:

> What do your MP numbers look like for WCET?
>> On 6 Aug 2014, at 9:45 am, "Gernot Heiser" <gernot at> wrote:
>>> On 6 Aug 2014, at 7:19 , Yuxin Ren <ryx at> wrote:
>>> Hi,
>>> Sorry, it's my typo.
>>> The worse case is 200us.
>>> In my test, before the client sends IPC, I record the time using rdtsc.
>>> When the server receives this IPC, I also do rdtsc.
>>> The difference between this is the response time. I run this many iterations and the maximum value is the worse case result.
>>> I filter out the timer interrupt, but do not flush the cache and tlb.
>> A worst case of 200µs isn’t bad, if it’s really the worst case. The problem is that you can never be sure you caught the worst case, and most likely you didn’t. When we started analysing seL4, we found pathological cases where the worst case (on an otherwise very fast kernel) was about a second. These bad cases typically happen when dismantling complex data structures, eg revoking derived capabilities. You probably didn’t test that.
>> For seL4 we found we could get the safe upper bound of the WCET to around 300µs (on ARM11), the real worst case is probably around half that (but you can’t be sure).
>> I think it should be possible to get it down to 10–20µs, but that would complicate the kernel code significantly (and, in seL4’s case, would be tough to verify).
>> Gernot
>> _______________________________________________
>> l4-hackers mailing list
>> l4-hackers at

More information about the l4-hackers mailing list