kirancodes.me
To Proof Maintenance & Beyond!

The Choice Construct in the Soufflé Language

Xiaowen Hu, Joshua Karp, David Zhao, Abdul Zreika, Xi Wu, Bernhard Scholz

Abstract

Datalog has become a popular implementation language for solving large-scale, real-world problems, including bug finders, network analysis tools, and disassemblers. These applications express complex behaviour with hundreds of relations and rules that often require a non-deterministic choice for tuples in relations to express worklist algorithms. This work is an experience report that describes the implementation of a choice construct in the Datalog engine Souffle. With the choice construct, we can express worklist algorithms such as spanning trees in a few lines of code. We highlight the differences between rule-based choice as described in prior work, and relation-based choice introduced by this work. We show that a choice construct enables certain worklist algorithms to be computed up to 10kx faster than having no choice construct.

Related papers