一句话：首次在 Hoare 风格程序逻辑中引入 prophecy variables，并在 Iris/Coq 中形式化，用于验证并发算法的逻辑原子性。
Hoare 逻辑早期引入辅助变量以编码程序执行历史，但 Abadi 和 Lamport 指出有时还需预知程序的未来行为，并提出 prophecy variables；然而将其集成到 Hoare 逻辑的工作几乎空白。本文首次在 Hoare 风格程序逻辑中给出 prophecy variables 的完整处理：利用分离逻辑中的所有权（ownership）编码解析预言的独占权，从而以非常简单的证明规则保证预言的可靠性，并在 Coq 的 Iris 框架中形式化。该方法足够灵活，可验证并发文献中经典例子（如 RDCSS 与 Herlihy-Wing 队列）的逻辑原子性（logical atomicity，线性一致性的近亲）。
Early in the development of Hoare logic, Owicki and Gries introduced auxiliary variables as a way of encoding information about the history of a program’s execution that is useful for verifying its correctness. Over a decade later, Abadi and Lamport observed that it is sometimes also necessary to know in advance what a program will do in the future . To address this need, they proposed prophecy variables , originally as a proof technique for refinement mappings between state machines. However, despite the fact that prophecy variables are a clearly useful reasoning mechanism, there is (surprisingly) almost no work that attempts to integrate them into Hoare logic. In this paper, we present the first account of prophecy variables in a Hoare-style program logic that is flexible enough to verify logical atomicity (a relative of linearizability) for classic examples from the concurrency literature like RDCSS and the Herlihy-Wing queue. Our account is formalized in the Iris framework for separation logic in Coq. It makes essential use of ownership to encode the exclusive right to resolve a prophecy, which in turn enables us to enforce soundness of prophecies with a very simple set of proof rules.
@article{paperbot545,
title = {The future is ours: prophecy variables in separation logic},
author = {Ralf Jung and Rodolphe Lepigre and Gaurav Parthasarathy and Marianna Rapoport and Amin Timany and Derek Dreyer and Bart Jacobs},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371113}
}