Untangling the intricacies of thread synchronization in the PREEMPT-RT linux kernel

This article proposes an automata-based model for describing and validating the behavior of threads in the Linux PREEMPT-RT kernel, on a single-core system. 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 are used, initially, to validate the model, but preliminary results were enough to point to two problems in the Linux kernel. Finally, 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, showing how it is possible to take advantage of the model for analyzing the thread wake-up latency, without any need for watching the corresponding kernel code.