Search papers, labs, and topics across Lattice.
This paper formalizes predicate pushdown optimization for data pipelines containing user-defined functions (UDFs) by framing it as a bisimulation between programs processing different data subsets. They develop a sound and complete verification framework and a synthesis algorithm to automatically construct optimal pushdown decompositions, identifying strongest pre-filters and weakest post-filters. Implemented in a tool called Pusharoo, the approach achieves significant speedups (2.4x on average, up to 2 orders of magnitude) on real-world pandas and Spark pipelines compared to prior work.
Pusharoo automatically synthesizes optimal predicate pushdown transformations for data pipelines with user-defined functions, achieving up to 2 orders of magnitude speedup.
Predicate pushdown is a long-standing performance optimization that filters data as early as possible in a computational workflow. In modern data pipelines, this transformation is especially important because much of the computation occurs inside \emph{user-defined functions (UDFs)} written in general-purpose languages such as Python and Scala. These UDFs capture rich domain logic and complex aggregations and are among the most expensive operations in a pipeline. Moving filters ahead of such UDFs can yield substantial performance gains, but doing so requires \emph{semantic} reasoning. This paper introduces a general semantic foundation for predicate pushdown over stateful fold-based computations. We view pushdown as a correspondence between two programs that process different subsets of input data, with correctness witnessed by a \emph{bisimulation invariant} relating their internal states. Building on this foundation, we develop a sound and relatively complete framework for verification, alongside a synthesis algorithm that automatically constructs \emph{optimal pushdown decompositions} by finding the strongest admissible pre-filters and weakest residual post-filters. We implement this approach in a tool called Pusharoo and evaluate it on 150 real-world pandas and Spark data-processing pipelines. Our evaluation shows that Pusharoo is significantly more expressive than prior work, producing optimal pushdown transformations with a median synthesis time of 1.6 seconds per benchmark. Furthermore, our experiments demonstrate that the discovered pushdown optimizations speed up end-to-end execution by an average of 2.4$\times$ and up to two orders of magnitude.
