| 研究課題/領域番号 |
25330087
|
|---|
| 研究種目 |
基盤研究(C)
|
| 研究機関 | 首都大学東京 |
|---|
研究代表者 |
福永 力 首都大学東京, 理工学研究科, 教授 (00189961)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | 並列システム記述理論 / 形式理論 / timed-CSP / FDR（失敗-発散-詳細化）解析 / 国際情報交換（英国、米国） |
|---|
| 研究概要 |
時間概念を取り組んだCSPを理論的土台とした並列処理システムの失敗-発散-詳細化解析プログラムの構築が我々の本課題の目標である．そのためには1）（machine-readable）timed-CSPで記述された並列システムのコンパイラの作成、2）そのFDR解析、3）CSP記述の拡張（Mobile-channelあるいは共有メモリ）とそれに応じたコンパイラの拡張、といったステップで研究を進めている．またさまざまな時間概念にクリティカルな並列システムの例の収集も行う．
上記3段階でもっとも時間のかかると思われるものが1）のコンパイラの作成である．コンパイラが柔軟であると3）で示した拡張も比較的スムーズに行えると期待できる．しかしこのコンパイラ作成をまともに取り組むと時間と人手もかかる大きな仕事となってしまう．我々の先行研究であるtimed CSP Explorerの作成ではコンパイラを作らずCSPの各言語成分を関数言語（ML）で置き換えることにより行ってきた．しかしこれではCSPの持ついくつかの重要な記述が十分に表現できず、FDR解析のなかでトレース集合のみを活かした安全性解析のみの検証しか行えなくなってしまった．そこで今回は精度の良いコンパイラの作成に取り組むことにしたところである．
我々はこのコンパイラとしてナノパスコンパイラの概念を導入しようと思っている．またその基本記述言語をHaskellすることも決定した．ナノパスコンパイラはコンピュータ言語の成分を細かく分解して（ナノパス）そのうち有用なものをつなぎあわせて大きなプログラムのコンパイルを行おうというものである．現在このナノパスコンパイラの構築を行っており本年度前半でまず第１バージョンを完成させるべく取り組みを行っている．このコンパイラの作成が終了した時点で研究集会、学会においてその公表を行っていこうと考えている．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
まずTimed CSP（CSPとはCommunicating Sequential Processesの略）について、取組状況の調査を行った．そしてCSPにtiming概念を入れた並列プログラムの構築への取り組みに新規性があることを確認した．その過程でCSPおよびその競合理論としてのπ-calculusの比較研究を行い我々の目指すtimed-CSPの拡張性を調査した．25年度前半はこの調査に集中して作業を進めた．
CSPとπ-calculusはともに並列して走る2つのプロセス間のデータ交換をチャンネルという概念をもって行い、共有メモリは持たないという考え方で並列システムを構築させるが、大きな違いはπ-calculusのチャンネルでチャンネルを転送できる仕組み（Mobile-channel）がCSPには欠けているということであった．このMobile-channelの概念は動的ネットワークを構築できるという意味で大きな魅力でありCSPにこの概念が欠けていた．しかしイギリスのグループを中心にOccam-πというCSPおよびその発展をコンピュータ言語として実装されたものが公表されその中でMobile-Channelおよび共有メモリの概念をCSPの実装レベルで取り入れる事例が散見されるようになった．これらの概念および我々の目指す「時（timing）」が引き起こすイベントの概念を取り組んだtimed CSPを持ってすれば現代でも十分に通用するかなり良い並列システム検証システムが構築できると確信した．この調査は第11回CSP研究会（2013年5月25日 at 東洋大学）で「π-calculusとOccam-π」という題目で公表した．Occam-πはCSPを具現化したコンピュータ言語である．CSPという理論は変更せず実装において実質的に新たな概念を組み込んでいく手法は大いに参考になった．
|
| 今後の研究の推進方策 |
初項および前項で述べたように研究の推進方法・ステップは明確に定義されている．多少手間取っている面もあるが並列システムのコンパイラ作成はナノパスコンパイラ手法にのっとりHaskellベースでその開発が進められている．コンパイラはmachine readable CSP言語で記述されたプログラム（CSPプロセス）をHaskell記述の関数に書き換え実行させるものである．実行後はそのプロセスがたどった痕跡をトレース集合、失敗集合、発散集合をリストとして出力する．この出力を分析することによりプロセスの持つ危険性、安全性などの検証を行う．前項で記したようにしたがってこのコンパイラの制作が現在もっとも集中して行っているところである．また検証すべきプロセス例として教科書レベルの単純なものではなく複雑な並列システムの例を多く収集してプログラム開発のデバッグに役立てていきたいと思っている．Mobile channelなどのCSPの実装的改造はmachine readable CSP言語において対応させる．これはOccam-πの先例をすでに調査してきているのでその取組を参考にしていきたい．
本課題の研究は1年が過ぎて基本的な環境が整い、システム開発の基本骨子が固まってきた．Haskellベースのナノパスコンパイラによるシステム構築である．イギリスのKent大学にはこれらの研究を行っている研究者が数多く存在している．Occam-πもその大学のグループにより開発された．26年度には情報交換のために一度そちらに出向きお互いの研究進捗状況について議論していきたいと考えている．
|
| 次年度の研究費の使用計画 |
25年度、他のプロジェクトの研究（都産技研との共同研究）事業が行われていた．この研究は本課題研究と内容として重なる部分もあり、物品費、人件費および旅費はこの予算を登用した．共同研究は最終年度でもありそちらを優先的に利用しようということでもあった．
本年度イギリスのKent大学の研究者との情報交換、またシアトルで開催されるIEEE研究会での公表などの計画があり海外出張旅費としての利用を計画している．また本年度の予算と合わせてプログラマの雇用の人件費に上乗せしようと考えている．
|
