# An Executable Sequential Specification for Spark Aggregation

## TL;DR

This paper introduces PureSpark, a formal Haskell specification for Spark aggregation, enabling analysis of deterministic outcomes and correctness in parallel data aggregation programs.

## Contribution

It provides the first executable formal specification for Spark aggregation, allowing precise analysis of determinism and correctness in Spark programs.

## Key findings

- Identifies conditions for deterministic outcomes in Spark aggregation
- Analyzes correctness of Spark programs using the specification
- Supports case studies on Spark aggregation behaviors

## 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.