2022 Fiscal Year Annual Research Report
Theory and Application for Robust and High-Performance Systems Programming Languages
| Project/Area Number |
21J20459
|
|---|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
松下 祐介 東京大学, 情報理工学系研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2021-04-28 – 2024-03-31
|
| Keywords | Rust / プログラム検証 / 分離論理 / システムプログラミング |
|---|
| Outline of Annual Research Achievements |
トップ国際会議 ACM PLDI 2022 に前年度に条件付きで採択された主著論文 "RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code"（松下、Denis、Jourdan、Dreyer）について、論文およびアーティファクト（ソースコード等）の最終版を提出し、論文の最終的な採択・アーティファクトの再利用可能性評価を得て、正式に出版した。さらに、論文の上位約1割にのみ与えられる Distinguished Paper Award を受賞した。
この論文は、RustHorn（松下ら、2020）で提案された、Rust の所有権型と預言（未来の情報の先取り）の手法を利用して Rust プログラムを効率よく検証する手法の正当性を、様々な API を含む Rust の広いサブセットに対し一般に証明するための枠組みを提案し、定理証明支援系 Coq と分離論理フレームワーク Iris で機械化して実証した、というものである。
そして、アメリカ・サンディエゴで開催された国際会議 ACM PLDI 2022 に現地参加し、コロナ禍で長らく難しかった世界の研究者たちとの対面による密な交流を果たし、主著論文 "RustHornBelt" について口頭で発表・議論した。また、世界の最新の研究動向について知見を得て、自分の研究についても知ってもらえるように働きかけた。
東京大学大学院理学系研究科・理学部ニュース 2022年5月号 の「理学のススメ」に単著で一般向けの研究紹介記事「ソフトウェアの世界を切り拓く」を寄稿した。この記事では、研究分野の背景、研究という営みに対して抱いている思い、RustHorn のアイデアなどについて書いている。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
新しい分離論理（システムプログラムの挙動の正しさを検証するための論理）の構築方法 Syng を開発し、定理証明支援系 Agda 上で論理体系・健全性証明を機械化し、論文を執筆して ACM PLDI 2023 に11月に投稿した。
Syng の主な狙いは、可変データの共有を分離論理命題で表現されたプロトコルを使って検証する「命題的共有」の仕組みを一般的に提供することにある。既存研究の Iris（Jung ら、2015）は定理証明支援系 Coq 上の分離論理フレームワークであり、命題的共有を本格的に導入したことにより、Rust プログラムのメモリ・スレッド安全性を一般に保証する RustBelt（Jung ら、2018）などの高度な検証プロジェクトを実現してきた。しかし Iris では命題的共有の中身にアクセスした際に必ず「later 様相」で命題が弱まるという制約があり、これは証明が複雑化することに加え、停止性を含む liveness 性質の検証ができないという問題があった。
Syng では分離論理の「深い埋め込み」あるいは分離論理命題の構文を利用することで、later 様相による弱化なしに命題的共有を実現する、という仕組みを提唱した。この論文は2月に不採択の査読結果が通知されたものの、主に完成度の不十分さが指摘され、方向性については肯定的であった。
その後も研究を続けたところ、深い埋め込みにより later 様相なしに命題的共有をする、というアイデアを発展させて、より汎用的で拡張可能な分離論理フレームワーク Nola を実現できることを3月に発見し、定理証明支援系 Coq 上での機械化・論文執筆を本格的に始めた。Nola は様々な検証プロジェクトへの発展が広く期待されるものであり、Iris 研究の中心メンバーを含む国内外の研究者たちとその可能性について議論した。
|
| Strategy for Future Research Activity |
上述の新しい分離論理フレームワーク Nola について、定理証明支援系 Coq 上での機械化・論文を完成させ、7月に ACM POPL 2024 に論文を投稿する。Nola 研究の今後の課題としては、具体例を通した検証能力の評価、later 様相を扱うための既存手法との比較、推論規則を不用意に強めた時に生じるパラドクスの分析、論文のプレゼンテーションの洗練などがある。
また、Nola の応用にも取り組む。特に、RustBelt・RustHornBelt の Iris 上のモデルを Nola の later 様相のない命題的共有を使って洗練させ、RustHorn（松下ら、2020）方式の預言を使ったポインタ除去が Rust プログラムの safety（部分正当性）検証だけでなく liveness 性質（完全正当性や時相論理的性質など）の検証においても一般に健全であることを証明し、実際にこの検証手法の有用性を確かめる、というプロジェクトに着手する予定である。
以上の方針で研究を進めていって、分離論理フレームワーク Nola およびその応用を主貢献として博士論文を執筆し、最終的に12月に提出する。
8月頃にはヨーロッパに渡航し、スイス連邦工科大学チューリッヒ校 (ETH Zurich) の Ralf Jung 氏のグループ・Peter Mueller 氏のグループ、ドイツ・マックスプランクソフトウェアシステム研究所 (MPI-SWS) の Derek Dreyer 氏のグループなどを訪問し、Nola について研究発表をし、今後の共同研究の可能性について話す予定である。これにより、博士課程修了後にヨーロッパの研究機関でポスドクとして働くための基盤を築いていく。
また、1月にはロンドンに渡航して国際会議 ACM POPL 2024 に参加し、世界の研究者と議論・交流する予定である。
|
