Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations

Bernhard Beckert
(Karlsruhe Institute of Technology)
Timo Bingmann
(Karlsruhe Institute of Technology)
Moritz Kiefer
(Karlsruhe Institute of Technology)
Peter Sanders
(Karlsruhe Institute of Technology)
Mattias Ulbrich
(Karlsruhe Institute of Technology)
Alexander Weigl
(Karlsruhe Institute of Technology)

Distributed programs are often formulated in popular functional frameworks like MapReduce, Spark and Thrill, but writing efficient algorithms for such frameworks is usually a non-trivial task. As the costs of running faulty algorithms at scale can be severe, it is highly desirable to verify their correctness.

We propose to employ existing imperative reference implementations as specifications for MapReduce implementations. To this end, we present a novel verification approach in which equivalence between an imperative and a MapReduce implementation is established by a series of program transformations.

In this paper, we present how the equivalence framework can be used to prove equivalence between an imperative implementation of the PageRank algorithm and its MapReduce variant. The eight individual transformation steps are individually presented and explained.

In John P. Gallagher, Rob van Glabbeek and Wendelin Serwe: Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation (MARS/VPT 2018), Thessaloniki, Greece, 20th April 2018, Electronic Proceedings in Theoretical Computer Science 268, pp. 185–199.
Published: 23rd March 2018.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: