KIT | KIT-Bibliothek | Impressum | Datenschutz

Proving equivalence between imperative and MapReduce implementations using program transformations

Beckert, B. ORCID iD icon 1; Bingmann, T. 1; Kiefer, M. 1; Sanders, P. ORCID iD icon 1; Ulbrich, M. ORCID iD icon 1; Weigl, A. ORCID iD icon 1
1 Institut für Theoretische Informatik (ITI), Karlsruher Institut für Technologie (KIT)

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.


Preprint §
DOI: 10.5445/IR/1000083954
Veröffentlicht am 01.04.2019
Originalveröffentlichung
DOI: 10.4204/EPTCS.268.7
Scopus
Zitationen: 1
Dimensions
Zitationen: 1
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2018
Sprache Englisch
Identifikator ISSN: 2075-2180
urn:nbn:de:swb:90-839543
KITopen-ID: 1000083954
HGF-Programm 46.12.02 (POF III, LK 01) Data Activities
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 Dimensions
Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page