Paper Info
Title
COMPASS: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic
Abstract
Several functional correctness criteria have been proposed for relaxed-memory consistency libraries, but most lack support for modular client reasoning. Mevel and Jourdan recently showed that logical atomicity can be used to give strong modular Hoare-style specifications for relaxed libraries, but only for a limited instance in the Multicore OCaml memory model. It has remained unclear if their approach scales to weaker implementations in weaker memory models. In this work, we combine logical atomicity together with richer partial orders (inspired by prior relaxed-memory correctness criteria) to develop stronger specifications in the weaker memory model of Repaired C11 (RC11). We show their applicability by proving them for multiple implementations of stacks, queues, and exchangers, and we demonstrate their strength by performing multiple client verifications on top of them. Our proofs are mechanized in Compass, a new framework extending the iRC11 separation logic, built atop Iris, in Coq. We report the first mechanized verifications of relaxed-memory implementations for the exchanger, the elimination stack, and the Herlihy-Wing queue.
Year
DOI
Venue
2022
10.1145/3519939.3523451
PROCEEDINGS OF THE 43RD ACM SIGPLAN INTERNATIONAL CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '22)
Keywords
DocType
Citations 
C11, relaxed memory models, separation logics, linearizability, logical atomicity, Iris
Conference
0
PageRank 
References 
Authors
0.34
0
7
Name
Order
Citations
PageRank
Hoang-Hai Dang111.70
Jaehwang Jung200.34
Jaemin Choi300.34
Duc-Than Nguyen400.34
William Mansky500.34
Jeehoon Kang600.34
Derek Dreyer754230.97