借用チェックを逆から考える新しい視点
Valen の借用チェッカーは安全性パスを関数の最後の文から最初へと逆方向に実行する。Evan Ovadia が、逆順にたどることでループとミューテーションの追跡がなぜ簡単になるのかを説明する。
日本語
コピー
時間をさかのぼって、未来を最初から知っておく
奇妙なアイデアを思いついて、それがうまくいったのに、どうしても信じられない。そんな経験はないだろうか。
今の私は Valen の借用チェッカーにまさにそう感じている。
なぜならこれは時間をさかのぼるからだ。
もっと大げさに言わずに言えば、関数を逆向きに歩く。それでも十分に_奇妙_ではある。
何年も前なら、関数を逆順に反復するのが良いことだと言われたら、頭がおかしいと返しただろう。
実際のところ、そうするにはちゃんとした理由があり、たとえば最適化パスを書くときにはごく普通のことだ。1 ただし、メモリ安全性の検査のためにこれをやった人はいないと思う。
借用チェックの世界をとことん深く覗いてみたいなら、このまま読み進めてほしい。
これから奇妙なものを見ることになる。2
これは借用チェックアルゴリズムのかなり深い内部の話だ。代わりに壮大で面白い読み物が欲しいなら、最近書いたThe Golden Spike, and Resurrecting the Vale(n) Programming Languageの記事をどうぞ。
奇妙な種類の借用チェッカー
よくある shared-xor-mutable の borrow checking ではない。
これはValenの借用チェッカーで、shared-xor-mutable を任意にするものであり、境界をまたいだメモリ安全性を保ったままRust の関数を呼び出せる。
Valen はまだ非常に実験的だ。多くの箇所に穴や尖った角があり、おそらく 2 月のどこかで v0.1 が出るまではそうだろう。数か月に及ぶ大規模なリファクタリングはすでに始まっている(この新しい借用チェッカーもその一環だ)。Valen リポジトリを覗いてみるのは自由だが、竜が出るので覚悟しておいてほしい。3
Rust の借用チェッカーに似ているが、メモリ安全な mutable aliasing も備えている。詳しく知りたければこの記事を読んでほしい。とはいえ、この記事の大半を理解するのにその知識は要らない。
……そして奇妙な、逆向きの実装!
Valen は関数を 4 つのフェーズでコンパイルする。4
- 関数をパースし、ソーステキストを AST に変換する。
- 静的型付けを行い、すべての変数、引数、式の型を決める。
- 静的グルーピングを行い、すべての参照がどの変数(あるいは変数のどの_部分_)を指しているかを把握する。5
- 関数を安全性検査し、参照が無効化された後に使われていないことを確かめる。
詳しくは以下で説明する。
一番奇妙なのは、第 4 フェーズが逆向きに進むことだ。 関数の最後の文から始めて、関数の先頭にたどり着くまで逆方向に歩いていく。
これが奇妙なのは、私の知る限り、安全性の検査を逆向きに進める唯一の借用チェッカーだからだ。6
なぜ逆向きに進むのかは後ほど説明する(ヒント:利便性、ループ、速度)。
まずはどう動くのか、そして逆向きに進むとはそもそも_どういうことか_を見ていこう。
フェーズ 1 は飛ばして、フェーズ 2 から始める。
フェーズ 2:静的型付け
静的型付けのパスは、人によってはおなじみだろう。変数に型を割り当てる。
たとえば、次のプログラムを:
exported func main() {
let fuel = 5;
let force = fuel;
}
こうする:
exported func main() {
let fuel i64 = 5;
let force i64 = fuel;
}
ごく普通のことで、多くのコンパイラがやっている。
コンパイラは通常、これを前向きのパスとして実行する。関数の先頭から末尾へ歩きながら、その場で型を決めていく。
フェーズ 3 では、_似ているがもっと奇妙な_ことをする。フェーズ 3 がやるのは静的グルーピングだ。
フェーズ 3:静的グルーピング
これも前向きのパスで、各参照がどこを指しているかを見つける。7
たとえば、次のプログラムでは:
func print_first_fuel_cell(s &Ship) {
let first_ref = &s.fuel_cells[0];
print_int(first_ref);
}
静的グルーピングは、first_ref が s.fuel_cells[] を指していることを突き止める:8
func print_first_fuel_cell(s &Ship) {
// Static typing says: first_ref &int
// Static grouping says: first_ref &int in s.fuel_cells[]
let first_ref = &s.fuel_cells[0];
print_int(first_ref);
}
つまり、s.fuel_cells[] 配列のどこかにある int を指している。
この情報は今や_変数の型の一部_になっている。
この情報は次のフェーズで使う。次のフェーズが、実際に use-after-free を検査する。
フェーズ 4:安全性検査
この記事は半分は遊びだが、同時にアルゴリズムへのフィードバックを求めてもいる。 誰もこんなやり方をしたことがないと思うし、それには相応の理由があるのかもしれない。このアプローチに問題を見つけたら、コメントを残して助けてほしい。修正する(あるいは捨てる!)ために。9
さて、フェーズ 3 が計算したすべてを使える。
use-after-free を検査するフェーズだ。
予告したとおり、逆向きのスキャンで行う。
もう少し大きな例で見てみよう:
struct Entity { hp int; buffs []int; }
func add_buff(self &Entity mut) { ... }
func foo(e &Entity mut) {
let buff = &e.buffs[0];
e.add_buff();
print_int(buff);
}
このプログラムはuse after freeを起こしている。コンパイラに指摘させたい。
まず、より明示的な構文に脱糖する:
struct Entity { hp int; buffs []int; }
func add_buff<g'>(self &Entity in g) mut(g) { ... }
func foo<g'>(e &Entity in g) mut(g) {
let buff = &e.buffs[0];
e.add_buff();
print_int(buff);
}
ここでコメントをいくつか加える。どれも後方走査の結果として付けられるものだ。
「DECLARE」「USE」「MUTATE」が何を意味するかは後述する。
struct Entity { hp int; buffs []int; }
func add_buff<g'>(self &Entity in g) mut(g) { ... }
func foo<g'>(
e &Entity in g // DECLARE e (group g)
) mut(g) {
let buff = &e.buffs[0]; // DECLARE buff (group g.buffs[])
e.add_buff(); // USE e (group g)
// MUTATE group g
print_int(buff); // USE buff (group g.buffs[])
}
アルゴリズムは関数の末尾から先頭へ、逆方向に歩く。
上へ向かって走査しながら、次のイベントを探す:
- 変数を USE したら、pending リストに追加する。
- 何かを MUTATE したら、pending 内の変数が無効化されないことを確認する。
- 変数を DECLARE したら、pending リストから削除する。
pending には、下で USE されたもののうち、上で DECLARE されるはずのものがすべて入っている。
pending に入っているものへの MUTATE は、見つからないことを願う。
一番しっくりくる捉え方はこうだ。pending には、関数の下の方、つまり後で使われる予定の変数がすべて入っており、それまでは有効であり続けるべきだ。
理解を深めるため、実際の動きを見てみよう。
まず、最後の行を見る:
print_int(buff); // USE buff (group g.buffs[])
これは USE なので、pending リストに追加する。pending はこうなる:
- buff(group g.buffs[])
さらに逆方向に進み、その上の行に出くわす:
e.add_buff(); // USE e (group g)
// MUTATE group g
MUTATE があるので、pending 内の変数が無効化されないことを確認する。
具体的には、pending 内の何かが e の配下を指していないことを確かめる。
- buff(group g.buffs[])... 一致した! コンパイルエラーを出す。
何が起きたかというと、buff は g.buffs[] を指しており、その先頭は add_buff で今まさに MUTATE した g だ。つまり buff は使われる行より上で無効化されている。これが use-after-free だ。
そこでコンパイラはここでエラーを出す。やった!
もう一つの例
今度は正しいプログラムを見て、後方走査が宣言に出くわす様子を確かめよう。
同じプログラムだが、e.add_buff(); を上に移して関数の最初の行にしてある。
struct Entity { hp int; buffs []int; }
func add_buff<g'>(self &Entity in g) mut(g) { ... }
func foo<g'>(
e &Entity in g // DECLARE e (group g)
) mut(g) {
e.add_buff(); // USE e (group g)
// MUTATE group g
let buff = &e.buffs[0]; // DECLARE buff (group g.buffs[])
print_int(buff); // USE buff (group g.buffs[])
}
前と同じく末尾から始めて、この行にたどり着く:
print_int(buff); // USE buff (group g.buffs[])
…USE なので、buff を pending リストに追加する:
- buff(グループ g.buffs[])
では 1 行上に戻って、この行を見る:
let buff = &e.buffs[0]; // DECLARE buff (group g.buffs[])
ここで buff を DECLARE しているので、pending から削除する。
pending は空になる。
(つまり、この関数の後ろでは使われない変数しか残っていないということになる。)
さらに 1 行上に戻って、この行を見る:
e.add_buff(); // USE e (group g)
// MUTATE group g
MUTATE があるので、pending 内の変数が無効化されないことを確認する。
pending には変数がないので、何も起きない。
次に e を USE しているので、pending に追加する:
- e(グループ g)
これで関数は終わり。
最後まで進んでも、pending 内の変数を MUTATE する箇所はなかった。つまりこのプログラムはメモリ安全だ。
なぜ逆方向に進むのか
理由は 3 つある。便利さ、ループ、そして速さだ。
一般に、逆方向に進むとあるものが最後に使われるのはいつかを突き止めるのが楽になる。
たとえば、次の関数を見てみよう:
func attack(a &Entity in g, d &Entity in g) mut(g) {
let a_power = a.calculate_attack_power();
let a_energy_cost = a.calculate_attack_cost(d);
let d_armor = d.calculate_defense();
let d_energy_cost = d.calculate_defend_cost(a);
a.use_energy(a_energy_cost);
d.use_energy(d_energy_cost);
d.damage(a_power - d_armor);
}
a が宣言されたときに_処理 X_を行い、a が不要になったときに_処理 Y_を行いたいとする。10 方法は 2 つある:
- 前方向に走査する。a の宣言に出会ったら X を行う。そのまま進み、a の使用箇所を記録していく。関数の終端に達したら、記録した最後の位置まで移動してY を行う。
- 後ろ方向に走査する。a の最後の使用箇所に出会ったら Y を行う。そのまま進み、a の宣言を探す。見つかったら X を行う。
前方向の走査では、最後の使用箇所に出会った時点ではそれが最後だと分からないため、余分な移動が必要になる点に注目してほしい。
後ろ方向の走査のほうが単純だ。
逆方向の走査がデストラクタの挿入に役立つ別の例は、2024 年の私の LLVM talk で見られる。コンパイラに携わる人の多くが言うように、逆方向の走査はさまざまな場面で役立つ。
逆方向に進むことはループにも有利だ。
ループを考えるときに私が使ってきた例をいくつか挙げる:11
これは正しいプログラムだが、あの observe(e) が妥当かどうかを判断するのがいかに難しいかを示している。
exported func main() {
let arr = ArrayList<int>(3);
let e = &arr[0];
while ... {
observe(e); // Valid `e` use.
add_element(&arr);
set e = &arr[0];
}
}
この e は実際には 2 か所から来る可能性がある:
- ループの前の e = &arr[0];。
- ループの末尾の set e = &arr[0];。
前方向の走査で observe(e) に出会ったとき、それが有効だと結論づけるには set e まで先読みする必要がある。
これは set e がない類似の例だ。
exported func main() {
let arr: ArrayList<int> = ...;
let e = &arr[0];
while ... {
observe(e); // Invalid `e` use.
add_element(&arr);
}
}
set e がなければ、ループ内の e はループの_前のイテレーション_によって無効化される。
前方向の走査をするなら、e を復活させる set e が存在しないことを確かめるために先読みが要る。
厄介な問題だ。方法はいくつかある:
- それらの set を求めて先をスキャンする(そして後ろにジャンプする)。
- 前方パスを繰り返し、そのたびに情報を増やして、収束するまで続ける(「データフロー不動点」)。
- 前方パスで情報を集めておき、チェックは後回しにする。
最後の方法は魅力的だった。だが、そのデータ構造は結局ひどく複雑になり、上記の func 攻撃の例で見たのと同じ「フェッチ/ナビゲート」問題を抱えていた。
V2 の逆走査アプローチにそのまま進むほうが簡単だった。
V2 のアプローチのほうが速いことも、ほぼ確実だと思う。フェーズ 3 の前方パスで各ノードを一度、フェーズ 4 の後方パスでもう一度処理するだけで済むからだ。12
ベンチマークは取っていないので、話半分に聞いてほしい。13
もちろん、逆走査アプローチがループを無償で扱えるわけではない。まだ調整が必要だ。
ループを伴う逆走査
ループを扱うには、アルゴリズムにもう少し追加が要る。14
具体的には、MUTATE と DECLARE を別のやり方で処理し、LOOP START にも反応する。
上方向にスキャンしながら、これらのイベントを探す:
- 変数を USE したら、pending リストに追加する。
- 何かを MUTATE したら:
- pending 内の変数が無効化されないことを確認する。
- その変更を、所属するループの mutations_after_this リストに追加する。
- 変数を DECLARE したら:
- pending リストから削除する。
- mutations_after_this 内の何かによって無効化されていなければ、所属するループの revived_after_this リストに追加する。
- LOOP START に到達したら:
- pending 内の各項目について、ループの mutations_after_this 内の何かによって無効化されるなら、同じくループの revived_after_this にも含まれることを確認する。15
この例で何が起きるか見てみよう。これは正しいプログラムなので、コンパイルエラーは出ないはずだ。
exported func main() {
let arr: ArrayList<int> = ...; // DECLARE arr (group arr)
let e = &arr[0]; // DECLARE e (group arr[])
while ... { // LOOP START
observe(e); // USE e (group arr[])
add_element(&arr); // MUTATE arr (group arr)
set e = &arr[0]; // DECLARE e (group arr[])
}
}
後ろから歩いていくので、最後の行から始める。
set e = &arr[0]; // DECLARE e (group arr[])
これは DECLARE 16 なので、2 つのことをする。
- pending リストから取り除く。リストに入っていないので、何も起きない。
- それを含む mutations_after_this の中の何かによって無効化されていなければ(空なので無効化されていない)、revived_after_this に追加する。
revived_after_this にはエントリが 1 つ入った。e だ。
1 行上に戻ると、こうなっている。
add_element(&arr); // MUTATE arr (group arr)
これは MUTATE なので、2 つのことをする。
- pending 内の変数が無効化されないことを確認する。pending は空なので、何も起きない。
- そのミューテーションを、それを含むループの mutations_after_this リストに追加する。
mutations_after_this にはエントリが 1 つ入った。arr だ。
1 行上に戻ると、こうなっている。
observe(e); // USE e (group arr[])
これは USE なので、pending リストに追加する。
pending にはエントリが 1 つ入った。e(グループ arr[])だ。
1 行上に戻ると、ループの開始地点がある。
while ... { // LOOP START
ここで LOOP START のチェックを行う。pending の各項目について、ループの mutations_after_this の中の何かによって無効化されているなら、その項目がループの revived_after_this に入っていることを確認する。
この場合、pending には e(グループ arr[])がある。e は mutations_after_this の中の何かによって_確かに_無効化されている。そこで、ループの revived_after_this に入っているか確認する(入っている)。チェックは通った、問題なし。
上の 2 つの DECLARE については、前回説明したので省略する。
そして関数の先頭に到達した!エラーは一度も出なかったので、借用チェッカーはこの関数はメモリ安全であると結論できる。
以上だ。この新しい逆方向借用チェッカーでループをどう扱うかは、こういう仕組みになっている。
Rust の借用チェッカーにもっと近づける?
最終的に変えたい大きな点がもう 1 つある。
Rust には、関数の_どこからでも_事実を使って参照のライフタイムを推論できる、とても便利な機能がある。
たとえばこの Rust プログラムは、後ろの方にある r = &b[0]; を見て、r が a または b を指していると判断する。
fn main() {
let a = vec![1, 2, 3];
let b = vec![4, 5, 6];
let mut r = &a[0];
if some_condition() {
r = &b[0];
}
println!("{}", r);
}
Valen はまだこれをやっていない。Valen のフェーズ 3(静的グルーピング)は、まだ通常の一方向の推論を行っている。
ただ、rustc と同じようにフェーズ 3 を完全な求解に変えれば、似たような超能力が手に入る。
面白いのは、そのためにフェーズ 4 の後方パスを変える必要がないことだ。最終的にはフェーズ 3 用のソルバと、フェーズ 4 用の後方パスが揃う。
これがどれほど凄いことか、うまく説明できない。こういう瞬間に、自分はコンパイラオタクなのかもしれないと思う。やった!
今回はここまで
Valen の借用チェッカーはまだまだ若く、たった 3,600 行しかない。
しかも全然完成していない!制御フローの中断(break、continue)17、関連グループ、クロージャ18、その他もろもろ、まだまだ追加すべきものが山ほどある。
いつかそこに到達する。その日は輝かしいものになるだろう。
読んでくれてありがとう!
次の数記事では、参照カウントと世代参照をどう組み込んでいくかをもう少し詳しく説明したい。それから、同じように新しいメモリ安全性のアプローチを模索している他の言語についても書くつもりだ(Ante、Carbon、Zeta、Fang、exclusion typingなどなど!)。
これは氷山の一角にすぎない。続きを知りたい人は、RSS フィード、r/valen、Valen discordの購読・参加を。それから Bluesky と Mastodon もフォローしてほしい!
では。
- Evan Ovadia
Footnotes
-
この記事は 0% AI が書いたものだ。詳しい考えはこちら。私の立場:誰かに時間をかけて読んでもらいたいなら、自分も時間をかけて手で書くべきだ。読んでくれてありがとう =) ↩
-
具体的には緑のドラゴン。 ↩
-
秘密の第 5 フェーズもあり、そこではどの操作がどのグループを変更しうるかを記述するために LLVM に送る属性を計算する。ただしこの記事の範囲外だ。 ↩
-
どの命令の mut エフェクトによって無効化されるグループもすべて洗い出す。 ↩
-
例えば:
- Rust(NLL と現在の Polonius)はリージョン推論のために制約求解を行い、その後前方パスで競合をチェックする。(rustc は各変数がどこで使われるかを調べるために後方スキャンも行うが、実際のメモリ安全性チェックは前方パスで行われる。)
- Vale の型付けパスはリージョンを決定し、その後の前方パスがリージョン借用チェックを行って、実行時の世代チェックを安全に省略できるタイミングを判断する。(Vale のリージョン借用チェッカーは実際にはインスタンシエータ/モノモーファイザと融合していた。)
- Valen の以前の借用チェッカーも Vale と同じ方式だった。型付けパスがグループを決定し、その後の前方パスが各使用箇所で、そのグループが「無効化」された時点より後に宣言されているかをチェックしていた。
- 他にも借用チェッカーはたくさんあるが、安全性チェックを逆方向に行うものは聞いたことがない。知っている人がいたら教えてほしい!
-
「group」という用語は近いうちにやめて「path」に切り替えるつもりだ。意見募集中。 ↩
-
V1 の静的グループ化フェーズでは、参照が いつ 行われたかも把握していた。たとえば s.fuel_cells[] にある &int というだけでなく、それが 7.2 行目時点の s.fuel_cells[] にある &int だと分かっていた。これはかなり凄かった。変数の型に時間と空間の情報を密輸していたのだから。新しい V2 では後方スキャンを行うため、その必要がない。次の節で見る。 ↩
-
最初に壊した人には賞品を贈る! ↩
-
この帳簿処理は、参照カウントのデクリメントであったり、デストラクタ呼び出しの追加であったり、use-after-free のチェックであったりする。 ↩
-
注:これらの例では ArrayList という名前を使っているが、実際の Valen コンパイラでは奇妙な歴史的経緯から Array と呼ばれている。近いうちに変わる予定だ。 ↩
-
注:これはまだアルゴリズムが O(n)だという意味ではない。MUTATE は依然として保留リスト内のすべてをチェックする必要がある。ただ、そのチェックを大幅に高速化する方法があると思う。うまくいってほしい! ↩
-
V1 には完全なループサポートがなかったので、比較対象となるベンチマークが実質存在しない。 ↩
-
イースターエッグ注:スタビー軍曹は第一次世界大戦で第 102 歩兵連隊のスターであり、部隊とともにフランスへ渡りフランス軍と共に戦った。18 か月間従軍し、西部戦線で 17 の戦闘と 4 つの攻勢に参加。金メダル、負傷章、2 つのパープルハートを含む多くの賞を受賞した。スタビー軍曹は大戦で最も多くの勲章を受けた戦犬、また戦闘を通じて軍曹への推薦と昇進を果たした唯一の犬と呼ばれている。(出典:Wikipedia) この注を見つけたら、コメントに「gold」という単語をこっそり入れてほしい!(最初に見つけたtimpi4everとgavinmorrowに敬意を!) ↩
-
ここでは保留リストから何も削除しない。これらの保留中の使用は、ループより上のコードによって依然として満たされる必要があるからだ。 ↩
-
そう、DECLARE と名付けたことを後悔している。実際には既存の変数の参照先を変えているだけだからだ。 ↩
-
現状の計画では、まず借用チェッカーが型付き AST ではなく制御フローグラフを見るようにリファクタリングする。そうすれば制御フローの中断はずっと楽になるはずだ。 ↩
-
クロージャにはかなり期待している。動かすための_とても_エレガントな方法を見つけたと思う。続報を待たれたい。 ↩