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.
Wed 22 Jan
|14:00 - 14:21|
Ralf JungMPI-SWS, Rodolphe LepigreMPI-SWS, Gaurav ParthasarathyETH Zurich, Marianna RapoportUniversity of Waterloo, Amin Timanyimec-Distrinet KU-Leuven, Derek DreyerMPI-SWS, Bart Jacobsimec-DistriNet, Dept. CS, KU LeuvenLink to publication DOI Media Attached
|14:21 - 14:43|
Paulo Emílio de VilhenaInria, François PottierInria, France, Jacques-Henri JourdanCNRS, LRI, Université Paris-SudLink to publication DOI Media Attached File Attached
|14:43 - 15:05|
Jonas Kastberg HinrichsenIT University of Copenhagen, Jesper BengtsonIT University of Copenhagen, Robbert KrebbersDelft University of TechnologyLink to publication DOI Media Attached File Attached