Pith. sign in

REVIEW

An Executable Sequential Specification for Spark Aggregation

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1702.02439 v1 pith:KIYUJD3U submitted 2017-02-08 cs.DC cs.LO

Yu-Fang Chen , Chih-Duo Hong , Ondřej Lengál , Shin-Cheng Mu , Nishant Sinha , Bow-Yaw Wang This is my paper · ORCID
classification cs.DCcs.LO
keywords sparkaggregationspecificationdatadeterministicexecutableexecutionoutcomes
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the 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.

Discussion (0). Continue with ORCID to comment.

Pith tools