Persistent Memory

The emerging class of storages between DRAM and SSD

Persísto, ergo sum.
—Unknown

Persistent memory is an emerging class of storage technology that simultaneously provides (1) byte addressability, low latency, and high throughput as DRAM does; and (2) durability (data persistency across system crashes) and high capacity as SSD does. These powerful properties, however, have brought about existing issues such as (1) concurrency control for thread safety and (2) persistency control for data consistency.

We aim to understand how to properly use this attractive memory in a program. In addition, we aim to exploit its potentiality to build innovative transational systems!

Publications

  • (Ph.D. Dissertation 2024) Principles of Byte-Addressable Persistency.
    Kyeongmin Cho .
    School of Computing, KAIST (Outstanding PhD Thesis Award).
    [paper: local] ​ ​ ​

    Abstract

    Persistent memory (PM) is an emerging storage technology that combines the performance of DRAM with the durability of SSD, offering the benefits of both. A key feature of PM is its byte-addressable persistency, enabling data to be efficiently loaded and stored with byte-level granularity. This capability is crucial for enhancing performance by adapting various data structures and algorithms for DRAM to storage devices. However, designing these approaches in PM presents significant challenges due to the potential for crashes, particularly in addressing two types of persistency challenges: (1) at the instruction level, managing CPU instruction reordering that complicates the understanding of persistent programs; and (2) at the object level, carefully designing and composing data structures to prevent data loss while maintaining high performance.

    This dissertation presents systematic programming principles to tackle these challenges through formal abstractions for byte-addressable persistency, advancing the reliability and performance of PM systems. (1) To address the challenge of managing CPU instruction reordering, we present Px86view and PArmv8view: hardware persistency semantic models that formally standardize instruction descriptions for major architectures, Intel-x86 and Armv8, in a unified manner using the notion of views. Based on these models, we develop a model checker to verify the correctness of several representative persistent programs. (2) To address the challenge of designing crash-consistent and high-performance data structures, we present Memento: a programming framework for PM that ensures generally applicable to various data structures and algorithms. We prove that data structures designed using Memento are crash-consistent and perform comparably to existing hand-tuned alternatives.

  • (PLDI 2023) Memento: A Framework for Detectable Recoverability in Persistent Memory.
    Kyeongmin Cho, Seungmin Jeon, Azalea Raad, Jeehoon Kang .
    ACM SIGPLAN conference on Programming Languages Design and Implementation.
    [paper: doi, local] ​ [artifact: development] ​ ​

    Abstract

    Persistent memory (PM) is an emerging class of storage technology that combines the performance of DRAM with the durability of SSD, offering the best of both worlds. This had led to a surge of research on persistent objects in PM. Among such persistent objects, concurrent data structures (DSs) are particularly interesting thanks to their performance and scalability. One of the most widely used correctness criteria for persistent concurrent DSs is detectable recoverability, ensuring both thread safety (for correctness in non-crashing concurrent executions) and crash consistency (for correctness in crashing executions). However, the existing approaches to designing detectably recoverable concurrent DSs are either limited to simple algorithms or suffer from high runtime overheads.

    We present Memento: a general and high-performance programming framework for detectably recoverable concurrent DSs in PM. To ensure general applicability to various DSs, Memento supports primitive operations such as checkpoint and compare-and-swap and their composition with control constructs. To ensure high performance, Memento employs a timestamp-based recovery strategy that requires fewer writes and flushes to PM than the existing approaches. We formally prove that Memento ensures detectable recoverability in the presence of crashes. To showcase Memento, we implement a lock-free stack, list, queue, and hash table, and a combining queue that detectably recovers from random crashes in stress tests and performs comparably to existing hand-tuned persistent DSs with and without detectable recoverability.

  • (PLDI 2021) Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8.
    Kyeongmin Cho, Sung-Hwan Lee, Azalea Raad, Jeehoon Kang .
    ACM SIGPLAN conference on Programming Languages Design and Implementation.
    [paper: doi, local] ​ [artifact: proofs, model checker] ​ ​

    Abstract

    Non-volatile memory (NVM) is a cutting-edge storage technology that promises the performance of DRAM with the durability of SSD. Recent work has proposed several persistency models for mainstream architectures such as Intel-x86 and Armv8, describing the order in which writes are propagated to NVM. However, these models have several limitations; most notably, they either lack operational models or do not support persistent synchronization patterns.

    We close this gap by revamping the existing persistency models. First, inspired by the recent work on promising semantics, we propose a unified operational style for describing persistency using views, and develop view-based operational persistency models for Intel-x86 and Armv8, thus presenting the first operational model for Armv8 persistency. Next, we propose a unified axiomatic style for describing hardware persistency, allowing us to recast and repair the existing axiomatic models of Intel-x86 and Armv8 persistency. We prove that our axiomatic models are equivalent to the authoritative semantics reviewed by Intel and Arm engineers. We further prove that each axiomatic hardware persistency model is equivalent to its operational counterpart. Finally, we develop a persistent model checking algorithm and tool, and use it to verify several representative examples.