seL4 is just a micro-kernel, It is not an operating system, even the timer-ticks for the scheduler, is a bared interrupt, It hasn’t a mechanism like jiffies in Linux. If you want to measure the execution time, the accuratly method is Profile-Trace supported by hardware development board, It is very expensive.

发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 xurongfeik
发送时间: 2016年3月31日 14:53
收件人: devel@sel4.systems
主题: [seL4] seL4 Documentation/Tutoria

Hi folks

Is there any Documentation/Tutorial about execution time for typical invocations of the seL4 system calls?

Thanks!

--
许荣飞

Rongfei Xu

北京航空航天大学

Beihang University