Sporadic Server Implementation Details
Hi all, I hope this is the right forum to be posting this question. I've reached out to Anna Lyons, the first author on the EuroSys 2018 "Scheduling Context Capabilities" paper (https://ts.data61.csiro.au/publications/csiro_full_text//Lyons_MAH_18.pdf), but I do not know if her listed email address is still active. I want to ask for more clarification on the sporadic server implementation in seL4. My interpretation of how the Lyons et al. paper describes the implementation is different than my understanding of the sporadic server definition as described by Sprunt et al. in 1989 (https://link.springer.com/article/10.1007/BF02341920). However, looking at the seL4 kernel source code, it seems that the actual implementation follows very closely with the improved POSIX sporadic server mechanism described by Stanovic et al. in 2010 (https://www.cs.fsu.edu/~awang/papers/rtas2010.pdf). In particular, the Lyons et al. paper states that when a thread is preempted at time t, a replenishment is scheduled for time t + T. My understanding of the sporadic server is that if a thread becomes active at time t, the replenishment is scheduled for time t + T. In other words, the replenishment is scheduled one period from when the thread begins execution, not when it ends execution. Further, a thread becomes active when it becomes unblocked (i.e. returns from a blocking system call, or is activated by the release of an aperiodic task that it handles). In other words, a thread that is preempted by a higher-priority thread is not considered to have become inactive, according to the sporadic server definition. This seems to be the case in both the Sprunt and Stanovic papers. I think the distinction is significant in a system (like seL4) where only a finite number of replenishments are tracked. Determining what number of replenishments each thread’s server must track is much easier if only voluntary yielding of the processor, and not preemption by higher-priority threads, triggers a replenishment. Can somebody explain to me in more detail how the sporadic server has been implemented in seL4? Like I said, from my reading of the kernel source, it seems that it has been implemented according to the improved POSIX sporadic server detailed by Stanovic, but I’m not certain that I’ve identified all conditions that cause a replenishment to be scheduled.
Hi, I've moved on from Data61, but I can now be reached at this email (anna@gh.st).
However, looking at the seL4 kernel source code, it seems that the actual implementation follows very closely with the improved POSIX sporadic server mechanism described by Stanovic et al. in 2010 (https://www.cs.fsu.edu/~awang/papers/rtas2010.pdf).
Correct. I mostly followed the Stanovic paper and work done in one of the Quest-V papers which also uses sporadic servers. This is a very timely email, as recently we've discovered some inconsistencies with the implementation in seL4 and the sporadic server algorithm. Namely, the sporadic server algorithm in seL4 is not work conserving, which can result in very low utilisation, which is what you have also discovered. We're working on how to adjust this in a way that satisfies all uses of seL4, particularly in the case of adversarial threads, and will provide an RFC or an update to the documentation with the proposed changes. This is mostly led by Curtis Millar who is doing all the hard work, with advice from me and others.
Can somebody explain to me in more detail how the sporadic server has been implemented in seL4?
There's a more detailed explanation in my phd (the implementation chapter is probaly the most useful).: https://github.com/pingerino/phd/blob/master/phd.pdf The key differences are: * threads do not run at a lower priority once they are out of replenishments * currently the execution time is bounded by the sliding window constraint, due to the lack of work conserving. This is implemented via the fact that any pre-emption point causes replenishments to be delayed. * the number of replenishments is set by user level * the kernel does not do an admission test, and only guarantees that the highest priority threads with available replenishments are scheduled It would be best to continue these enquiries either here on the mailing list or on the seL4 discourse (https://sel4.discourse.group/), as many others have insights, and I am not deep into scheduling theory now. [https://aws1.discourse-cdn.com/free1/uploads/sel4/original/1X/f196583f81bd64...]https://sel4.discourse.group/ seL4 - microkernel trustworthy systemshttps://sel4.discourse.group/ Systems related seL4 discussions: kernel design decisions, how to do X with seL4, how to port seL4 to a new architecture. sel4.discourse.group Thanks, Anna. Confidentiality Note:This email is intended only for the person or entity to which it is addressed and may contain information that is privileged, confidential or otherwise protected from disclosure. Unauthorized use, dissemination, distribution or copying of this email or the information herein by anyone other than the intended recipient is strictly prohibited. If you have received this email in error, please notify the sender immediately and destroy the original message, any attachments thereto and all copies.
Hi Anna,
Thank you for the reply! And thank you for pointing me toward your dissertation; this will certainly be valuable for the research I am doing. I’ll take a look at the Quest-V paper as well.
I thought I would note another key difference, and ask if I’m interpreting this correctly as well: there is a minimum budget defined, equal to the kernel worst-case execution time on the given hardware. A scheduling context cannot be defined with this budget. Further, a replenishment remnant less than this minimum budget will be merged with the next replenishment in the circular buffer. Is this correct?
Thanks again. I’d love to stay in the loop as improvements are made, and contribute where possible. I’ve signed up for the discourse (pending approval), and can continue this conversation there if preferred.
Marion Sudvarg
From: Anna Lyons
However, looking at the seL4 kernel source code, it seems that the actual implementation follows very closely with the improved POSIX sporadic server mechanism described by Stanovic et al. in 2010 (https://www.cs.fsu.edu/~awang/papers/rtas2010.pdf).
Correct. I mostly followed the Stanovic paper and work done in one of the Quest-V papers which also uses sporadic servers. This is a very timely email, as recently we've discovered some inconsistencies with the implementation in seL4 and the sporadic server algorithm. Namely, the sporadic server algorithm in seL4 is not work conserving, which can result in very low utilisation, which is what you have also discovered. We're working on how to adjust this in a way that satisfies all uses of seL4, particularly in the case of adversarial threads, and will provide an RFC or an update to the documentation with the proposed changes. This is mostly led by Curtis Millar who is doing all the hard work, with advice from me and others.
Can somebody explain to me in more detail how the sporadic server has been implemented in seL4?
There's a more detailed explanation in my phd (the implementation chapter is probaly the most useful).: https://github.com/pingerino/phd/blob/master/phd.pdf The key differences are: * threads do not run at a lower priority once they are out of replenishments * currently the execution time is bounded by the sliding window constraint, due to the lack of work conserving. This is implemented via the fact that any pre-emption point causes replenishments to be delayed. * the number of replenishments is set by user level * the kernel does not do an admission test, and only guarantees that the highest priority threads with available replenishments are scheduled It would be best to continue these enquiries either here on the mailing list or on the seL4 discourse (https://sel4.discourse.group/), as many others have insights, and I am not deep into scheduling theory now. [https://aws1.discourse-cdn.com/free1/uploads/sel4/original/1X/f196583f81bd64...]https://sel4.discourse.group/ seL4 - microkernel trustworthy systemshttps://sel4.discourse.group/ Systems related seL4 discussions: kernel design decisions, how to do X with seL4, how to port seL4 to a new architecture. sel4.discourse.group Thanks, Anna. Confidentiality Note:This email is intended only for the person or entity to which it is addressed and may contain information that is privileged, confidential or otherwise protected from disclosure. Unauthorized use, dissemination, distribution or copying of this email or the information herein by anyone other than the intended recipient is strictly prohibited. If you have received this email in error, please notify the sender immediately and destroy the original message, any attachments thereto and all copies.
participants (3)
-
Anna Lyons -
msudvarg＠wustl.edu -
Sudvarg, Marion