The Future is Ours

Prophecy Variables in Separation Logic

Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs.
POPL 2020.

Paper Artifact (with VM) Source code repositories

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.

Source code repositories

  • Basic support for prophecy variables, their proof rules and the erasure theorem are provided by Iris itself.
  • Our Iris case studies and the "typed" prophecy variable interface can be found in the Iris Examples repository, in the logatom and proph folders.
  • VeriFast comes with examples demonstrating prophecy variables:
    • splitcounter: a simple concurrent data structure that implements a single abstract counter in terms of two physical counters
    • jayanti: a snapshot algorithm by Jayanti, as quoted in Delbianco, Sergey, Nanevski, and Banerjee, "Concurrent data structures linked in time", ECOOP 2017
    • mcas: the Restricted Double Compare Single Swap (RDCSS) and Multiple Compare And Swap (MCAS) algorithms by Harris et al., as quoted in Vafeiadis' PhD thesis
This paper was realized using Iris.