Safe Deferred Memory Reclamation with Types

Kuru, Ismail, Gordon, Colin S.

European Symposium on Programming (ESOP 2019), April 2019, doi: 10.1007/978-3-030-17184-1_4

pdf springer arXiv

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 placed on a \emph{deferred} free list, 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 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 abstract semantics for RCU memory management primitives which captures the fundamental properties of RCU. Our type system allows us to give the first proofs of memory safety for RCU linked list and binary search tree implementations without requiring full verification.

Bibtex

@inproceedings{esop19,
  abbr = {ESOP},
  bibtex_show = {true},
  title = {{A Type System for Read-Copy-Update Concurrency}},
  author = {Kuru, Ismail and Gordon, Colin S.},
  eprint = {https://arxiv.org/abs/1811.11853},
  arxiv = {1811.11853},
  booktitle = {{European Symposium on Programming (ESOP 2019)}},
  month = {April},
  note = "Acceptance Rate 32.6\% (28/86).",
  address = {Prague, Czech Republic},
  year = 2019,
  selected={true},
  pdf = {papers/esop19.pdf},
  doi = {10.1007/978-3-030-17184-1_4},
  springer = {https://link.springer.com/chapter/10.1007/978-3-030-17184-1_4},
  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 placed on a \emph{deferred} free list, 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 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 abstract semantics for RCU memory management primitives which captures the fundamental properties of RCU. Our type system allows us to give the first proofs of memory safety for RCU linked list and binary search tree implementations without requiring full verification.
  }
}