Does seL4 support periodic thread

ぷ风过无痕??

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!!

Attachments:

attachment.html (text/html — 2.1 KB)

Show replies by date

Anna Lyons

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@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.

Gerwin Klein

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 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

3310

Age (days ago)

3311

Last active (days ago)

List overview

Download

2 comments

3 participants

participants (3)

Anna Lyons
Gerwin Klein
ぷ风过无痕??