Extending Parallel Datalog with Lattice
Open Access
- Author:
- Gong, Qing
- Graduate Program:
- Computer Science and Engineering
- Degree:
- Master of Science
- Document Type:
- Master Thesis
- Date of Defense:
- March 26, 2020
- Committee Members:
- Gang Tan, Thesis Advisor/Co-Advisor
Danfeng Zhang, Committee Member
Chitaranjan Das, Program Head/Chair - Keywords:
- Datalog
Lattice
Scalability
Soufflé - Abstract:
- There have been more and more studies on Datalog, a logic programming language which is originally a query language for deductive databases. The application of Datalog in static program analysis has been noticed and explored in the last two decades. Datalog provides a general way to implement static analysis using Semi-Naïve Evaluation. We can use facts and rules to represent a specific static analysis and send them to a Datalog evaluator to solve it, without manually writing the static analyzer and corresponding debugging work. However, some static analyses with large or infinite lattices cannot be efficiently solved in the traditional powerset scheme. To overcome this drawback, we need the natural lattice scheme in such static analysis to extend the range of application of Datalog, more specifically, Soufflé. This thesis discusses some backgrounds including the history and evaluation of Datalog, static analysis and lattice, the architecture of two Datalog variants: Soufflé and FLIX. We describe the framework of lattice including conditional operator, unary and binary case functions, lattice declaration, lattice association, and the modifications in the Semi-Naïve Evaluation algorithms in RAM program. The details of extending Soufflé with the designed lattice framework are described. The implementation has been put on Github: https://github.com/QXG2/souffle. We evaluate the functionality and scalability of the lattice scheme on extending Soufflé, and the results show that extended Soufflé is very efficient on Sign Analysis and Constant Propagation Analysis.