SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Thu 26 Oct 2023 11:54 - 12:12 at Room II - language semantics Chair(s): Sebastian Erdweg

The restricted logic programming language Datalog has become a popular implementation target for deductive-analytic workloads including social-media analytics and program analysis. Modern Datalog engines compile Datalog rules to joins over explicit representations of relations—often B-trees or hash maps. While these modern engines have enabled high scalability in many application domains, they have a crucial weakness: achieving the desired algorithmic complexity may be impossible due to representation-imposed overhead of the engine’s data structures. In this paper, we present the "Bring Your Own Data Structures" (Byods) approach, in the form of a DSL embedded in Rust. Using Byods, an engineer writes logical rules which are implicitly parametric on the concrete data structure representation; our implementation provides an interface to enable "bringing their own" data structures to represent relations, which harmoniously interact with code generated by our compiler (implemented as Rust procedural macros). We formalize the semantics of Byods as an extension of Datalog’s; our formalization captures the key properties demanded of data structures compatible with Byods, including properties required for incrementalized (semi-naïve) evaluation. We detail many applications of the Byods approach, implementing analyses requiring specialized data structures for transitive and equivalence relations to scale, including an optimized version of the Rust borrow checker Polonius; highly-parallel PageRank made possible by lattices; and a large-scale analysis of LLVM utilizing index-sharing to scale. Our results show that Byods offers both improved algorithmic scalability (reduced time and/or space complexity) and runtimes competitive with state-of-the-art parallelizing Datalog solvers.

Thu 26 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
language semanticsOOPSLA at Room II
Chair(s): Sebastian Erdweg JGU Mainz
11:00
18m
Talk
The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog
OOPSLA
Qinlin Chen Nanjing University, Nairen Zhang Nanjing University, Jinpeng Wang Nanjing University, Tian Tan Nanjing University, Chang Xu Nanjing University, Xiaoxing Ma Nanjing University, Yue Li Nanjing University
DOI
11:18
18m
Talk
Regular Expression Matching using Bit Vector Automata
OOPSLA
Alexis Le Glaunec Rice University, Lingkun Kong Rice University, Konstantinos Mamouras Rice University
DOI
11:36
18m
Talk
Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Manipulation of Objects
OOPSLA
Xing Zhang Peking University, Guanchen Guo Peking University, Xiao He University of Science and Technology Beijing, Zhenjiang Hu Peking University
DOI
11:54
18m
Talk
Bring Your Own Data Structures to DatalogDistinguished Paper
OOPSLA
Arash Sahebolamri Syracuse University, Langston Barrett Galois, Scott Moore Galois, Kristopher Micinski Syracuse University
DOI
12:12
18m
Talk
Rhombus: A New Spin on Macros without All the Parentheses
OOPSLA
Matthew Flatt University of Utah, Taylor Allred University of Utah, Nia Angle independent, Stephen De Gabrielle independent, Robert Bruce Findler Northwestern University, Jack Firth independent, Kiran Gopinathan National University of Singapore, Ben Greenman University of Utah, Siddhartha Kasivajhula independent, Alex Knauth independent, Jay McCarthy Reach, Sam Phillips independent, Sorawee Porncharoenwase University of Washington, Jens Axel Søgaard independent, Sam Tobin-Hochstadt Indiana University
DOI Pre-print