RustのTree Borrowsとは？メモリ安全と最適化を両立する新モデル！

このコメントは当たり前すぎない？どのコードもUBがないことに依存してるんだし。Rustの強みは、Miriを含め、UBを避けるツールがめっちゃいいところだよ。

Stacked Borrowsについては、2020年と2018年にスレッドがあったよ。
https://news.ycombinator.com/item?id=22281205
https://news.ycombinator.com/item?id=17715399

PLDIのトークもここにあるよ: https://www.youtube.com/watch?v=CJi_Fcs4bak

論文の例4で「このRustコードはコンパイラに拒否される」って主張、試してみたんだけど、安定版コンパイラじゃそうならないみたいだよ？
fn main() {
let x = &mut 0;
let y = x as *mut i32;
*x = 10; // ←これが拒否されるはずだけど
unsafe {*y = 15 };
}

Stacked BorrowsはMiriのランタイムモデルだよ。Miriで実行すればエラーが出るはず。「Undefined Behavior: attempting a write access using […] but that tag does not exist in the borrow stack for this location」ってね。rustc自身は*mutはライフタイム関係がないから拒否しないんだ。

論文にMiriでTree Borrowsを実装したって書いてあったけど、これってMiriのデフォルトモデルになる可能性あるのかな？

論文は提案されたTree Borrowsモデルでの挙動を説明してるんだよ。現在のボローチェッカーの実装はもっと限定的な分析をしてて、この特定の競合は検出しないんだ。

Miriでの実装はこちらだよ：https://github.com/rust-lang/miri/tree/master/src/borrow_tra…

すごい仕事だね！Tree Borrowsの仕様をNevinのサイトで読んだことあるけど、かなり厄介な問題をエレガントに解決してるのに感動したよ。
Stack Borrowsだと違法なコードも、Tree Borrowsなら sensible になるんだ。
参考：[1] https://github.com/Voultapher/sort-research-rs/blob/main/wri… Miri column
[2] https://github.com/rust-lang/rust/blob/6b3ae3f6e45a33c2d95fa…

Rustとか将来のプログラミング言語が、いろんな特性（コンパイル速度、実行速度、アルゴリズムの柔軟性とか）を持った複数の借用チェッカーを選べるようになるのかな？

既に複数のアプローチがあるんだよ、例えばRustが使ってるaffine typesとか、linear types、effects、dependent types、formal proofsとかね。
それぞれ実装、パフォーマンス、開発体験でコストと機能が違うんだ。
Rust以外の言語は、ほとんどが自動リソース管理（どういう方法であれ）と上記の型システムを組み合わせて、パフォーマンス critical なコードパスで使ってるよ。

＞ affine types (Rustが使ってるもの)
ちょっと口を挟ませてほしいんだ。「affine types」って言ってるけど、実はUniqueness Typesだよ。
違いは「unrestricted types」との相互作用にあるんだ。Rustでは、これらの「unrestricted types」は参照（Copy を実装してるから複数回使える）だね。
Uniqueness types は呼び出し元に制約をかける（「この引数は私に渡すときにエイリアスしちゃダメだよ」）けど、呼び出され側には制限がないんだ。
これはRustにとって便利なんだ。なぜなら、値がエイリアスされてないと、解放しても解放済みのデータへの参照を残さないって確信できるからね。
Affine types は逆で、呼び出し元が呼び出され側に制約をかける（「この値を渡すけど、せいぜい一回しか使っちゃダメだよ」）んだけど、Rustの型システムでは表現できないんだ。なぜなら、呼び出され側は常に引数から参照を作って、その参照を複数の関数に渡せるからね。

Rustの型システムをaffineと呼ぶのは完全に正確だと思うよ。
「affine」の核心は、型システムに exchange と weakening があるけど contraction はないってことで、まさにRustの型システムを特徴づけてるんだ。
これらの用語の意味は https://math.stackexchange.com/questions/3356302/substructur… を見てみてね（これは論理学の文脈だけど、Curry-Howard correspondence を通して型システムでも同じだよ）。
これは「一度以上使っちゃダメ」というルールで説明されることが多いけど、それが実際の定義じゃないし、君の例が示すように、単純化された説明を文字通りに解釈すると混乱を招くことがあるんだ。
＞ 参照を渡すのは実際の値を渡すのとは違うから、affinity と矛盾しないよ。

＞ 参照を渡すのは実際の値を渡すのとは違うから、affinity と矛盾しないよ。
参照を渡すのが実際の値を渡すのと同じじゃないのは同意するよ。もしそうなら、参照の意味がなくなっちゃうもんね。でも、affinity とは矛盾するんだ。具体的には、同じ値から複数の参照が作れることと、参照の性質が組み合わさると affinity と矛盾するんだ。
＞ 「affine」の核心は、型システムに exchange と weakening があるけど contraction はないってことで、まさにRustの型システムを特徴づけてるんだ。
Rustの型システムは確かに contraction をサポートしてるよ。だって参照を複数回使えるんだからね。これは contraction じゃないの？Rustは少なくとも参照については contraction をサポートしてるように見えるけどね。
でも実際には、contraction が全くないってのは affine の定義としてはあまり役に立たないんだ。だって、そんなプログラミング言語は実用的じゃないし、Turing complete にすらならないだろうからね。代わりに、通常は「affine world」と「exponential world」（「unrestricted」、つまり好きなように使える値のこと）があるんだ。
そして、値は exponential world から affine world に行けるけど、逆はダメっていうのが慣例なんだ。だから affine な値を取る関数にはどんな値も渡せるけど、affine な方法で使う必要があって、その間、exponential（unrestricted）な値を取る関数には exponential な値しか渡せないし、affine な値は渡せないんだ。
信じられないなら、linear Haskell を使ってみてごらんよ。linear な引数を取る関数には non-linear な引数も渡せるけど、逆はダメなことに気づくはずだよ。
Rustの型システムをこう解釈するなら、参照を exponentials と解釈するのが自然だね。でも参照は逆の慣例なんだ。所有された値から参照には行けるけど、逆はダメで、linear/affine な型システムの慣例とはまさに逆の状況なんだ。
これらのシステムは使うと全然違う感じがするし、全く異なる性質を強制するから、両方を「affine」と呼ぶのではなく、別々の名前を持つことが重要だと思うんだ。Rustのようなシステムの通常の名前は「uniqueness types」だよ。Idris のドキュメント https://docs.idris-lang.org/en/latest/reference/uniqueness-t… や Wikipedia の記事 https://en.wikipedia.org/wiki/Uniqueness_type を見てみてね。

＞ Rustの型システムは確かに contraction をサポートしてるよ。だって参照を複数回使えるんだからね。これは contraction じゃないの？Rustは少なくとも参照については contraction をサポートしてるように見えるけどね。
いい質問だね！共有参照については、それらは Copy だから確かに contraction があるよ。Affinity は、contraction が普遍的な性質ではないってことを意味するだけで、一部の型や命題には contraction があってもいいんだ。
可変参照については、実際には複数回使えないんだ。でも、affinity がチェックされる前に desugaring フェーズがあって、可変参照 r の使用はどこでも \u0026mut *r に置き換えられるんだ。これは contraction を使ってるわけじゃないし、文字通り r をどこかに渡してるわけでもないんだ。r に対して特定の（そして興味深い）操作（「reborrowing」）を呼び出してるだけなんだ。
Rustは単なる affine system じゃない、借用で拡張された affine system なんだ。でも、Rustを affine system と呼ぶのは完全に妥当だと思うよ。言語が変数を二度「使う」のを防ぐという単純な事実があるからね。「reborrowing」は「使う」ケースじゃなくて、それ自身の特別なルールを持つ特別なケースなんだ。
＞ でも実際には、contraction が全くないってのは affine の定義としてはあまり役に立たないんだ。
もちろんRustには Copy と呼ばれる「複製可能な」型があるよ。それは本質じゃないけどね。
＞ Rustの型システムをこう解釈するなら、参照を exponentials と解釈するのが自然だね。
なぜそれが自然なの？可変参照は複製可能ですらないんだから、君の言ってることは参照全般にはあまり意味がないよ。たぶん共有参照のことだよね。それらは単に複製可能な型の一例だよ。
Rustにはあらゆる型を複製可能にするようなモダリティが型システムにないから、exponentials に相当するものはないんだ。（特に、\u0026T は T を囲むモダリティじゃないよ。それは異なる型で、異なる表現を持ってるんだ。そして君が言ったように、たとえそれがモダリティだったとしても、exponentials に対応するわけじゃないんだ。）
でも型システムは exponentials がなくても affine/linear でありうるから、この発言の意図がわからないな。
Uniqueness types は値への参照がいくつあるかについてのことらしいね。線形/affine 型を使ってそういう uniqueness な性質を強制できるし（そして実際Rustはそうしてる）、でもそれは線形/affine な型システムだって事実をなくすものじゃないよ。
＞ これらのシステムは使うと全然違う感じがするし、全く異なる性質を強制するから、
「感じ」については語れないな。affine 言語でプログラミングしたことないからね（Rust以外はね；）。でも性質の面では、Rustがやってることは affine logic にすごく近いんだ。核となる性質は「ものが複製されない」ことだね。俺のRustのモデル、RustBelt は、Rustの型システムの性質をエンコードするのに affine separation logic を使ってるんだけど、separation logic と linear logic の間にはたくさんの重複があるんだ。だからRustを affine 言語と呼ぶのは完全に理にかなってるっていう強い証拠がさらにあるんだね。

Affine logic の主なポイントは contraction を許さないことだけど、Rustの型システムは色々な形で contraction を許してるよね。Rustはいったいどういう点で「affine language」なの？
あと、Curry-Howard correspondence に関する主張は間違いだよ。それがRustが affine language だってことを証明するわけじゃない：https://liamoc.net/forest/loc-000S/index.xml
でも Swift は「Non copyable」型で contraction を許さない affine types を持ってるよ。

借用チェッカーって false negatives はあるけど false positives はないって理解で合ってる？
もしかしたらバカな質問かもしれないけど、複数の実装を並行スレッドで実行して、最初にポジティブな結果を出した方が勝ちってできないのかな？

マジで欲しいのは分離論理ってやつで、それがあれば関数の事前条件を正確に決めたり、途中の条件を証明したりできるんだ。最適化ツールはその”レンマ”を使って、決められた範囲で自由に動けるようになるよ。”Rust”は、この文脈だと”みんなが欲しがる普通の不変条件”と”それを前提にした最適化のセット”って感じだね。

これはチェッカーが組み合わせ可能って前提に立ってるけど、バラバラなチェッカーの実装だとそうじゃないかもね。あるチェッカーでOKでも、別のチェッカーと組み合わせたら結局無効なプログラムになっちゃうリスクがあるかも。まぁ、実際にはそんなことないのかもしれないけどね。

Rustには、Stringとかベクター、ボックスみたいに、収縮させない型もあるんだ。それが、借用チェッカーがメモリ安全を保証するためにめちゃくちゃ大事なんだよ。

モデル変更時にコードを変えなくていいって話かな？でもRustにはRefCellっていう、実行時に借用チェックを遅らせる仕組みがすでにあるって言っとくね。これは可変な借用のエイリアシングを許す排他ルールを変えるわけじゃないけど、コンパイル時じゃなく処理する別の選択肢にはなるよ。

簡単な例で君のコメントを教えてくれない？slice::split_atとslice::split_at_mutを見てみてよ：
fn split_at(&self, mid: usize) -＞ (&[T], &[T])
fn split_at_mut(&mut self, mid: usize) -＞ (&mut [T], &mut [T])
分離論理だと、これのトリプルってどうなるの？

Rustはもう借用チェッカーの実装切り替えをサポートしてるんだ。スコープベースから非語彙的、そして実験的なPoloniusもあるよ。でも、新しいのが使えるようになったら古いのは捨てることになる。だって、新しい方が速くて正しいプログラムをより多く受け入れるんだから。RcとRefCell型を使えば、ランタイムチェックのコストはかかるけど、もっと柔軟になるよ。

それがどう機能するのか想像できないな。違う借用ルールを期待するコードを組み合わせるなんて無理でしょ。借用チェッカーの実装の数だけ、実質的にサブの方言ができちゃうことになるよ。

うん、それは本当だね。
複数の不変な共有参照は収縮の一種だけど、可変参照はアフィンなんだ。SwiftはRustみたいに参照がないし、危険な生ポインタもダングリングさせずに持てない。だからSwiftはRustより制約が強くて、できることが少ないんだよ。

借用チェッカーは誤検知（false positive）はないけど、見逃し（false negative）はあるんだよね？健全な静的解析のはずだよね。Ralf Jungのhttps://news.ycombinator.com/item?id=44511416でのコメントによると、Tree Borrowsの健全性はまだ証明されてないみたい。
複数の実装を並行で走らせて、一番最初にOK出したやつが勝ち！ってできない？まぁ、妥当なサイズのプログラムだとすでに全コア使ってるし、余計な作業が増えるなら並列化してもそんなにメリットないと思うけどね。

借用チェックって関数の中だけで完結するから、モデルが同じで、違うチェッカーを関数ごとに動かすなら、そんなリスクはないよ。

実行時に処理を後回しにするのは、常に良いとは限らないよ。ランタイムオーバーヘッドがかかるし、違反が検知されたらコードがパニックを起こす可能性もあるからね。

うん、なるほどね。Rustの型システムはアフィン論理のような「アフィン」ではないよ。アフィン論理は厳密に禁止している収縮を、Rustは様々な形で許しているからね。Curry-Howard対応が型システムについて何かを証明すると主張する人もいるけど、それは依存型言語にしか当てはまらない。それに、その証明はプログラムの振る舞いに関するものでもないよ。詳細は https://liamoc.net/forest/loc-000S/index.xml を見てみて。

Kotlinみたいな言語にもアフィン型があったらいいのに。コードの整理がもっときれいになると思うな。言語がガベージコレクトされるから、純粋に「構文的」なものでも問題ないよ。何が何を所有しているか明確にして、複数の参照を明示するだけでも素晴らしいね。Kotlinの機能でエフェクトシステムみたいなものもシミュレートできるし。プログラミング言語理論って本当に面白いよね！

「Rustは異なる形式の収縮を許すが、アフィン論理はそれを厳密に禁じる」ってのは間違ってるよ。アフィン論理でも一部の命題には収縮があるし、Curry-Howard対応は依存型言語以外にも存在する。例えば、単純型付きラムダ計算と命題論理の間には美しい対応があるんだ。どうやら理解していない主張を繰り返すのはやめてほしいな。

この質問への長い答えは、https://research.ralfj.de/thesis.html にあるよ :)

Ralfの答えも見てほしいけど、少し補足させて。これらの関数はメモリにアクセスせず、操作的には p, n -＞ (p, p + n) だ。分離論理は検証対象プログラムと外部推論を明確に区別するから、「この式の主型は？」という質問は当てはまらない。Rustで面白いのは関数自体じゃなく & と &mut。これらは多様な文脈の代わりなんだ。分離論理では、あらゆる目的に合う単一の & や &mut はないかもしれない。split_atの最も再利用可能な形は、僕が書いた純粋関数に等しいよ。呼び出し元がプロパティの継承を証明すればよく、フレームルールを知っていれば可能だ。

Rustの借用チェッカーはコンパイル時のコストがかなり最小限で、コード生成には全く影響しないよ。コンパイル時間のほとんどは、トレイト解決、モノモーフィゼーション、LLVMの最適化パス、そしてリンキングに費やされているんだ。

Curry-Howard対応を持ち出したのは、「アフィン論理」に関するSOの投稿を使って「アフィン言語」の定義について議論する理由を説明するためだよ。両方とも「（普遍的な）収縮がない」という同じ方法で定義されている。この主張は明らかに正しいから、あなたがどの主張に反対しているのか、もっと具体的に説明してほしいな。（収縮とアフィン論理に関するもう一つの部分は、他の返信で既に反論されているから、繰り返さないよ。）

アフィン型システムっていうのは、一部のものが収縮を持たないシステムのことだよ。何もかも収縮がないわけじゃないんだ。

「アフィン論理の要点は収縮を許さないことで、Rustの型システムは異なる形の収縮を許す。Rustは一体どうやって『アフィン言語』なの？」という疑問に対して。アフィン論理の要点は、普遍的で制約のない収縮を許さないことで、特定の状況下で収縮と同じ特性を持つ操作が全くできないわけじゃないんだ。Rustの型システムも同じだよ。

Proof checkerのバグが指数関数的に安全性の問題を悪化させる可能性があるって心配してるんだ。分散システムでの単一障害点みたいなもんかなって。

「複数イミュータブル共有参照は収縮」ってのは違うよ。あれはアフィン論理の拡張であって、RustBeltで証明済みなんだから！

「コンパイルで全コア使う」ってのはフルリビルドだけだよね。普段はそんなに使わないし、CPUが並列化進むと、スレッド数のが多くなってくるから、もっと工夫が必要になるはずだよ。

論文のコード例、&mut *ptrを2つ渡すやつ、あれって同じ変数に複数可変参照してるから未定義動作じゃないの？もしかして、俺が論文の主張を誤解してるのかな？

Tree Borrowsの目的は未定義動作の正確な境界を定めることだよ。Rustコンパイラは受け入れるけどルール違反なコードや、Borrow Checkerじゃチェックできないけど合法なコードもあるから、それらを明確にしたいんだ。Stacked Borrowsより範囲が広くて安全性が高いんだって。

「証明可能に安全」って言ってるけど、まだ証明は終わってないんだよね。Borrow Checkerが受け入れるコードが全部TBと互換性あるってのは、今はまだ推測の域を出ないんだ。でも、ちゃんとテストはしてるよ。

「どのルールに違反してるか、正確なUBの定義は？」ってのが重要で、Tree Borrowsはその定義を提案してるんだよ。「こういうコードも書ける」ってのは、Tree Borrowsがないと何が悪いのか説明できないってことなんだ。君は既にTree Borrowsみたいなのが必要だって理解してるみたいだね。

「can」って言葉を誤解してるよ。unsafeコードを使えばあれは書けるし、それが未定義動作なんだ。ほら、このリンク見てみろよ。
https://play.rust-lang.org/?version=stable&mode=debug&editio…

多くの返信があるけど、これ以上増やしたくはないな。でも、意図を一番はっきりさせるのは、次の段落の最初にあるこの部分だと思うよ。＞Rustコンパイラの開発者がエイリアシング最適化を明らかにサポートしたがってるんだから、上の反例みたいなのを考慮から「除外」する何らかの方法が必要なんだ。

それがまさにポイントだと思うね。複数の可変参照を許さないみたいな制約を破るのは簡単すぎるんだ。Unsafeは、Rustのライフタイム解析でコードの妥当性を証明するのが難しいケースのためにあるけど、それ以上のことに悪用されかねないんだ。

ここで言う「できる」は「許されている」って意味じゃないよ。「Unsafeコードは以下のものを表現できるけど、それは未定義動作、UBだよ」ってことだね。

著者のNeven Villaniが、Cédric Villani（2010年のフィールズ賞受賞者）の息子だって今気づいたよ。やっぱり、才能って遺伝するんだね。

これは素晴らしいね。たぶん、自分の言語にこのモデルを実装すると思うよ。

デジャヴじゃないはずだよ。この投稿、2〜3ヶ月に一度は見てる気がするんだけど…。

この論文、何年もかかって作られたものだよ。今回やっと公開されたんだ。

「ツリーボローズ」
「金返せ、この野郎！」
「ふむ、焦るな！」
「48時間以内に引き渡せ、さもなきゃ苗木がどうなるか分からねえぞ、ツリービアード。」