型システムが許したレース

このプロジェクトが自分に課す規則は、実測された soundness の穴は他のどんな仕事より優先する、だ。 だからサーバの回の負債は、新機能のどれよりも先に満期を迎えた: 型システムは可変 Map の thread 間 共有を許し、Map はレースした。設計が問われたのではない。言語の並行性の規律は、捕獲される全ての値を Sync（共有せよ）、Send（move せよ）、どちらでもない（捕獲を拒否せよ）に分類し、region に束ねられた 可変コンテナは常に thread-local であるつもりだった —— 文書はその言葉どおりに書いていた。分類器が その意図を実装していなかっただけだ。汎用規則はコンストラクタを型引数で判定する。コンテナの第一引数は region marker で、region marker は未解決の型変数で、規則は未解決を安全とみなした。よりにもよって 最悪の場所での楽観 —— runtime がその場で書き換えられるロックなし配列である、まさにその種の値で。

何も変えなかった修正

修理は三行に見えた: Map、Vec、string builder は、汎用規則が引数を見る前に、明示的に Send でも Sync でもない。owned-vector 型は move の意味論を保つ —— drop 型であり、構成からして単一所有者で、 move によって thread を越えることこそがその存在理由だ。channel は Send かつ Sync のまま。祝福された パターンだからだ。気持ちいいはずの瞬間は、サーバの naive な初稿を再コンパイルして、失敗する様を 眺めることだった。通ってしまった。分類器は正しく、move 検査器も正しく、それでもプログラムはビルド された —— つまり問題はもう、解析が何を結論するかではなく、誰かが解析に尋ねているかだった。

一度も走っていなかった検査

答えは、インフラのバグだけが持つ種類の気まずさだった。interpreter のパイプラインは全列を走らせて いた: 型推論、次に channel 要素の Send 義務、借用衝突の検査、spawn 捕獲の move 解析。コンパイルの 入口 —— C・LLVM・WebAssembly の三 backend が共有する —— は、型推論をしてそのままコード生成へ進んで いた。言語が並行性と region のために建てた安全解析の全てが、バイナリを作るときには単に飛ばされて いた。region の借用を spawn した thread に捕獲させるプログラムは、mere run には拒否され、 mere -c には無言でビルドされる —— そして両方の経路が存在して以来ずっとそうだった。修正は、どの backend がプログラムを見るより前に、コンパイル経路にも同じ三つの解析を走らせること。これでようやく naive なサーバ初稿はコンパイルに失敗した。最初からそうあるべきだったエラーと共に: Map は thread 境界を越えて捕獲できない、それは Send でも Sync でもない。

証明としてのサーバ

この回を正しく閉じる細部が二つある。第一に、actor model のサーバ —— 三話前の回避策 —— は、厳しく なった規則の下で無変更のままコンパイルされる。channel は Send で、store は thread を越えないからだ: あの回避策は、最初からずっと、いま型が強制する設計そのものだった。それはテストスイートに、祝福された パターンが生き残ることの生きた証明として座っている。第二に、正直な非対称性: この穴を見つけたのは 監査ではなく、レースした一本のプログラムだった。dogfood 法が意図どおりに機能した、ということであり —— 同時に、建てたものしか見つけられないという戒めでもある。soundness の主張は全プログラムについての 主張で、dogfood が検査するのは常にもう一本だけだ。型システムが正しい場所で「否」と言うようになった いま、残る負債は最大のそれ —— 決して返ってこないメモリ —— であり、次の二話がそれを払う。