Date of Award

8-4-2023

Degree Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Department

Electrical Engineering and Computer Science

Advisor(s)

Kristopher Micinski

Keywords

Data Structures;Datalog;Logic Programming;Program Analysis;Programming Languages;Static Analysis

Subject Categories

Computer Sciences | Physical Sciences and Mathematics

Abstract

Using logic programming languages has seen a resurgence in the domain of static program analysis. Such languages like Datalog, while useful, suffer from limitations in expressivity and real-world applicability. This dissertation explores tackling these limitations from different angles. \emph{Slog} extends Datalog with nested facts. By allowing facts to reference other facts, Slog becomes a Turing-complete language, allowing it to express a wider range of analyses. Moreover, Slog has been designed with an eye towards automatic non-shared-memory parallelization. \emph{Ascent} embeds a logic programming language like Datalog in Rust, a high-performance, type-safe programming language. By embedding Ascent in Rust, a wealth of Rust-provided abstractions like functions and data types become available to Ascent, enhancing the expressivity of logic programs, and allowing Ascent programs to seamlessly interoperate with arbitrary logic written in Rust. Ascent also utilizes Rust's trait system to enable defining fixed-point computations on non-powerset lattices. \emph{BYODS} further extends Ascent by providing a mechanism for users to bring their own data structures to back relations in Ascent programs. This alleviates a significant pain point of logic programming: lack of control over data structures means many analyses that are expressible in Datalog suffer from severe algorithmic inefficiencies, rendering their implementation in Datalog of little practical use. Explicit representation of transitive and equivalence relations as sets-of-facts in Datalog are examples of such algorithmic inefficiencies. For Slog, I formalize the core of the language, this includes presenting machine checked proofs demonstrating this core language has properties desired of a Datalog-derived language. I also present benchmarks showing the superior performance of the Slog backend compared with Souffl\'e on a program analysis task that requires manipulating structured data, a task to which Slog is well-suited. To evaluate Ascent, I reimplement the Rust borrow checker, a static analysis required by the Rust compiler, demonstrating the usefulness of Ascent. I also use benchmarks to compare the performance of Ascent vs Flix and Souffl\'e. To evaluate \byods{}, I implement a multitude of data structure providers for equivalence and transitive relations, index-sharing, and a reimplementation of lattices as a data structure provider. I use these data structure providers to implement an improved Rust borrow checker, PageRank, along with smaller, more targeted benchmark programs. My evaluation shows speedups, including improvements in time and space complexity when using these data structure providers.

Access

Open Access

Download

Share

COinS