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