Declarative Distirbuted Programming based on Combinatorial Topology

Research Project

Project/Area Number	20K11678
Research Category	Grant-in-Aid for Scientific Research (C)
Allocation Type	Multi-year Fund
Section	一般
Review Section	Basic Section 60010:Theory of informatics-related
Research Institution	Kyoto University
Principal Investigator	西村進京都大学, 理学研究科, 准教授 (10283681)
Project Period (FY)	2020-04-01 – 2025-03-31
Project Status	Granted (Fiscal Year 2020)
Budget Amount *help	¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000) Fiscal Year 2024: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000) Fiscal Year 2023: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000) Fiscal Year 2022: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000) Fiscal Year 2021: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000) Fiscal Year 2020: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Keywords	並行分散計算 / 数理論理モデル / 宣言的プログラミング / 並行分散システム / 組合せトポロジー
Outline of Research at the Start	並行分散計算の組合せトポロジー論は、幾何的モデルを用いて並行分散システムの振舞いについて理解を得るための手法である。本研究は、この組合せトポロジー論の適用範囲を従来より強力な計算モデルにまで拡張し、並行分散システムの計算構造を宣言的に記述するプログラミング手法を提案する。これによって並行分散システムを、並行プロセス毎の逐次プログラムの寄せ集めではなく、一体のシステムとして宣言的にプログラミングすることを可能にする。また、このような宣言的記述から、実行可能なプログラムを自動的に導出する手法を与える。導出されたプログラムが効率よく実行されるような最適化の技法も合わせて開発する。
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	本年度の研究成果を発展させ、まず繰り返しプロセス間通信を行う場合にも適用できるように、認識論理を用いた枠組みを拡張する。また、この枠組みがより多様な分散計算問題や分散計算プロトコルに対応できることが期待されることから、当初の計画を前後させて、排他制御の機構を持つ共有メモリ型システムに現れる分散計算モデルについても考察・研究を行う予定である。この方向での研究がうまく成功すれば、単純な並行分散システムだけではなく、より多様なシステムに対する宣言的プログラミングを可能にするための礎を築くことができる。また、数理論理的モデルに基づいて宣言的プログラミングを行うための手法についても調査と考察を進める。より具体的には、既存の認識論理や他の数理論理に基づくプログラミング手法について調査し、並行分散計算に適した宣言的並行分散論理型プログラミングのふさわしい形について考察していく。