If you look at the abstract spec starting at call_kernel in Syscall_A and working in towards timer_tick in Interrupt_A, you'll see that a timer interrupt results in a call to timer_tick which decrements the current thread's time slice and interacts with the scheduler through reschedule_required if the thread or domain time slice expires. You could investigate to see how closely the C code corresponds. On 11 November 2015 at 16:19, Raymond Jennings <shentino(a)gmail.com> wrote:

On 12 Nov 2015, at 19:38 , Raymond Jennings <shentino@gmail.com<mailto:shentino@gmail.com>> wrote: So this basically means that the microkernel has its own driver code for the timing hardware? Yes. The microkernel has two drivers: the interrupt controller (needed to assign interrupts to handlers) and a timer (needed for preemption). When compiled for debugging there’s also a serial driver. Gernot ________________________________ 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.