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, 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 counter-factual reasoning to infer invariants. With precisely computed dependence relations, these are true invariants, i.e., necessary conditions for the program to behave correctly through power loss and recovery; with imprecise dependence relations, these are likely invariants. We have evaluated our method on benchmark programs including eight persistent data structures and two distributed storage applications, Redis and Memcached. The results show that our method can infer PM properties quickly and these properties are of higher quality than those inferred by a state-of-the-art technique. We also demonstrate the usefulness of the inferred properties by leveraging them for bug detection, which significantly improves the performance of a state-of-the-art bug detection technique.
Tue 29 OctDisplayed time zone: Pacific Time (US & Canada) change
16:30 - 17:30 | Program analysis 1Research Papers / Tool Demonstrations at Compagno Chair(s): Mugdha Khedkar Heinz Nixdorf Institute at Paderborn University | ||
16:30 15mTalk | Parf: Adaptive Parameter Tuning for Abstract Interpretation Research Papers Zhongyi Wang Zhejiang University, China, Linyu Yang Zhejiang University, Mingshuai Chen Zhejiang University, Yixuan Bu Zhejiang University, Zhiyang Li Zhejiang University, Qiuye Wang Fermat Labs, Huawei Inc., Shengchao Qin Fermat Labs, Huawei, Xiao Yi Fermat Labs, Huawei Inc., Jianwei Yin Zhejiang University | ||
16:45 15mTalk | Discovering Likely Program Invariants for Persistent Memory Research Papers Zunchen Huang , Srivatsan Ravi University of Southern California, Chao Wang University of Southern California | ||
17:00 10mTalk | flowR: A Static Program Slicer for R Tool Demonstrations | ||
17:10 10mTalk | Slicer4D: A Slicing-based Debugger for Java Tool Demonstrations Sahar Badihi University of British Columbia, Canada, Sami Nourji The University of British Columbia, Julia Rubin The University of British Columbia Pre-print |