Hi, I am trying to understand the timer design of both seL4 as a kernel and as a hypervisor on ARM architecture. I understand that in both cases, seL4 uses a timer in order to preempt its threads. This means that seL4 must keep the control over that timer and cannot let threads use it directly. I also understand that seL4 does not provide any timer API to its threads. It seems then that the intended use is to implement a timer driver in userland in order for other application to access timing functions. But this timer driver cannot access the same timer as seL4. Does this mean that at least two physical timers (or at least two physical timer interfaces) are necessary? ARM virtualization extensions offers a virtual timer to be used by VMs and which is implemented with an offset register. They also offer different timers (one for an hypervisor, one for kernel/application and one for the virtual timer). It seems that the current seL4 as a hypervisor project does not use these extenstions. Do they? If not why? Thank you for your answers