论文标题
基于查看的Owicki-Gries推理持续X86-TSO（扩展版）
View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version)
论文作者
论文摘要
持续记忆的兴起正在破坏计算的核心。我们的工作旨在通过提供有关使用低级操作（例如内存访问和围栏）以及诸如Flushes之类的持久性原始原则的X86代码的程序逻辑来帮助程序员浏览这个勇敢的新世界。我们的逻辑Pierogi受益于基于视图的简单基础操作语义，能够处理优化的冲洗操作，并且在Isabelle/Hol Proof Assistant中进行了机械化。我们详细介绍了Pierogi的证明规则，并证明它们的声音。我们还展示了Pierogi如何用于推理一系列具有挑战性的单线和多线程持续程序。
The rise of persistent memory is disrupting computing to its core. Our work aims to help programmers navigate this brave new world by providing a program logic for reasoning about x86 code that uses low-level operations such as memory accesses and fences, as well as persistency primitives such as flushes. Our logic, Pierogi, benefits from a simple underlying operational semantics based on views, is able to handle optimised flush operations, and is mechanised in the Isabelle/HOL proof assistant. We detail the proof rules of Pierogi and prove them sound. We also show how Pierogi can be used to reason about a range of challenging single- and multi-threaded persistent programs.
