Roland Meyer
Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
Concurrent data structures (CDS) form the backbone of today’s computing infrastructure: there is no operating system, storage center, or programming language without concurrent and low-latency access to shared data. The way to achieve low latency is fine-grained synchronization, a programming style known for its efficiency but also notorious for its intricacy. Indeed, CDS are so difficult to get right that a whole branch of programming language research is devoted to their verification. The progress has been amazing, from the Gödel-award-winning separation logic to scalable testing methods. Still, there is an assumption behind these techniques that limits their applicability.
The existing verification techniques for CDS assume garbage collection and do not carry over to programming languages with manual memory management like C++. To see that the difference is substantial, consider a concurrent list. A thread will not know whether other threads are about to access its node (this would require prohibitive synchronization). But then, when is it safe for a thread to delete a node? Never! The way out is to accompany the CDS with a so-called safe memory reclamation algorithm (SMRA) responsible for the deletions. Garbage collection can be understood as an SMRA, but there are more efficient variants. With hazard pointers, for example, a thread actively protects the memory it intends to access. While SMRA are common programming practice, programming language research has not found a satisfactory way of including them into the verification cycle.
We propose a tool chain that reduces the problem of verifying CDS that manage their memory with the help of an SMRA to verification under garbage collection. Verification under garbage collection is an established task with a large research community, an active tool development, and mature off-the-shelf tools. With our tool chain, all this becomes available to manual memory management. At the hear of our tool chain is a type system that checks whether a CDS properly manages its memory. If the type check succeeds, it is safe to ignore the SMRA and consider the CDS under garbage collection. Intuitively, our types track the protection of pointers as guaranteed by the SMRA. There are two design decisions. The type system does not maintain any shape information, which makes it extremely lightweight. The SMRA is not hard-coded but a parameter of the type system definition.
The talk is based on joint work [1, 2] with Sebastian Wolff (NYU).
[1] Roland Meyer, Sebastian Wolff:
Decoupling lock-free data structures from memory reclamation for static analysis. Proc. ACM Program. Lang. 3(POPL): 58:1-58:31 (2019)
[2] Roland Meyer, Sebastian Wolff:
Pointer life cycle types for lock-free data structures with memory reclamation. Proc. ACM Program. Lang. 4(POPL): 68:1-68:36 (2020)
The existing verification techniques for CDS assume garbage collection and do not carry over to programming languages with manual memory management like C++. To see that the difference is substantial, consider a concurrent list. A thread will not know whether other threads are about to access its node (this would require prohibitive synchronization). But then, when is it safe for a thread to delete a node? Never! The way out is to accompany the CDS with a so-called safe memory reclamation algorithm (SMRA) responsible for the deletions. Garbage collection can be understood as an SMRA, but there are more efficient variants. With hazard pointers, for example, a thread actively protects the memory it intends to access. While SMRA are common programming practice, programming language research has not found a satisfactory way of including them into the verification cycle.
We propose a tool chain that reduces the problem of verifying CDS that manage their memory with the help of an SMRA to verification under garbage collection. Verification under garbage collection is an established task with a large research community, an active tool development, and mature off-the-shelf tools. With our tool chain, all this becomes available to manual memory management. At the hear of our tool chain is a type system that checks whether a CDS properly manages its memory. If the type check succeeds, it is safe to ignore the SMRA and consider the CDS under garbage collection. Intuitively, our types track the protection of pointers as guaranteed by the SMRA. There are two design decisions. The type system does not maintain any shape information, which makes it extremely lightweight. The SMRA is not hard-coded but a parameter of the type system definition.
The talk is based on joint work [1, 2] with Sebastian Wolff (NYU).
[1] Roland Meyer, Sebastian Wolff:
Decoupling lock-free data structures from memory reclamation for static analysis. Proc. ACM Program. Lang. 3(POPL): 58:1-58:31 (2019)
[2] Roland Meyer, Sebastian Wolff:
Pointer life cycle types for lock-free data structures with memory reclamation. Proc. ACM Program. Lang. 4(POPL): 68:1-68:36 (2020)
back to overview
Watch Recording
Biography
Professor at TU Braunschweig, Head of the Institute of Theoretical Computer Science.Roland is interested in verification and synthesis problems for concurrent programs, with a focus on automated approaches and a sympathy for theory. He is a professor at TU Braunschweig, head of the Institute of Theoretical Computer Science, and head of the Department of Computer Science. From 2010 to 2016, he was an assistant and associate professor at TU Kaiserslautern.
