Automatic Rollback Suggestions for Incremental Datalog Evaluation
summary
A debugging method computes incremental provenance to identify which inserted or deleted Datalog input tuples enable each error derivation, encodes the minimal rollback as an integer linear program over proof trees, and returns a smallest set of inputs whose removal disables all derivations. It is implemented against an incremental Soufflé prototype with Python ILP glue, evaluated on Doop DaCapo Java benchmarks, and yields up to a 26.9× speedup versus delta debugging while failing only on one large bloat case with huge proof trees.
AI-written summary · about
chapters (12)
- 0:00Intro
- 1:11Datalog for Program Analysis
- 2:01Typical Workflow
- 3:22Points-to Analysis in Datalog
- 5:08Bottom-Up Datalog Evaluation
- 5:59Incremental Evaluation
- 12:12Computing Incremental Provenance
- 13:33Incremental Provenance and Rollback Suggestions
- 14:37Minimum Proof Tree Cover Problem
- 17:28Summary of Other Datalog Features
- 19:21Experimental Setup
- 21:54Conclusion
related talks
24mU-Turn: Enhancing Incorrectness Analysis by Reversing Direction
28mGradual Verification: Assuring Software Incrementally
19mProof Automation for Linearizability in Separation Logic
15mTP-DejaVu: Combining Operational and Declarative Runtime Verification
14mSynthesizing Implication Lemmas for Interactive Theorem Proving
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
13mRevealing Sources of (Memory) Errors via Backward Analysis
20mOn Extending Incorrectness Logic with Backwards Reasoning