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