C3: Finding Counting-related Crash Consistency Atomicity Bugs for Persistent Memory

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 article 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.