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?
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@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@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.
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@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@sel4.systems https://sel4.systems/lists/listinfo/devel
So this basically means that the microkernel has its own driver code for the timing hardware? On Wed, Nov 11, 2015 at 1:05 AM, Harry Butterworth <heb1001@gmail.com> wrote:
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@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@sel4.systems https://sel4.systems/lists/listinfo/devel
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.
participants (4)
-
Gernot Heiser -
Gerwin Klein -
Harry Butterworth -
Raymond Jennings