Hi Raymond,
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.
Cheers,
Gerwin
On 11 Nov 2015, at 9:19 am, Raymond Jennings
<shentino(a)gmail.com> wrote:
Where does the seL4 microkernel actually get the timing information it needs to enforce
scheduling decisions?
I can imagine some sort of interrupt or I/O access is required to get it from the raw
hardware.
How does it get from the timing hardware to the scheduling code?
_______________________________________________
Devel mailing list
Devel(a)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.