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.

翻译：谓词下推是一项长期存在的性能优化技术，旨在计算工作流中尽可能早地对数据进行过滤。在现代数据处理流程中，由于大量计算发生在用Python和Scala等通用语言编写的**用户自定义函数（UDF）**中，这一变换尤为重要。这些UDF封装了丰富的领域逻辑和复杂聚合操作，是流程中开销最大的环节之一。将过滤器移至此类UDF之前可带来显著性能提升，但这需要**语义**层面的推理。本文为基于状态折叠计算的谓词下推建立了通用语义基础。我们将下推视为处理输入数据不同子集的两个程序之间的对应关系，其正确性通过连接两者内部状态的**互模拟不变量**来保证。基于此基础，我们开发了一个可靠且相对完备的验证框架，并设计了一种合成算法，通过寻找最强可允许前置过滤器和最弱残余后置过滤器，自动构建**最优下推分解**。我们在名为Pusharoo的工具中实现了该方法，并在150个真实世界的pandas和Spark数据处理流程上进行了评估。评估表明，Pusharoo的表达能力显著优于现有工作，每个基准测试的中位合成时间为1.6秒即可生成最优下推变换。此外，实验证明所发现的下推优化使端到端执行速度平均提升2.4倍，最高可达两个数量级。