Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations

Autor:	Beckert, Bernhard, Bingmann, Timo, Kiefer, Moritz, Sanders, Peter, Ulbrich, Mattias, Weigl, Alexander
Rok vydání:	2018
Předmět:	Computer Science - Programming Languages Computer Science - Logic in Computer Science
Zdroj:	EPTCS 268, 2018, pp. 185-199
Druh dokumentu:	Working Paper
DOI:	10.4204/EPTCS.268.7
Popis:	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. Comment: In Proceedings MARS/VPT 2018, arXiv:1803.08668
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1803.10328 Zobrazit plný text záznamu View this record from Arxiv