Fri 17 Jun 2022 13:30 - 13:50 at Kon-Tiki - Verification I Chair(s): Ralf Jung
Sat 18 Jun 2022 01:30 - 01:50 at Kon-Tiki - Verification I

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.

Fri 17 Jun

Displayed time zone: Pacific Time (US & Canada) change

13:30 - 14:50
Verification IPLDI at Kon-Tiki +12h
Chair(s): Ralf Jung MPI-SWS
13:30
20m
Talk
Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic
PLDI
Hoang-Hai Dang MPI-SWS, Jaehwang Jung KAIST, South Korea, Jaemin Choi KAIST, Duc-Than Nguyen University of Illinois at Chicago, William Mansky University of Illinois at Chicago, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS
DOI
13:50
20m
Talk
Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris
PLDI
Ike Mulder Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen, Herman Geuvers Radboud University Nijmegen, Netherlands
Link to publication DOI Pre-print
14:10
20m
Talk
Islaris: Verification of Machine Code Against Authoritative ISA Semantics
PLDI
Michael Sammler MPI-SWS, Angus Hammond University of Cambridge, Rodolphe Lepigre MPI-SWS, Brian Campbell University of Edinburgh, Jean Pichon-Pharabod Aarhus University, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS, Peter Sewell University of Cambridge
DOI
14:30
20m
Talk
RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code
PLDI
Yusuke Matsushita The University of Tokyo, Xavier Denis Université Paris-Saclay, CNRS, ENS Paris-Saclay, INRIA, Laboratoire Méthodes Formelles, Jacques-Henri Jourdan Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Derek Dreyer MPI-SWS
DOI

Sat 18 Jun

Displayed time zone: Pacific Time (US & Canada) change

01:30 - 02:50
Verification IPLDI at Kon-Tiki
01:30
20m
Talk
Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic
PLDI
Hoang-Hai Dang MPI-SWS, Jaehwang Jung KAIST, South Korea, Jaemin Choi KAIST, Duc-Than Nguyen University of Illinois at Chicago, William Mansky University of Illinois at Chicago, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS
DOI
01:50
20m
Talk
Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris
PLDI
Ike Mulder Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen, Herman Geuvers Radboud University Nijmegen, Netherlands
Link to publication DOI Pre-print
02:10
20m
Talk
Islaris: Verification of Machine Code Against Authoritative ISA Semantics
PLDI
Michael Sammler MPI-SWS, Angus Hammond University of Cambridge, Rodolphe Lepigre MPI-SWS, Brian Campbell University of Edinburgh, Jean Pichon-Pharabod Aarhus University, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS, Peter Sewell University of Cambridge
DOI
02:30
20m
Talk
RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code
PLDI
Yusuke Matsushita The University of Tokyo, Xavier Denis Université Paris-Saclay, CNRS, ENS Paris-Saclay, INRIA, Laboratoire Méthodes Formelles, Jacques-Henri Jourdan Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Derek Dreyer MPI-SWS
DOI