A Separation Logic for Heap Space under Garbage Collection

on YouTube ↗19m

" summary

A separation logic (called SLgc in the paper) models heap space under tracing GC by treating allocation budget as space credits consumed on allocation and regained by a ghost logical de-allocation when a block or group is provably unreachable; reachability is tracked locally with pointed-by assertions recording predecessors. The authors formalize a low-level calculus SpaceLang, prove soundness on top of Iris with a fixed heap bound S, and support bulk de-allocation of cyclic groups; artifacts are available.

AI-written summary · about

" chapters (21)

1. 0:00Introduction
2. 0:13Verify Heap Space Usage
3. 0:43Heap Space as a Resource
4. 2:35Reason in the Presence of GC
5. 3:01Logical Deallocation
6. 4:16Update Axiom
7. 4:57The Problem
8. 5:40Example
9. 6:36Solution
10. 7:23Problem
11. 9:06The System
12. 11:33SpaceLang
13. 12:13Operational semantics
14. 13:04Reasoning rules
15. 14:21Deallocation
16. 15:08Soundness Theorem
17. 15:52Stack
18. 16:52POPL
19. 17:06Logically Deallocate
20. 17:34Conclusion
21. 17:59Future work