A separation logic for refining concurrent objects


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).