paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Bring Your Own Data Structures to Datalog

把自定义数据结构带入 Datalog
OOPSLA 7(OOPSLA2)2023匹配度 3/10 · 该论文属于程序语言与静态分析基础设施工作,提升 Datalog 引擎表达能力并用于 Polonius、LLVM 等程序分析,与用户对静态分析和形式化的宽泛兴趣有交集;但完全不涉及 LLM/Agent、浮点程序分析或贝叶斯程序分析,未命中用户当前核心研究画像。引用 11 inbox
Arash Sahebolamri, Langston Barrett, Scott Moore, Kristopher Micinski
crossref: 2026-09-10

AI 速览

一句话:提出 Byods:一种嵌入 Rust 的 DSL,使 Datalog 规则对关系的数据结构表示参数化,从而突破引擎内置表示带来的算法复杂度瓶颈。

现代 Datalog 引擎通常把规则编译为对关系显式表示(B 树、哈希表等)的连接操作,虽具备良好可扩展性,但引擎固定数据结构的表示开销会使某些分析无法达到理想的算法复杂度。本文提出 "Bring Your Own Data Structures"(Byods)方法,以嵌入 Rust 的 DSL 形式实现:程序员书写的逻辑规则隐式地对关系的具体数据结构表示参数化,并可「自带」数据结构来表示关系,与编译器(以 Rust 过程宏实现)生成的代码协同工作。作者将 Byods 语义形式化为 Datalog 的扩展,刻画了兼容数据结构必须具备的关键性质,包括支持增量式(半朴素)求值所需性质。评估覆盖多类需要专门数据结构才能扩展的分析:传递与等价关系、Rust 借用检查器 Polonius 的优化版本、由格驱动的并行 PageRank,以及利用索引共享扩展的大规模 LLVM 分析。结果表明 Byods 改善了算法可扩展性(降低时间/空间复杂度),运行时间也与当前先进的并行 Datalog 求解器相当。

问题
现代 Datalog 引擎把关系固定表示为 B 树、哈希表等具体结构,表示层开销可能使分析无法达到期望的算法复杂度,且用户无法为特定关系选择更合适的数据结构。
方法
提出 Byods:用嵌入 Rust 的 DSL 编写逻辑规则,规则隐式地对关系的数据结构表示参数化,用户可自带数据结构并与编译器(Rust 过程宏)生成的代码协作;并将语义形式化为 Datalog 扩展,刻画兼容数据结构及半朴素增量求值所需性质。
评估
在传递/等价关系分析、优化版 Polonius 借用检查、格驱动的并行 PageRank 和基于索引共享的大规模 LLVM 分析上实现并测量,考察时间/空间复杂度与运行时间,并与先进并行 Datalog 求解器对比。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1863,
  title = {Bring Your Own Data Structures to Datalog},
  author = {Arash Sahebolamri and Langston Barrett and Scott Moore and Kristopher Micinski},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {OOPSLA2},
  year = {2023},
  doi = {10.1145/3622840}
}