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 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 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 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 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倍，最高可达两个数量级。