Software

Linux kernel

I am a Linux kernel contributor, working mainly in real-time related subsystems, such as the PREEMPT_RT and the schedulers. I am currently the maintainer of the Runtime Verification subsystem, the latency/noise-related tracers in the Linux kernel, and the rtla (Real-time Linux Analysis) toolset. I am also a reviewer for the scheduler code, mainly regarding the SCHED_DEADLINE changes.

Runtime Verification subsystem

Runtime Verification (RV) is a lightweight (yet rigorous) method that complements classical exhaustive verification techniques (such as model checking and theorem proving) with a more practical approach for complex systems.

Instead of relying on a fine-grained system model (e.g., a re-implementation of instruction level), RV works by analyzing the trace of the system’s actual execution and comparing it against a formal specification of the system behavior.

The main advantage is that RV can give precise information on the runtime behavior of the monitored system without the pitfalls of developing models that require a re-implementation of the entire system in a modeling language.

The RV subsystem idea originated during my Ph.D. I am the original author and the maintainer of this subsystem.

RTLA

The rtla is a meta-tool that includes a set of commands that aims to analyze the real-time properties of Linux. But instead of testing Linux as a black box, rtla leverages kernel tracing capabilities to provide precise information about unexpected results’ properties and root causes. It has been hosted in the Linux kernel repository since version 5.17.

osnoise tracer

The osnoise tracer runs a busy-loop workload in the kernel, with preemption, SoftIRQs and IRQs enabled, thus allowing all the sources of *osnoise* during its execution. Osnoise takes note of the entry and exit point of any source of interferences, increasing a per-cpu interference counter. The osnoise tracer also saves an interference counter for each source of interference. The interference counter for NMI, IRQs, SoftIRQs, and threads is increased anytime the tool observes these interferences’ entry events. When a noise happens without any interference from the operating system level, the hardware noise counter increases, pointing to a hardware-related noise. In this way, osnoise can account for any source of interference. At the end of the period, the osnoise tracer prints the sum of all noise, the max single noise, the percentage of CPU available for the thread, and the counters for the noise sources. osnoise was merged on Linux 5.14.

timerlar tracer

The timerlat tracer aims to help the preemptive kernel developers to find sources of wakeup latencies of real-time threads. Like cyclictest, the tracer sets a periodic timer that wakes up a thread. The thread then computes a *wakeup latency* value as the difference between the *current time* and the *absolute time* that the timer was set to expire. The main goal of timerlat is tracing in such a way to help kernel developers.

The tracer creates a per-cpu kernel thread with a real-time priority that prints two lines at every activation. The first is the *timer latency* observed at the *hardirq* context before the activation of the thread. The second is the *timer latency* observed by the thread. The ACTIVATION ID field serves to relate the *irq* execution to its respective *thread* execution. The *irq*/*thread* splitting is important to clarify in which context the unexpected high value is coming from. The *irq* context can be delayed by hardware-related actions, such as SMIs, NMIs, IRQs, or by thread masking interrupts. Once the timer happens, the delay can also be influenced by blocking caused by threads. For example, by postponing the scheduler execution via preempt_disable(), by the scheduler execution, or by masking interrupts. Threads can also be delayed by interference from other threads and IRQs. timerlat was merged on Linux 5.14.

stalld

I idealized the software and did the first version of it. It started as a workaround in shell script (named raggiro), which then became a daemon in C. I developed it while chatting with Juri Lelli, and then Clark Williams jumped in with many improvements – including the packaging. It is now available many distributions. The project is here: https://gitlab.com/rt-linux-tools/stalld.