Automatically Testing Datalog Engines to find Optimization Bugs
31/03/2023
Speaker
Abstract
Datalog is a popular and widely-used declarative logic programming language, consisting of rules that are applied to facts. To detect optimization bugs in Datalog engines, in this talk, 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 non-optimized program; any difference indicates a bug in the Datalog engine. It is challenging to obtain a non-optimized program in a black-box way, because we cannot generally assume the presence of optimization options. Our core insight is that, for an optimized Datalog program, we can evaluate all rules individually by incrementally 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 three mature Datalog engines, namely Soufflé, DDlog, and µZ, and discovered a total of 23 bugs. We believe that the simplicity—the core algorithm is implemented in less than 200 lines of code—and the generality of the approach will lead to its wide adoption in practice.
Bio
Chi Zhang is a PhD student from Nanjing University, China, and is currently visiting the NUS TEST lab. His research interests span static analysis, fuzzing, symbolic execution, and the combination of software engineering with artificial intelligence, focusing on detecting the bugs in software.