Using Coq in specification and program extraction of Hadoop MapReduce applications

Kosuke Ono, Yoichi Hirai, Yoshinori Tanabe, Natsuko Noda, Masami Hagiya

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages350-365
Number of pages16
Volume7041 LNCS
DOIs
Publication statusPublished - 2011
Externally publishedYes
Event9th International Conference on Software Engineering and Formal Methods, SEFM 2011 - Montevideo
Duration: 2011 Nov 142011 Nov 18

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7041 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other9th International Conference on Software Engineering and Formal Methods, SEFM 2011
CityMontevideo
Period11/11/1411/11/18

Fingerprint

Specifications

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Ono, K., Hirai, Y., Tanabe, Y., Noda, N., & Hagiya, M. (2011). Using Coq in specification and program extraction of Hadoop MapReduce applications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7041 LNCS, pp. 350-365). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7041 LNCS). https://doi.org/10.1007/978-3-642-24690-6_24

Using Coq in specification and program extraction of Hadoop MapReduce applications. / Ono, Kosuke; Hirai, Yoichi; Tanabe, Yoshinori; Noda, Natsuko; Hagiya, Masami.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7041 LNCS 2011. p. 350-365 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7041 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Ono, K, Hirai, Y, Tanabe, Y, Noda, N & Hagiya, M 2011, Using Coq in specification and program extraction of Hadoop MapReduce applications. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 7041 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7041 LNCS, pp. 350-365, 9th International Conference on Software Engineering and Formal Methods, SEFM 2011, Montevideo, 11/11/14. https://doi.org/10.1007/978-3-642-24690-6_24
Ono K, Hirai Y, Tanabe Y, Noda N, Hagiya M. Using Coq in specification and program extraction of Hadoop MapReduce applications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7041 LNCS. 2011. p. 350-365. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-24690-6_24
Ono, Kosuke ; Hirai, Yoichi ; Tanabe, Yoshinori ; Noda, Natsuko ; Hagiya, Masami. / Using Coq in specification and program extraction of Hadoop MapReduce applications. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7041 LNCS 2011. pp. 350-365 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{4e0b7a0b416a4952b4f10740ed48686e,
title = "Using Coq in specification and program extraction of Hadoop MapReduce applications",
abstract = "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.",
author = "Kosuke Ono and Yoichi Hirai and Yoshinori Tanabe and Natsuko Noda and Masami Hagiya",
year = "2011",
doi = "10.1007/978-3-642-24690-6_24",
language = "English",
isbn = "9783642246890",
volume = "7041 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "350--365",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

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

VL - 7041 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 350

EP - 365

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -