Re: [seL4] timing

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