Spark聚合的可执行顺序规范
An Executable Sequential Specification for Spark Aggregation
摘要：
Spark是一种新型的可扩展数据并行计算平台。它提供了几个高级应用程序编程接口（API）来执行并行数据聚合。由于Spark中并行聚合的执行本质上是不确定的，因此Spark程序的一个自然要求是对同一数据集的任何执行都给出相同的结果。我们提出了PureSpark，一个可执行的正式Haskell规范的Spark聚合组合子。我们的规范允许我们从Spark聚合中推导出确定性结果的精确条件。我们报告的案例研究分析确定性的结果和正确性的火花程序。
英文摘要：
Spark is a new promising platform for scalable data-parallel computation. It provides several high-level application programming interfaces (APIs) to perform parallel data aggregation. Since execution of parallel aggregation in Spark is inherently non-deterministic, a natural requirement for Spark programs is to give the same result for any execution on the same data set. We present PureSpark, an executable formal Haskell specification for Spark aggregate combinators. Our specification allows us to deduce the precise condition for deterministic outcomes from Spark aggregation. We report case studies analyzing deterministic outcomes and correctness of Spark programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
