 |  |
18 March 2024
|
|
This site uses |
Last updated on
18 March 2024 |
D. B. de Oliveira, R. S. de Oliveira, T. Cucinotta. "Untangling the Intricacies of Thread Synchronization in the PREEMPT RT Linux Kernel," in Proceedings of the 22nd IEEE International Symposium on Real-Time Distributed Computing (IEEE ISORC 2019), May 7-9, 2019, Valencia, Spain.
This article proposes an automata-based model for describing and validating the behavior of threads in the Linux PREEMPT RT kernel. The automata model defines the events and how they influence the timeline of threads’ execution, comprising the preemption control, interrupt handlers, interrupt control, scheduling and locking. This article also presents the extension of the Linux trace features that enable the trace of the kernel events used in the modeling. The model and the tracing tool cross-check the kernel execution, enabling the improvement of both. As an example of the usage of the model, the analysis of the events involved in the activation of the highest priority thread is presented in terms of necessary and sufficient conditions, describing the delays occurred in this operation in the same granularity used by kernel developers. It illustrates how it is possible to take advantage of the model for analyzing the preemption model of Linux, without any need for studying the corresponding kernel code. Finally, we describe in details two problems in the kernel revealed by the model, along with reports and fixes for the Linux kernel developers.
Copyright by IEEE.
See paper on publisher website
|
|
Last updated on
18 March 2024 |