Send と Sync：安全性が乗る述語、そしてその一つの穴

前回の並行処理の設計は、その安全性の物語のすべてを、型システムがどの値についても答えられねば ならない二つの問いに乗せる：別スレッドに move して安全か（その性質を Send と呼ぶ）、そして それへの参照をスレッド間で共有して安全か（Sync）。その二つの述語を正しくすれば、設計が防ぐ ために存在するデータ競合は起こり得ない；間違えれば、保証全体が虚構だ。今回は、それらがどう建てられ たか —— 意図して小さく —— と、その小ささが隠すのを許した微妙な穴についてだ。

trait システムでなく、もう二つの述語

言語全体が回る抑制と整合して、Send と Sync は宣言された instance と solver を持つ trait システム ではない。それらは構造的述語 —— 型を与えられて、その型の形を見て yes か no かを決める関数 —— で、言語がすでに追っていた Trivial と片付けを要する区別の傍らに、四つ目と五つ目として加えられた。 「これは region に住めるか？」に答えるのと同じ機構が、いまや「これはスレッドを越えられるか？」にも 答える。

導出の大半は機械的だ。プリミティブは Send かつ Sync。タプルは、その要素すべてが move して安全なら 安全だ。クロージャとチャネルは move も共有も安全。region 借用 —— region に紐づく参照 —— は決して Send でない。これは小さく荷重を担う規則だ：借用が越えられないから、子スレッドは親のメモリへの参照を 単純に持てず、「各スレッドは自分の region を得る」保証が、別途の追跡を要さず無料でこぼれ落ちる。

構造で足りないところは、作者が型に印をつける。リソースを所有するケイパビリティは move 可能だが単一 所有者なので、Send だが Sync でない。自分自身の内部ロックを持つケイパビリティは共有可能と印づけ られる —— Send も Sync も。生のファイルディスクリプタのような本質的に単一スレッドの何かを持つ ケイパビリティは、どちらでもないと印づけられる。印は現れるところで authoritative；印のないものはその 構造から答えを導く。それはちょうど、メモリモデルの Trivial 規則の形 —— 印づけられた型は宣言により、 印のない型はその中身により —— を、スレッド境界に再利用したものだ。

穴：名前で止まる

その導出に健全性のバグがあり、それは立ち止まる価値がある。構造的な流儀が生む正確な危険だからだ。 述語はタプルを正しく扱った —— タプルは透明で、その全要素をチェックするのは自然だった。だが名前の あるレコードや variant は違う：その名前は一つのもので、その中身 —— フィールド、ペイロード —— は 別の宣言に住む。述語は、印のない名前つき型に出会うと、その型引数をチェックしたが、その実際の中身 まで決して見通さなかった。名前で止まったのだ。

帰結は本物の穴だった。意図して Send でない型 —— 生のディスクリプタを持つ接続、thread-local と印づけ られた —— を取る。それを一行のレコードや variant に包む：単一フィールドがその接続である Box。述語は、 Box が Send かと問われて、Send でない型引数を持たない印のない名前つき型を見て、yes と答えた —— Box を開けて中の Send でない接続を見つけることを決してしなかったから。それは、設計がスレッド境界を 越えることを特に禁じる値を取り、些細なレコードに包み、咎められずに越えて手渡せることを意味する。並行 処理モデル全体が不可能にするために建てられたまさにそのデータ競合が、ラッパー越しに到達可能だった。

穴は単純さの影だ

このバグは実装の偶然ではない；前回なされた選択の特定のリスクだ。trait solver なら、誰かが Box は Send だと宣言することを要し、コンパイラはその宣言を Box の中身に対して検査しただろう —— そこの 穴は、拒否された宣言として自らを告げる。構造的述語は何も宣言しない；それは静かに答えを導く。それは より軽く boilerplate を要さなかった —— そしてそれこそ穴が静かだった理由だ。述語が型の構造を読んで 決めるとき、それが健全なのは、構造のすべてを読むときだけだ。その一部を読むことは、声高に失敗しない； それは自信ありげな、間違った yes を返す。Send と Sync を安価にした抑制は、この特定の誤りを可能に した同じ抑制だ。

修正は設計を保ち、隙間を閉じる。印は authoritative のまま —— 印づけられた型の答えは宣言により、 変わらない。印のないレコードや variant について、述語はいまや型の実際の中身を引き、型パラメータを 置換してコンテナの要素型がそれが実際に持つものに解決されるようにし、その中身へ再帰する —— すでに 訪問中の型を追うガード付きで、だから再帰的な型（自分自身を参照するリストノード）がチェックを無限 ループへ送れない。修正後、包まれた Send でない値は正しく Send でなく、述語は Trivial 規則が常に そうだったのとちょうど同じに振る舞う：上に印、下までずっと構造。

失敗でなく、見ることで見つかった

一つの細部が修正と同じくらい重要だ：穴がどう見つかったか。それは失敗したテストから浮かんだのではない —— thread-local な値をレコードに包んで送ろうとするテストはたまたま無く、通るスイートは不健全な述語の 上で緑を報告し続けただろう、無期限に。それは意図的な監査で見つかった —— 同じ領域の無関係なバグに 促された、Send/Sync 機構の横断的なレビューで。誰かが、噛まれるのを待つのでなく、保証の穴を探しに 行ったのだ。

それが、この種の健全性バグが問題になる前に捕まる唯一の道だ。その署名は沈黙だから：間違った答えは、 特定の敵対的なプログラムが現れるまで、正しい答えとちょうど同じに見える。全売りが検証可能な正しさで ある言語は、自分自身の保証を、仮定するのでなく能動的に攻撃されるべきものとして扱わねばならない —— そして連載が何度も立ち返る正直な姿勢は、その懐疑を自分自身の型検査器に向けることを含む。

値がスレッド境界を越えてよいかを決める述語は、いま健全だ。スレッド間で値を動かすもう半分は、値が いつ手渡されたかを追い、その後の使用を捕まえることだ。それは構造でなくフローの問題で、それ自身の 微妙なケースを持つ。次回：move 追跡。