2021 Fiscal Year Research-status Report
正しさと効率の形式的証明を備えたスケルトン並列プログラミング環境に関する研究
| Project/Area Number |
19K11903
|
|---|
| Research Institution | Kyushu Institute of Technology |
|---|
Principal Investigator |
江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | BSP モデル / 並列スケルトン / 定理証明支援系 / 計算量証明 / 持続型例外処理 |
|---|
| Outline of Annual Research Achievements |
今年度は、大きくふたつの観点で研究を進め結果を得た。
ひとつめの成果として、BSP モデルに基づく並列プログラム記述のための低レベル並列スケルトンの計算量記述を伴う形式化がある。BSP モデルに基づく並列プログラムを記述するための BSPLib について、そのプリミティブ（低レベル並列スケルトン）を定理証明支援系 Coq 上で計算量記述を伴う形で形式化した。これにより、ユーザは、形式化されたプリミティブに、具体的な計算を記述したユーザ定義関数を与え、それらを組み合わせることで、計算量記述を伴う並列プログラムを Coq 上に記述できるようになった。その記述の際には、計算量に関する記述の正しさの証明がユーザに課せられる。そして、その証明を終えてプログラム記述を完了したならば、そのプログラムに関する計算量の記述が形式的に正しいと保証され、つまりは計算量の保証を伴ったプログラムコードの記述が得られたことになる。構築した形式化の具体的な応用として、最大部分列和問題の並列プログラムを記述し、その計算量が想定通りの並列計算量を持つことを証明できた。
もうひとつの成果として、動的負荷分散による並列プログラム等を記述できる、計算状態操作機構の形式化がある。計算状態操作機構とは、計算状態（関数呼び出し先祖のローカル変数など）の動的な変更を安全に行うための機構の総称であり、動的負荷分散による効率的な並列計算の実現に有用である。本研究では、計算状態操作機構のうちの持続型例外処理機構について、Scheme 言語をベースとして定理証明支援系 Coq 上にそのセマンティクスの形式化を与えた。これにより、持続型例外処理を用いて記述されたプログラムについて、その仕様（望ましくない実行状態にならないことや、終了時に正しい計算結果が得られていることなど）を形式的に検証することが可能となった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
いくらかの問題点はあるものの、研究の大きな目標である、並列スケルトンを用いた並列プログラム開発（スケルトン並列プログラミング）において計算量証明を伴う形でのプログラム記述を行える環境が構築された。よって上記の判断とする。
ただし、解決しなければならない問題点として、当初の想定よりもユーザプログラムの記述が煩雑になってしまうという問題点が明らかになった。この点の解決が今後の課題となる。具体的には、本研究は既存研究と同様に計算量に関する記述を関数の戻り値の型に埋め込むこととしているが、関数をカリー化して扱う（複数の引数を取る関数を、「引数を一つ受け取って、別の関数（残りの引数を受け取って処理をする関数）を返す」という関数として扱う）際に、引数の個数分だけ計算量記述がネストすることとなり（およそ引数の個数分の関数を返すことになり、それら全ての型に計算量記述が必要なため）、ユーザ定義関数の戻り値の型がとても煩雑になってしまう。特に、低レベルな並列スケルトンの組み合わせで並列プログラムを記述しようとした際にはカリー化した関数を多用するため、この問題が顕著となる。
この問題点の解決策としては、高レベルな並列スケルトンを提供することによる全体的な記述量とカリー化した関数の利用機会の削減と、Coqの暗黙引数や構文拡張の機能を応用することによる型記述の削減と、IDEやエディタでの支援を与えることとなどが考えられる。
|
| Strategy for Future Research Activity |
今年度得られた並列スケルトンの計算量記述を伴う形式化をベースとして、その有用性を高めるためにいくつかの観点で研究を進める。
まず、形式化した低レベル並列スケルトンを用いて、より抽象度の高い高レベル並列スケルトンの記述を行う。これにより、ユーザプログラムの記述量の削減が期待され、現状判明している記述の煩雑さの問題がある程度緩和されると期待される。
次に、計算量証明を伴った記述から並列プログラムを抽出しその性能を評価する。また、他の応用プログラムの記述を行う。これらにより、提案手法の定量的な評価を行う。
さらに、並列スケルトンに渡すユーザ定義関数の記述を支援する仕組みの開発を行う。可能であれば、なるべく諸々の明記を避けられる形になるよう、Coq の暗黙引数の機能等をうまく応用する。明記を避けられない部分については、IDEやエディタでの支援とすることを考える。
|
| Causes of Carryover |
旅費としての出費が抑えられたことや他資金との関連から高性能計算機の購入計画を変更したことによる。次年度、当初計画よりも多くのコアを備えた計算機の購入を行い、提案手法の性能評価に使用する。
|
Research Products
(2 results)
