Publication details

D. B. de Oliveira, T. Cucinotta, R. S. de Oliveira. "Modeling the Behavior of Threads in the PREEMPT_RT Linux Kernel Using Automata," in Proceedings of the International Workshop on Embedded Operating Systems (EWILI 2018), October 10th, 2018, Torino, Italy.

Abstract

This article proposes an automata-based model for describing and verifying the behavior of thread management code in the Linux PREEMPT_RT kernel, on a single-core system. The automata model defines the events that influence the timing behavior of the execution of threads, and the relations among them. This article also presents the extension of the Linux trace features that enable the trace of such events in a real system. Finally, one example is presented of how the presented model and tracing tool helped catching an inefficiency bug in the scheduler code and ultimately led to improving the kernel.

Download paper

See paper on publisher's website

Last updated on
18 March 2024