Loading...
C3: Finding Counting-related Crash Consistency Atomicity Bugs for Persistent Memory
Zhang, Yunmo Qiu, Junqiao Xu, Hong Xue, Jason
Zhang, Yunmo
Qiu, Junqiao
Xu, Hong
Xue, Jason
Files
Loading...
3786994.pdf
Adobe PDF, 649.9 KB
Supervisor
Department
Computer Science
Embargo End Date
Type
Journal article
Date
License
http://creativecommons.org/licenses/by/4.0/
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. Prior work on PM property inference has focused on ordering properties and offers limited support for reasoning about atomicity. 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. These properties are prevalent in PM programs but are not adequately addressed by existing techniques. We introduce C3, a tool designed to infer these counting-related atomicity properties and detect related bugs in PM programs. Our approach begins by proposing invariants to capture the necessary behaviors of counting-correlated variables. We then 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. Our bug detection method is based on the existing output checking approach, but adapted to be aware of input properties to detect and confirm the atomicity bugs efficiently. Our evaluation shows that C3 has found 14 atomicity bugs (including 11 previously unknown ones) from real-world PM programs.
Citation
Y. Zhang, J. Qiu, H. Xu, C.J. Xue, "C3: Finding Counting-related Crash Consistency Atomicity Bugs for Persistent Memory," ACM Transactions on Storage, https://doi.org/10.1145/3786994.
Source
ACM Transactions on Storage
Conference
Keywords
46 Information and Computing Sciences, 4612 Software Engineering
Subjects
Source
Publisher
Association for Computing Machinery