- Rust言語のunsafeコードにおける最適化の限界を克服するための新しいメモリモデルであるTree Borrowsを提案
- 既存のStacked Borrows方式では実務のRustコードでよく使われる複数のパターンを許容できなかったが、Tree Borrowsはツリー構造でこれを解決し、より現実的で柔軟な規則を提供
- Tree BorrowsはStacked Borrowsより54%多く、実世界のコードのテストケースを通過
- Rustの主要なメモリ安全性と最適化可能性(特にread-read reorderingなど)の大半を維持しつつ、最新のRust borrow checkerの高度な機能まで反映
- ツリーベースの状態機械モデルを導入し、Rustの最適化と安全性検証研究における重要なマイルストーンを提示
Rustの所有権システムとunsafeコードの限界
- Rustは所有権ベースの型システムにより、メモリ安全性やデータレース防止などの強力な保証を提供
- しかしRustにはunsafe escape hatchが存在し、この場合の安全性検証はコンパイラではなく開発者の責任となる
- コンパイラは強力な最適化のためにポインタのエイリアス規則を活用したいが、誤ったunsafeコードによってこうした最適化が無力化される可能性がある
Stacked Borrowsとその限界
- 従来はStacked Borrowsというモデルがunsafeコードの「不正な動作」を定義し、最適化の基準を提示していた
- しかしこの方式は、実際のRustコードで一般的なさまざまなunsafeパターンを許容できず、最近導入されたRustのborrow checker機能も反映できていなかった
Tree Borrowsの登場
- Tree BorrowsはStacked(スタック)構造の代わりにツリー構造でメモリ権限を追跡する新しいモデル
- これにより、より多くの実務Rustコードのパターンを安全に許容し、borrow規則の柔軟性と現実での適用性を大きく高める
- 30,000件の人気Rustクレートの評価で、Stacked Borrowsより54%多くのテストケースを通過
Tree Borrowsの特徴と利点
- 既存のStacked Borrowsの**主要な最適化(例: read-read reorderings)**の大半を維持
- さらに、最新のRust borrow checkerの高度な機能(例: 非定型なborrowパターン、複雑なポインタ操作など)も反映可能
- ツリーベースの状態機械モデルを導入し、安全性と最適化可能性のバランスを取る
結論と意義
- Tree Borrowsは、Rustコンパイラにおけるunsafeコード処理と最適化研究に新たな基準を提示
- 実務Rustコードと最新のborrow checker方針まで包含する現実的で堅牢なメモリモデルと評価される
- 関連論文、アーティファクト、ソースコードは公開されており、Rustコンパイラおよび検証研究コミュニティに大きな影響を与える見込み
1件のコメント
Hacker Newsの意見
最近のRalf Jungのブログ記事で、さらに多くの文脈が提供されている リンク
おまけ: Rustの実行意味論をRustの方言で明確に指定しようとする研究グループの最近の発表もおすすめ YouTube
コンパイラの立場から、ポインタのエイリアシングに関する型システムの強力な保証を活用して強力な最適化ができるという主張があるが、実際にどれほど効果があるのか気になる
Linus Torvaldsは、Cのstrict aliasing規則はあまり有用ではなく、むしろ問題を引き起こすと長年主張してきた
彼の例の投稿も興味深い
Rustが本質的にCと根本的に違うのか気になるが、個人的な経験では、特にunsafeが絡むと大差ないように感じる
Cのstrict aliasing規則は本当にひどいと思う
Rustで提案されている規則はずっと異なっていて、コンパイラにとってもより有用で、プログラマにとっての負担も少ないと思う
言語内でopt-outとしてraw pointerを使えるし、コードを検査できるツールもある
結局のところ、あらゆる言語設計と同じく妥協だ
Rustはこの最適化領域で新しいバランスを見つけたように思えるし、その判断の結果は時間が示すだろう
Rustのエイリアシング規則はCとはかなり違う
Cではrestrictキーワードはほぼ関数引数にしか意味がなく、型ベースのエイリアシング(type-based aliasing)は実際にはあまり使われないか、使いにくい
Rustではライフタイムや可変性を精密に表現でき、型そのものとは無関係にさまざまな方法でメモリを安全に扱える
重なり合う&mut参照さえ生じなければ、複数のnon-overlappingな&mutに分割して利用できる点が大きい
実際にこれがどれほど性能に影響するのか、もっと広範な分析が気になる
単純にエイリアシング情報をLLVMに渡す部分をcompilerからすべて取り除いて性能を比較すれば、すぐに分かるはずだ
noaliasアノテーションがランタイムで約5%性能を改善するという主張もあり、関連するコメントがある(データは古いが)Linusがコンパイラについて語ることは割り引いて考えた方がよい
OSカーネルとコンパイラは完全に別の分野だ
今ではエイリアス解析が本当に強力な性能向上の鍵になっている
最大の効果は単純なヒューリスティクスから得られ、複雑なエイリアス問い合わせはそれ自体ではあまり活用されない
理論的に完全なエイリアス解析が性能をどれだけ向上させるのか実験してみたいが、一般的なコードでもせいぜい約20%が限界だと思う
もちろん非常に高度な最適化(例: データレイアウト変換)は、エイリアス解析がなければ試みることすらしないという限界がある
Cのstrict aliasingとRustのaliasingは概念が異なる
Cは型ベース解析(TBAA)が中心で、Rustはこれを意図的に採用していない
Stacked Borrowsに関する過去スレッドが2020年、2018年にあった
2020年のスレッド
2018年のスレッド
Tree Borrowsの仕様をNevinのウェブサイトで数年前に読んだが、複雑な問題も優雅に解決していて印象的だった
実際の経験上、Tree BorrowsはStacked Borrowsでは不可能な合理的なコードを可能にする
Rust標準ライブラリのサンプルコードも参考になる
Rustや次世代PLが、特性や目的(コンパイル速度、ランタイム速度、アルゴリズムの柔軟性など)の異なる複数のborrow checker実装から選べるように発展する可能性があるのか気になる
Rustはすでにborrow checker実装の切り替えを経験している
スコープベースから非レキシカルに変わり、Poloniusという実験的実装もオプションとして存在する
新実装の準備ができれば旧版をわざわざ残すことはしない
ランタイムチェックが必要なRc、RefCellなどを使って、より柔軟にすることもできる
affine type(Rustで使用)、linear type、効果システム、dependent type、形式的証明など、さまざまな方法がすでに存在する
各方式ごとに実装コスト、性能、開発体験などの特性が異なる
Rust以外でも、生産性の高い自動リソース管理と型システムの組み合わせが志向されている
実際に必要なのは、関数のpreconditionを精密に記述し、中間条件の証明までできるseparation logicだ
Rustのアプローチは、人々が実際に望む通常の不変条件をシステム化して、強力な最適化を保証するものだ
borrow checkerの結果はfalse negativeだけでfalse positiveはないのか気になる
もしそうなら、複数実装をスレッドで並列実行して、最も早く終わった結果を使うことも可能なのではないかと思う
複数のborrow checker実装を同時に許容すると、エコシステムが分裂しやすいため望ましくない
論文に出てくるRustコードを実際にテストしてみたが、最新の安定版コンパイラでは拒否されないことを確認した
例のコード:
miriで上のコードを実行すると、
*x = 10;でエラーを報告するが、write(x);ではエラーは発生しないrustcは型システムの観点ではyが*mutなので、どちらのバージョンも拒否する理由がない
論文ではunsafeコードの問題として、以下の例を挙げている:
これが実際に可能なのか疑問だ
同一変数に複数のmutable参照をポインタで使うのは明らかにUBだが、自分が何か誤解しているのか気になる
上のコードはRustコンパイラが受理しても、規則には違反している
どんな規則か?
borrow checkerを通過するコードは合法
unsafeでは不正/UBも表現できる
borrow checkerの範囲より広いが、それでも合法な規則集合がある
この研究の目的は、その境界を厳密に定めることにある
Stacked Borrowsの論文はより単純だが、実際のunsafeコードには限界があり、Tree Borrowsはより広い安全範囲を認める
「複数のmutable参照ポインタが同時に存在してはならない」という点は明らかだが、それが正確にどの規則違反なのか明示された箇所がない
Tree Borrowsはまさにそのような定義を提案している
「コードがこういうことをできる」という表現は、実際にそのコードを書いて実行すると何かが動いてしまうが、Tree Borrowsのような定義がなければ、なぜそれが誤りなのかの根拠を立てにくい、という意味だ
自分でもTree Borrowsのような明確な規則の必要性をすでに受け入れているように見える
unsafeコードはあのように実際に可能であり、それがUBだということだ
例: playgroundリンク
関連する文脈を知りたければ、論文の直後の段落の冒頭が意図をよく表している
まさにそこがポイントだ
複数mutable参照禁止の規則を守るのは難しく、unsafeはrustのlifetimeシステムで保証される以上のことをはるかに多く許してしまうことを反映している
著者の一人であるNeven Villaniは、2010年のFields medal受賞者Cédric Villaniの息子だ
林檎は木から遠くへは落ちない、という比喩を思い出す
そして「qualitiesもtreeからborrowしたと言える」と気の利いたことを言ってみたかった
私は父親(Fields medal受賞者)とオフィスが近かったこともある
政界進出前の話だ
このモデルは本当に素晴らしい
自分が作っている言語にも実装してみるつもりだ
デジャヴであるはずがない
この投稿を2〜3か月ごとに見ている気がする