Inferring Likely Counting-related Atomicity Program Properties for Persistent Memory

Explore a research presentation on inferring counting-related atomicity program properties for persistent memory systems. Learn about the crash consistency challenges faced by Persistent Memory (PM) technologies and discover how researchers from City University of Hong Kong, The Chinese University of Hong Kong, and MBZUAI address the limitations of existing PM testing tools. Understand the concept of counting correlation - important atomicity properties between container-like arrays and their logical size variables that are common in PM programs but beyond current approaches' capabilities. Examine the proposed invariants designed to capture necessary behaviors of counting-correlated variables, and see how symbolic range analysis extracts PM program behaviors and encodes them into SMT constraints. Discover how these constraints are validated against invariants to infer likely PM program properties, and learn about the practical application of these inferred properties for PM bug detection, which successfully identified 14 atomicity bugs including 11 previously unknown bugs in real-world PM programs.