Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic

Jun 18, 2022

Speakers

About

Several functional correctness criteria have been proposed for \emph{relaxed-memory} consistency libraries, but most lack support for \emph{modular client reasoning}. M'{e}vel and Jourdan recently showed that \emph{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 \emph{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 exchanger, the elimination stack, and the Herlihy-Wing queue.

Organizer

Categories

Store presentation

Should this presentation be stored for 1000 years?

How do we store presentations

Total of 0 viewers voted for saving the presentation to eternal vault which is 0.0%

Recommended Videos

Presentations on similar topic, category or speaker

Interested in talks like this? Follow PLDI