2018 Fiscal Year Research-status Report
Session-typed programming in unreliable communication environment
| Project/Area Number |
17K12662
|
|---|
| Research Institution | Gifu University |
|---|
Principal Investigator |
今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | セッション型 / 関数型プログラミング / 型システム / 線形型 / OCaml / 構文拡張 / デッドロック |
|---|
| Outline of Annual Research Achievements |
マルチパーティセッション型を一般的な静的型付きプログラミング言語で利用可能にするための技法を考案し、OCaml言語において実装した。本技法は、デッドロックフリー性の核となるグローバル型の整合性を、ホスト言語の型検査機構によって検査する。これにより、型検査に成功した（コンパイルに成功した）並行分散プログラムは、デッドロックなしで動作することが保証される。
従来、マルチパーティセッション型は外部ツールからのコード生成によって実現されており、拡張性・柔軟性に乏しかったが、本技法により、マルチパーティセッション型が静的型付きプログラミング言語のライブラリの形で利用可能になる。これによりデッドロックがないプログラムを容易に効率よく実装できるようになるため、並行分散システムの信頼性向上が期待できる。本研究は次年度において国際会議に投稿・発表する。
さらに、昨年度に国際会議で発表した OCaml におけるバイナリーセッション型の実装 session-ocaml を拡張し、論文誌 Science of Computer Programming に extended version として投稿し、採択された。この拡張は、線形型システムを OCaml 上で模倣する枠組みの上にバイナリーセッション型を実装するものであり、線形型を用いた他のプログラミング言語との親和性が高い。
さらに、本研究の副産物的な結果として、パラメタ化モナドと表層構文の工夫により線形型プログラミングを可能にする枠組みを提案した。その実装である LinOCaml は GitHub 上で公開されている。この枠組みにより、リストや木といった構造をもつ線形型付きのデータを扱うことが可能になった。この結果は論文誌 Journal of Information Processing に採択された。
|
| 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 |
マルチパーティセッション型の型付けに関する論文を発表するとともに、メッセージの到達性に関する理論について調査を継続する。通信オートマトン (Communicating Finite State Machine) の理論において、従来の制限を取り払う形での文献が発表されている。これに基づき、メッセージの不達性をエンコードする方法などを検討する。
|
| Causes of Carryover |
7月から8月にかけて英国の共同研究者が来日し、マルチパーティセッション型のプログラミングが想定より早く実現した。このことから、2018年の出張旅費を抑えることができた。理論研究の進展と研究成果の最大化のため、2019年度に英国インペリアルカレッジロンドンへの研究出張と先方研究者の招聘を計画した。その結果として、次年度使用額が生じた。
次年度においては、英国への研究出張と先方研究者の招聘に用いる計画である。
|
