A computational model for MapReduce job flow

Abstract

Massive quantities of data are today processed using parallel computing frameworks that parallelize computations on large distributed clusters consisting of many machines. Such frameworks are adopted in big data analytic tasks as recommender systems, social network analysis, legal investigation that involve iterative computations over large datasets. One of the most used framework is MapReduce, scalable and suitable for data-intensive processing with a parallel computation model characterized by sequential and parallel processing interleaving. Its open-source implementation - Hadoop - is adopted by many cloud infrastructures as Google, Yahoo, Amazon, Facebook. In this paper we propose a formal approach to model the MapReduce framework using model checking and temporal logics to verify properties of reliability and load balancingof the MapReduce job flow.

-

Introduction and motivation

In this paper we propose a formal approach to model the MapReduce framework using model checking and tempora l logics to verify some relevant properties as reliability, load balancing, lack of deadlock of the MapReduce job flow. To the best of our knowledge only two works have combined MapReduce and model checking with a di↵erent aim from ours: in [ 2 ] MapReduce is adopted to compute distributed CTL algorithms and in [ 6 ] MapReduce is modeled using CSP formalism. The remaining of the paper is organized as follows. In Section 2 we recall basics of model checking and temporal logics, the formalism used to define and simulate our model. Section 3 provides a brief overview of the main features of MapReduce. Section 4 proposes our formal model of job flow in Mapreduce computation while Section 5 proposes an analytical model in the Uppaal model checker language with properties to be checked. Conclusion and future works are drawn in the last section. 2

Model Checking and Temporal Logics The logical language we use for the model checking task is the Computation Tree Logic (CTL), a propositional, branching, temporal logic [ 5 ].

The syntax of the formulae can be defined, using Backus-Naur form, as follows (where p is an atomic proposition): , ::= p | ^ | _ | ¬ | ! | $ | EF | EX | EG | E(U ) | AG | AF | AX | A(U ). An atomic proposition is the formula true or a ground atom CTL formulae can also contain path quantifiers followed by temporal operators. The path quantifier E specifies some path from the current state, while the path quantifier A specifies all paths from the current state. The temporal operators are X, the neXt-state operator; U , the Until operator; G, the Globally operator; and F the Future operator. The symbols X, U , G, F cannot occur without being preceded by the quantifiers E and A.

The semantics of the language is defined through a Kripke structure as the triple (S, ! , L) where S is a collection of states, ! is a binary relation on S ⇥ S, stating that the system can move from state to state. Associated with each state s, the interpretation function L provides the set of atomic propositions L(s) that are true at that particular state [ 3 ]. The semantics of boolean connectives is as usual. The semantics for temporal connectives is as follows: X specifies that holds in the next state along the path. U specifies that holds on every state along the path until is true. G specifies that holds on every state along the path. F specifies that there is at least one state along the path in which is true. The semantics of formulae is defined as follows: EX : holds in some next state; EF : a path exists such that holds in some Future state ; EG : a path exists such that holds Globally along the path; E(U ): a path exists such that Until holds on it; AX : holds in every next state; AF : for All paths there will be some Future state where holds; AG : for All paths the property holds Globally; A(U ): All paths satisfy Until . The model checking problem is the following: Given a model M , an initial state s and a CTL formula , check whether M, s |= . M |= ehen the formula must be checked for every state of M . 336 3

MapReduce Overview and proposed model MapReduce is a software framework for solving large-scale computing problems over large data-sets and data-intensive computing. It has grown to be the programming model for current distributed systems, i.e. cloud computing. It also forms the basis of the data-center software stack [ 4 ].

MapReduce framework was developed at Google Research as a parallel programming model with an associated implementation. The framework is highly scalable and location independent. It is used for the generation of data for Google’s production web search service, for sorting, for data-intensive applications, for optimizing parallel jobs performance in data-intensive clusters. The most relevant feature of MapReduce processing is that computation runs on a large cluster of commodity machines [ 1 ]; while the main feature with respect to other existing parallel computational models is the sequential and parallel computation interleaving.

The MapReduce model is made up of the Map and Reduce functions, which are borrowed from functional languages such as Lisp [ 1 ]. Users’ computations are written as Map and Reduce functions. The Map function processes a key/value pair to generate a set of intermediate key/value pairs. The Reduce function merges all intermediate values associated with the same intermediate key. Intermediate functions of Shu✏e and Sorting are useful to split and sort the data chunks to be given in input to the Reduce function. We now define the computational model for MapReduce framework. We model jobs and tasks in MapReduce using the flow description as shown in Figure 1.

Definition 1 (MapReduce Graph (MRG)). A MapReduce Graph (MRG) is a Direct Acyclic Graph G = {N, E}, where nodes N in the computation graph are the tasks of computation – N = M [ S [ SR [ R (M = map, S = shuf f le, SR = sort, R = reduce) – and edges e 2 E are such that: 1. E ✓ (M ⇥ S) [ (S ⇥ SR) [ (SR ⇥ R), i.e. “edges connect map with shu✏e, shu✏e with sort and sort with reduce tasks”; 2. e 2 M ⇥ S breaks input into tokens; e 2 S ⇥ SR sorts input tokens by type; e 2 SR ⇥ R gives sort tokens to reducer. 3. Reduce sends input data for cluster allocation to the file system Definition 2 (MapReduce Task). A MapReduce task t is a token of computation such that t 2 (M [ S [ SR [ R).

Definition 3 (MapReduce Job). A MapReduce Job is the sequence t1 ! t2 . . . ! tn of MapReduce tasks where

tj1 = (Mi, .., Mi+p) ! tj2 = Sk ! tj3 = SRk ! tj4 = Rk with Mi 2

M, i = 1 . . . n, Sj 2 S, SRj 2 SR, Rj 2 R, j = 1 . . . m.

Uppaal simulation model In this Section we briefly describe the implemented model in the Uppaal2 model checker’s formalism. Uppaal model is described in XML data format of model checker description language and shown in the graphical interface of the tool as a graph model.

The analytical model is made up of three templates: job, mapper and Google File System (GFS). Figure 2 shows only the Uppaal graph model of the job described using the statechart notation. Main states of the job template are Map, Shu✏e , Sort and Reduce as defined in the theoretical model in Section 3. Other states manage the flow of the job: Starvation models the state in which the task waits for unavailable resource, Middle state manages exceptions, receiving input and receiving keyval manage data during job flow. Finally medium level checks input data for the Shu✏e state. Mapper template is made up of states: Prevision that checks the behavior of the mappers working for the given job. The Prevision state is followed by Error and out of order state in case of wrong behavior of the mapper, or Work state in case of correct behavior of the mapper. Finally the GFS template only manages the job execution.

To test the validity of the approach we simulated the model by instantiating a given number of jobs with relative mappers. We checked the two main properties of MapReduce framework, i.e. load balancing and fault tolerance.

Load Balancing. This property checks that the load of the Job J will be distributed to all tasks of the Mapper Mi with given map and reduce tasks. Hence when the job enters the state Map all the previson state of the mapper are veryfied, this means that the load is balanced between all the mappers.

EG(J.M ap) ^ AG(Mi.P revision)

Fault Tolerance. If the Mi map is out of service the job mapper schedules an alternative task to perform the missed function that belongs to remaining 2 http://www.uppaal.org/ Mi. In the simulation model, mappercount is the counter of the total number of mappers and mappersched is the variable that counts the scheduled mappers. The assigned value, m is the number of mappers.

EF (M.Out of order) ^ AG(mapper count = m ^ mapper sched = m) From the simulation results we checked that the model ensures load balancing and fault tolerance. 5

Conclusion and future work We proposed a formal model of MapReduce framework for data-intensive and computing-intensive environment. The model introduces the definition of MapReduce graph and MapReduce job and task. At this stage of the work we implemented and simulated the model with Uppaal model checker to verify basics properties of its computation as fault tolerance, load balancing and lack of deadlock. We are currently modeling other relevant features as scalability, data locality and extending the model with advanced job management activities such as job folding and job chaining.

We acknowledge support of project “A Knowledge based Holistic Integrated Research Approach” (KHIRA - PO3N3902 00563 3446857).

References

1. Je ↵rey Dean and Sanjay Ghemawat . Mapreduce: Simplified data processing on large clusters, OSDI04: Sixth symposium on operating system design and implementation , san francisco, ca, december, 2004 . S. Dill, R. Kumar , K. McCurley , S. Rajagopalan , D. Sivakumar, ad A. Tomkins , Self-similarity in the Web , Proc VLDB , 2001 .

2. Feng Guo , Guang Wei, Mengmeng Deng, and Wanlin Shi . Ctl model checking algorithm using mapreduce . In Emerging Technologies for Information Systems, Computing, and Management , pages 341 - 348 . Springer, 2013 .

3. M.R.A. Huth and M.D. Ryan . Logic in Computer Science. Cambridge University Press, 1999 .

4. Krishna Kant . Data center evolution: A tutorial on state of the art, issues, and challenges . Computer Networks , 53 ( 17 ): 2939 - 2965 , 2009 .

5. Edmund M. Clarke , Orna Grumberg, and Doron A. Peled. Model Checking . Cambridge, Massachusetts, USA: MIT press., 1999 .

6. Fan Yang , Wen Su, Huibiao Zhu, and Qin Li . Formalizing mapreduce with csp . In Engineering of Computer Based Systems (ECBS) , 2010 17th IEEE International Conference and Workshops on, pages 358 - 367 . IEEE, 2010 .