Turso のハードニング: Formal Methods と Quint を用いた SQLite バグの発見

データベースを構築するすべてのチームにとって、SQLite は信頼性の金字塔です。Turso は SQLite のリライトであるため、同じレベルの信頼性を維持することは単なる目標ではなく、必須事項です。これを実現するために、Turso は Deterministic Simulation Testing (DST)、差分テスター、ファザー、並行シミュレータなどを含む厳格なテストスタックを採用しています。

この包括的なアプローチにもかかわらず、チームは戦略にギャップがあることに気付きました：形式手法です。従来はアクセスしにくい、あるいは過度に複雑と見なされてきましたが、形式手法は従来のテストでは得られない数学的確実性を提供します。Quint という現代的な形式検証ツールを統合することで、Turso はハードニングプロセスをさらに進め、最終的に SQLite 自体のバグを 10 件以上発見しました。

形式手法の課題

形式手法（例：TLA+）はシステムの正確性を検証する業界標準です。しかし、参入障壁が高く、"who watches the watchmen" 問題—モデル自体が正しいかどうかを検証する難しさ—に直面します。

この課題を克服するため、Turso はコミュニティメンバーの Pavan Nambi と協力し、Quint を活用しました。Quint は Temporal Logic of Actions (TLA) の理論的基盤に、モダンな型チェックと開発ツールを組み合わせ、エンジニアにとってよりアクセスしやすくしています。

SQLite 全体をモデル化するという不可能に近い課題に取り組む代わりに、チームは C API に注力しました。C API は文書化が充実しており、ほとんどの SQLite ドライバの主要インターフェースであるため、モデル化することでカバレッジに対する高いレバレッジポイントを提供します。このアプローチにより、API 仕様を真実の情報源として使用し、モデルと実装の両方を検証できました。

「Quinting」プロセス

バグを見つけるための手法は、繰り返し行われる 4 ステップのサイクルでした：

  1. 契約をモデル化: 文書化された SQLite C API の契約を特定し、必要な状態とプロパティを Quint でモデル化する。
  2. トレース生成: Quint を使用して、契約に違反する可能性のある状態のシーケンス（トレース）を生成する。
  3. 実行: これらのトレースを小さな C プログラムに変換し、SQLite に対して実行する。
  4. 比較: システムの観測された挙動を文書化された結果と比較する。

モデルチェッカーが失敗を検出すると、カウンタ例—違反につながる特定の状態シーケンス—が生成されます。多くのカウンタ例はモデルが正しいことを検証するだけでしたが、他の例ではシステムが自身の仕様から逸脱していることが明らかになりました。

ケーススタディ: sqlite3_deserialize()

顕著な例として、sqlite3_deserialize() 関数があります。この関数はシリアライズされたデータベースイメージを接続にロードし、インメモリデータベースとして使用できるようにします。

仕様によれば、対象データベースが現在読み取りトランザクション中またはバックアップ操作中である場合、sqlite3_deserialize() は SQLITE_BUSY を返すべきです。Quint モデルは次のシーケンスを持つトレースを生成しました：

  1. データベースをオープン → テーブル作成 → データベースをシリアライズ。
  2. データベースからの読み取りを開始。
  3. 読み取りトランザクションがアクティブな状態で sqlite3_deserialize() を呼び出す。

期待される戻りコードは SQLITE_BUSY でしたが、実際の結果はシステムクラッシュでした。クラッシュはほぼ意図された動作ではないため、バグが実装側にあることが即座に確認できました。この問題はその後 SQLite のソースで修正されました。

結果と所見

Quint を用いた探索は非常に生産的で、最適化におけるロジックエラーから重大なクラッシュまで、幅広いバグを発見しました。主な所見は以下の通りです：

  • 最適化失敗: EXISTS-to-join 最適化が LIMIT/OFFSET を誤って適用したり、外部相関を失って有効な行を除外したりする問題。
  • 制約違反: 引用された制約名が削除できなくなったり、xfer 最適化がチェック制約を回避してデータベースが不整合になるバグ。
  • 安定性問題: 内部テーブルでの ALTER ADD CHECK 実行中や sqlite3changegroup_change_finish() における NULL pzErr に起因するクラッシュ。
  • メモリとアラインメント: sqlite3_mutex の 128 バイトアラインメントに関する未定義動作。

結論

SQLite は現存するソフトウェアの中でも最も徹底的にテストされたものの一つです。しかし、Quint を通じて形式手法を適用することで、Turso は何十年にもわたる従来のテスト手法をすり抜けていたバグを発見できました。

形式的トレースを実行可能な C プログラムに変換することで、Turso は自らの実装をハードニングしただけでなく、SQLite エコシステム全体の安定性にも大きく貢献しました。これは、C API のような特定かつ明確に定義されたインターフェースに形式手法を適用することが、現代ソフトウェアの信頼性向上に強力なツールであることを示しています。

Sources