同一段 checkpoint 流程在 SQLite 裡跑了十六年沒出事，直到有人用形式化模型把它的並發交錯全部攤開——第二十個狀態，資料庫就少了一頁。這一頁，到底是怎麼弄丟的？
二十步走到損毀：TLA+ 逼出 SQLite 藏了十六年的 checkpoint 競態
Canonical 的 dqlite 團隊（Marco Manino 與 Alberto Carretero）在 2026 年 6 月 25 日貼出一篇拆解，起點是一個很實際的擔憂：SQLite 剛修掉一個 WAL checkpoint 的並發 bug，而 dqlite 正是把 SQLite 當成儲存核心的分散式資料庫——「the crucial question」，他們寫道，就是 dqlite 到底會不會中招。要回答這個問題，得先精確知道這個 bug 是怎麼觸發的。麻煩在於，它「has been present since 2010, _for 16 years_」，藏了十六年沒人踩到，靠肉眼讀程式碼很難把觸發它的那串交錯順序拼出來。
於是他們沒有再讀一遍原始碼，而是「we will be using TLA+ to model SQLite's behavior and quickly find a trace」——把 checkpoint 與寫入之間那幾個共享欄位建成一個狀態機，讓 model checker 自己去窮舉所有交錯，把觸發損毀的最短路徑吐出來。結果乾淨得有點嚇人：「It takes only 20 states to witness a missing page in the database」。這篇要拆的就是這條二十步的路徑：哪個欄位被設錯、為什麼一頁會憑空消失、為什麼 dqlite 剛好站在窗口之外，以及新版怎麼把窗口關掉。
少掉的那一頁，藏在三個東西之間
先把舞台擺出來。WAL 模式下，一次寫入不是直接改資料庫檔，而是把新頁面追加到 WAL 檔尾巴；checkpoint 再擇時把 WAL 裡的頁面搬回資料庫檔。協調這兩件事的狀態，不在磁碟上，而在一塊叫 WAL-Index 的共享記憶體裡。真正牽涉這個 bug 的欄位其實只有三個，加上兩把鎖。
三個欄位各司其職。walSalt 是「a counter that is incremented each time the WAL is reset」——WAL 每被重置一次，這個計數器就加一，它等於 WAL 內容的世代編號。mxFrame 是「the length of the WAL」，也就是 WAL 目前有多長。nBackfill 是「the amount of pages that have been already checkpointed」，記錄已經搬回資料庫的頁數，換句話說 [nBackfill+1, mxFrame] 這段還沒落地。兩把鎖也很直白：checkpoint 鎖「taken before running a checkpoint to prevent multiple from happening at the same time」，write 鎖「taken before appending new pages to the WAL」。這裡有個關鍵細節：checkpoint 一開始會把 WAL 的 header（連同裡頭的 salt）複製一份到自己這邊，之後才慢慢把 frame 搬進資料庫——它做決定時看的是那份快照，而快照跟共享記憶體裡的即時值，可能已經對不上了。
WAL 模式的整套安全性，建立在一個看似顯然的假設上：進過 WAL 的每一頁，遲早都會依序被搬進資料庫檔。checkpoint 就是履行這個承諾的那隻手。一旦它把某頁誤記成「已經搬過」，那頁就永遠卡在中間——WAL 這頭被重置後覆蓋掉，資料庫那頭又從沒收到，紀錄就這樣蒸發。更棘手的是這種損毀是安靜的：沒有 crash，沒有錯誤碼，資料庫檔在結構上依然合法，只是內容少了一塊，等到某次查詢正好讀到那頁才會爆出來，而那時離真正出事，往往已經隔了很久。
這裡的「複製一份 header」不是實作瑕疵，而是刻意的設計：checkpoint 不想在整段搬運過程裡一直鎖住 WAL-Index，於是先抄一份自己要用的欄位，放開手讓寫入繼續。問題在於，抄下來的 salt 是一個會過期的值，而原本的程式碼把它當成整段過程都不變的常數在用。所謂重置 WAL，是 checkpoint 把 WAL 搬空之後、讓下一批寫入從檔頭重新開始的正常機制，每重置一次 salt 就換一個新值，用來昭告「檔頭這批 frame 屬於新的一代」。salt 存在的唯一理由，就是讓讀 WAL 的人分辨手上的 frame 還屬不屬於當前這一代——諷刺的是，這個 bug 正是 checkpoint 自己抄了 salt，卻沒在關鍵時刻回頭核對。
一個藏了十六年的 bug，通常不是因為它難修，而是因為它難踩到。這個競態要成立，得同時滿足好幾個很窄的條件：兩個 checkpoint 前後腳發生、重置的 commit 精準插進第二個 checkpoint 複製 header 之後的那個瞬間、事後又要有足夠的寫入把被誤跳的區間撐開。任何一環錯開，資料庫都毫髮無傷。正是這種需要天時地利的觸發條件，讓它在 2010 到 2026 這十六年裡躲過了無數次 code review、fuzzing 與真實線上流量——直到有人不再靠運氣，改用一台會窮舉所有交錯的機器去逼它現形。
為什麼不是再讀一遍程式碼，而是動用 TLA+
這種 bug 的難處不在單一函式寫錯，而在於它只有在兩條連線以某個特定順序交錯時才會現形。checkpoint 的啟動、寫入交易的 commit、WAL 的重置，這幾件事誰先誰後有很多種排列，人腦讀程式碼很難保證窮舉到那唯一致命的一種。形式化方法的價值正在這裡：把「有趣的欄位」抽出來寫成狀態機，剩下的交給 model checker 去搜。
TLA+ 是 Leslie Lamport 設計的形式化規格語言，專門用來描述並發與分散式系統的行為；配套的 TLC model checker 會把規格展開成狀態圖，自動搜尋違反不變式的路徑。它擅長的，正是人類最不擅長的那塊：把所有可能的交錯順序一個不漏地想過一遍。你不必寫得出攻擊，也不必猜哪個順序有問題，只要把系統的合法動作與該守的性質寫清楚，搜尋交給機器。這也是為什麼近年愈來愈多資料庫與共識系統，會在關鍵協定上先寫一份 TLA+ 規格，再動手實作。
| 共享欄位／鎖 | 意義 | 在這個 bug 裡的角色 |
|---|---|---|
walSalt | WAL 的世代計數器，每次重置 +1 | 被 checkpoint 快照下來，但重置後沒被重新比對，這是漏洞的核心 |
nBackfill | 已 checkpoint 到第幾個 frame | 被第二個 checkpoint 設成錯的值，害後續 checkpoint 跳過真正還沒搬的 frame |
mxFrame | WAL 目前長度 | 重置後歸零再增長，決定哪些 frame 落在被誤跳的區間 |
CKPT_LOCK | checkpoint 鎖 | 只擋「兩個 checkpoint 同時跑」，擋不住 checkpoint 與寫入交錯 |
WRITE_LOCK | write 鎖 | append 時才拿；SQLite 不在 checkpoint 全程握著它，窗口因此打開 |
model checker 的工作方式，是把系統所有可能的狀態看成一張圖，從初始狀態出發，窮舉每一個合法的下一步，直到踩進違反不變式的狀態為止。難點永遠是狀態爆炸——多幾個變數、多幾條連線，狀態數就指數膨脹。這裡之所以可行，是因為真正相關的只有那三個欄位與兩把鎖，其餘細節都能抽掉。把模型收斂到剛好夠描述競態、又不多一分的程度，本身就是形式化建模最吃功力的一步。
他們連 checkpoint 自己也建成一個小狀態機：從「未開始」，到「已複製 header」，到「等待鎖」，再回到「未開始」。這個切分是為了讓 model checker 能在「已複製 header」這個中間狀態上，插入另一條連線的重置動作——競態的本質就是「一個操作進行到一半，被另一個操作插隊改了共享狀態」，而狀態機正好把「一半」這個模糊的說法，變成一個機器能逐一列舉的具體狀態。少了這層切分，那個中途的空檔根本無從表達，機器也就搜不到它。
他們驗的不變式（invariant）寫得很白：資料庫不能有「洞」，而且「All the frames that were added to the WAL have landed in order.」——所有進過 WAL 的 frame 都得依序落地。把這個性質交給 model checker，它會嘗試所有交錯，一旦找到某條路徑讓某個 frame 沒落地，就回報一條反例 trace。人要證明「不存在這種順序」幾乎不可能；機器要找出「存在這麼一種順序」，只是搜尋而已。這就是為什麼這裡選 model checker，而不是再開一次 code review。
對工程師來說，一條反例 trace 比一句「這裡可能有 race」有用得多。它不是模糊的警告，而是一份可重播的劇本：第幾步誰做了什麼、哪個欄位在哪個瞬間變成什麼值，全都釘死在那二十個狀態裡。你可以照著它回頭在真實程式碼裡定位每一步，也可以照著它寫一個回歸測試。形式化方法真正交付的，往往不是「證明沒有 bug」，而是這種「這就是 bug，它長這樣」的鐵證。
二十個狀態，一頁就這樣不見
反例 trace 攤開來是六步，每一步都只是一件再正常不過的操作，合起來卻精準地把一頁擠出資料庫。你可以把它想成兩條連線在同一塊共享記憶體上的一次不幸交會。
拖動滑桿改變 WAL 重置的時機，看第二個 checkpoint 何時漏看它 · 可切換修復
把六步逐一切開看更清楚。前兩步是常規節奏，第三步是那次致命交會，後三步只是把後果放大到看得見。
nBackfill 設成一個聲稱「這些 frame 已經 checkpoint 過」的值，但實際上根本沒有。核心就在第四步那一個字：race。C2 動手前那份 header 是複製來的快照，它沒有在真正 backfill 之前再回頭確認「共享記憶體裡的 salt 是不是還等於我當初抄下來的 S0」。只要重置剛好卡在複製與 backfill 之間，C2 就會用一個過期的世代編號去更新 nBackfill，把新世代的 frame 誤當成舊帳算掉。model checker 走到第二十個狀態時，資料庫就出現了那個洞——某一頁進過 WAL，卻沒依序落地。
nBackfill 被設錯之所以致命，在於它是一個單調的承諾：後續每一個 checkpoint 都相信 [1, nBackfill] 這段已經安全落地，只會去處理 [nBackfill+1, mxFrame]。第二個 checkpoint 把 nBackfill 記過頭，等於替後面所有 checkpoint 立了一張假收據；它們照著這張收據做事，理直氣壯地跳過那筆其實從沒落地的交易。錯誤不是在最後爆出來的那一刻造成的，而是在更早、那個被悄悄設錯的欄位裡就已經埋好。這也是為什麼肉眼審查難以抓到它：出事的 checkpoint 本身每一行都對，錯的是它信任了一份幾步之前就被污染的狀態。
把二十步收斂成一句話：一筆本來要寫進資料庫的頁面，因為記帳欄位被前一個 checkpoint 用過期的世代編號改壞，被後面的 checkpoint 當成早就處理過而略過，於是它進了 WAL、卻永遠沒進資料庫。上面那張互動圖裡被畫叉的第 4 頁，就是這個角色的替身——它存在於 WAL 的某一代，也被 mxFrame 算進了長度，唯獨在最終的資料庫檔裡缺席。拖動滑桿時你會發現，致命的其實不是「重置」這個動作本身，而是它落下的那個精確位置：早一點、晚一點都沒事，只有卡在複製與 backfill 之間那道窄縫裡，資料才會漏。
dqlite 為什麼逃過一劫
回到那個一開始的問題：dqlite 會不會中招？答案是不會，而且理由乾脆——「dqlite is not affected by the bug at all!」關鍵在鎖策略。這個競態需要「一個 checkpoint 正在進行」與「另一條連線重置 WAL」同時存在；只要這兩件事永遠不可能重疊，窗口就不存在。
作者的描述是：dqlite「by taking the write lock for both appending and checkpointing, they cannot proceed simultaneously」——append 與 checkpoint 都去拿同一把 write 鎖，兩者不可能同時推進，也就沒有 data race。落到 TLA+ 模型上，dqlite 版本「the only difference for our model is that the write lock is taken before starting a checkpoint」：checkpoint 一開始就先握住 write 鎖，這一改，重置（本身要 write 鎖才能做）就被擋在 checkpoint 之外，複製 header 與 backfill 之間那段時間裡，沒有任何人能重置 WAL。同一個不變式丟回這個模型，model checker 不再回報反例。dqlite 之所以安全，不是因為它繞過了 SQLite 的程式碼，而是因為它序列化 checkpoint 的做法，剛好把觸發窗口整個抹平。
dqlite 是 Canonical 拿 SQLite 當儲存核心、用 Raft 做複製的分散式資料庫，天生就是單一寫入者的架構：所有寫入與 checkpoint 都走同一條序列化的路徑。這條路徑原本是為了配合共識協定對「操作有明確先後順序」的要求，卻在這裡意外地成了護城河——序列化本身就把並發交錯的可能性拿掉了。值得記住的是這種安全帶著一點運氣的成分：dqlite 不是因為預見了這個 salt 競態才去序列化 checkpoint，而是它為了別的理由做的架構決定，恰好落在窗口之外。換個並發策略更激進的 SQLite 使用者，就未必這麼幸運。
salt 比對，把窗口關上
SQLite 那邊當然不能靠「全程握 write 鎖」來修——那會犧牲 WAL 模式讀寫並行的整個賣點。「Recently SQLite published a new version with a fix to a long-standing bug」，修法走的是另一條路：不阻止交錯，而是讓 checkpoint 在真正 backfill 之前，多做一次 salt 比對。
拖動分隔線，比較修復前後 checkpoint 的決策
互動圖表
修復前 checkpoint 憑舊 salt 快照直接記帳；修復後在寫回前比對 salt，世代已變就放棄 backfill，漏掉的那頁保住。
差別只是一個判斷：checkpoint 開始時把 salt 抄成 S0，等到要 backfill 那一刻，先比對此刻共享記憶體裡的 salt 還是不是 S0。若已經變成 S1，代表 WAL 在這中間被重置過，這次 backfill 的前提已經失效，就放棄、不去改 nBackfill。這樣一來，第四步那個「用過期世代去記帳」的動作根本發不出來，被誤跳的那頁自然保住。作者把修好後的模型連同同一個不變式再跑一次 model checker，這回不再有反例——修法確認有效。這個 bug 從 2010 年進到程式碼，到現在被形式化方法逼出來、在新版（版本 3.51.3）補上，中間隔了十六年。
這個修法的漂亮之處，在於它幾乎不花成本：不加鎖、不改介面，只在既有流程裡多插一次記憶體比對。它保住了 WAL 模式讀寫並行的整個賣點，代價僅是偶爾一次 backfill 被放棄、留給下一個 checkpoint 重做——而那本來就是 checkpoint 該有的容錯行為。相比之下，dqlite 用全程握鎖換來的安全，是拿並發度去交易的。兩邊都對，只是站在不同的取捨點上：SQLite 要服務千百種並發模式，只能在最小的地方補一針；dqlite 反正已經序列化，多這一針對它沒有意義。同一個 bug，兩種正確的回應，取決於你的系統把讀寫並行看得多重。
對正在用 SQLite 的人，這件事的實際意義很具體：如果你的應用是多連線並發寫入、又開了 WAL 模式，那麼升級到含這個修法的版本值得排進近期待辦；如果你像 dqlite 一樣把寫入與 checkpoint 收斂到單一序列化路徑，那你本來就在窗口之外，可以從容一點。判斷自己屬於哪一種，不必去翻 SQLite 的原始碼，只要問一句：我的系統裡，會不會有一個 checkpoint 正在跑、同時另一條連線把 WAL 重置掉？答案是「不會」的話，這個 bug 與你無關；答案是「有可能」的話，那份新版就得盡快裝上。
值得往外推一層的是，這類「抄一份快照、事後照它辦事」的模式在系統程式裡到處都是：讀一次組態、快取一份中繼資料、複製一份 header 再放手讓別人繼續改。它們共享同一個弱點——快照與現實之間永遠有一段窗口，而正確性取決於那段窗口裡有沒有人動了原件。多數時候沒人動，程式便跑得好好的；直到某一天，某條並發路徑剛好在那段窗口裡改了原件，而你的程式碼從來沒想過要回頭再看它一眼。SQLite 這一頁遺失的資料，說到底就是這種疏忽在十六年後寄回的帳單。
下次先看哪裡：當一段程式碼「先抄一份快照、之後再依快照做決定」，真正要盯的不是抄的那一步，而是抄與用之間有沒有人動過原件——這種只在特定交錯下才現形的並發 bug，與其一遍遍讀程式碼賭自己想得到那串順序，不如把幾個關鍵欄位寫成狀態機，交給 model checker 去替你窮舉；而你的系統受不受影響，最後往往取決於一件很無趣的事：你到底怎麼序列化 checkpoint 與寫入。