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

18. Červen 2022

Řečníci

O prezentaci

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.

Organizátor

Kategorie

Uložení prezentace

Měla by být tato prezentace uložena po dobu 1000 let?

Jak ukládáme prezentace

Pro uložení prezentace do věčného trezoru hlasovalo 0 diváků, což je 0.0 %

Doporučená videa

Prezentace na podobné téma, kategorii nebo přednášejícího

Zajímají Vás podobná videa? Sledujte PLDI