Abstract

We propose a method for automatically discovering likely program invariants for persistent memory (PM), which is a type of fast and byte-addressable storage device that can retain data after power loss. The invariants, also called PM properties or PM requirements, specify which objects of the program should be made persistent and in what order. Our method relies on a combination of static and dynamic analysis techniques. Specifically, it relies on static analysis to compute dependence relations between LOAD/STORE instructions and instruments the information into the executable program. Then, it relies on dynamic analysis of the execution traces and counterfactual reasoning to infer PM properties. With precisely computed dependence relations, the inferred properties are necessary conditions for the program to behave correctly through power loss and recovery; with imprecise dependence relations, these are …

Date

October 27, 2024

Authors

Zunchen Huang, Srivatsan Ravi, Chao Wang

Book

Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering

Pages

1795-1807