プログラムの模倣合同性の危険対解析による自動判定

Research Project

Project/Area Number	22K17850
Research Category	Grant-in-Aid for Early-Career Scientists
Allocation Type	Multi-year Fund
Review Section	Basic Section 60010:Theory of informatics-related
Research Institution	Kyoto University
Principal Investigator	室屋晃子京都大学, 数理解析研究所, 助教 (00827454)
Project Period (FY)	2022-04-01 – 2025-03-31
Project Status	Granted (Fiscal Year 2022)
Budget Amount *help	¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000) Fiscal Year 2024: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000) Fiscal Year 2023: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000) Fiscal Year 2022: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Keywords	項書き換え系 / 危険対解析 / 文脈等価性 / プログラム等価性
Outline of Research at the Start	プログラムの「文脈等価性」、つまりプログラムの部分的な変更がプログラム全体の振る舞いを変えないことを簡便に立証することは、特にコンパイラ最適化の安全性保証などにおいて重要である。文脈等価性の立証アプローチの一つに、プログラムの「模倣合同性」を示すものがある。模倣合同性を示す従来手法はプログラムの多様な振る舞いに対応できる汎用性を持つ一方で、自動化が容易でないことが知られている。本研究では、項書き換え系理論における自動化可能な基盤技術である「危険対解析」を応用することで、模倣合同性を通じた文脈等価性の汎用的かつ自動化可能な立証手法を新規に提案することを目的とする。
Outline of Annual Research Achievements	本研究は、模倣合同性の立証手法を提案・自動化することにより、プログラム等価性の自動証明手法を与えることを目指すものである。本年度では、制限つきの項書き換え系において模倣合同性の立証手法を定式化し、それに基づいて自動判定アルゴリズムを構築することを目標として研究を行い、制限つきの項書き換え系として「項評価系」を提案した。この項評価系について、項書き換え系に関するワークショップ58th TRS Meeting (2023年2月)での発表を行った。プログラムの実行を項書き換え系で表現するためには、既知の2種類の制限を加える必要があると予想されていた。1つ目は書き換えの場所を制限する手法(Lucas 1995)であり、2つ目は書き換え対象を構文的に制限する手法(Hamana et al. 2020)である。ところが、必要な制限はこの2つだけではなく、書き換えの順序を制限する手法が新たに必要であることが分かった。プログラム実行のモデリングにおいては、評価文脈を用いて書き換えの場所・順序を制限する手法が主流となっている。そこで、項書き換え系に評価文脈を組み合わせることで、書き換えの場所・順序が制限できるような新たな系を開発し、項評価系と名づけた。この成果は、項書き換え系理論の知見をプログラム意味論へ応用する上での大きなステップと捉えられる。プログラム実行がしばしば項書き換え系と見なされうるにも関わらず、項書き換え系理論からプログラム意味論への知見・技術の移植は進んでいない現状がある。項評価系という本年度の研究成果は、そのような状況に対して、プログラム意味論で基本的な概念である評価文脈が項書き換え系には欠如していることが根本的な原因であることを示唆するものである。項評価系に項書き換え系の技術を移転することで、項書き換え系の技術をプログラム意味論へ応用することが可能になると考えられる。
Current Status of Research Progress	Current Status of Research Progress 3: Progress in research has been slightly delayed. Reason 当初計画では、本年度は制限つき項書き換え系において模倣合同性の立証手法を構築・自動化する予定であった。制限つき項書き換え系は既知の2種類の制限(Lucas 1995, Hamana et al. 2020)を組み合わせることで得られるという予想を立てていたが、この予想に反し、評価文脈という基本的かつ新たな制限が必要であることが明らかになった。本年度はまず、よりシンプルな一階の項評価系を構築することに注力し、プログラム実行のモデリングに必要となる高階の項評価系の構築には至らなかった。それに伴い、一階の項評価系での模倣合同性の立証手法を考察することはできたものの、高階の項評価系での模倣合同性の立証手法を提案・自動化するには至らなかった。
Strategy for Future Research Activity	次年度以降は、模倣性の具体的定義を拡張することで提案手法の適用範囲を広げる研究を行う予定であったが、本年度の積み残しに優先的に取り組み、その後に当初予定の研究を続行する計画である。本年度の積み残しの1つ目は、高階の項評価系を構築することである。これは一階の項評価系を元に比較的容易に構築できると考えられる。積み残しの2つ目は、模倣合同性の立証手法を提案・自動化することである。本年度、一階の項評価系において模倣合同性の立証手法を考察した結果、標準的な危険対解析を用いることのできる項評価系のクラスは予想よりも限定的であることが明らかになった。より広範な項評価系に提案手法を適用するには、危険対解析そのものも併せて拡張する必要があることが示唆された。次年度は、まず限定的な項評価系での標準的な危険対解析を実装し、それにより模倣合同性の立証手法を提案・自動化することを行う。並行して危険対解析の拡張を模索する。ここでは、一階の項書き換え系から高階の項書き換え系に危険対解析を拡張する標準的な手法に、項書き換え系から実用的な項評価系に危険対解析を拡張する新たな手法を組み合わせることになる。