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.