Hi everyone,I have some questions about seL4's timer. I know seL4 is controlling the
timer device. In the current release version, scheduling is tick-based, there's a
periodic interrupt that feeds into the scheduler. I wanna know if seL4 support periodic
thread. I want to implement a periodic process in Refos which is above seL4 kernel.And, if
seL4 does not support periodic thread, could I modify the kernel scheduler? Does it
influences formal verification? I find that Refos modifies _thread_state_t
enumeration-type variables (kernel\include\object\structures.h ). Does it influences
formal verification? Thank you so much!!