Loops handling by BPF verifier and what should we do about it?

on YouTube ↗28m

" summary

Scalar evolution analysis infers algebraic formulas for loop-varying registers and solves for iteration counts, but works on assembly so stack spills and aliasing force conservative bailouts; a prototype lowering that reserves a temporary register for spill tracking exists but breaks backwards compatibility. Loop structure reconstruction and collection of algebraic expressions complete, recursive relation construction is in progress, nested loops verify inner-first and outer sees modified values as unknown. A correctness bug in precision-bit propagation prompts using strongly connected components and propagating marks on the CFG; DFA-based liveness analysis has landed and DFA-based value-range analysis is planned, with verifier abandoning paths when inferred assumptions prove invalid.

AI-written summary · about

" chapters (12)

1. 0:00Introduction to loop verification
2. 1:26Scalar evolution analysis
3. 5:22Stack spills and fields challenge
4. 7:50Workaround for stack tracking
5. 9:18Assumption-based verification
6. 13:45Nested loop handling
7. 15:58Irreducible loops status
8. 16:19Precision marks propagation bug
9. 19:37Strongly connected components
10. 22:48Read and precision marks tracking
11. 24:34Subprogram call handling
12. 25:45Q&A on loop analysis