SQLiteの16年越しのバグに学ぶ、並行処理の難しさとAI時代の形式手法

みなさんこんにちは。

「あの人も読んでる」、第22回目の投稿です。maguro（X @yusuktan）がお届けします。

今回は、TailscaleがSQLiteに16年間潜んでいたバグを突き止めた記録、「How we tracked down a 16-year-old SQLite bug」を紹介します。

この記事を起点に、AIが書くコードが増えるなかで、形式仕様によるモデル検査やDSTなど、機械的に不具合を探す手法の重要性についても考えます。

僕は以前の「も読」で、分散システムのバグを再現可能な形で探す決定論的シミュレーションテスト（Deterministic Simulation Testing、DST）について書きました。
今回は、実装を動かして状態空間を探索するDSTとは少し違う方法で、膨大な組み合わせから不変条件を破る短い処理順序を取り出す過程についても触れていきます。

AI時代、ソフトウェアが期待通りに正しく動くことを機械的に検証できる方法の価値が上がっていると思います。
分散システムそのものの開発に携わる機会のある方はそこまで多くないかもしれませんが、「そんな手法もあるんだー」というくらいの気持ちで気軽に読んでいただければと思います。

「枯れた技術」で起きた19回のデータベース破損

Tailscaleは2022年から、端末やネットワークの設定を管理・配布するコントロールプレーンの主要なデータベースとしてSQLiteを使っています。

Tailscaleのコントロールプレーンは、ユーザーごとのプライベートネットワークであるtailnetを単位として、複数のシャードに分かれています。1つのシャードが複数のtailnetを担当し、その情報を1つのSQLiteデータベースへ保存します。各シャードでは、1つのGoプロセスだけがそのSQLiteデータベースへアクセスするsingle-writer構成になっています。

Tailscale自身も記事の中で、SQLiteを良い意味での「boring technology」と表現しています。
広く使われ、挙動がよく知られた技術を選んだので、データベースそのものに長期間悩まされることはないはずでした。

Tailscaleは数分おきにSQLiteデータベース全体のスナップショットを作り、そのファイルをS3へ保存していました。あるとき、そのバックアップを読み取るデータパイプラインが、とあるエラーを報告します。

データやインデックスなど、SQLiteファイル内部の整合性を検査するPRAGMA integrity_checkを実行すると、実際にデータベースが壊れていました。
その後も発生は止まらず、Tailscaleは約6カ月のあいだに19回のデータベース破損に見舞われました。

Tailscaleのデータベースには、ユーザーの秘密鍵やネットワークトラフィックは保存されていません。それでも、復旧中は対象シャードのコントロールプレーンを停止する必要があり、初期のインシデントでは停止が1時間を超えました。すでに接続している端末同士の通信は続きますが、新しく起動した端末は接続先の情報を取得できず、管理画面やAPIも利用できなくなります。

発生条件には、なかなか共通点が見つかりませんでした。特定のシャード、ユーザー、機能、時刻、負荷の高さとは結びつかず、発生間隔も数時間から数週間までばらばらでした。人工的に再現できないため、Tailscaleは次の発生を待ちながら、本番環境へ少しずつ観測点を追加していきます。

ここが一番厄介なところです。
データベース破損は確かに発生しているのに、そこに至るための手順が分からない。観測点を追加しながら、本番で次に起きる1回を待つしかありませんでした。めったに起きない並行処理のバグを、本番環境で追いかける難しさがよく表れています。

WALのリセットとチェックポイント処理の競合

Tailscaleは調査を進めるため、SQLiteの開発者と有償のサポート契約を結びました。

調査の中で、SQLiteの開発者は、ファイル操作を担当するVirtual File System（VFS）層へ詳細な追跡情報を追加するtmstmpvfsという診断用shimを作りました。このshimを本番環境へ導入し、次の破損時に得られたログをSQLiteの開発者が解析したことで、原因がようやく特定されました。

その原因を理解するには、SQLiteのWrite-Ahead Log（WAL）について少しだけ知る必要があります。
WALモードでは、更新されたページをすぐにデータベース本体へ書かず、まずWALファイルへ追記します。WALへ追加されたページは、あとからデータベース本体へコピーされます。この処理をチェックポイント処理と呼びます。すべてのページをコピーし終えると、WALをリセットし、先頭から再利用していきます。

今回のバグは、WALのリセットとチェックポイント処理が特殊なタイミングで重なったことで発生しました。
チェックポイント処理が、まだデータベース本体へコピーしていないページをコピー済みだと誤認し、本当はまだコピーされていないページをコピー対象から外してしまったのです。その結果、データとそれを参照するインデックスなどの整合性が崩れ、データベースが破損しました。

先ほども述べた通り、アプリケーションからSQLiteへ書き込むプロセスは1つでした。
しかし、アプリ側のプロセスが1つであっても、データ書き込みとチェックポイント処理が並行で実施されることは起こり得ます。これによってバグが発生しました。

SQLiteは、チェックポイント処理の開始後にWALがリセットされたことを検出した場合、その処理を中止するよう修正しました。

このバグは少なくとも2010年から存在していたと推定されています。
一般的なSQLiteの構成では発生確率が低い一方、Tailscaleは一貫したバックアップを作るため、チェックポイント処理を手動かつ高頻度で実行していました。
正式にサポートされた使い方ではありますが、多くのSQLite利用者とは異なる運用によって、まれな競合へ到達しやすくなっていました。

TLA+が見つけた短い処理順序

Canonicalのdqlite^[1]チームは、「Hunting a 16-year-old SQLite bug with TLA+: is dqlite affected?」で、SQLiteで見つかったバグが自分たちのシステムにも影響するのかを調べました。
dqliteでもSQLiteのWALを使うため、同じバグが発生するかは切実な問題です。

Canonicalは、SQLiteの処理をTLA+でモデル化しました。TLA+は、システムが持つ状態、その状態を変える操作、常に守るべき不変条件を書き、不変条件が破られる処理順序がないかを調べるための形式仕様言語です。

実際のSQLiteは巨大ですが、今回必要なモデルはかなり小さくできます。
データの各ページを連番の整数、WALを整数の列、データベース本体を整数の集合としてモデル化します。そのうえで、データベースへの書き込みによるWALへの追加、チェックポイント処理によるデータベース本体へのコピー、WALのリセットといった操作を定義します。

このモデルで確かめる不変条件は、次のシンプルなものです。

データベース本体にコピーされたページの番号が、1から欠番なく並んでいること。

モデルチェッカーを実行すると、不変条件を破る具体的な処理順序が、初期状態を含む20個の状態をたどる形で見つかりました。モデル検査では、このように不変条件を破る例を反例（counterexample）と呼びます。その処理順序は、SQLiteが公開したWAL-Resetバグの説明とよく似ていました。

TLA+はあくまでモデル化されたSQLiteに対しての検査を実行しただけであり、本物のSQLiteを解析したわけではありません。
TailscaleとSQLiteの開発者が数カ月かけて原因を突き止めたあと、Canonicalが必要な状態だけをモデルへ移し、壊れる処理順序を短い反例として再現した、ということです。

この反例を使うことで、dqliteでも同じ処理順序へ到達する可能性があるのかを調べることができました。

調査の結果、dqliteでは、チェックポイント処理中はデータベースへの読み書きを止めるようにしていたため、書き込みとチェックポイント処理が並行して動くことはない、と判明。この動作をTLA+のモデルへ加えると、ページが失われる反例は出なくなりました。

つまり、dqliteのモデル上では、Tailscaleが直面したWAL-Resetバグは発生しないことが確認できました。

celldのコード調査から見つかった二重の書き込み権限

Canonicalの事例は、すでにSQLiteで見つかっていたバグをTLA+で再現し、dqliteへの影響を調べるものでした。

一方、mizchiさんの「時相論理の形式仕様の Quint を使って、denoland/celld の二重 writer バグを見つけた」では、コード調査を起点にQuint^[2]を使ってcelldの設計をモデル化し、バグを見つけました。

celldはDenoチームが開発している、セルフホスト可能なCloudflare WorkersとDurable Objectsの実行環境です。celldでは、ユーザー、ドキュメント、チャットルームなど、独立して状態を持たせたい単位ごとにcellを作ります。1つのcellは、リクエストを処理するプログラムと専用のSQLiteデータベースを持つ、小さなサーバーのようなものです。

各マシンではcelldのプロセスが動いており、これをnodeと呼びます。
複数のnodeのどれでもcellを処理できますが、同じcellを担当してSQLiteへ書き込めるnodeは、同時に1つだけでなければなりません。

どのnodeがcellを担当しているかは、オブジェクトストレージ上の記録で管理します。
担当するnodeは、自分が動いていることを示すleaseを定期的に更新し、更新が止まって期限が切れると、別のnodeがcellを引き継げます。

ここで注意が必要なのが、マシンごとに時計が異なることです。
分散システムでは、すべてのマシンが完全に同じ時刻を共有している、という前提を置くことは基本的にはできません。

NTP^[3]などで同期していても時計にはずれがあるため、時刻を使って期限を判断するシステムは、そのずれを前提に設計する必要があります。
マシン間で時刻や出来事の順序をどう扱うかは、Leslie Lamport^[4]の古典的論文「Time, Clocks, and the Ordering of Events in a Distributed System」でも扱われている、分散システムの基本的な問題です。

ここでwall-clockとmonotonic clockの2つの用語を説明します。

wall-clockは、日時を表すための時計です。
例えば「2026年9月7日14時」のような現在時刻を返します。
NTPによる時刻合わせなどで値が補正されるため、時計が進んだり戻ったりすることがあり、マシンごとのずれも生じます。

monotonic clockは、ストップウォッチのように経過時間を測るための時計です。
wall-clockの時刻合わせには影響されず、値が後戻りしません。
ただし、基準となる時点はマシンごとに異なるため、別のマシンの値とは比較できません。

celldでは、新しく担当になるnode Bが、自分のwall-clockを使って、以前の担当であるnode Aのleaseが期限切れかを判断します。一方、Aは自分のmonotonic clockで経過時間を測り、まだ自分に書き込み権限があるかを判断していました。

mizchiさんは、コードを読んだ段階で、時計のずれによって書き込み権限が重なる可能性に目星をつけていました。
記事では、この仕組みをQuintでモデル化し、「同じcellへの書き込み権限を持つnodeは常に1つ以下」という不変条件を検査しています。

見つかった反例は、次のようなものでした。

• leaseの有効期間は10秒
• node Bのwall-clockはnode Aより1秒進んでいる
• 現実には9秒が経過している

現実には9秒しか経過していなくても、1秒進んでいるBの現在時刻は、Aが自分のwall-clockを基準に記録したleaseの期限に達します。Bはその期限と自分の現在時刻を比較し、Aのleaseが切れたと判断してcellを引き継ぎます。

しかし、Aのmonotonic clockではまだ9秒しか経っていないため、Aも自分には書き込み権限があると判断します。

短い時間ですが、AとBの両方が、同じcellへの書き込み権限を持つ状態になります。これはバグです。

mizchiさんは、この結果をQuintのモデルだけで終わらせず、同じleaseの有効期間、時計のずれ、経過時間を使ったRustの回帰テストを書きました。
修正前の実装では、node Aとnode Bの両方が書き込みを受け付ける結果になり、モデルで見つけた問題が実装にも存在することを確認しています。この問題はGitHub Issueとして報告されました。修正版はv0.2.0で公開され、Issueはcloseされています。

DSTとモデル検査で見ているもの

僕は大学院のDistributed Computingというコースの課題で、Paxos^[5]を使った分散キーバリューストアを実装しました。
課題ではDSLabsというフレームワークを使い、各ノードをステートマシンとして実装します。
テストフレームワークがネットワーク通信やタイマーを制御し、メッセージの遅延、欠落、順序の入れ替わりなどを探索できるようになっていました。

Paxos自体の難しさもありましたが、プログラムが一度期待通りに動いただけでは安心できない、という感覚を強く持つようになりました。
ある順序では成功しても、別の順序では2つのノードが食い違うかもしれません。
そして、その順序を人間がテストケースとして先回りしてすべて書くことはできません。
DSLabsで状態空間を探索し、思いもよらない反例を短い手順として示してもらえた経験が、僕がDSTに惹かれるきっかけになりました。

DSTとTLA+やQuintによるモデル検査は、同じものではありません。DSTは本物の実装、あるいはそれに近いプログラムを動かし、制御した非決定性の中からバグを探します。実装上の細かなミスも発見できる一方、状態が大きくなりやすく、すべての組み合わせを探索することは困難です。

形式仕様では、調べたい不変条件に関係しない実装の詳細を捨て、モデルを機械的に検査できる大きさにします。
CanonicalのモデルではSQLiteのページを整数として表し、mizchiさんのモデルではcelldの実装からlease、cellの所有権、書き込み権限に関する状態だけを取り出しました。
モデルを有限にできれば、モデルチェッカーは、その中で到達可能な状態を網羅的に調べられます。
Canonicalのモデルでは初期状態を含む20個の状態、celldのモデルでは「9秒経過、時計のずれ1秒」という、人間が確認できる大きさの反例が見つかりました。

ただし、網羅的なのはあくまでモデルの中です。
今回のSQLiteのモデルではページの中身を捨て、celldのモデルではV8、SQLite、S3、HTTPなどを捨てています。

何を捨ててよいかを決めるのはそんなに簡単ではありません。
モデルから落とした状態によってバグが起きるなら、残った状態をいくら網羅的に検査しても見つけられません。
形式仕様を書くうえで重要なのは、記法を覚えることだけではなく、実装のどの状態をモデルに残すかを判断することです。

AIで形式手法は身近になるか

形式仕様を書き始める前段として、TLA+やQuintの記法を覚え、モデルチェッカーを動かせるところまで持っていくのも、僕には高いハードルに感じられていました。

mizchiさんの記事では、AIを使ってcelldのコードを調査し、Quintのモデルを作っています。
AIがモデルのたたき台を作り、記法のエラーを直し、反例の読み方を説明してくれるなら、形式仕様を書き始めるまでのハードルはかなり下がりそうです。

ただし、どんな不変条件を検査するかも検討する必要があります。
SQLiteのモデルでは「データベース本体にコピーされたページの番号が、1から欠番なく並んでいる」、celldのモデルでは「同じcellへの書き込み権限を持つnodeが常に1つ以下」という不変条件を置いています。
不変条件が弱すぎれば、本来は満たすべき条件に違反した状態を見逃してしまいます。
AIが提案した不変条件が、確かめたい性質を表しているかは、人間が確認する必要があります。

モデルチェッカーが反例を返しただけで、実装のバグが確定するわけではありません。モデルが実装では起こらない処理順序を許している可能性もあるためです。
celldの記事では、Quintの反例に含まれていた具体的な値と処理順序をRustの回帰テストへ移し、実装でも同じ問題が起きることを確認していました。
モデルで見つけた反例を実装のテストへつなげることで、抽象化した際のずれを確かめながら不具合を追えます。

おわりに

Tailscaleは本番での破損を繰り返し観測しながら原因を追い、Canonicalは原因判明後にモデルを作ってdqliteへの影響を調べました。
celldの事例では、コード調査から生まれた疑いをモデルへ移し、反例を実装テストで再現していました。

AIが書くコードが増えるほど、人間の注意力だけに頼らない機械的な確認手段の価値は上がっていくはずです。
通常のテスト手法に加え、モデル検査やDST、さらには最近話題になることも多いLean^[6]なども含めて、この領域をもっと勉強していきたいと思いました。

また次回、おすすめコンテンツを紹介していきます。
お楽しみに！

maguroさんの「も読」過去記事

• Mozillaでの10年、最短ではないキャリアと「実はすごい」Web（8月10日公開）
• 積ん読を動画で崩す！Systems Performance読書シリーズと名門大学の無料講義（7月10日公開）
• TSKaigi 2026で見た、TypeScriptエコシステムの変化、Go移植、Deno 2.8、AI生成スライド（6月15日公開）

執筆者へのお便り