Applying Program Verification to Linux Kernel Code: Challenges, Practices, and...
summary
Shows concrete results from applying deductive verification to Linux scheduler code, focusing on the task scheduler and functions like is_core_idle where formal specs and loop invariants expose semantic bugs found earlier in select_idle_core and load‑balance patches. Describes an automated pipeline that extracts a minimal self-contained file from large macros and headers (example reduced to ~60 lines) and tools to infer common loop invariant patterns for CPU iteration, while noting manual annotations remain necessary.
AI-written summary · about
chapters (11)
- 0:00Introduction to verification
- 1:48What is formal verification
- 7:33How verifiers work
- 8:35Verification example
- 12:01Automating verification
- 16:02Challenges of specifications
- 17:52Summary and limitations
- 19:19Q&A on verification scope
- 20:48Q&A on specification languages
- 22:20Q&A on readable specifications
- 24:28Q&A on specification inference
related talks
37mReal-time Scheduling Fault Simulation
16mChallenges in CPU DV: Why "It Boots Linux" Is Not Verification
21mCombined Dynamic and Formal Verification Approach to Processor Verification
18mPreview: Verification (Correctness)
18mPreview: Verification (Correctness & Debugging)
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
01h 07mThe seL4 verification: the art and craft of proof and the reality of commercial s
42mExercising the Linux scheduler with Yogini