Composing Detectably Recoverable Concurrent Data Structures in Persistent Memory
Jeehoon Kang is an Assistant Professor in the School of Computing at KAIST. Before joining KAIST in February 2019, he worked on developing a compiler for AI accelerators as Chief R&D Officer in FuriosaAI. He received his Ph.D. (2019) in Computer Science from Seoul National University. His research interests are in the design and verification of concurrent and parallel systems. Recently, his group has been focusing on concurrent data structures, persistent memory, and hardware description language. He is a recipient of various awards including POPL 2022 and PLDI 2017 distinguished paper awards.
Persistent memory (PM) is as fast as DRAM and as durable as SSD. Thanks to these properties, PM is expected to significantly optimize transaction systems such as file systems and database management systems. However, it is challenging to program PM for two reasons. (1) Reordering: due to compiler and CPU optimizations, PM accesses may be reordered. (2) Recovery: should a system crash, persistent objects in PM should be recovered to preserve their invariants.
In this talk, we present approaches to the above challenges. (1) To formally understand reordering, we define an operational semantics of PM (PLDI 2021). Unlike the prior work, our semantics targets real-world ISAs such as Intel-x86 and Armv8, and precisely describes the allowed behaviors. (2) To assist programmers to write recovery functions, we prove a failure transparency theorem for a large class of programs (Submitted). Unlike the prior work, our construction supports general control constructs and lock-free programming patterns. The key idea is a control flow-aware generic recovery function based on timestamps.