The ERA Theorem for Safe Memory Reclamation
summary
Shows that no reclamation algorithm can simultaneously provide ease of integration, robustness (a bound on retired-but-unreclaimable nodes) and wide applicability. Uses concrete systems: compares epoch-based, hazard pointers and optimistic-access schemes, points out optimistic reads are fast with tiny memory overhead but need rollbacks, and gives a simple constructive impossibility proof using Harris’s linked list and a two-thread cycle that forces reuse of retired nodes. Concludes ERA theorem holds: pick two of the three.
AI-written summary · about
chapters (11)
- 0:00Memory reclamation basics
- 1:04History and motivation
- 4:22Challenges in concurrent settings
- 8:14Traditional schemes and limits
- 15:32Evolution of techniques
- 19:04Optimistic approach trade-offs
- 20:12Impossibility of ideal reclamation
- 25:15Formalizing properties
- 30:20Proof of ERA impossibility
- 31:42Implications and future work
- 32:26Q&A
related talks
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
01h 04mWe Live in Interesting Times
57mInvited Talk: Bridging Safety and Performance
28mReasoning about Distributed Reconfigurable Systems
01h 03mPrinciples of Persistent Programming
01h 33mSafe and Sane C++ Types
15mTowards a Formal Foundation of Intermittent Computing
54mAn Introduction to Residuality Theory