26 Nov
2015
26 Nov
'15
7:14 p.m.
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!!
27 Nov
27 Nov
8:34 a.m.
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(a)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.
12:09 p.m.
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(a)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(a)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(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
2446
days inactive
2447
days old
2 comments
3 participants
participants (3)
-
Anna Lyons -
Gerwin Klein -
ぷ风过无痕??