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 <[email protected]> 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 > [email protected] > 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. _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
