Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications
Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications
复制标题
DOI：
10.1007/978-3-642-24690-6_24
复制
发表时间：
2011-11
期刊：
影响因子：
--
通讯作者：
K. Ono;Yoichi Hirai;Yoshinori Tanabe;N. Noda;M. Hagiya
中科院分区：
文献类型：
--
作者：
K. Ono;Yoichi Hirai;Yoshinori Tanabe;N. Noda;M. Hagiya
Hadoop MapReduce 是一个用于键值对分布式计算的框架。本研究的目的是验证 MapReduce 应用程序的实际运行代码。我们首先使用证明助手 Coq 构建了 MapReduce 计算的抽象模型。在该模型中，MapReduce 计算中的映射器和规约器被建模为 Coq 中的函数，并且 MapReduce 应用程序的规范以涉及其映射器和规约器的函数之间的不变量来表达。该模型还提供了不依赖于应用程序的模块化证明。为了实现这一目标，我们研究了两种方法的可行性。在一种方法中，我们将经过验证的映射器和减速器函数转换为 Haskell 程序，并在 Hadoop Streaming 下执行它们。在另一种方法中，我们使用Krakatoa验证了mapper和reducer的Java程序上的JML注释，将它们翻译成Coq公理，并从中证明了Coq规范。无论采用哪种方法，我们都能够验证在 Hadoop MapReduce 框架上实际运行的 MapReduce 应用程序的正确性。
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.