一句话：提出增量规则求值方法 IRE，通过对比优化程序与禁用跨规则优化的参考程序，自动检测 Datalog 引擎的优化缺陷。
Datalog 是流行的声明式逻辑编程语言，其引擎会执行大量跨规则优化，这些优化中的缺陷会导致结果不正确。为检测此类缺陷，论文提出自动化测试方法 IRE（增量规则求值），协同解决测试预言与测试用例生成问题：测试预言的核心思想是比较经过优化的程序与未做跨规则优化的程序的结果，差异即表明引擎存在缺陷；其洞见在于，对增量生成的优化 Datalog 程序，可通过构造参考程序禁用多规则间优化，从而单独求值每条规则。增量生成测试用例使每条新规则都能立即应用测试预言，并以一定概率保证新规则产生非空结果，同时避免重算已推出的事实。作者实现工具 Deopt，在 Soufflé、CozoDB、μZ 与 DDlog 四个成熟引擎上评测，共发现 30 个缺陷，其中 13 个为逻辑错误，其余为崩溃与错误类缺陷；Deopt 覆盖了最先进方法 queryFuzz 发现的全部缺陷，而其中 5 个 queryFuzz 无法发现。增量生成也高效：在含 60 条规则的用例上，其产生的有效非空测试用例数是朴素随机方法的 1.17 倍（DDlog）至 31.02 倍（Soufflé）。
Datalog is a popular and widely-used declarative logic programming language. Datalog engines apply many cross-rule optimizations; bugs in them can cause incorrect results. To detect such optimization bugs, we propose an automated testing approach called Incremental Rule Evaluation (IRE), which synergistically tackles the test oracle and test case generation problem. The core idea behind the test oracle is to compare the results of an optimized program and a program without cross-rule optimization; any difference indicates a bug in the Datalog engine. Our core insight is that, for an optimized, incrementally-generated Datalog program, we can evaluate all rules individually by constructing a reference program to disable the optimizations that are performed among multiple rules. Incrementally generating test cases not only allows us to apply the test oracle for every new rule generated—we also can ensure that every newly added rule generates a non-empty result with a given probability and eschew recomputing already-known facts. We implemented IRE as a tool named Deopt, and evaluated Deopt on four mature Datalog engines, namely Soufflé, CozoDB, μZ, and DDlog, and discovered a total of 30 bugs. Of these, 13 were logic bugs, while the remaining were crash and error bugs. Deopt can detect all bugs found by queryFuzz, a state-of-the-art approach. Out of the bugs identified by Deopt, queryFuzz might be unable to detect 5. Our incremental test case generation approach is efficient; for example, for test cases containing 60 rules, our incremental approach can produce 1.17× (for DDlog) to 31.02× (for Soufflé) as many valid test cases with non-empty results as the naive random method. We believe that the simplicity and the generality of the approach will lead to its wide adoption in practice.
@article{paperbot2556,
title = {Finding Cross-Rule Optimization Bugs in Datalog Engines},
author = {Chi Zhang and Linzhang Wang and Manuel Rigger},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649815}
}