Hmm, what do you mean by measuring the time?

You can measure the typical execution time of various system calls easily enough by checking the CPU cycle counter.

There is an internal "sel4bench" project which is similar to "sel4test" but measures timing information of some system calls. My understanding is that this will be released at some point in the near future.

It's also possible to calculate the worst-case execution time of the kernel for some platforms. There's been a lot of research work on this http://ssrg.nicta.com.au/projects/TS/realtime.pml by various people at Data61/NICTA. It's probably possible to replicate for some platform of interest, but it might be quite difficult to do.

Cheers,
Thomas.

On 29/03/16 14:06, xurongfeik wrote:

Hello，everyone：

When given a specific platform， is it possible to measure the execution time of seL4 API？

Anyone who has the relative data please send it to me， many thanks！！

--
许荣飞
Rongfei Xu

北京航空航天大学

Beihang University
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.