Higher-Order, Data-Parallel Structured Deduction

TL;DR

This paper introduces a new data-parallel approach to structured deduction in Datalog, enabling scalable, high-performance formal systems through a semantic extension and implementation of the $DL_s$ language.

Contribution

It presents a novel semantic extension of Datalog with first-class facts and higher-order relations, along with an implementation that achieves scalable parallelism for formal systems.

Findings

Achieved up to 1000-thread scalability on cloud and supercomputing platforms.

Demonstrated orders-of-magnitude performance improvements over existing systems.

Successfully built control-flow analyses and type systems using the proposed approach.

Abstract

State-of-the-art Datalog engines include expressive features such as ADTs (structured heap values), stratified aggregation and negation, various primitive operations, and the opportunity for further extension using FFIs. Current parallelization approaches for state-of-art Datalogs target shared-memory locking data-structures using conventional multi-threading, or use the map-reduce model for distributed computing. Furthermore, current state-of-art approaches cannot scale to formal systems which pervasively manipulate structured data due to their lack of indexing for structured data stored in the heap. In this paper, we describe a new approach to data-parallel structured deduction that involves a key semantic extension of Datalog to permit first-class facts and higher-order relations via defunctionalization, an implementation approach that enables parallelism uniformly both across sets of disjoint facts and over individual facts with nested structure. We detail a core language, $DL_s$, whose key invariant (subfact closure) ensures that each subfact is materialized as a top-class fact. We extend $DL_s$ to Slog, a fully-featured language whose forms facilitate leveraging subfact closure to rapidly implement expressive, high-performance formal systems. We demonstrate Slog by building a family of control-flow analyses from abstract machines, systematically, along with several implementations of classical type systems (such as STLC and LF). We performed experiments on EC2, Azure, and ALCF's Theta at up to 1000 threads, showing orders-of-magnitude scalability improvements versus competing state-of-art systems.