TY - GEN
T1 - Using Coq in specification and program extraction of Hadoop MapReduce applications
AU - Ono, Kosuke
AU - Hirai, Yoichi
AU - Tanabe, Yoshinori
AU - Noda, Natsuko
AU - Hagiya, Masami
PY - 2011
Y1 - 2011
N2 - Hadoop MapReduce is a framework for distributed computation on key-value pairs. The goal of this research is to verify actual running code of MapReduce applications. We first constructed an abstract model of MapReduce computation with the proof assistant Coq. In the model, mappers and reducers in MapReduce computation are modeled as functions in Coq, and a specification of a MapReduce application is expressed in terms of invariants among functions involving its mapper and reducer. The model also provides modular proofs of lemmas that do not depend on applications. To achieve the goal, we investigated the feasibility of two approaches. In one approach, we transformed verified mapper and reducer functions into Haskell programs and executed them under Hadoop Streaming. In the other approach, we verified JML annotations on Java programs of the mapper and reducer using Krakatoa, translated them into Coq axioms, and proved Coq specifications from them. In either approach, we were able to verify correctness of MapReduce applications that actually run on the Hadoop MapReduce framework.
AB - Hadoop MapReduce is a framework for distributed computation on key-value pairs. The goal of this research is to verify actual running code of MapReduce applications. We first constructed an abstract model of MapReduce computation with the proof assistant Coq. In the model, mappers and reducers in MapReduce computation are modeled as functions in Coq, and a specification of a MapReduce application is expressed in terms of invariants among functions involving its mapper and reducer. The model also provides modular proofs of lemmas that do not depend on applications. To achieve the goal, we investigated the feasibility of two approaches. In one approach, we transformed verified mapper and reducer functions into Haskell programs and executed them under Hadoop Streaming. In the other approach, we verified JML annotations on Java programs of the mapper and reducer using Krakatoa, translated them into Coq axioms, and proved Coq specifications from them. In either approach, we were able to verify correctness of MapReduce applications that actually run on the Hadoop MapReduce framework.
UR - http://www.scopus.com/inward/record.url?scp=81055138346&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=81055138346&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-24690-6_24
DO - 10.1007/978-3-642-24690-6_24
M3 - Conference contribution
AN - SCOPUS:81055138346
SN - 9783642246890
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 350
EP - 365
BT - Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Proceedings
T2 - 9th International Conference on Software Engineering and Formal Methods, SEFM 2011
Y2 - 14 November 2011 through 18 November 2011
ER -