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!!
Hi Bryan, seL4 does not currently support periodic threads. You can implement support for this at user level with a user level timer driver (there are some implemented in libplatsupport, with seL4 specific wrappers in libsel4platsupport). Periodic threads are on our roadmap and will be released with the realtime extensions for seL4 (see https://sel4.systems/Info/Roadmap/). We may do a pre-release of the seL4 source with realtime extensions to the public soon, however that will not yet be verified. Feel free to play around with the kernel scheduler yourself :). Thanks, Anna. On 26/11/2015 7:14 pm, ぷ风过无痕?? wrote:
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 Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Hi Bryan, in terms of verification: if you follow Anna’s suggestion of a user-level timer driver, the verification is still valid. If you change the scheduler code, the verification will not apply any more. Cheers, Gerwin
On 27 Nov 2015, at 10:34 am, Anna Lyons <Anna.Lyons@nicta.com.au> wrote:
Hi Bryan,
seL4 does not currently support periodic threads. You can implement support for this at user level with a user level timer driver (there are some implemented in libplatsupport, with seL4 specific wrappers in libsel4platsupport).
Periodic threads are on our roadmap and will be released with the realtime extensions for seL4 (see https://sel4.systems/Info/Roadmap/). We may do a pre-release of the seL4 source with realtime extensions to the public soon, however that will not yet be verified.
Feel free to play around with the kernel scheduler yourself :).
Thanks, Anna.
On 26/11/2015 7:14 pm, ぷ风过无痕?? wrote:
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 Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
participants (3)
-
Anna Lyons -
Gerwin Klein -
ぷ风过无痕??