Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage(…)
summary
IrisFit is a separation logic, formalized in Coq on top of the Iris framework, that uses space credits to bound heap usage for a concurrent call-by-value language with tracing GC. It proves two theorems: safety (no crashes and heap stays ≤ declared bound) and liveness (with polling points, each allocation completes in bounded time). New language features are protected sections and polling points; case studies include Treiber’s stack and the Michael-Scott queue, all mechanized.
AI-written summary · about
chapters (21)
- 0:00Introduction
- 0:21Motivation
- 1:03Separation logic basics
- 2:28Garbage collection challenges
- 3:31Iris-Fit contributions
- 4:13Proving unreachability
- 5:58Heap assertions
- 7:23Tracking roots in GCs
- 8:49Thread assertions
- 10:33Space recovery proof
- 11:18Iris-Fit soundness
- 11:41Lock-free data structures issue
- 12:46Linearizability and stack spec
- 14:10Problematic interleaving
- 15:16Protected sections
- 16:40Reasoning rules for protected sections
- 17:24Liveness issues
- 18:13Polling points analogy
- 18:55Future work
- 19:37Conclusion
- 20:22Q&A
related talks
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
19mAn Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T...
20mTrillium: Higher-Order Concurrent and Distributed Separation Logic for Intension...
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
14mExecution domains in GHC/Haskell (Lightning Talk)
27mThe Mutability Matrix of Pain
24mSaturn: a library of verified concurrent data structures for OCaml 5