11 Nov
2015
11 Nov
'15
10:05 a.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 <shentino(a)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(a)sel4.systems
https://sel4.systems/lists/listinfo/devel