エイリアスベースの借用チェッカーの定式化 (2018年)

Rustの全社ミーティング以来、私はRustの借用チェッカーの代替定式化を実験してきました。その目標は、現在の提案のいくつかの欠点を克服し、かつ計算速度も速くなるような定式化を見つけることです。私はこの分析のためのプロトタイプを実装しました。それは完全なNLLテストスイートをパスし、現在のNLL分析では扱えないいくつかのケース（例: #47680）も扱えます。しかし、パフォーマンスはまだ改善の余地が大きいです（現在は既存の分析よりも遅いです）。とはいえ、まだ最適化を始めてすらいないので、私がやっていることが非常に単純で非効率的であり、間違いなく改善できることはわかっています。そのため、そこで大きな進歩を遂げられると楽観視しています。 また、昨日、4月26日が借用チェックの6回目の「誕生日」であったことを指摘されました。当時の私のコミットを見るのは面白いです。当時のRustがどのようなものだったかがよくわかります。 エンドユーザーは気にする必要はありません まず最初に述べておくべきことは、この提案はRustのエンドユーザーの視点からは何も違いがないということです。つまり、借用チェッカーはNLL提案の下で動作するであろうものと、多かれ少なかれ同じように動作するはずです。 しかし、この提案には、コンパイラがあなたのプログラムをどのように考えているかという点で、いくつかの微妙な変化があり、それが将来の言語機能に影響を与える可能性があります。 最初の例 この分析はMIR（Mid-level Intermediate Representation）上で動作しますが、ここでは簡単なRustの例で説明します。最初の例を、例Aと呼びます。この例は、ご覧の通りコンパイルされないはずです。 ```rust fn main() { let mut x: i32 = 22; let mut v: Vec<&i32> = vec![]; let r: &mut Vec<&i32> = &mut v; let p: &i32 = &x; // 1. `x` は `p` を作成するためにここで借用されます r.push(p); x += 1; // <-- エラー！借用中に `x` をミューテートできません take(v); } // 3. `x` への参照は後でここで使用されます fn take<T>(p: T) { .. } ``` リージョンはローンの集合です この新しいアプローチにおける最大のシフトは、`&'a i32` のような型を持つ場合、`'a` の意味が変わることです。 NLL RFCで説明されているシステムでは、`'a`（ライフタイムと呼ばれる）は、最終的にはソースプログラムまたは制御フローグラフの一部に対応していました。 この提案では、`'a`（これをリージョンと呼びます）は、ローンの集合、つまり借用式の集合（例Aの `&x` や `&mut v`）に対応します。アイデアは、参照 `r` が型 `&'a i32` を持つ場合、`'a` のローンの条件のいずれかを無効にすると `r` も無効になるということです。 ローンの条件を無効にするとは、ローンによって借用されたパスへの不正なアクセスを実行することです。例えば、`r = &mut v` のようなミュータブルローンがある場合、値 `v` にアクセスできるのは参照 `r` を介してのみです。`v` に直接アクセスする（読み取り、書き込み、移動のいずれであっても）と、ローンが無効になります。`p = &x` のような共有ローンでは、`x`（または `p`）を介した読み取りは許可されますが、`x` の書き込みやミューテーションはローンの条件を無効にします（`p` を介した書き込みも不可能です）。 参照のサブタイピング規則は、リージョンがプログラムポイントではなくローンの集合になったため、少し異なります。ポイントの場合は、ライフタイムを短縮することで参照を近似できますが、ローンの集合の場合は、集合を拡大することで近似できます。言い換えれば： `'a ⊆ 'b` ------------------ `&'a u32 <: &'b u32` Rustの構文では、`'a ⊆ 'b` は `'a: 'b` という表記に対応し、これを記事の残りの部分で使用します。私たちは伝統的にこれをアウトライブ関係と呼んできましたが、リージョンの新しい意味にふさわしく、これをサブセット関係と呼びます。 リージョンをローンの集合として直感的に理解するために、このプログラムを考えてみてください。 ```rust let x = vec![1, 2]; let p: &'a i32 = if random() { &x[0] // Loan L0 } else { &x[1] // Loan L1 }; ``` ここで、リージョン `'a` は集合 `{L0, L1}` に対応します。なぜなら、ローン `L0` によって生成されたデータ、あるいはローン `L1` によって生成されたデータに参照する可能性があるからです。 Datalog この記事全体を通して、Datalogルールを使用して分析を定義していきます。Datalogは、ある意味で、効率的な実行のために設計されたPrologのサブセットです。基本的には次のようなルールに対応します（Souffleプロジェクトの構文を使用）： ```datalog .decl cfg_edge(P:point, Q:point) .input cfg_edge .decl reachable(P:point, Q:point) reachable(P, Q) :- cfg_edge(P, Q). reachable(P, R) :- reachable(P, Q), cfg_edge(Q, R). ``` ここに見られるように、Datalogプログラムは事柄間の関係を定義します。ここでは、それらの関係は `.decl` で宣言されています。一部の関係は `.input` で宣言された入力であり、その値はユーザーによって事前に与えられます（これらは事実とも呼ばれます）。このプログラムでは、それが `cfg_edge` です。`reachable` のような他の関係は、これらの事実から新しいものを合成するルールを介して定義されます。Prologと同様に、大文字の識別子は変数であり、変数が2回現れるときは常に同じ値でなければなりません。 サブセットであるため、DatalogはPrologのより「プログラミング言語的」な特性の多くを回避することに注意してください。例えば、Datalogプログラムは、有限個の事実に対して実行される場合（上記の例のように再帰する場合でも）、常に終了します。また、Datalogプログラムでは否定的な推論を使用しても問題ありません。否定的なサイクルを排除しているため、「論理的否定」と「失敗としての否定」の区別に関する微妙な懸念はありません。 これらのルールを実装するために、私はFrank McSherryの素晴らしい`differential-dataflow`クレートを使用しています。これは非常に良い経験でした。使い方がわかれば、Datalogルールを非常に直接的に翻訳できるため、1〜2時間で新しい設計を迅速にプロトタイプ化できます。さらに、結果の実行は非常に高速です（最新の設計ではパフォーマンスをあまり測定していませんが）。 リージョン変数 リージョンをローンの集合として説明しましたが、今はそれをすべて忘れてください。私が定義した分析は、少なくとも最初は、これらの集合を直接操作しません。代わりに、「リージョン変数」を使用して、プログラム内のすべてのリージョンを表します。これらを `'0`, `'1` のような「番号付き」リージョンとして示します。 私たちのプログラムをこれらの抽象リージョン（基本的に、MIRが持つであろうすべての場所に番号付きリージョンを持つ）を使用して書き直すと、次のようになります。 ```rust fn main() { let mut x: i32 = 22; let mut v: Vec<&'0 i32> = vec![]; let r: &'1 mut Vec<&'2 i32> = &'3 mut v; let p: &'5 i32 = &'4 x; r.push(p); x += 1; take::<Vec<&'6 i32>>(v); } fn take<T>(p: T) { .. } ``` これらの抽象リージョンは、Datalogルール全体に現れます。ここでは「リージョン」を表す `R` で示します。 リージョン間の関係 前述の抽象リージョンは、まだ意味を持ちません。次に、型システムのルールを標準的な方法で歩き回って適用します。これにより、前述の「サブセット」関係がリージョン間に生じます。例えば、例Aの次の行を考えてみましょう。 `let p: &'5 i32 = &'4 x;` ここで、式 `&'4 x` は型 `&'4 i32` の値を生成します。この型は `p` の型 `&'5 i32` のサブタイプでなければならないため、次のようになります。 `&'4 i32 <: &'5 i32` これはさらに `'4: '5` を要求します。プログラムを見ると、多くのサブタイプ関係が現れることがわかります。それぞれを結果のサブセット関係とともに書き留めます。 ```rust fn main() { let mut x: i32 = 22; let mut v: Vec<&'0 i32> = vec![]; let r: &'1 mut Vec<&'2 i32> = &'3 mut v; // 要求: &'3 mut Vec<&'0 i32> <: &'1 mut Vec<&'2 i32> // => '3: '1, '0: '2, '2: '0 let p: &'5 i32 = &'4 x; // 要求: &'4 i32 <: &'5 i32 // => '4: '5 r.push(p); // 要求: &'5 i32 <: &'2 i32 // => '5: '2 x += 1; take::<Vec<&'6 i32>>(v); // 要求: Vec<&'0 i32> <: Vec<&'6 i32> // => '0: '6 } fn take<T>(p: T) { .. } ``` 最終的に、これらのサブセット関係はシステムへの入力事実となります。後で明らかになる理由から、これらを「ベースサブセット」関係と呼びます。 `.decl base_subset(R1:region, R2:region, P:point)` `.input base_subset` 言い換えれば、`base_subset(R1, R2, P)` は、ポイント `P` で `R1: R2` が真である必要があることを意味します。 このベースサブセットがすぐに...