Making Formulog Fast: An Argument for Unconventional Datalog Evaluation (Extended Version)

TL;DR

This paper introduces eager evaluation, a novel concurrent Datalog evaluation method, significantly improving the performance of the Formulog language for SMT-based static analysis tasks by surpassing traditional semi-naive evaluation techniques.

Contribution

It develops and demonstrates eager evaluation, an alternative to semi-naive evaluation, leading to substantial speedups in Formulog's performance for static analysis applications.

Findings

Eager evaluation achieves up to 7.6x speedup over traditional methods.

Formulog with eager evaluation outperforms hand-tuned analyses in most benchmarks.

Eager evaluation improves SMT workload distribution and solving times.

Abstract

By combining Datalog, SMT solving, and functional programming, the language Formulog provides an appealing mix of features for implementing SMT-based static analyses (e.g., refinement type checking, symbolic execution) in a natural, declarative way. At the same time, the performance of its custom Datalog solver can be an impediment to using Formulog beyond prototyping -- a common problem for Datalog variants that aspire to solve large problem instances. In this work we speed up Formulog evaluation, with surprising results: while 2.2x speedups are obtained by using the conventional techniques for high-performance Datalog (e.g., compilation, specialized data structures), the big wins come by abandoning the central assumption in modern performant Datalog engines, semi-naive Datalog evaluation. In its place, we develop eager evaluation, a concurrent Datalog evaluation algorithm that explores the logical inference space via a depth-first traversal order. In practice, eager evaluation leads to an advantageous distribution of Formulog's SMT workload to external SMT solvers and improved SMT solving times: our eager evaluation extensions to the Formulog interpreter and Souffl\'e's code generator achieve mean 5.2x and 7.6x speedups, respectively, over the optimized code generated by off-the-shelf Souffl\'e on SMT-heavy Formulog benchmarks. Using compilation and eager evaluation, Formulog implementations of refinement type checking, bottom-up pointer analysis, and symbolic execution achieve speedups on 20 out of 23 benchmarks over previously published, hand-tuned analyses written in F#, Java, and C++, providing strong evidence that Formulog can be the basis of a realistic platform for SMT-based static analysis. Moreover, our experience adds nuance to the conventional wisdom that semi-naive evaluation is the one-size-fits-all best Datalog evaluation algorithm for static analysis workloads.