Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters
summary
A semantics change returns a delta store (partial map of only changed addresses) instead of an updated store, enabling a single evaluation rule to interleave abstract garbage collection while preserving perfect stack precision and context irrelevance. The paper proves—mechanised in Rocq—that DSS yields equal-or-better precision than small-step GC and shows empirical results matching or improving precision. A prototype times out on ~1/3 of benchmarks, but flow-sensitive store widening reduces timeouts to four (and zero for context-insensitive runs); replay handles non‑tail overwrites.
AI-written summary · about
chapters (10)
- 0:00Delta Store Semantics intro
- 2:10Garbage in abstract interpreters
- 5:42Integrating GC challenges
- 7:06Delta Store Semantics explained
- 9:57GC with DSS integration
- 12:44Traditional vs stackless GC
- 14:52DSS scalability issues
- 16:59Flow-sensitive widening solution
- 18:45Final approach summary
- 19:49Q&A
related talks
25mCall-Guarded Abstract Definitional Interpreters
18mCertified Semantics for Disequality
14mHigher-Order Demand-Driven Symbolic Evaluation
23mAn Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
22mMechanised Semantics for Gated Static Single Assignment
25mBig-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
15mSymbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
01h 00mState of Dotty