一句话：结合静态依赖分析与动态反事实推理，自动推断持久内存程序的持久化对象与顺序性质，并用于缺陷检测。
持久内存（PM）是一种断电后仍能保留数据的快速字节可寻址存储，程序需明确哪些对象应被持久化以及以何种顺序持久化，这类性质（PM 不变式）通常难以人工编写。本文提出自动发现此类不变式的方法：先用静态分析计算 LOAD/STORE 指令之间的依赖关系，并将该信息插桩进可执行程序；再对执行轨迹做动态分析与反事实推理，推断 PM 性质。当依赖关系被精确计算时，推断出的性质是程序在断电与恢复过程中正确行为的必要条件；当依赖关系不精确时，则得到疑似程序不变式。作者在八个持久数据结构以及 Redis、Memcached 两个分布式存储应用上评估，结果显示推断速度快、性质质量优于当前最先进技术，并可将推断出的性质用于 PM 缺陷检测，显著提升已有检测技术的效果。
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 likely program 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 PM bug detection, which significantly improves the performance of a state-of-the-art PM bug detection technique.