A High-Level Separation Logic for Heap Space under Garbage Collection

on YouTube ↗23m

" summary

Logic gives a concrete way to prove heap-space bounds under a GC that follows the free-variable rule: allocation consumes space credits, deallocation returns them when a block is provably unreachable via pointed-by assertions plus novel stackable assertions (fractional, splitable predicates that track invisible roots). Examples: a map on lists whose peak space is either 0 or linear depending on reachability, closure-based counters that free closure+ref when unreachable, CPS/stack examples and three stack implementations with amortized space analyses. Main theorem: verification under S credits implies live heap ≤ S; mechanized in Coq on top of Iris.

AI-written summary · about

" chapters (14)

1. 0:00Start
2. 2:39Formal Verification of Heap Space Bounds, with GC
3. 3:54Challenges of High-Level Languages
4. 4:51What are the roots considered by real-life GCs?
5. 6:54The Stackable Assertion
6. 7:47Handling Invisible Roots
7. 9:12Reasoning rules
8. 11:58The Soundness Theorem
9. 13:40Playing with Closures: Counter Objects
10. 14:50Specifying Closures
11. 15:38Closures are challenging
12. 16:24Read the Paper for Details
13. 17:13Conclusion
14. 21:58A New Consequence Rule