KIT | KIT-Bibliothek | Impressum | Datenschutz

Proving equivalence between imperative and MapReduce implementations using program transformations

Beckert, B.; Bingmann, T.; Kiefer, M.; Sanders, P.; Ulbrich, M.; Weigl, A.

Abstract (englisch):
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.

Open Access Logo

Preprint §
DOI: 10.5445/IR/1000083954
Veröffentlicht am 01.04.2019
DOI: 10.4204/EPTCS.268.7
Zitationen: 1
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Jahr 2018
Sprache Englisch
Identifikator ISSN: 2075-2180
KITopen-ID: 1000083954
Erschienen in 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018; Thessaloniki; Greece; 20 April 2018. Ed.: R. van Glabbeek
Verlag Open Publishing Association
Seiten 185-199
Serie Electronic Proceedings in Theoretical Computer Science, EPTCS ; 268
Projektinformation SPP 1593 (DFG, DFG KOORD, BE 2334/7-2)
SPP 1593 (DFG, DFG KOORD, UL 433/1-2)
Nachgewiesen in Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page