Memory reclamation for optimistic concurrency in unmanaged programming languages is a challenging problem that poses trade-offs between performance and guaranteeing safety. For example, reference counting provides an easy-to-use safe interface but suffers from performance bottlenecks, whereas manual methods like Hazard Pointers and epoch-based reclamation are highly efficient but prone to usage errors that lead to critical bugs.

In this talk, I will present our recent work on addressing this challenge from two angles. First, I will introduce Concurrent Immediate Reference Counting (CIRC), which achieves both high throughput and ease of use by wrapping the intricacy of fast manual algorithms in a safe interface of reference counting. At the same time, CIRC features immediate recursive reclamation, which is essential for quickly reclaiming linked structures. Second, I will discuss our work on formal verification to enhance confidence in the correctness of performant but difficult manual reclamation methods. Our approach is built on modular specifications using concurrent separation logic, enabling compositional verification.

Jaehwang Jung is a Ph.D. candidate at KAIST under the supervision of Prof. Jeehoon Kang. His research centers on high-performance concurrent and parallel systems, with a strong emphasis on ensuring correctness through safe programming interfaces and formal verification. Leveraging deep insights from formal verification, he has designed several advanced concurrent memory reclamation algorithms. His work has been published in PLDI, OOPSLA, and SPAA, where he received the SPAA 2024 best paper award.