SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Fri 22 Oct 2021 11:35 - 11:50 at Zurich C - Algorithms, Libraries and Databases Chair(s): Hans-J. Boehm
Fri 22 Oct 2021 19:35 - 19:50 at Zurich C - Algorithms, Libraries and Databases - mirror Chair(s): Fabian Muehlboeck

Multicopy search structures such as log-structured merge (LSM) trees are optimized for high insert/update/delete (collectively known as upsert) performance. In such data structures, an upsert on key $k$, which adds $(k,v)$ where $v$ can be a value or a tombstone, is added to the root node even if $k$ is already present in other nodes. Thus there may be multiple copies of $k$ in the search structure. A search on $k$ aims to return the value associated with the most recent upsert. We present a general framework for verifying linearizability of concurrent multicopy search structures that abstracts from the underlying representation of the data structure in memory, enabling proof-reuse across diverse implementations. Based on our framework, we propose template algorithms for (a) LSM structures forming arbitrary directed acyclic graphs and (b) differential file structures, and formally verify these templates in the concurrent separation logic Iris. We also instantiate the LSM template to obtain the first verified concurrent in-memory LSM tree implementation.

Fri 22 Oct

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

10:50 - 12:10
Algorithms, Libraries and DatabasesOOPSLA at Zurich C +8h
Chair(s): Hans-J. Boehm Google
10:50
15m
Talk
UDF to SQL Translation through Compositional Lazy Inductive SynthesisVirtual
OOPSLA
Guoqiang Zhang North Carolina State University; Facebook, Yuanchao Xu North Carolina State University, Xipeng Shen North Carolina State University; Facebook, Işıl Dillig University of Texas at Austin
DOI
11:05
15m
Talk
LXM: Better Splittable Pseudorandom Number Generators (and Almost as Fast)Virtual
OOPSLA
Guy L. Steele Jr. Oracle Labs, Sebastiano Vigna University of Milan
DOI
11:20
15m
Talk
FPL: Fast Presburger Arithmetic through TransprecisionIn-PersonDistinguished Paper
OOPSLA
Arjun Pitchanathan IIIT Hyderabad, Christian Ulmann ETH Zurich, Michel Weber ETH Zurich, Torsten Hoefler ETH Zurich, Tobias Grosser University of Edinburgh
DOI
11:35
15m
Talk
Verifying Concurrent Multicopy Search StructuresIn-Person
OOPSLA
Nisarg Patel New York University, Siddharth Krishna Microsoft Research, Dennis Shasha New York University, Thomas Wies New York University
DOI
11:50
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA

18:50 - 20:10
Algorithms, Libraries and Databases - mirrorOOPSLA at Zurich C
Chair(s): Fabian Muehlboeck IST Austria
18:50
15m
Talk
UDF to SQL Translation through Compositional Lazy Inductive SynthesisVirtual
OOPSLA
Guoqiang Zhang North Carolina State University; Facebook, Yuanchao Xu North Carolina State University, Xipeng Shen North Carolina State University; Facebook, Işıl Dillig University of Texas at Austin
DOI
19:05
15m
Talk
LXM: Better Splittable Pseudorandom Number Generators (and Almost as Fast)Virtual
OOPSLA
Guy L. Steele Jr. Oracle Labs, Sebastiano Vigna University of Milan
DOI
19:20
15m
Talk
FPL: Fast Presburger Arithmetic through TransprecisionIn-PersonDistinguished Paper
OOPSLA
Arjun Pitchanathan IIIT Hyderabad, Christian Ulmann ETH Zurich, Michel Weber ETH Zurich, Torsten Hoefler ETH Zurich, Tobias Grosser University of Edinburgh
DOI
19:35
15m
Talk
Verifying Concurrent Multicopy Search StructuresIn-Person
OOPSLA
Nisarg Patel New York University, Siddharth Krishna Microsoft Research, Dennis Shasha New York University, Thomas Wies New York University
DOI
19:50
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA