Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Fri 22 Jan 2021 18:50 - 19:00 at POPL-B - Logic and Decision Procedures

Logic programming languages such as Datalog have become popular as Domain Specific Languages (DSLs) for solving large-scale, real-world problems, in particular, static program analysis and network analysis. The logic specifications that model analysis problems process millions of tuples of data and contain hundreds of highly recursive rules. As a result, they are notoriously difficult to debug. While the database community has proposed several data provenance techniques that address the Declarative Debugging Challenge for Databases, in the cases of analysis problems, these state-of-the-art techniques do not scale.

In this article, we introduce a novel bottom-up Datalog evaluation strategy for debugging: Our provenance evaluation strategy relies on a new provenance lattice that includes proof annotations and a new fixed-point semantics for semi-naïve evaluation. A debugging query mechanism allows arbitrary provenance queries, constructing partial proof trees of tuples with minimal height. We integrate our technique into Soufflé, a Datalog engine that synthesizes C++ code, and achieve high performance by using specialized parallel data structures. Experiments are conducted with DOOP/DaCapo, producing proof annotations for tens of millions of output tuples. We show that our method has a runtime overhead of 1.31× on average while being more flexible than existing state-of-the-art techniques.

Fri 22 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:00
Logic and Decision ProceduresPOPL at POPL-B
18:30
10m
Talk
Cyclic Proofs, System T, and the Power of Contraction
POPL
Denis Kuperberg LIP, ENS de Lyon, Laureline Pinault LIP, ENS de Lyon, Damien Pous CNRS
Link to publication DOI
18:40
10m
Talk
egg: Fast and Extensible Equality SaturationDistinguished Paper
POPL
Max Willsey University of Washington, USA, Chandrakana Nandi University of Washington, USA, Yisu Remy Wang University of Washington, Oliver Flatt University of Utah, Zachary Tatlock University of Washington, Seattle, Pavel Panchekha University of Utah
Link to publication DOI Pre-print
18:50
10m
Talk
Debugging Large-Scale Datalog: A Scalable Provenance Evaluation StrategyTOPLAS
POPL
David Zhao The University of Sydney, Pavle Subotic Microsoft and Mathematical Institute, Serbian Academy of Sciences and Arts (SASA), Bernhard Scholz University of Sydney, Australia
Link to publication DOI