RV and the deadline scheduler: how to verify your subsystem at runti...
summary
Runtime Verification runs inside the kernel to check the deadline scheduler by compiling models into kernel monitors, adding timed automata and per-object monitors, and adding tracepoints for events like replenish throttle switch_in. The model flags violations where a server boosts a fair task after its deadline (example trace shows replenish at 0s, switch_in at ~5.7s but throttle at ~4.7s), leads to three upstream fixes, and requires adapting models when scheduler tracepoints or behavior change.
AI-written summary · about
chapters (11)
- 0:00Introduction to runtime verification
- 1:03Motivation for validating scheduler
- 4:21Runtime verification basics
- 8:35Adding trace points to kernel
- 10:47Adapting models to kernel changes
- 14:06Fixes discovered via RV
- 14:29Steps to create a new model
- 22:40Future directions for RV
- 23:44Q&A on model abstraction
- 35:08Q&A on model tracking and overhead
- 41:42Q&A wrap-up and conclusion
related talks
45mRV: where are we?
50mSCHED_DEADLINE: It's Alive!
40mRT Linux in Safety-Critical Systems: The Potential and the Challenges
50mrtla timerlat: Debugging Real-Time Linux Scheduling Latency
37mReal-time Scheduling Fault Simulation
18mScheduler Tracing With ftrace + eBPF
23mSCHED_DEADLINE desiderata and slightly crazy ideas
26mReal-time Linux: what is next?