SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Fri 27 Oct 2023 17:12 - 17:30 at Room XII - separation logic Chair(s): Jonathan Aldrich

This paper introduces semi-ring dictionaries, a powerful class of compositional and purely functional collections that subsume other collection types such as sets, multisets, arrays, vectors, and matrices. We developed SDQL, a statically typed language that can express relational algebra with aggregations, linear algebra, and functional collections over data such as relations and matrices using semi-ring dictionaries. Furthermore, thanks to the algebraic structure behind these dictionaries, SDQL unifies a wide range of optimizations commonly used in databases (DB) and linear algebra (LA). As a result, SDQL enables efficient processing of hybrid DB and LA workloads, by putting together optimizations that are otherwise confined to either DB systems or LA frameworks. We show experimentally that a handful of DB and LA workloads can take advantage of the SDQL language and optimizations. SDQL can be competitive with or outperforms a host of systems that are state of the art in their own domain: in-memory DB systems Typer and Tectorwise for (flat, not nested) relational data; SciPy for LA workloads; sparse tensor compiler taco; the Trance nested relational engine; and the in-database machine learning engines LMFAO and Morpheus for hybrid DB/LA workloads over relational data.

Fri 27 Oct

Displayed time zone: Lisbon change

16:00 - 17:30
separation logicOOPSLA at Room XII
Chair(s): Jonathan Aldrich Carnegie Mellon University
16:00
18m
Talk
Verification-Preserving Inlining in Automatic Separation Logic Verifiers
OOPSLA
Thibault Dardinier ETH Zurich, Gaurav Parthasarathy ETH Zurich, Peter Müller ETH Zurich
DOI
16:18
18m
Talk
Leaf: Modularity for Temporary Sharing in Separation Logic
OOPSLA
Travis Hance Carnegie Mellon University, Jon Howell VMware Research, Oded Padon VMware Research, Bryan Parno Carnegie Mellon University
DOI
16:36
18m
Talk
Proof Automation for Linearizability in Separation Logic
OOPSLA
Ike Mulder Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen
DOI Pre-print
16:54
18m
Talk
Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
OOPSLA
Jaehwang Jung KAIST, Janggun Lee KAIST, Jaemin Choi KAIST, Jaewoo Kim KAIST, Sunho Park KAIST, Jeehoon Kang KAIST
DOI
17:12
18m
Talk
Functional collection programming with semi-ring dictionaries
OOPSLA
Amir Shaikhha University of Edinburgh, Mathieu Huot University of Oxford, Jaclyn Smith Oxford University, Dan Olteanu University of Zurich
Link to publication DOI