Safe Deferred Memory Reclamation with Types
Ismail Kuru, Colin S. Gordon

TL;DR
This paper introduces a static type system that guarantees safe memory deallocation in lock-free data structures using RCU, ensuring correctness without full verification of implementations.
Contribution
It provides the first formal proof of memory safety for RCU-based linked list and binary search tree implementations using a novel type system.
Findings
Type system ensures nodes are deallocated exactly once
Guarantees safe memory reclamation in RCU data structures
Simplifies correctness proofs for concurrent memory management
Abstract
Memory management in lock-free data structures remains a major challenge in concurrent programming. Design techniques including read-copy-update (RCU) and hazard pointers provide workable solutions, and are widely used to great effect. These techniques rely on the concept of a grace period: nodes that should be freed are not deallocated immediately, and all threads obey a protocol to ensure that the deallocating thread can detect when all possible readers have completed their use of the object. This provides an approach to safe deallocation, but only when these subtle protocols are implemented correctly. We present a static type system to ensure the correct use of RCU memory management: that nodes removed from a data structure are always scheduled for subsequent deallocation, and that nodes are scheduled for deallocation at most once. As part of our soundness proof, we give an…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDistributed systems and fault tolerance · Security and Verification in Computing · Parallel Computing and Optimization Techniques
