Publication detail

An Executable Sequential Specification for Spark Aggregation

LENGÁL, O. HONG, C. CHEN, Y. MU, S. SINHA, N. WANG, B.

Original Title

An Executable Sequential Specification for Spark Aggregation

Type

conference paper

Language

English

Original Abstract

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.

Keywords

Data Parallel Computation, Functional Specification, Requirements, Verification, Spark

Authors

LENGÁL, O.; HONG, C.; CHEN, Y.; MU, S.; SINHA, N.; WANG, B.

Released

27. 5. 2017

Publisher

Springer Verlag

Location

Heidelberg

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Number

10299

State

Federal Republic of Germany

Pages from

421

Pages to

438

Pages count

15

URL

https://www.fit.vut.cz/research/publication/11330/

BibTex

@inproceedings{BUT146257,
  author="Ondřej {Lengál} and Chih-Duo {Hong} and Yu-Fang {Chen} and Shin-Cheng {Mu} and Nishant {Sinha} and Bow-Yaw {Wang}",
  title="An Executable Sequential Specification for Spark Aggregation",
  booktitle="Proceedings of NETYS'17",
  year="2017",
  journal="Lecture Notes in Computer Science",
  number="10299",
  pages="421--438",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-319-59647-1\{_}31",
  issn="0302-9743",
  url="https://www.fit.vut.cz/research/publication/11330/"
}

Documents

netys17.pdf