Where academic tradition
meets the exciting future

Formal Derivation of Distributed MapReduce

Inna Pereverzeva, Michael Butler, Asieh Salehi Fathabadi, Linas Laibinis, Elena Troubitsyna, Formal Derivation of Distributed MapReduce. In: Y. Ait Ameur, K.-D. Schewe (Eds.), Proceedings of ABZ 2014, Lecture Notes in Computer Science 8477, 238–254, Springer, 2014.

Abstract:

MapReduce is a powerful distributed data processing model that is currently adopted in a wide range of domains to efficiently handle large volumes of data, i.e., cope with the big data surge. In this paper, we propose an approach to formal derivation of the MapReduce framework. Our approach relies on stepwise refinement in Event-B and, in particular, the event refinement structure approach – a diagrammatic notation facil- itating formal development. Our approach allows us to derive the system architecture in a systematic and well-structured way. The main principle of MapReduce is to parallelise processing of data by first mapping them to multiple processing nodes and then merging the results. To facilitate this, we formally define interdependencies between the map and reduce stages of MapReduce. This formalisation allows us to propose an alternative archi- tectural solution that weakens blocking between the stages and, as a result, achieves a higher degree of parallelisation of MapReduce computations.

BibTeX entry:

@INPROCEEDINGS{inpPeBuFaLaTr14a,
  title = {Formal Derivation of Distributed MapReduce},
  booktitle = {Proceedings of ABZ 2014},
  author = {Pereverzeva, Inna and Butler, Michael and Fathabadi, Asieh Salehi and Laibinis, Linas and Troubitsyna, Elena},
  volume = {8477},
  series = {Lecture Notes in Computer Science},
  editor = {Ait Ameur, Y. and Schewe, K.-D.},
  publisher = {Springer},
  pages = {238–254},
  year = {2014},
  keywords = {formal modelling, Event-B, refinement, event refinement structure, MapReduce},
  ISSN = {1503-111X},
}

Belongs to TUCS Research Unit(s): Embedded Systems Laboratory (ESLAB)

Publication Forum rating of this publication: level 1

Edit publication