A data race that doesn't compile (in Rust)
Rustの型システムを活用してデータ競合をコンパイル時に検出する技法について解説。型レベルの排他性(disjointness)を用いることで、実行時エラーではなくコンパイルエラーとしてデータ競合を捕捉できる仕組みを、具体的なコード例とともに紹介する。Rustの所有権と借用のモデルを拡張する発想が、安全な並行プログラミングにどのように貢献するかを示す記事。
背景メモ
- Rustはメモリ安全性をコンパイル時に保証する言語だが、その型システムをすり抜ける「データ競合」が理論上は可能だと、この記事の著者がデモンストレーションしている。
- カギとなるのは「型レベルで素集合(disjointness)を表現する」という高度な技法。通常のRustではmut参照と共有参照の排他ルールで競合を防ぐが、内部可変性(Cell/RefCell)や raw pointer を組み合わせると、型検査をパスしつつ複数の場所から同じメモリに書き込める経路が作れる。
- 著者は型レベル集合(type-level set)と幽霊型(phantom type)を使って、Rustの借用チェッカーには見えない「別々の変数だが実際には同じメモリ領域」という状況を構築。このテクニックは「Type-Level Disjointness」と呼ばれ、理論的にはunsafeコードなしでもデータ競合を引き起こせることを示す。
- これはRustの安全性に関する「既知の抜け穴」として学術的・コミュニティ的に認識されている話題で、実際のプロダクトコードで使われるものではなく、型システムの限界を探る探求。ZigやC言語との対比でよく引き合いに出される。