Runtime verification monitors for real-time

on YouTube ↗19m

" summary

Mainline PREEMPT_RT makes the kernel real-time capable but userspace still causes surprises; runtime verification monitors use kernel tracepoints and currently warn on page faults, warn when a lower-priority task wakes a higher-priority task, and flag RT tasks sleeping on non‑RT APIs. The monitors run in-kernel, emit warnings (logs/crashes configurable), and the roadmap asks whether to extend checks to blocking read/write on timerfd/ext4/socket/eventfd, blocking epoll/poll/ioctl, and explicit detection of non‑PI futexes plus a configurable whitelist and strictness levels.

AI-written summary · about

" chapters (6)

1. 0:00Introduction to runtime verification
2. 1:26Kernel runtime verification monitors
3. 7:29Defining real-time requirements
4. 12:07User expectations and design phase
5. 14:59Detecting common real-time issues
6. 18:16Tooling and guidance for developers

" related talks

• 21mRTLA Requests and TODOsDaniel Bristot de Oliveira · Linux Plumbers Conference 2023
• 26mLightweight Preemptible FunctionsAnuj Kalia, Michael Kaminsky, David G. Andersen, Sol Boucher · USENIX ATC '20
• 02mprovides a new look for software developersDr. Johan Kraft · embedded world 2016
• 42mWhat Really Happens When You Hit a BreakpointSy Brand · GOTO Copenhagen 2025
• 46mThe Hidden Secrets of DebuggingShai Almog · DevDays 2023
• 44mSpeeding up Kernel Testing and Debugging with virt-mengAndrea Righi · Linux Plumbers Conference 2023
• 23mRiker: Always-Correct and Fast Incremental Builds from Simple SpecificationsDaniel W. Barowy, Charlie Curtsinger · USENIX ATC '22
• 18mRT: Regular Types for the Streaming ShellKonstantinos Mamouras, Lukas Lazarek, Nikos Vasilakis, Evangelos Lamprou, Zekai Li, George Kapetanakis · 20th USENIX Symposium on Operating Systems Design and Implementation (OSDI '26)