[seL4] timing

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?