timing - Devel - lists.sel4.systems

newer
CAmkES-vm Build Question

timing

older
CAmkES Tutorial

Raymond Jennings

11 Nov 2015 11 Nov '15

7:19 p.m.

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?

Attachments:

attachment.html (text/html — 342 bytes)

Reply

Sign in to reply online Use email software

Show replies by date

Gerwin Klein

11 Nov 11 Nov

8:03 p.m.

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.

Reply

Sign in to reply online Use email software

Harry Butterworth

8:05 p.m.

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

Reply

Sign in to reply online Use email software

Raymond Jennings

12 Nov 12 Nov

7:38 p.m.

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

Reply

Sign in to reply online Use email software

Gernot Heiser

13 Nov 13 Nov

3:19 a.m.

On 12 Nov 2015, at 19:38 , Raymond Jennings 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.

Reply

Sign in to reply online Use email software

3325

Age (days ago)

3326

Last active (days ago)

Download

4 comments

4 participants

tags

participants (4)

Gernot Heiser
Gerwin Klein
Harry Butterworth
Raymond Jennings