Tree Borrows

多くの場合、過剰なことは不足と同様に悪い問題です。

Tree Borrows は ETH Zurich のプログラミング言語基礎実験室が提案した新しい規範で、Rust プログラミング言語における unsafe ブロックが未定義動作(Undefined Behavior, UB)を引き起こす境界を正確に定義することを目的としています。Rust は所有権概念を型システムに採用し、メモリ安全を保証し、データ競合を回避する強力な保証を持っていますが、unsafe ブロックはプログラマが手動で安全性を維持する必要がある例外です。unsafe コードの誤用を防ぐため、かつ強力なコンパイラ内部最適化(例えば指針別名最適化)を維持する必要があるため、従来の Stacked Borrows モデルは関連する規範を定義しようと試みたが、実務で一般的なパターンに合わないため過度に厳格だった。Tree Borrows はスタックを木構造に置き換え、元の制限を補完し、さらに多くの文法パターンをサポートしています。

研究チームの実験では、Tree Borrows は 30,000 個の広く使用されている Rust パッケージを分析した結果、Stacked Borrows に比べて不適切な使用法を拒否するケースが 54% 減少した。また、論文では Rocq ツールを用いて、この新しい規範がほとんどの既存の最適化戦略を保持しつつ、読み込み間の再配置などの新たな最適化を導入していることを示した。

論壇では、一部のユーザーが 2018 年と 2020 年に注目を集めた早期の Stacked Borrows モデルの主な問題が、unsafe コードの挙動を過度に狭隘に定義していたことだったと述べた。複数の論壇参加者が強調したのは、Rust コンパイラが特定のコードを受理する可能性があるが、これらのコードが厳格な複数の可変参照の共存を禁止するルールを違反しているため、未定義動作を引き起こす可能性があるということだった。別のユーザーは Ralf Jung のブログを引用し、Tree Borrows はこれらの反例を除去するだけでなく、今後の Rust の操作語意(operational semantics)をより正確に記述するための理論的基盤を提供していると補足した。

この研究は unsafe コードの境界問題に関する深入りした解析と革新的な解決策により、PLDI'25 の Distinguished Paper Award を受賞し、Rust 言語の安全性と最適化理論の新たな飛躍を促進する重要な成果とみなされている。論壇ではさらに興味深いことに、著者である Neven Villani が著名な数学者 Cédric Villani の息子であることが指摘され、学術界と実務界の両方で広く注目されている。

https://news.ycombinator.com/item?id=44510600