SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Thu 21 Oct 2021 11:35 - 11:50 at Zurich F - PLDI 2020 Papers 1 Chair(s): Luís Pina

Concurrent separation logics have had great success reasoning about
concurrent data structures.
This success stems from their application of modularity on multiple levels, leading to proofs that are decomposed according to program structure, program state, and individual threads.
Despite these advances, it remains difficult to achieve proof reuse across
different data structure implementations.
For the large class of \emph{search structures}, we demonstrate how one can achieve further proof modularity by decoupling the proof of thread safety from the proof of structural integrity.
We base our work on the \emph{template} algorithms of Shasha and
Goodman that dictate how threads interact but abstract from the
concrete layout of nodes in memory.
Building on the recently proposed flow framework of compositional abstractions and the separation logic Iris, we show how to prove correctness of template algorithms, and how to instantiate them to obtain multiple verified implementations.

We demonstrate our approach by mechanizing the proofs of three concurrent search
structure templates, based on link, give-up, and lock-coupling synchronization, and deriving verified implementations based on B-trees, hash tables, and linked lists.
These case studies include algorithms used in real-world file systems
and databases, which have been beyond the capability of prior automated or mechanized verification techniques.
In addition, our approach reduces proof complexity and is able to achieve significant proof reuse.

Thu 21 Oct

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

10:50 - 12:10
PLDI 2020 Papers 1SIGPLAN Papers at Zurich F
Chair(s): Luís Pina University of Illinois at Chicago
10:50
15m
Talk
Armada: Low-Effort Verification of High-Performance Concurrent Programs
SIGPLAN Papers
Jacob R. Lorch Microsoft Research, n.n., Yixuan Chen Yale University, USA, Manos Kapritsos University of Michigan, USA, Bryan Parno Carnegie Mellon University, USA, Shaz Qadeer Novi, USA, Upamanyu Sharma University of Michigan, USA, James R. Wilcox University of Washington, Xueyuan Zhao Carnegie Mellon University, USA
DOI
11:05
15m
Talk
Decidable Verification under a Causally Consistent Shared Memory
SIGPLAN Papers
Ori Lahav Tel Aviv University, Udi Boker IDC Herzliya, Israel
11:20
15m
Talk
Efficient Handling of String-Number Conversion
SIGPLAN Papers
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Yu-Fang Chen Academia Sinica, Taiwan, Bui Phi Diep Uppsala University, Sweden, Julian Dolby IBM Research, USA, Petr Janků Brno University of Technology, Czechia, Hsin-Hung Lin Academia Sinica, Taiwan, Lukáš Holík Brno University of Technology, Wei-Cheng Wu University of Southern California, USA
11:35
15m
Talk
Verifying Concurrent Search Structure Templates
SIGPLAN Papers
Siddharth Krishna Microsoft Research, Nisarg Patel New York University, Dennis Shasha New York University, Thomas Wies New York University
11:50
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers