2020 Fiscal Year Research-status Report
Declarative Distirbuted Programming based on Combinatorial Topology
| Project/Area Number |
20K11678
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
西村 進 京都大学, 理学研究科, 准教授 (10283681)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Keywords | 並行分散計算 / 数理論理モデル / 宣言的プログラミング |
|---|
| Outline of Annual Research Achievements |
宣言的プログラミングとは、プログラムの動作内容ひとつひとつではなく、プログラムのあるべき動作(入力と出力の関係)を記述するプログラミングのスタイルである。宣言的に並列分散プログラムを書くには、並列分散に関わる計算構造の本質的な理解が必要不可欠である。並列分散計算の組合せ幾何的モデルの理論により、n+1プロセスからなるシステムの並列分散実行はn次元単体的複体から別のn次元単体的複体への関数で特徴づけられるため、(プロセス数が大きいときの)計算構造は一般高次元の幾何的構造に対応する。しかしながら、このような一般高次元を扱うための幾何的手法はプログラミングの理論や方法論とは概念的に隔たりがあり、このことが宣言的な並列分散プログラミングの実現を困難にしている。
本年度の研究では、宣言的なプログラミングとより親和性が高いと思われる、認識論理の枠組みを用いた分散並列計算の数理論理モデルについて研究を行った。認識論理を用いた手法はGoubaultらによって近年提案されたもののその具体的な適用についてはほとんど例がない状態であったが、本研究では分散計算システムにおける本質的な問題のひとつであるk集合合意問題が不可解であることの別証明を与えることに成功した。しかも、統一的な議論により、標準的な故障モデルであるwait-freeだけでなくより一般のadversaryに対する不可解性を示すことができた。(大学院生との共同研究) この結果は、認識論理を用いた数理論理的手法が分散計算理論において重要な問題に適用可能なことを示すだけではなく、宣言的プログラミングを実現するための計算構造のより本質的な理解に寄与するものである。
現在この枠組を拡張して、並行プロセスどうしが何回でも通信を行った場合にも対応できるように拡張を行っており、その成果を国際研究集会に投稿準備中である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
並行分散プログラミングを宣言的に行うためにもっとも重要なのが、効率的な宣言的記述を可能にする計算モデルの開発である。本年度の研究で明らかになったのは、認識論理に基づく数理論理的モデルが分散計算の不可能性証明の強力な道具となることである。しかも数理論理的モデルは、異なる故障モデルに統一的に対応でき、繰り返しプロセス間通信を行う場合にも拡張できそう(現在進行中の研究)であり、さらにはモデルの構成がプログラミング概念と親和性がよい。
このことは、数理論理的モデルが宣言的プログラミングを実現するための基礎となりうることを強く示唆するものである。数理論理的モデルを利用することは当初の構想とはやや異なるが、このことは既存の提案とは全く異なる並行分散論理プログラミングの形に繋がるものと大いに期待できる。
|
| Strategy for Future Research Activity |
本年度の研究成果を発展させ、まず繰り返しプロセス間通信を行う場合にも適用できるように、認識論理を用いた枠組みを拡張する。また、この枠組みがより多様な分散計算問題や分散計算プロトコルに対応できることが期待されることから、当初の計画を前後させて、排他制御の機構を持つ共有メモリ型システムに現れる分散計算モデルについても考察・研究を行う予定である。この方向での研究がうまく成功すれば、単純な並行分散システムだけではなく、より多様なシステムに対する宣言的プログラミングを可能にするための礎を築くことができる。
また、数理論理的モデルに基づいて宣言的プログラミングを行うための手法についても調査と考察を進める。より具体的には、既存の認識論理や他の数理論理に基づくプログラミング手法について調査し、並行分散計算に適した宣言的並行分散論理型プログラミングのふさわしい形について考察していく。
|
| Causes of Carryover |
新型コロナ感染症の流行により、国内外ともに学会出席・研究出張が困難になったために旅費をほとんど執行できなかったためである。
次年度中に状況が改善すれば、学会出席・研究出張を行って順次執行していきたいと考えている。あまり状況が改善しない場合は、オンライン学会出席・発表等の環境を改善するため、ノートPCの更新を当初予定していたより上位機種に変更するなどの対応を考えている。
|
| Remarks |
研究成果の内容は arXiv論文として公開されている。
|
