Re: [seL4] timing

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 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@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.