It depends on your use case. If you are looking to monitor the execution times of threads
for debugging and/or benchmarking purposes, you can use our kernel benchmarking support,
detailed here .
Otherwise, you could consider using the mcs branch of the kernel, which allows you to
obtain the execution time of a thread via the seL4_SchedContext_Consumed invocation .
If you need to use the master branch of the kernel, then you would need to intercept the
scheduler on thread switch, by running a high priority thread which enables other
From: Devel <devel-bounces(a)sel4.systems> on behalf of Mr. Peace
Sent: Monday, 9 July 2018 3:34 AM
Subject: [seL4] seL4 - getting the execution time of different threads
I was wondering how you do get the execution time in seL4 if you are using multiple
In the initial thread I can use the timer as it is shown in the tutorial about timers
since I do have the bootinfo, vka, allocman and so on.
But how do I use the timer to measure the execution time of the other threads without
stopping their execution to "pull" the time from the initial thread? Is it
possible to share the timer or create new ones in the other threads? Or is there another
way to measure the execution time?
Some background information:
The threads have different VSpace's and CSpace's.
Used tutorials: seL4-tutorial 4, seL4-tutorial timer.
The other threads do not have a bootinfo in their environment.