Spark聚合的可执行顺序规范
分布式、并行与集群计算
2017-02-09 v1 计算机科学中的逻辑
摘要
Spark是一个用于可扩展数据并行计算的有前途的新平台。它提供若干高层应用程序编程接口(APIs)以执行并行数据聚合。由于Spark中并行聚合的执行本质上是非确定性的,对Spark程序的一个自然要求是在同一数据集上任何执行给出相同结果。我们提出PureSpark,一个针对Spark聚合组合子的可执行形式化Haskell规范。我们的规范使我们能够推导出Spark聚合确定性结果的精确条件。我们报告了分析Spark程序确定性结果和正确性的案例研究。
引用
@article{arxiv.1702.02439,
title = {An Executable Sequential Specification for Spark Aggregation},
author = {Yu-Fang Chen and Chih-Duo Hong and Ondřej Lengál and Shin-Cheng Mu and Nishant Sinha and Bow-Yaw Wang},
journal= {arXiv preprint arXiv:1702.02439},
year = {2017}
}
备注
an extended version of a paper accepted at NETYS'17