Making Formulog Fast: An Argument for Unconventional Datalog Evaluation
summary
Compiles Formulog to Soufflé and replaces semi-naive batching with eager evaluation, a concurrent work stealing DFS that specializes rules on novel facts and reuses semi-naive inner machinery. Conventional optimizations give ~2.2× speedups, but implementing eager evaluation in the Formulog interpreter and Soufflé code generator yields mean 5.2× and 7.6× speedups respectively over optimized Soufflé on SMT‑heavy benchmarks, beats hand‑tuned F#, Java, and C++ on 20/23 cases, and trades weaker performance on SMT‑light workloads.
AI-written summary · about
chapters (11)
- 0:00Formulog introduction
- 2:52Contributions and results
- 3:35Formulog as analysis platform
- 4:17Formulog to Soufflé compiler
- 5:23Semi-naive limits for SMT
- 7:52Eager evaluation for Datalog
- 9:18Eager evaluation in practice
- 12:30Implementation and performance
- 13:15Impact on benchmarks
- 14:22Key takeaways and future
- 15:27Q&A
related talks
17mBring Your Own Data Structures to Datalog
15mThe Choice Construct in the Soufflé Language
17mInteractive Debugging of Datalog Programs
17mBetter Together: Unifying Datalog and Equality Saturation
26mDebugging Large-Scale Datalog: A Scalable Provenance Evaluation Strategy
13mAccelerating Program Analyses in Datalog by Merging Library Facts
15mUniversal Scalability in Declarative Program Analysis (with Choice-Based Combination(…)
17mFixpoints for the Masses: Programming with First-Class Datalog Constraints