strange response time question

Gernot Heiser gernot at cse.unsw.edu.au
Wed Aug 6 01:45:15 CEST 2014


On 6 Aug 2014, at 7:19 , Yuxin Ren <ryx at gwmail.gwu.edu> 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


More information about the l4-hackers mailing list