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