Finding Cross-Rule Optimization Bugs in Datalog Engines
Article No.: 98, Pages 110 - 136
Abstract
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.
Supplementary Material
The supplementary material of Deopt, including the description of the bugs found by Deopt.
- Download
- 453.40 KB
References
[1]
Serge Abiteboul and Richard Hull. 1988. Data Functions, Datalog and Negation. In Proceedings of the 1988 ACM SIGMOD International Conference on Management of Data (SIGMOD ’88). Association for Computing Machinery, New York, NY, USA. 143–153. isbn:0897912683 https://doi.org/10.1145/50202.50218
[2]
Serge Abiteboul, Richard Hull, and Victor Vianu. 1995. Foundations of databases. 8, Addison-Wesley Reading.
[3]
Mario Alviano, Wolfgang Faber, Gianluigi Greco, and Nicola Leone. 2012. Magic sets for disjunctive datalog programs. Artificial Intelligence, 187 (2012), 156–192.
[4]
Tony Antoniadis, Konstantinos Triantafyllou, and Yannis Smaragdakis. 2017. Porting Doop to Soufflé: A Tale of Inter-Engine Portability for Datalog-Based Analyses. In Proceedings of the 6th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis (SOAP 2017). Association for Computing Machinery, New York, NY, USA. 25–30. isbn:9781450350723 https://doi.org/10.1145/3088515.3088522
[5]
Samuel Arch, Xiaowen Hu, David Zhao, Pavle Subotić, and Bernhard Scholz. 2022. Building a Join Optimizer for Soufflé. In Logic-Based Program Synthesis and Transformation, Alicia Villanueva (Ed.). Springer International Publishing, Cham. 83–102. isbn:978-3-031-16767-6
[6]
Molham Aref, Balder ten Cate, Todd J Green, Benny Kimelfeld, Dan Olteanu, Emir Pasalic, Todd L Veldhuizen, and Geoffrey Washburn. 2015. Design and implementation of the LogicBlox system. In Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data. 1371–1382.
[7]
John Backes, Sam Bayless, Byron Cook, Catherine Dodge, Andrew Gacek, Alan J Hu, Temesghen Kahsai, Bill Kocik, Evgenii Kotelnikov, and Jure Kukovec. 2019. Reachability analysis for AWS-based networks. In International Conference on Computer Aided Verification. 231–241.
[8]
Isaac Balbin and Kotagiri Ramamohanarao. 1987. A generalization of the differential approach to recursive query evaluation. The Journal of Logic Programming, 4, 3 (1987), 259–262.
[9]
Francois Bancilhon, David Maier, Yehoshua Sagiv, and Jeffrey D Ullman. 1985. Magic Sets and Other Strange Ways to Implement Logic Programs (Extended Abstract). In Proceedings of the Fifth ACM SIGACT-SIGMOD Symposium on Principles of Database Systems (PODS ’86). Association for Computing Machinery, New York, NY, USA. 1–15. isbn:0897911792 https://doi.org/10.1145/6012.15399
[10]
Francois Bancilhon and Raghu Ramakrishnan. 1986. An amateur’s introduction to recursive query processing strategies. In Proceedings of the 1986 ACM SIGMOD international conference on Management of data. 16–52.
[11]
Aaron Bembenek, Michael Greenberg, and Stephen Chong. 2020. Formulog: Datalog for SMT-based static analysis. Proceedings of the ACM on Programming Languages, 4, OOPSLA (2020), 1–31.
[12]
Conrado Borraz-Sánchez, Diego Klabjan, Emir Pasalic, and Molham Aref. 2018. SolverBlox: algebraic modeling in datalog. In Declarative Logic Programming: Theory, Systems, and Applications, Michael Kifer and Yanhong Annie Liu (Eds.) (ACM Books, Vol. 20). ACM / Morgan & Claypool, 331–354. https://doi.org/10.1145/3191315.3191322
[13]
Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly declarative specification of sophisticated points-to analyses. In Proceedings of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications. 243–262.
[14]
Lexi Brent, Anton Jurisevic, Michael Kong, Eric Liu, Francois Gauthier, Vincent Gramoli, Ralph Holz, and Bernhard Scholz. 2018. Vandal: A scalable security analysis framework for smart contracts. arXiv preprint arXiv:1809.03981.
[15]
Francesco Buccafurri, Nicola Leone, and Pasquale Rullo. 1997. Strong and weak constraints in disjunctive datalog. In Logic Programming And Nonmonotonic Reasoning, Jürgen Dix, Ulrich Furbach, and Anil Nerode (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 2–17. isbn:978-3-540-69249-2
[16]
F. Buccafurri, N. Leone, and P. Rullo. 2000. Enhancing Disjunctive Datalog by constraints. IEEE Transactions on Knowledge and Data Engineering, 12, 5 (2000), 845–860. https://doi.org/10.1109/69.877512
[17]
Rafael Caballero, Yolanda García-Ruiz, and Fernando Sǽnz-Pérez. 2008. A theoretical framework for the declarative debugging of datalog programs. In International Workshop on Semantics in Data and Knowledge Bases. 143–159.
[18]
Rafael Caballero, Yolanda García-Ruiz, and Fernando Sǽnz-Pérez. 2015. Debugging of wrong and missing answers for Datalog programs with constraint handling rules. In Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming. 55–66.
[19]
Stefano Ceri, Georg Gottlob, and Letizia Tanca. 1989. What you always wanted to know about Datalog(and never dared to ask). IEEE transactions on knowledge and data engineering, 1, 1 (1989), 146–166.
[20]
Tsong Y Chen, Shing C Cheung, and Shiu Ming Yiu. 2020. Metamorphic testing: a new approach for generating next test cases. arXiv preprint arXiv:2002.12543.
[21]
Tsong Yueh Chen, Fei-Ching Kuo, Huai Liu, Pak-Lok Poon, Dave Towey, TH Tse, and Zhi Quan Zhou. 2018. Metamorphic testing: A review of challenges and opportunities. ACM Computing Surveys (CSUR), 51, 1 (2018), 1–27.
[22]
Mariano P. Consens and Alberto O. Mendelzon. 1990. Low complexity aggregation in graphlog and Datalog. In ICDT ’90, Serge Abiteboul and Paris C. Kanellakis (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 379–394. isbn:978-3-540-46682-6
[23]
Neil Conway, William R Marczak, Peter Alvaro, Joseph M Hellerstein, and David Maier. 2012. Logic and lattices for distributed programming. In Proceedings of the Third ACM Symposium on Cloud Computing. 1–14.
[24]
Edsger Wybe Dijkstra. 1970. Notes on structured programming.
[25]
Neville Grech, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. 2019. Gigahorse: thorough, declarative decompilation of smart contracts. In 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE). 1176–1186.
[26]
S. Greco. 1999. Dynamic programming in Datalog with aggregates. IEEE Transactions on Knowledge and Data Engineering, 11, 2 (1999), 265–283. https://doi.org/10.1109/69.761663
[27]
Todd J. Green, Shan Shan Huang, Boon Thau Loo, and Wenchao Zhou. 2013. Datalog and Recursive Query Processing. Foundations and Trends® in Databases, 5, 2 (2013), 105–195. issn:1931-7883 https://doi.org/10.1561/1900000017
[28]
Todd J Green, Shan Shan Huang, Boon Thau Loo, and Wenchao Zhou. 2013. Datalog and recursive query processing. Foundations and Trends® in Databases, 5, 2 (2013), 105–195.
[29]
Elnar Hajiyev, Mathieu Verbaere, and Oege de Moor. 2006. Codequest: Scalable source code queries with datalog. In European Conference on Object-Oriented Programming. 2–27.
[30]
Kryštof Hoder, Nikolaj Bjørner, and Leonardo de Moura. 2011. μ Z–an efficient engine for fixed points with constraints. In International Conference on Computer Aided Verification. 457–462.
[31]
Xiaowen Hu, Joshua Karp, David Zhao, Abdul Zreika, Xi Wu, and Bernhard Scholz. 2021. The Choice Construct in the Soufflé Language. In Asian Symposium on Programming Languages and Systems. 163–181.
[32]
Xiaowen Hu, David Zhao, Herbert Jordan, and Bernhard Scholz. 2021. An Efficient Interpreter for Datalog by De-Specializing Relations. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021). Association for Computing Machinery, New York, NY, USA. 681–695. isbn:9781450383912 https://doi.org/10.1145/3453483.3454070
[33]
Ziyang Hu. 2023. CozoDB: Hippocampus for AI, with Embedded Datalog. https://www.cozodb.org/ Accessed: 2023-05-16
[34]
Zu-Ming Jiang, Jia-Ju Bai, and Zhendong Su. 2023. DynSQL: Stateful Fuzzing for Database Management Systems with Complex and Valid SQL Query Generation. In Proceedings of the 32nd USENIX Security Symposium (Security’23).
[35]
Herbert Jordan, Bernhard Scholz, and Pavle Subotić. 2016. Soufflé: On synthesis of program analyzers. In International Conference on Computer Aided Verification. 422–430.
[36]
Herbert Jordan, Pavle Subotić, David Zhao, and Bernhard Scholz. 2019. Brie: A specialized trie for concurrent datalog. In Proceedings of the 10th International Workshop on Programming Models and Applications for Multicores and Manycores. 31–40.
[37]
Herbert Jordan, Pavle Subotić, David Zhao, and Bernhard Scholz. 2019. A specialized B-tree for concurrent datalog evaluation. In Proceedings of the 24th symposium on principles and practice of parallel programming. 327–339.
[38]
Herbert Jordan, Pavle Subotić, David Zhao, and Bernhard Scholz. 2022. Specializing parallel data structures for Datalog. Concurrency and Computation: Practice and Experience, 34, 2 (2022), e5643.
[39]
Bas Ketsman and Paraschos Koutris. 2022. Modern Datalog Engines. Foundations and Trends® in Databases, 12, 1 (2022), 1–68.
[40]
Werner Kieß ling and Ulrich Güntzer. 1994. Database reasoning—a deductive framework for solving large and complex problems by means of subsumption. In Workshop on Information Systems and Artificial Intelligence. 118–138.
[41]
Sven Köhler, Bertram Ludäscher, and Yannis Smaragdakis. 2012. Declarative datalog debugging for mere mortals. In International Datalog 2.0 Workshop. 111–122.
[42]
Monica S Lam, John Whaley, V Benjamin Livshits, Michael C Martin, Dzintars Avots, Michael Carbin, and Christopher Unkel. 2005. Context-sensitive program analysis as database queries. In Proceedings of the twenty-fourth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems. 1–12.
[43]
Yu Liang, Song Liu, and Hong Hu. 2022. Detecting Logical Bugs of $DBMS$ with Coverage-based Guidance. In 31st USENIX Security Symposium (USENIX Security 22). 4309–4326.
[44]
Boon Thau Loo, Tyson Condie, Minos Garofalakis, David E Gay, Joseph M Hellerstein, Petros Maniatis, Raghu Ramakrishnan, Timothy Roscoe, and Ion Stoica. 2009. Declarative networking. Commun. ACM, 52, 11 (2009), 87–95.
[45]
Magnus Madsen, Ming-Ho Yee, and Ondrej Lhoták. 2016. From Datalog to flix: a declarative language for fixed points on lattices. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, Chandra Krintz and Emery D. Berger (Eds.). ACM, 194–208. https://doi.org/10.1145/2908080.2908096
[46]
Muhammad Numair Mansur, Maria Christakis, and Valentin Wüstholz. 2021. Metamorphic Testing of Datalog Engines. In Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2021). Association for Computing Machinery, New York, NY, USA. 639–650. isbn:9781450385626 https://doi.org/10.1145/3468264.3468573
[47]
Muhammad Numair Mansur, Valentin Wüstholz, and Maria Christakis. 2023. Dependency-Aware Metamorphic Testing of Datalog Engines. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023, Seattle, WA, USA, July 17-21, 2023, René Just and Gordon Fraser (Eds.). ACM, 236–247. https://doi.org/10.1145/3597926.3598052
[48]
William M McKeeman. 1998. Differential testing for software. Digital Technical Journal, 10, 1 (1998), 100–107.
[49]
Raymond J Mooney. 1996. Inductive logic programming for natural language processing. In International conference on inductive logic programming. 1–22.
[50]
Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. 337–340.
[51]
Patrick Nappa, David Zhao, Pavle Subotić, and Bernhard Scholz. 2019. Fast parallel equivalence relations in a Datalog compiler. In 2019 28th International Conference on Parallel Architectures and Compilation Techniques (PACT). 82–96.
[52]
Raghu Ramakrishnan and Jeffrey D Ullman. 1995. A survey of deductive database systems. The journal of logic programming, 23, 2 (1995), 125–149.
[53]
John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison, and Xuejun Yang. 2012. Test-Case Reduction for C Compiler Bugs. Proceedings of the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation, 47, 6 (2012), jun, 335–346. issn:0362-1340 https://doi.org/10.1145/2345156.2254104
[54]
Manuel Rigger and Zhendong Su. 2020. Detecting Optimization Bugs in Database Engines via Non-Optimizing Reference Engine Construction. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2020). Association for Computing Machinery, New York, NY, USA. 1140–1152. isbn:9781450370431 https://doi.org/10.1145/3368089.3409710
[55]
Manuel Rigger and Zhendong Su. 2020. Finding bugs in database systems via query partitioning. Proceedings of the ACM on Programming Languages, 4, OOPSLA (2020), 1–30.
[56]
Manuel Rigger and Zhendong Su. 2020. Testing database engines via pivoted query synthesis. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). 667–682.
[57]
Kenneth A. Ross. 1990. Modular Stratification and Magic Sets for DATALOG Programs with Negation. In Proceedings of the Ninth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS ’90). Association for Computing Machinery, New York, NY, USA. 161–171. isbn:0897913523 https://doi.org/10.1145/298514.298558
[58]
Leonid Ryzhyk and Mihai Budiu. 2019. Differential Datalog. Datalog, 2 (2019), 4–5.
[59]
Konstantinos Sagonas, Terrance Swift, and David S. Warren. 1994. XSB as an Efficient Deductive Database Engine. In Proceedings of the 1994 ACM SIGMOD International Conference on Management of Data (SIGMOD ’94). Association for Computing Machinery, New York, NY, USA. 442–453. isbn:0897916395 https://doi.org/10.1145/191839.191927
[60]
Bernhard Scholz. 2022. Commercial-Grade Static Analyzers in Datalog. SAS 2022.
[61]
Bernhard Scholz, Herbert Jordan, Pavle Subotić, and Till Westmann. 2016. On Fast Large-Scale Program Analysis in Datalog. In Proceedings of the 25th International Conference on Compiler Construction (CC 2016). Association for Computing Machinery, New York, NY, USA. 196–206. isbn:9781450342414 https://doi.org/10.1145/2892208.2892226
[62]
Sergio Segura, Gordon Fraser, Ana B Sanchez, and Antonio Ruiz-Cortés. 2016. A survey on metamorphic testing. IEEE Transactions on software engineering, 42, 9 (2016), 805–824.
[63]
Andreas Seltenreich. 2023. SQLsmith. https://github.com/anse1/sqlsmith Accessed: 2023-01-25
[64]
Damien Sereni, Pavel Avgustinov, and Oege de Moor. 2008. Adding Magic to an Optimising Datalog Compiler. In Proceedings of the 2008 ACM SIGMOD International Conference on Management of Data (SIGMOD ’08). Association for Computing Machinery, New York, NY, USA. 553–566. isbn:9781605581026 https://doi.org/10.1145/1376616.1376673
[65]
Alexander Shkapsky, Mohan Yang, Matteo Interlandi, Hsuan Chiu, Tyson Condie, and Carlo Zaniolo. 2016. Big data analytics with datalog queries on spark. In Proceedings of the 2016 International Conference on Management of Data. 1135–1149.
[66]
Donald R Slutz. 1998. Massive stochastic testing of SQL. In VLDB. 98, 618–622.
[67]
Pavle Subotić, Herbert Jordan, Lijun Chang, Alan Fekete, and Bernhard Scholz. 2018. Automatic index selection for large-scale datalog computation. Proceedings of the VLDB Endowment, 12, 2 (2018), 141–153.
[68]
Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Buenzli, and Martin Vechev. 2018. Securify: Practical security analysis of smart contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. 67–82.
[69]
Jeffrey D Ullman. 1989. Bottom-up beats top-down for datalog. In Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems. 140–149.
[70]
Allen Van Gelder. 1989. The alternating fixpoint of logic programs with negation. In Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems. 1–10.
[71]
John Whaley and Monica S Lam. 2004. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In Proceedings of the ACM SIGPLAN 2004 conference on Programming Language Design and Implementation. 131–144.
[72]
Chi Zhang, Linzhang Wang, and Manuel Rigger. 2024. Artifact for "Finding Cross-Rule Optimization Bugs in Datalog Engines". https://doi.org/10.5281/zenodo.10609061
[73]
David Zhao, Pavle Subotić, and Bernhard Scholz. 2020. Debugging Large-Scale Datalog: A Scalable Provenance Evaluation Strategy. ACM Trans. Program. Lang. Syst., 42, 2 (2020), Article 7, apr, 35 pages. issn:0164-0925 https://doi.org/10.1145/3379446
[74]
Rui Zhong, Yongheng Chen, Hong Hu, Hangfan Zhang, Wenke Lee, and Dinghao Wu. 2020. Squirrel: Testing database management systems with language validity and coverage feedback. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security. 955–970.
Index Terms
- Finding Cross-Rule Optimization Bugs in Datalog Engines
Recommendations
Understanding and Finding Java Decompiler Bugs
Java decompilers are programs that perform the reverse process of Java compilers, i.e., they translate Java bytecode to Java source code. They are essential for reverse engineering purposes and have become more sophisticated and reliable over the years. ...
Finding Atomicity-Violation Bugs through Unserializable Interleaving Testing
Multicore hardware is making concurrent programs pervasive. Unfortunately, concurrent programs are prone to bugs. Among different types of concurrency bugs, atomicity violations are common and important. How to test the interleaving space and expose ...
Detecting optimization bugs in database engines via non-optimizing reference engine construction
ESEC/FSE 2020: Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software EngineeringDatabase Management Systems (DBMS) are used ubiquitously. To efficiently access data, they apply sophisticated optimizations. Incorrect optimizations can result in logic bugs, which cause a query to compute an incorrect result set. We propose Non-...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
April 2024
1492 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 29 April 2024
Published in PACMPL Volume 8, Issue OOPSLA1
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- National Natural Science Foundation of China
- Fundamental Research Funds for the Central Universities
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 230Total Downloads
- Downloads (Last 12 months)230
- Downloads (Last 6 weeks)69
Reflects downloads up to 22 Nov 2024
Other Metrics
Citations
Cited By
View allView Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in