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 <[email protected]> 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 <[email protected]> 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 >> [email protected] >> https://sel4.systems/lists/listinfo/devel >> >> >
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
