Refinement Proofs in Rust Using Ghost Locks

あなたは、巨大で高速なデジタル都市を建設していると想像してください。手元には、交通信号や郵便配達、電力網が理論上どのように機能すべきかを示す、美しい完璧な設計図（抽象モデル）がナプキンに描かれています。一方で、目の前には、実際の作業員、錆びたパイプ、渋滞が存在する、混沌とした実際の建設現場（具体的な実装）があります。

ここでの大きな問題は、コンピュータサイエンスにおける問いです。「どうすれば、現実の混沌とした建設作業が、あの完璧なナプキンの設計図通りに進んでいることを、建設速度を落としたり、作業員に終わりのない書類作成を強いたりすることなく証明できるのか？」ということです。

長い間、これを行うためのツールには、2つの極端な選択肢がありました。選択肢Aは、設計図に基づいて都市を代わりに建設してくれるロボットです。それは完璧ですが、建物は無骨で遅く、不適切な材料を使用しています。選択肢肢Bは、実在の都市のレンガ一つひとつを検査する検査官チームです。彼らは徹底していますが、都市を非常に特定の、硬直した方法で建設することを要求し、彼ら独自の古臭い道具を使わない限り機能しません。

主要な発見：「ゴーストロック」のトリック
この論文の著者たちは、Rustプログラミング言語を用いて、この隔たりを埋める新しい方法を考案しました。彼らはこれを**「ゴーストロックを用いたRustにおけるリファインメント証明（Refinement Proofs in Rust Using Ghost Locks）」**と呼んでいます。

ゴーストロックを、魔法の、目に見えない鍵だと考えてください。

• 設計図（モデル）： チームは、コードの中に都市のルールの「ゴースト（幽霊）」バージョンを作成します。このゴースト都市は、（例えば「郵便箱に何通の手紙があるか？」といった）完璧な状態を追跡します。
• 現実の都市（コード）： 実際のプログラムは高速に動作し、現代的で効率的なテクニックを使用します。
• 鍵： 作業員（コンピュータのスレッド）が何かを変更する必要があるとき、彼らはまずゴーストロックを手に取らなければなりません。
  • ロックを保持している間、彼らはゴースト都市を覗き見て、現在の状態を確認できます。
  • 彼らは自分の仕事を行います。
  • 仕事が終わったら、ロックを元の場所に戻します。しかし、ここに魔法があります。彼らはロックに対して、自分が何をしたかを正確にささやかなければなりません（例：「手紙を1通送った」あるいは「手紙を1通ゴミ箱に捨てた」）。
  • ロックはチェックします。「今行ったことは、ゴースト都市のルールと一致しているか？」もし一致していれば、成功です。もし一致していなければ、証明は失敗します。

このロックは「ゴースト（幽霊）」であるため、プログラムが実際に実行されるときには消滅します。これは動作を遅らせることはありません。それは、ルールに従っていることを確認するためにあなたの想像の中にだけ存在するセキュリティガードのようなもので、あなたが建物を出る瞬間に消えてしまうのです。

彼らが「ノー」と言うもの
著者たちは、自分たちの手法が何では「ない」のかを明確にしています。

• ロボットによる建設者ではない： 彼らは、設計図からコードを自動生成するという考えを明確に拒絶しています。彼らは、既存の、人間が書いた高速なコードが正しいことを証明したいのであって、それを遅い自動生成コードに置き換えることが目的ではありません。
• 硬直した構造ではない： 彼らは、数学を容易にするためにプログラマにコードを特定の硬直した形に書かせるような手法に反対しています。彼らの手法は、マルチスレッド・プログラムのように多くのことが同時に起こる、乱雑で複雑な現実世界のコード構造でも機能します。
• 「おそらく」の安全性ではない： 彼らは、自分たちの手法が機能することを単に示唆しているのではなく、証明しました。単にシミュレーションを実行したのではなく、論理をステップバイステップでチェックし、現実のコードが必ず設計図に従うことを確認するために、フォーマル・ベリファイア（超知能な数学ロボット）を使用しました。

「ライブネス（生存性）」のパズル
安全性（Safety）は簡単です。「列車は衝突したか？」（いいえ、ならOK）という問いです。
しかし、**ライブネス（Liveness）**はどうでしょうか？ これは、「列車はいつか到着するか？」という問いです。
著者たちもこれを解決しました。彼らは特殊な論理（LTLと呼ばれます）を使用して、システムが単に衝突を回避するだけでなく、実際に前進し続けることを証明しました。彼らは「進捗」を一種の「負債」として扱いました。ノード（作業員）がメッセージを送ると約束した場合、彼らは最終的にその約束を「返済」しなければなりません。もし支払わずに遅延し続ければ、証明システムが彼らを捕らえます。

証明：実世界でのテスト
これが単なる面白い理論ではないことを示すために、彼らは3つの実在のものを構築し、検証しました。

1. Memcached： 有名なインターネット・キャッシング・システムの簡略版です。ネットワークエラーやメッセージの紛失が発生しても、システムが整合性を保つことを証明しました。彼らは3つのバージョンを作成しました。最初はシンプルなもの、次は多くのスレッドを持つもの、最後は非常に細かい粒度のロッキング（例えば、図書館の棚ごとに個別のロックを持つようなもの）を備えたものです。モデルは同じままですが、コードはより複雑になり、それでも証明は維持されました。
2. プロデューサー／コンシューマー・キュー： 一人がアイテムを列に入れ、もう一人がそれを取り出すシステムです。通常はクラッシュの原因となるリスクの高い低レベルなメモリ操作（unsafe code）を使用している場合でも、それが「検証済みセル（Verified Cell）」によってゴーストロックによってチェックされることで、正しく動作することを証明しました。
3. Paxosとハッシュセット： 彼らはまた、複雑な合意アルゴリズム（Paxos）とロックフリーのハッシュセットを検証し、その手法が異なる分散システムにおいても機能することを示しました。

数値
彼らは、Intel Core i9-10885H 2.40GHz CPU および 16 GiB RAM を搭載したコンピュータでテストを実行しました。

• Memcached システムにおいて、検証には約 334.7秒（最初のバージョン）から 379.7秒（最も複雑なバージョン）かかりました。
• モデルと証明のために書かれたコードは、トリッキーな「ライブネス（進捗）」の証明を含めても、総実行時間に加えた時間は約 10% であり、注釈の労力も同様でした。
• Memcached のモデル定義の総行数は約 225行 で、仕様／ゴーストコードは約 286行 でした。

結論
この論文は、高レベルで抽象的な計画から、Rustで書かれた複雑で効率的な現実世界のプログラムが、それを完璧に遵守していることを証明できることを示しています。彼らは、コードを遅くしたり硬直させたりすることなくこれを行いました。彼らは「ゴーストロック」を用いることで、プログラムがルールを覗き見、仕事を遂行し、ルールに従ったことを証明できるようにしました。そして、最終的な製品からはゴーストのガードマンが消え去るのです。これは、「高速で柔軟なコード」と「数学的に証明された安全性と進捗」の両方を手に入れる方法です。