Coqを使用したMapReduceアプリケーションの検証とScalaコード の抽出

摘要

あらましHadoop MapReduceはデータとしてキーと値による組を利用する大規模並列処理を行うための フレームワークであり,今日では広く利用されている.目的の処理を行うため,Map及びReduce処理の定 義を正しく与える必要がある.本論文では新たにDSLとしてFMR(Feather-light MapReduce)を提案する. FMRで記述されたMap処理及びReduce処理は定理証明支援系Coqで検証可能であり,自動的にHadoop MapReduce上で実行可能なScalaのプログラムへと変換することが可能である.Hadoop MapReduceにおけ る典型的な処理に着目し,FMRでは効率的な逐次入出力を記述可能にした.著者のグループの先行研究で作成 したMapReduceモデルを元に,FMRによる実装が仕様を満たすことを証明を用いて検証する.従来のCoq上 におけるMapReduceモデルから得られる定義より,実行性能の低下を抑制する効果を評価した.また,FMR を用いることによる証明コストの上昇についても評価を行った.