Loading...
Inferring Likely Counting-related Atomicity Program Properties for Persistent Memory
Zhang, Yunmo Qiu, Junqiao Xu, Hong Xue, Chun Jason
Zhang, Yunmo
Qiu, Junqiao
Xu, Hong
Xue, Chun Jason
Supervisor
Department
Computer Science
Embargo End Date
Type
Conference proceeding
Date
2025
License
Language
English
Collections
Research Projects
Organizational Units
Journal Issue
Abstract
Persistent Memory (PM) technologies provide fast, byte-addressable access to durable storage but face crash consistency challenges, motivating extensive work of testing and verification of PM programs. Central to PM testing tools is the specification of program properties for object persistence order and atomicity. Although several methods have been proposed for inferring PM program properties, most focus on ordering properties, offering limited support for atomicity properties. This paper explores a class of important atomicity properties between the container-like arrays and their logical size variables, referred to as the counting correlation, which are common in PM programs but exceed the capability of existing approaches. We propose invariants to capture the necessary behaviors of counting-correlated variables, utilize symbolic range analysis to extract PM program behaviors, and encode them into SMT constraints. These constraints are checked against the invariants to infer likely PM program properties. We demonstrate the utility of the inferred properties by leveraging them for PM bug detection, which discovers 14 atomicity bugs (including 11 new bugs) in real-world PM programs.
Citation
Y. Zhang, J. Qiu, H. Xu, C. Jason, and X. Mbzuai, “Inferring Likely Counting-related Atomicity Program Properties for Persistent Memory”,[Online]. Available: https://www.usenix.org/conference/atc25/presentation/zhang-yunmo
Source
Proceedings of the 2025 USENIX Annual Technical Conference, ATC 2025
Conference
2025 USENIX Annual Technical Conference, ATC 2025
Keywords
Subjects
Source
2025 USENIX Annual Technical Conference, ATC 2025
Publisher
USENIX Association