Session type embedding for practical concurrent/distributed programming

• Project/Area Number: 21K11827
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Gifu University
• Principal Investigator: 今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
• Project Period (FY): 2021-04-01 – 2024-03-31
• Project Status: Discontinued (Fiscal Year 2023)
• Budget Amount: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000); Fiscal Year 2024: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2023: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2022: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2021: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
• Keywords: 並行ソフトウェア / 通信プロトコル / セッション型 / 関数型プログラミング言語 / OCaml / モデル検査 / 並行プログラミング / 型システム / 分散プログラミング

Outline of Research at the Start

プログラミング言語の「型」は，整数や文字列などの「データ」を分類し間違いを事前に検出するための仕組みです．これに類似する枠組みとして，例えばインターネットで用いられる通信ポートは，HTTP や SMTP といった通信プロトコルで分類されています．セッション型はこの「通信ポート」のプロトコルを表す「型」であり，プログラムにおけるデッドロックや競合条件などの通信記述の誤りを事前に検出できます．
本研究は，セッション型をプログラミング言語において活用する軽量な方法を理論と実装の両面で開発します．これにより，多くの人が高信頼な並行分散ソフトウェアを手軽に構築できるようになることを目指します．

Outline of Annual Research Achievements

研究実績は大まかに次の3つに分けられる．
(1) セッション型，プログラミング言語の型システムとモデル検査の統合．具体的には，従来の，ソフトウェア全体の通信プロトコル設計とその安全性の検証が必要な「トップダウン型」の開発手法ではなく，それらが不要な「ボトムアップ」の手法を確立し，その実装であるkmclibを実装した．その成果に関する論文は， トップレベル会議の1つである TACAS 2022 に採択された．
(2) セッション型の表現能力に関する探究．(2-1) マルチパーティセッション型の混合選択に関する理論的な検討を行った．混合選択は，通信プロトコル参加者が特定の状態において送信と受信の双方を選択できる機能であるが，これは実用的に重要である一方でデッドロックフリー性などの信頼性に関する理論的な基礎は未整備である．本研究課題では，その無限のトレースを扱うための理論的基礎を検討した．(2-2) マルチパーティセッション型のプロトコルを文脈自由文法へと拡張し，処理系Session C#に実装した．
(3) これらからの派生的な研究．(3-1) 上述(1)の派生として，プログラミング言語OCamlのアドホック多相に関する拡張を設計し実装した．アドホック多相は単一の関数名に対して，引数型に応じた複数の定義本体を与える多重定義の機能である．これにより，OCamlプログラムにおいて型ベースのディスパッチが可能となり，プログラミングの効率向上が期待できる．(3-2) 上述(2-1)の派生として，高階項書換えシステムの活用を検討した．この際，共同研究者である群馬大学浜名准教授の高階項書換えシステムの処理系SOLの改修に関与した．停止性判定ツールのコンペティションTermComp2022に参加し，入賞した．
また，上記(2),(3-1)の進行中の内容や成果を国内ワークショップ・研究会にて発表した．

Research Products

• [Int'l Joint Research] Royal Holloway, University of London/Brunel University London(英国)
• [Int'l Joint Research] Imperial College London/Brunel University London/University of London Royal Holloway(英国)
• [Journal Article] Kmclib: Automated Inference and Verification of Session Types from OCaml Programs (2022)
  • Author(s): Keigo Imai, Julien Lange, Rumyana Neykova
  • Journal Title: TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science Volume: 13243 Pages: 379-386
  • DOI: 10.1007/978-3-030-99524-9_20
  • ISBN: 9783030995232, 9783030995249
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Presentation] Polymorphic Multiparty Session Handlers in OCaml (2022)
  • Author(s): Keigo Imai
  • Organizer: PLACES 2022: 13th Workshop on Programming Language Approaches to Concurrency- & Communication-cEntric Software, Munich, Germany
  • Int'l Joint Research
• [Presentation] The System SOL version 2022 (2022)
  • Author(s): Makoto Hamana, Keigo Imai
  • Organizer: WST 2022: 18th International Workshop on Termination
  • Int'l Joint Research
• [Presentation] 有界な余帰納的定義による非同期マルチパーティセッション型の無限トレース意味論 (2022)
  • Author(s): 今井 敬吾
  • Organizer: 第141回プログラミング研究発表会
• [Presentation] 伊藤 将希, 今井 敬吾 (2022)
  • Author(s): OCaml におけるプレースホルダ式によるアドホック多相の実現
  • Organizer: 第143回プログラミング研究発表会
• [Presentation] Verifying Session-Typed Concurrent Programs using Typed PPX in OCaml (2022)
  • Author(s): Keigo Imai, Julien Lange, Rumyana Neykova
  • Organizer: 第137回プログラミング研究発表会
• [Presentation] Kmclib: Automated Inference and Verification of Session Types (PPL Category 2) (2022)
  • Author(s): Keigo Imai, Julien Lange, Rumyana Neykova
  • Organizer: PPL 2022: 第 24 回プログラミングおよびプログラミング言語ワークショップ
• [Presentation] OCamlのための構文上の穴を用いたアドホック多相のプリプロセッサによる実装 (ポスター) (2022)
  • Author(s): 伊藤 将希, 今井 敬吾
  • Organizer: PPL 2022: 第 24 回プログラミングおよびプログラミング言語ワークショップ
• [Presentation] Polymorphic Multiparty Session Handlers in OCaml (2022)
  • Author(s): Keigo Imai
  • Organizer: PLACES 2022: 13th Workshop on Programming Language Approaches to Concurrency- & Communication-cEntric Software
  • Int'l Joint Research
• [Presentation] 文脈自由マルチパーティセッション型の実装 (ポスター) (2022)
  • Author(s): 木村 駿介, 今井 敬吾
  • Organizer: PPL 2022: 第 24 回プログラミングおよびプログラミング言語ワークショップ
• [Presentation] Multiparty Session Programming with Global Protocol Combinators (oral communication) (2021)
  • Author(s): Keigo Imai, Rumyana Neykova, Nobuko Yoshida, Shoji Yuen
  • Organizer: ICE 2021: 14th Interaction and Concurrency Experience, co-located with DisCoTec 2021
  • Int'l Joint Research
• [Presentation] Verifying Multiparty Communication Protocols using ML Type Systems (2021)
  • Author(s): Keigo Imai, Rumyana Neykova, Nobuko Yoshida, Shoji Yuen
  • Organizer: ML'21: ML Workshop 2021, co-located with ICFP 2021
  • Int'l Joint Research
• [Remarks] Kmclib
  • URL: https://github.com/keigoi/kmclib