Detail publikačního výsledku

An Executable Sequential Specification for Spark Aggregation

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

Originální název

An Executable Sequential Specification for Spark Aggregation

Anglický název

An Executable Sequential Specification for Spark Aggregation

Druh

Stať ve sborníku v databázi WoS či Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova


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

Klíčová slova v angličtině


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

Autoři

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

Rok RIV

2018

Vydáno

27.05.2017

Nakladatel

Springer Verlag

Místo

Heidelberg

Kniha

Proceedings of NETYS'17

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Číslo

10299

Stát

Spolková republika Německo

Strany od

421

Strany do

438

Strany počet

15

URL

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/"
}

Dokumenty