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