seL4 is controlling the timer device. In the current release version, scheduling is
tick-based, i.e. there’s a periodic interrupt that feeds into the scheduler.
We’re looking at a tick-less variant (also via timer interrupt), but that might be a while
before it makes it into the release.
On 11 Nov 2015, at 9:19 am, Raymond Jennings
Where does the seL4 microkernel actually get the timing information it needs to enforce
I can imagine some sort of interrupt or I/O access is required to get it from the raw
How does it get from the timing hardware to the scheduling code?
Devel mailing list
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.