RV and the Deadline Scheduler - How to Verify Your Subsystem at Runtime

Explore Runtime Verification (RV) implementation in the Linux Kernel through an interactive conference talk examining how to validate the deadline scheduler subsystem. Learn about RV's introduction in Linux Kernel v6.0 and its recent integration with scheduler and rtapp models, then dive into the practical application of timed automata for verifying timing requirements in deadline scheduling. Discover the collaborative process between subsystem maintainers and RV maintainers as speakers from Red Hat demonstrate modeling and validation techniques that can reveal subsystem inconsistencies, enhance documentation, and strengthen RV infrastructure. Gain insights into the unique challenges and capabilities that emerge when applying runtime verification to critical kernel subsystems, with hands-on exploration of how RV monitors can effectively validate complex timing-dependent operations in real-world Linux environments.