Improving Thread-Modular Abstract Interpretation

on YouTube ↗30m

" summary

Presents a thread‑modular framework that formalizes analyses as side-effecting constraint systems with a new local trace semantics, proves soundness of instances, and implements generalized versions of GOBLINT’s protection-based analysis and an improved Miné-style propagation in the Goblint analyzer. Shows the two classic approaches are precision‑incomparable, designs a refinement that strictly improves both, and reports on 13 benchmarks (600–3000 LOC): analyses agree on 11, Mini loses precision on two (6% and 16% of global reads), while protection-based is fastest.

AI-written summary · about

" chapters (23)

1. 0:00Thread-modular analysis intro
2. 1:25Multi-threaded analysis challenges
3. 2:28Thread-modular limits
4. 3:10Vajdani’s protection-based approach
5. 4:13Protecting lock sets for globals
6. 5:58Side effects in constraints
7. 7:43Unlock-to-lock propagation
8. 9:51Incomparable precision of both analysis styles
9. 10:35Contributions and framework
10. 11:18Local trace semantics
11. 13:05Local traces defined
12. 15:13Combining incompatible traces
13. 16:59Connection to Mini’s analysis
14. 18:03Deficiencies in analyses
15. 18:45Ingredients for precision
16. 20:12Combined analysis results
17. 20:55Implementation setup
18. 21:37Runtime benchmarks
19. 21:59Precision insights
20. 22:42Future work
21. 23:45Q&A: Synchronization primitives
22. 25:10Q&A: OS interrupts
23. 28:30Q&A: Strong updates