一句话:提出基于约束的程序修复方法,可修复持久内存的持久性与崩溃一致性错误并发现新修复策略。
持久内存(PM)编程中,程序可能违反持久性或崩溃一致性属性。本文提出一种基于约束的修复方法:以程序执行轨迹和被违反属性为输入,通过插入和重排 PM 指令生成修复建议。方法采用新的符号编码建模 PM 语义,避免显式枚举可能场景,从而高效探索大量修复。与当前最优方法相比,它不仅能修复持久性 bug,还能修复崩溃一致性 bug,并能发现新的修复策略而非依赖硬编码策略。在 Intel PMDK 库以及 Memcached、Recipe、Redis 等真实应用上的评估表明,该方法修复了全部 41 个已知 bug,而现有方法无法修复任何崩溃一致性 bug。
We propose a constraint based method for repairing bugs associated with the use of persistent memory (PM) in application software. Our method takes a program execution trace and the violated property as input and returns a suggested repair, which is a combination of inserting new PM instructions and reordering these instructions to eliminate the property violation. Compared with the state-of-the-art approach, our method has three advantages. First, it can repair both durability and crash consistency bugs whereas the state-of-the-art approach can only repair the relatively-simple durability bugs. Second, our method can discover new repair strategies instead of relying on repair strategies hard-coded into the repair tool. Third, our method uses a novel symbolic encoding to model PM semantics, which allows our symbolic analysis to be more efficient than the explicit enumeration of possible scenarios and thus explore a large number of repairs quickly. We have evaluated our method on benchmark programs from the well-known Intel PMDK library as well as real applications such as Memcached, Recipe, and Redis. The results show that our method can repair all of the 41 known bugs in these benchmarks, while the state-of-the-art approach cannot repair any of the crash consistency bugs.