The future is ours: prophecy variables in separation logic
Journal Paper
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 lets us enforce soundness of prophecies with a very simple set of proof rules.
The bibtex source for this publication:
@article{DBLP:journals/pacmpl/JungLPRTDJ20,
author = {Ralf Jung and
Rodolphe Lepigre and
Gaurav Parthasarathy and
Marianna Rapoport and
Amin Timany and
Derek Dreyer and
Bart Jacobs},
title = {The future is ours: prophecy variables in separation logic},
journal = {{PACMPL}},
volume = {4},
number = {{POPL}},
pages = {45:1--45:32},
year = {2020},
url = {https://doi.org/10.1145/3371113},
doi = {10.1145/3371113},
timestamp = {Mon, 13 Jan 2020 08:55:28 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/JungLPRTDJ20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}