Detail výsledku

An Executable Sequential Specification for Spark Aggregation

LENGÁL, O.; HONG, C.; CHEN, Y.; MU, S.; SINHA, N.; WANG, B. An Executable Sequential Specification for Spark Aggregation. In Proceedings of NETYS'17. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017. no. 10299, p. 421-438. ISSN: 0302-9743.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Lengál Ondřej, doc. Ing., Ph.D., UITS (FIT)
Hong Chih-Duo
Chen Yu-Fang
Mu Shin-Cheng
Sinha Nishant
Wang Bow-Yaw, FIT (FIT)
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

Rok
2017
Strany
421–438
Časopis
Lecture Notes in Computer Science, č. 10299, ISSN 0302-9743
Sborník
Proceedings of NETYS'17
Konference
The 5th international conference on networked systems
Vydavatel
Springer Verlag
Místo
Heidelberg
DOI
10.1007/978-3-319-59647-1_31
EID Scopus
2-s2.0-85019719038
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/"
}
Soubory
Projekty
Bezpečné a spolehlivé počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-17-4014, zahájení: 2017-03-01, ukončení: 2020-02-29, ukončen
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, zahájení: 2016-01-01, ukončení: 2020-12-31, ukončen
ROBUST - Verifikace a hledání chyb v pokročilém softwaru, GAČR, Standardní projekty, GA17-12465S, zahájení: 2017-01-01, ukončení: 2019-12-31, ukončen
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru