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