TLA+で16年前のSQLite WALバグを追跡する

この記事は、CanonicalのdqliteチームのMarco ManinoとAlberto Carreteroによって書かれました。 1. SQLiteバグの解剖 最近、SQLiteは、Write Ahead Log (WAL) のチェックポイント処理方法における長年のバグを修正する新しいバージョンを公開しました。このバグはデータベースの破損につながる可能性がありました。このバグの重要な側面は、その実際のインパクト（非常に低い）ではなく、リポジトリにどれだけ長く存在していたか、それを見つけるのがどれほど困難だったか、そしてそれを再現するのがどれほど困難だったかということです。実際、このバグは2010年から、つまり16年間存在していました！また、私たちdqliteチームにとっての重要な質問は、dqliteはこのバグの影響を受ける可能性があるのか？ということです。それを知るために、まずデータベース破損につながる正確な手順を理解する必要があります。そのために、SQLiteの挙動をモデル化するためにTLA+を使用し、バグについて推論できるトレースを迅速に見つけます。次に、dqliteがsqliteをどのように使用するかを記述する別のモデルを作成し、バグが発生するかどうかを確認します。 2. WALとSQLiteのチェックポイントの簡単な紹介 SQLiteは、リーダーがライターによってブロックされないようにするためにWALモードを使用します。それを達成する方法は、Write Ahead Log (WAL) と呼ばれる特別なステージングエリアに書き込むことです。ライターはWALの末尾に追記でき、リーダーはデータが安定するまで新しいデータを無視できます。最終的に、ステージングエリアはデータベースに移動されます。これはチェックポイントと呼ばれます。WALが無限に成長するのを防ぐために、ライターは、前のチェックポイントがすべてのページを移動できた場合、WALを「リセット」しようとします。つまり、それを上書きします。さらに詳しく知りたい場合は、公式ドキュメントで非常に明確な説明を見つけることができます。 SQLiteはロックと共有メモリを使用してWALへの変更をオーケストレーションします。私たちのユースケースでは、書き込みとチェックポイントの処理を考えるだけで十分です。そのため、2つのロックのみに関心があります。 - チェックポイントロック (CKPT_LOCK)：複数のチェックポイントが同時に発生するのを防ぐために、チェックポイントを実行する前に取得されます。 - 書き込みロック (WRITE_LOCK)：WALに新しいページを追記する前に取得されます。 共有メモリには、ライター、チェックポインター、リーダーをオーケストレーションするために必要な情報と、読み取りパフォーマンスのためのWAL内のページをインデックス化するためのデータ構造が含まれています。前述のように、リーダーは関与しないため、唯一興味深いフィールドは次のとおりです。 - walSalt：WALがリセットされるたびにインクリメントされるカウンターが含まれています。 - mxFrame：WALの長さが含まれています。 - nBackfill：すでにチェックポイントされたページの量が含まれています。つまり、[nBackfill+1, mxFrame] はまだデータベースにコピーされていません。 3. TLA+でのバグのモデリング TLA+の記述の難しさの一部は、何をモデル化し、何をモデル化しないかを決定することです。現実を忠実に再現し、モデルから有用な洞察を引き出すことができる、可能な限り最も単純な仕様を作成したいと考えています。最初にモデル化するのは、前のセクションで説明したデータベースとWALです。 * ファイル。 VARIABLE wal VARIABLE db * wal-インデックス変数： VARIABLE nBackfill VARIABLE mxFrame * saltのシーケンシャル部分のみをキャプチャします。 VARIABLE walSalt Init ≜ wal = ⟨⟩ ∧ db = {} ∧ nBackfill = 0 ∧ mxFrame = 0 ∧ walSalt = 0 データを生成することはモデルの範囲外であるため、より単純なアプローチを取ることができます。各データページを単一の一意の番号としてモデル化し、WALをそのような番号のシーケンス、データベースをそれらのセットとしてモデル化できます。特に、チェックポイントはWAL内のシーケンスからデータベースのセットにページを、WALに追加された順序で移動します。一意の番号を生成するには、常に増加するカウンターを使用するだけで十分です。 バグを生成して相互作用する2つのアクション、つまり追記とチェックポイントをモデル化する必要があります。まず、WALにページを追記するSQLiteのCコードを見て、TLA+アクションを定義しましょう。 WALにフレームを追記する責任のあるSQLiteコード static int walFrames( Wal *pWal, /* 書き込むWalハンドル */ int szPage, /* データベースページサイズ（バイト単位） */ PgHdr *pList, /* 書き込むダーティページのリスト */ Pgno nTruncate, /* このコミット後のデータベースサイズ */ int isCommit, /* コミットかどうか（真偽） */ int sync_flags /* OsSync()に渡すフラグ（または0） */ ){ int rc; /* リターンコードをキャッチするために使用 */ u32 iFrame; /* 次のフレームアドレス */ PgHdr *p; /* pListを走査するためのイテレータ。 */ PgHdr *pLast = 0; /* リストの最後のフレーム */ int nExtra = 0; /* 最後のページの追加コピーの数 */ int szFrame; /* 単一フレームのサイズ */ i64 iOffset; /* WALファイルでの次の書き込みバイト */ WalWriter w; /* ライター */ u32 iFirst = 0; /* 上書きされる可能性のある最初のフレーム */ WalIndexHdr *pLive; /* 共有ヘッダーへのポインタ */ assert( pList ); assert( pWal->writeLock ); /* このフレームセットがトランザクションを完了する場合、nTruncate>0。** nTruncate==0 の場合、このフレームセットはトランザクションを完了しません。 */ assert( (isCommit!=0)==(nTruncate!=0) ); #if defined(SQLITE_TEST) && defined(SQLITE_DEBUG) { int cnt; for(cnt=0, p=pList; p; p=p->pDirty, cnt++){} WALTRACE((