A Typed Multi-level Datalog IR and Its Compiler Framework
David Klopp, Sebastian Erdweg, André Pacak
摘要
The resurgence of Datalog in the last two decades has led to a multitude of new Datalog systems. These systems explore novel ideas for improving Datalog’s programmability and performance, making important contributions to the field. Unfortunately, the individual systems progress at a much slower pace than the overall field, because improvements in one system are rarely ported to other systems. The reason for this rift is that each system provides its own Datalog dialect with specific notation, language features, and invariants, enabling specific optimization and execution strategies. This paper presents the first compiler framework for Datalog that can be used to support any Datalog frontend language and to target any Datalog backend. The centerpiece of our framework is a novel typed multi-level Datalog IR that supports IR extensions and guarantees executability. Existing Datalog systems can provide a compiler frontend that translates their Datalog dialect to the extended IR. The IR is then progressively lowered toward core Datalog, allowing optimizations at each level. At last, compiler backends can target different Datalog solvers. We have implemented the compiler framework and integrated 4 Datalog frontends and 3 Datalog backends, using 16 IR extensions. We also formalize the IR’s flexible type system, which is bidirectional, flow-sensitive, bipolar, and uses three-valued typing contexts. The type system simultaneously validates type compatibility and precisely tracks bindings of logic variables while permitting IR extensions.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper1
问问它们各自怎么用它它引用的顶会 Paper7
- Incremental whole-program analysis in Datalog with latticesTamás Szabó, Sebastian Erdweg, Gábor BergmannPLDI 2021 · 被引用 39 次
- Better Together: Unifying Datalog and Equality SaturationYihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao 等PLDI 2023 · 被引用 38 次
- Formulog: Datalog for SMT-based static analysisAaron Bembenek, Michael Greenberg, Stephen ChongOOPSLA 2020 · 被引用 26 次
- Fixpoints for the masses: programming with first-class Datalog constraintsMagnus Madsen, Ondrej LhotákOOPSLA 2020 · 被引用 22 次
- Rhombus: A New Spin on Macros without All the ParenthesesMatthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle 等OOPSLA 2023 · 被引用 5 次
相关 Paper
- A systematic approach to deriving incremental type checkersAndré Pacak, Sebastian Erdweg, Tamás SzabóOOPSLA 2020 · 被引用 16 次
- Optimizing Parallel Recursive Datalog Evaluation on Multicore MachinesJiacheng Wu, Jin Wang, Carlo ZanioloSIGMOD 2022 · 被引用 9 次
- Datalog with First-Class FactsThomas Gilray, Arash Sahebolamri, Yihao Sun, Sowmith Kunapaneni 等VLDB 2025 · 被引用 3 次
- Incremental Inference for Probabilistic DatalogXuyang Li, Weiyi Chen, Isil Dillig, Jingbo WangCAV 2026
- Interactive Debugging of Datalog ProgramsAndré Pacak, Sebastian ErdwegOOPSLA 2023 · 被引用 4 次
