Improving Thread-Modular Abstract Interpretation

on YouTube ↗15m

" summary

Formalizes thread-modular non-relational value analyses with a new local trace semantics and a side-effecting constraint-system framework, casts Goblint’s generalization and Miné’s approach as instances, and builds improved lock-centered, write-centered and combined analyses. Evaluated in Goblint on 13 C programs (600–3000 LOC). Protection-based analysis runs up to an order of magnitude faster; all analyses agree on 11/13 benchmarks, and Miné-style misses precision on two benchmarks (6% and 16% of global reads). The combined analysis is strictly more precise than either prior approach.

AI-written summary · about

" chapters (17)

1. 0:00Intro
2. 0:13Multi-Threaded Programs
3. 0:32Analysis of Multithreaded Programs is challenging
4. 1:08Thread-Modular Analysis
5. 1:43Setting
6. 2:38Example Vojdani-style
7. 4:18Side Effecting Constraint Systems
8. 7:23Our Concrete Semantics
9. 7:48Global Trace
10. 9:16Side Effecting Formulation of the Local Trace Semantics
11. 10:57Close connection also with Mine style analysis
12. 11:36Possiblities for Improvement
13. 12:07Ingredients for more precise analyses: Globals
14. 13:28Preliminary Experimental Evaluation
15. 13:46Runtime
16. 13:59Precision
17. 14:42Future Work