Daniel Bristot de Oliveira, Daniel Casini, Rômulo Silva de Oliveira, Tommaso Cucinotta
Linux has become a viable operating system for many real-time workloads. However, the black-box approach adopted by cyclictest, the tool used to evaluate the main real-time metric of the kernel, the scheduling latency, along with the absence of a theoretically-sound description of the in-kernel behavior, sheds some doubts about Linux meriting the real-time adjective. Aiming at clarifying the PREEMPT_RT Linux scheduling latency, this paper leverages the Thread Synchronization Model of Linux to derive a set of properties and rules defining the Linux kernel behavior from a scheduling perspective. These rules are then leveraged to derive a sound bound to the scheduling latency, considering all the sources of delays occurring in all possible sequences of synchronization events in the kernel. This paper also presents a tracing method, efficient in time and memory overheads, to observe the kernel events needed to define the variables used in the analysis. This results in an easy-to-use tool for deriving reliable scheduling latency bounds that can be used in practice. Finally, an experimental analysis compares the cyclictest and the proposed tool, showing that the proposed method can find sound bounds faster with acceptable overheads.
The paper will be presented in the session
Operating systems and GPUs – Thursday, July 9, 13:00 – 14:00 (CET)
https://drops.dagstuhl.de/opus/volltexte/2020/12372/pdf/LIPIcs-ECRTS-2020-9.pdf
Artifact:
https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=12392
Short Bio: Daniel Bristot de Oliveira is a Principal Software Engineer at Red Hat working in the research and development of the Linux kernel, mainly regarding real-time and formal methods related topics. He is a member of the Retis Lab at Scuola Superiore Sant’Anna.
The slides for the presentation are available here.
A “companion page” for the paper, can be found here.