A separation logic for refining concurrent objects
Abstract
Fine-grained concurrent data structures are crucial for gaining
performance from multiprocessing, but their design is a subtle
art. Recent literature has made large strides in verifying these
data structures, using either atomicity refinement or separation
logic with rely-guarantee reasoning. In this paper we show how
the ownership discipline of separation logic can be used to
enable atomicity refinement, and we develop a new rely-guarantee
method that is localized to the definition of a data structure.
The result is a comprehensive and tidy account of concurrent
data refinement that clarifies and consolidates the existing
approaches.
Paper: pdf
Technical appendix and errata: pdf.
Gives the full proof of adequacy, refinement laws, fenced refinement
laws, the definition of simulation, and sketches the proof of Data2.
(Note: the appendix is not yet synchronized with the final POPL paper).