This program is tentative and subject to change.

Wed 19 Jan 2022 10:45 - 11:10 at Salon III - Separation Logic Chair(s): James Riely

Today’s compilers employ a variety of non-trivial optimizations to achieve good performance. One key trick compilers use to justify transformations of \emph{concurrent} programs is to assume that the source program has no \emph{data races}: if it does, they cause the program to have \emph{undefined behavior} (UB) and give the compiler free rein. However, verifying correctness of optimizations that exploit this assumption is a non-trivial problem. In particular, prior work either has not proven that such optimizations preserve program termination (particularly non-obvious when considering optimizations that move instructions out of loop bodies), or has treated all synchronization operations as external functions (losing the ability to reorder instructions around them).

In this work we present \emph{Simuliris}, the first simulation technique to establish termination preservation (under a fair scheduler) for a range of concurrent program transformations that exploit UB in the source language. Simuliris is based on the idea of using \emph{ownership} to reason modularly about the assumptions the compiler makes about programs with well-defined behavior. This brings the benefits of \emph{concurrent separation logics} to the space of verifying program transformations: we can combine powerful reasoning techniques such as framing and coinduction to perform \emph{thread-local} proofs of non-trivial concurrent program optimizations. Simuliris is built on a (non-step-indexed) variant of the Coq-based Iris framework, and is thus not tied to a particular language. In addition to demonstrating the effectiveness of Simuliris on standard compiler optimizations involving data race UB, we also instantiate it with Jung et al.’s Stacked Borrows semantics for Rust and generalize their proofs of interesting type-based aliasing optimizations to account for concurrency.

This program is tentative and subject to change.

Wed 19 Jan

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

10:20 - 12:00
Separation LogicPOPL at Salon III
Chair(s): James Riely DePaul University
10:20
25m
Talk
A Separation Logic for Heap Space under Garbage CollectionRemote
POPL
10:45
25m
Research paper
Simuliris: A Separation Logic Framework for Verifying Concurrent Program OptimizationsDistinguished PaperRemote
POPL
Lennard Gäher MPI-SWS & Saarland University, Michael Sammler MPI-SWS, Simon Spies MPI-SWS, Ralf Jung MIT, Hoang-Hai Dang MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS
11:10
25m
Research paper
Concurrent Incorrectness Separation LogicRemote
POPL
Azalea Raad Imperial College London, Josh Berdine Facebook, Derek Dreyer MPI-SWS, Peter W. O'Hearn Facebook and University College London
11:35
25m
Research paper
On Incorrectness Logic and Kleene Algebra With Top and TestsInPerson
POPL
Cheng Zhang Boston University, Arthur Azevedo de Amorim Boston University, USA, Marco Gaboardi Boston University
Hide past events