一句话：提出 eager evaluation，替代半朴素 Datalog 求值，大幅加速 Formulog 的 SMT 静态分析。
Formulog 结合 Datalog、SMT 与函数式编程，便于声明式实现精化类型检查、符号执行等 SMT 静态分析，但定制 Datalog 求解器性能阻碍其超越原型。本文发现常规高性能 Datalog 技术（编译、专用数据结构）仅加速约 2.2×；核心贡献是放弃半朴素求值，提出 eager evaluation：按深度优先遍历逻辑推理空间的并发 Datalog 求值算法，更好分发 SMT 工作负载并改善求解时间。在 Formulog 解释器和 Soufflé 代码生成器中实现后，SMT 密集型基准相较优化 Soufflé 平均加速 5.2× 和 7.6×。结合编译与 eager evaluation，精化类型检查、指针分析和符号执行在 23 个基准中的 20 个上超过已发表 F♯、Java、C++ 手写分析，表明 Formulog 可成为现实 SMT 静态分析平台，并挑战半朴素求值普遍最优的传统观点。
With its combination of Datalog, SMT solving, and functional programming, the language Formulog provides an appealing mix of features for implementing SMT-based static analyses (e.g., refinement type checking, symbolic execution) in a natural, declarative way. At the same time, the performance of its custom Datalog solver can be an impediment to using Formulog beyond prototyping—a common problem for Datalog variants that aspire to solve large problem instances. In this work we speed up Formulog evaluation, with some surprising results: while 2.2× speedups can be obtained by using the conventional techniques for high-performance Datalog (e.g., compilation, specialized data structures), the big wins come by abandoning the central assumption in modern performant Datalog engines, semi-naive Datalog evaluation. In the place of semi-naive evaluation, we develop eager evaluation, a concurrent Datalog evaluation algorithm that explores the logical inference space via a depth-first traversal order. In practice, eager evaluation leads to an advantageous distribution of Formulog’s SMT workload to external SMT solvers and improved SMT solving times: our eager evaluation extensions to the Formulog interpreter and Soufflé’s code generator achieve mean 5.2× and 7.6× speedups, respectively, over the optimized code generated by off-the-shelf Soufflé on SMT-heavy Formulog benchmarks. All in all, using compilation and eager evaluation (as appropriate), Formulog implementations of refinement type checking, bottom-up pointer analysis, and symbolic execution achieve speedups on 20 out of 23 benchmarks over previously published, hand-tuned analyses written in F♯, Java, and C++, providing strong evidence that Formulog can be the basis of a realistic platform for SMT-based static analysis. Moreover, our experience adds nuance to the conventional wisdom that traditional semi-naive evaluation is the one-size-fits-all best Datalog evaluation algorithm for static analysis workloads.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Bembenek0C24,
title = {Making Formulog Fast: An Argument for Unconventional Datalog Evaluation},
author = {Aaron Bembenek and Michael Greenberg and Stephen Chong},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689754}
}