2016 Fiscal Year Research-status Report
組合せ位相幾何に基づく高レベル仕様からの並列・分散プログラムの生成
| Project/Area Number |
16K00016
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
西村 進 京都大学, 理学研究科, 准教授 (10283681)
|
|---|
| Project Period (FY) |
2016-04-01 – 2020-03-31
|
| Keywords | 並行・分散プログラム / 位相幾何的手法 / プログラム導出 |
|---|
| Outline of Annual Research Achievements |
近年、分散計算の理論のひとつの重要な潮流として、分散タスクを組合せトポロジーにおける抽象単体的複体間の写像としてモデル化し、プロトコル実現性等の問題を位相幾何的性質の解析によって明らかにしようとする位相幾何的手法が大きく発展してきている。１年目の研究においては、プロトコル実現性を抽象単体的複体の変形可能性の問題に帰着し、この問題をある程度現実的な計算時間内で解くためのアルゴリズムを開発した。
分散タスクの仕様からcarrier複体と呼ばれる単体的複体を組合せ的操作によって導出し、プロトコル実現性の問題がこのcarrier複体内での適切な部分複体変形可能性に帰着できることを明らかにした。この問題は一般的には決定不可能であり、これを解く完全なアルゴリズムは存在し得ないが、なるべく広い範囲の分散タスクについて適用可能なもので、健全ではあるが完全ではない（変形可能と判定された場合は実際そうであるが、変形可能であってもそう判定されない可能性がある）アルゴリズムを得ることができた。
完全性をあきらめたとしても、この問題は組合せ的に解の探索空間が非常に大きくなりがちであるが、単体的複体をこれと等価なhypergraphで表し、これに既存の縮約アルゴリズムを適用することによって解の探索空間を大幅に縮退させる手法を開発することによってある程度小さなプロセス数（４くらいまで）の分散タスクに関しては現実的な計算時間で判定を行えることを確認した。また、この手法で正しく判定が行える分散タスクに関する条件を特定し証明を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
分散read-write共有メモリ型システムにおいて、分散タスクの仕様を満たすwait-free分散プロトコルが存在することの証拠を、タスクの仕様に内在する位相幾何的な性質を利用して自動的に発見するための理論とアルゴリズムの開発とその実証コードのプロトタイプまで行っており研究はおおよそ順調に進んでいる。
なお、上記研究の途中段階において、2016年7月に独Dagstuhlで行われたセミナーTopological Methods in Distributed Computing へ発表者の一人として招かれ、位相幾何的手法に関する一線級の研究者達と交流し意見交換を行った。
|
| Strategy for Future Research Activity |
前年度に開発したアルゴリズムは複体の変形を発見することにより分散タスクの実現可能性の判定までを行うものである。このアルゴリズムの正しさの証明は構成的なものなので、複体の変形が存在すればこれから実行可能な分散プログラムを生成することが原理的には可能なはずである。変形アルゴリズムを拡張して分散プログラムを生成できないか検討を行う。また、このアルゴリズムは色付き（各プロセスが固有のIDで識別される）分散タスクを対象としたものであったが、carrier複体を適切に定義し直すことによって色なし分散タスクにも適用できないかを考察する。
これまでの研究により、分散タスクの仕様から実行可能なプログラムを生成することが原理的には可能であることが明らかになった一方で、ある程度プロセス数が多い場合はこれをすべて自動で行うには計算量の観点から現実的でないと予想される。すべてを自動ではなく、分散タスクの仕様を、人間が介在して詳細化(refinement)することによって実行可能な分散プログラムを導出できるような枠組みを考案したい。既存のプログラム変換の研究で行われてきた手法（プログラム代数の運算等）が援用できないか考察を進めたい。
なお、変形アルゴリズムのために導入したcarrier複体は、分散タスクの仕様を組合せ的操作により単体的複体に埋め込んだものであり、この意味で高階の分散計算のモデルとなることが期待できる。このような視点からも研究を進めていきたいと考えている。
|
| Causes of Carryover |
昨年度の研究内容について、その正当性の証明等に少し手間取ってしまったためその成果の発表の機会を逃してしまったため。
|
| Expenditure Plan for Carryover Budget |
昨年度の成果については近々投稿予定であり、国際会議等への参加のために有効活用する。
|
Research Products
(2 results)
