GC 讀 MySQL，看到這個 blob 的引用數是零，判定可以刪；幾乎在同一時間，client 把同樣的 bytes 重新寫回 S3、在 MySQL commit 了一筆新引用——兩邊各自的判斷都沒有錯，資料還是不見了。
兩邊都做對了，資料還是不見了
這是 Depot Registry 的故事，而且是一種特別讓人不安的丟資料方式——不是硬碟壞掉，也不是誰手滑打錯指令，是兩段各自看起來完全正確的程式碼，湊在一起的時候把資料弄丟了。Depot Registry 用 content-addressable 的方式存 blob，路徑是 blobs/sha256/<digest>，digest 就是內容本身的雜湊值。同樣的 bytes 理論上永遠寫到同一個 key，重複上傳照理是最安全的操作之一。Depot 工程團隊把整套三層 garbage collector 的行為寫成 TLA+ spec，丟給 model checker TLC 檢查，結果找到一個「測試和 code review 都漏掉的 bug」：一個熱門的 base image「cycle 出去又 cycle 回來」的時候，GC 判定要刪的 blob，可能剛好是 client 前一刻才重新寫回去的那份資料。
原文開場點出的命題，正好是這整起事故的縮影：「最難找到的分散式系統 bug，不會出現在單一操作裡；是兩個流程各自做對了自己的事，只是順序沒人想過，資料就這樣不見了。」
兩層帳本，各自都沒說謊
Depot Registry 把「誰還在用這個 blob」跟「這個 blob 實際的 bytes」拆成兩套系統管：引用關係存在 MySQL，內容本身存在 S3。GC 的流程照原文說法是「標記一個零引用的 blob，等過 grace period，再驗證一次，才刪除」——先讀 MySQL 判斷沒人用了，記下來，等一段時間，再確認一次，最後才真的對 S3 送出刪除指令。除了 GC 之外，另外還有一套機制在管引用計數本身：Depot 用一個輕量的 saga 模式減少熱門 blob 上的鎖競爭——「先把引用計數加一，做完工作，如果失敗再用減一補償」；如果補償因為當機而沒能跑完，一個叫 reconciler 的角色會負責修回正確的計數。
把這兩層放在一起看，故事的謎題就出現了：MySQL 那邊讀到零引用的那一刻是真的零引用；S3 那邊寫入新版本、MySQL 那邊 commit 新引用的那一刻也是真的成功寫入。兩個讀寫動作單獨拿出來看都沒有問題，可是 GC 最後執行的刪除，砍掉的卻是剛剛才被重新引用的那份資料。要理解這是怎麼發生的，得先把「誰的責任是什麼、誰對另一邊一無所知」攤開來看。
content-addressable 只保證「同樣的 bytes 只會佔一份儲存空間」，不保證「同樣的 bytes 不會被重新上傳」——client 端不知道、也不需要知道 GC 現在對這個 blob 的判斷是什麼，它只是照常把 image 推上去；於是上傳跟刪除這兩件事，變成兩個完全不知道對方存在的動作。
點任一元件看它的職責與盲區 · 4 個元件
MySQL · 引用表
存每個 manifest 對應的 blob 引用狀態；GC 判斷「零引用、可以刪」靠的就是這張表在某個時間點的讀值。
不知道：S3 那把 key 現在實際有幾個 version、哪一個 version 才是 GC 當初看到的那份 bytes。
S3 · bytes 儲存
用 content-addressable key（blobs/sha256/<digest>）存實際內容；若開了 bucket versioning，同一把 key 再寫一次會疊出一個新版本，不會覆寫舊的。
不知道：MySQL 那邊這把 key 目前是不是還有人引用著。
GC worker · mark → grace period → re-verify → delete
讀 MySQL 判斷零引用後標記、等過 grace period、re-verify 一次，才真的對 S3 送出刪除。
不知道（修法前）：它送出的刪除，對到的是不是自己當初看到的那份 bytes——沒有 delete fence 之前，它問 S3 的是「這把 key」，不是「那個版本」。
並行的 pusher · 重新推 image
算出 blob digest、把 bytes 寫進 S3、在 MySQL commit 一筆新的引用——三個動作，跟 GC 的動作完全獨立執行。
不知道：GC 是不是已經把這把 key 標成要刪、現在是不是正好在它的 grace period 裡。
四個元件各自把自己的那一步做對，湊在一起卻可能把資料弄丟——這正是接下來要拆解的地方：如果不是任何一步算錯，問題會出在哪裡？
先懷疑：是不是引用計數算錯了
Depot 的系統裡本來就有一整套機制在防「引用計數算錯」：saga 模式的 compensate-on-failure、專門修正計數的 reconciler，還有 TLA+ 模型裡特地加的一個 drift 注入流程——原文形容它「用跟失敗補償、跟歷史上計數失準相同的方向去改動計數」，讓 TLC 能故意去戳計數算錯的各種情境。既然系統本身就承認計數會出錯、而且已經為此準備了修補機制，第一個合理的懷疑自然是：這次弄丟資料，是不是因為某個 blob 的引用計數被算成了零，但其實還有人在用它？這套 drift 模擬的用意很清楚：既然現實裡的補償會失敗、計數會因為歷史原因跑掉，TLC 就該連這些髒狀態一起檢查，而不是只驗證乾淨情境下的行為。
模型裡確實有一條 invariant 專門守著這件事：ManifestCountNeverUndercounts，寫成邏輯是「blob 處於 active 狀態時，blobManifestCount 必須大於等於 TrueGlobalManifestCount」——白話講就是只要一個 blob 還 active，MySQL 算出來的引用數就不准低於真正的全域引用數，寧可多算，不能少算。但這條懷疑在這起事故裡站不住腳。真正弄丟資料的那個時間點，GC 讀到零引用的那一刻，MySQL 裡的計數是準的；client 重新寫入之後，MySQL 裡的計數也是準的。兩次讀都沒有算錯。問題不出在「數字錯了」，而是「數字對的時候，剛好夾在中間的一段時間裡發生了另一件事」——這就得回到 MySQL 跟 S3 之間那道真正的縫隙。
這條 invariant 只往一個方向設防，合理的推測是：兩種算錯的後果並不對稱——引用數被多算，最壞的結果是該刪的 blob 暫時沒被刪，浪費一點儲存空間；引用數被少算，後果卻是一個還在用的 blob 被判定可以刪，資料真的會不見。安全的代價分佈不對稱，防線也該跟著不對稱。
真正的縫隙：MySQL 和 S3 之間沒有交易
原文把根因講得很直白：「引用存在 MySQL，bytes 存在 S3，沒有一個 transaction 能同時橫跨這兩個系統。」GC 判定要刪一個 blob，靠的是讀 MySQL；真正刪掉資料，靠的是對 S3 下指令。這兩個動作之間，隔著整套 grace period、re-verify 的流程，時間夠長，長到一次完整的並行推送——寫 S3、commit MySQL——可以完整地塞進這段窗口。
完整的序列是這樣的：「GC 驗證這個 blob 的引用數是零，決定要刪除它。與此同時，一個 client 推送了一個包含那個 blob 的 image——同樣的 digest，同樣的 key。這次上傳把資料寫進 S3，並且 commit 了一筆新的引用。GC 的刪除落地，砍掉了一個剛剛提交的 manifest 現在指向的物件。」兩邊各自的每一步都是對的：GC 讀到零引用的當下沒有算錯；client 寫入 S3、commit MySQL 也都成功了。錯的是順序——GC 手上那把「要刪除」的判斷，是在 client 重新寫入之前做出的，可是它真正執行刪除的時候，晚了。
grace period 與 re-verify 這兩道防線，原本是為了拉大反應時間、多一次機會重新讀 MySQL 確認引用數沒有變。但把前面兩句話拼起來看，這兩道防線守住的是「MySQL 內部的數字有沒有變」，不是「S3 那把 key 現在到底是不是我當初檢查過的那份 bytes」。只要 client 的寫入與 commit，能在 GC 最後一次檢查之後、真正送出刪除之前完成，這道防線就守不到——問題從來不是檢查次數不夠多，是檢查的對象，一直都只有 MySQL 這一邊。
拖動或用方向鍵掃過時間軸 · GC 與 pusher 兩條並行動作 · 6 個事件
把上面這條時間軸掃過一遍會發現，GC 跟 pusher 的動作完全沒有互相等待——標記、等待、重推、寫入、commit、刪除，六個步驟像兩條各走各的軌道，只有終點撞在一起。真正該問的不是「哪一步算錯了」，而是「GC 手上那份判斷，是什麼時候拍下的快照」。
TLC 探索了一千四百多萬種交錯
Depot 把這整套行為寫成 TLA+ spec：「模型涵蓋 registry 三層 garbage collector，模擬並行的 pusher、兩個 GC domain、一個計數 reconciler，以及人工注入的計數 drift，全部交錯在一起。」原文沒有進一步解釋這兩個 GC domain 具體分別對應什麼，但丟給 model checker TLC 之後，「TLC 在大約 21 分鐘內探索了 14,290,224 個不同的狀態，驗證了 10 個 safety invariant 和 2 個 liveness property」。這個數字之所以有意義，是因為交錯的組合是指數成長的：模型裡有並行的 pusher、兩個 GC domain、reconciler、drift 注入，四種角色的動作只要能任意交錯，光是排列組合就足以讓人手動想不完。原文用的動詞是 proves，不是「試過幾個劇本沒出事」——這 14,290,224 個相異狀態不是工程師事先猜測的那幾條路徑。
十個 safety invariant 裡，原文點名了幾條，各自守住不同的東西。最重要的一條擺在第一位：「已經 commit 的 manifest 永遠不會失去它的 blob 資料」——這條就是整起事故的病灶所在，也是修法真正要守住的底線，對應的公式是「任何一個有 manifest 存在的 pusher，它的 S3 版本集合都不可以是空的」。ManifestCountNeverUndercounts 守的是前面提過的「寧可多算，不能少算」；S3HeadOK 則是純粹的內部自洽檢查——S3 目前指到的版本，得跟它自己記錄的版本集合裡最新的那個吻合。三條各自守住一層，湊在一起才撐得住「刪除可以放心跟寫入賽跑」這句話。
safety 與 liveness 是兩種不同性質的保證：一個 safety property 禁止的是「執行過程中不該發生的壞事」，一個 liveness property 要求的是「某件好事最終一定要發生」。這起事故踩到的三條都是 safety——防止資料被錯誤刪除，屬於前者；文章沒有點名那兩條 liveness property 具體要求什麼，但它們守的通常是「GC 最終真的會把沒人用的 blob 清掉」這一類、跟安全性無關但同樣重要的另一半承諾。
3 個具名 invariant + 1 列總計 · 各自守住什麼
| 名稱 | 型別 | 守住什麼 |
|---|---|---|
| ManifestNeedsData | safety | 對每一個有已提交 manifest 的 pusher，它的 S3 版本集合都不可以是空的——最重要的一條，直接對應「已提交的 manifest 不會失去 blob 資料」。 |
| ManifestCountNeverUndercounts | safety | blob 處於 active 狀態時，MySQL 算出的 manifest count 不可以低於真正的全域 manifest count——寧可多算，不能少算。 |
| S3HeadOK | safety | S3 目前指到的版本，必須跟它自己記錄的版本集合裡最新的那一個一致——純粹的內部自洽檢查。 |
| （其餘 7 + 2） | safety／liveness | TLC 這次總共驗證了 10 個 safety invariant、2 個 liveness property，原文只點名上面三條，其餘未逐條列出定義。 |
手動寫測試案例，靠的是工程師想得到、覺得可能出事的那幾種交錯；TLC 窮舉的，是這套 spec 能描述出來的所有交錯——差別不在誰更聰明，在窮舉的範圍。這起事故被找到，靠的正是後者：14,290,224 個狀態裡，藏著一種沒人特地寫成測試案例、也沒在 code review 裡被點出來的順序。
delete fence：把「刪這把 key」換成「刪我當時看到的版本」
修法不是想辦法讓 MySQL 跟 S3 憑空多出一個橫跨兩邊的 transaction——這做不到。真正的修法換了一個問題：GC 不再問「請刪掉這把 key」，而是問「請刪掉我當初看到的那份 bytes」。方法是打開 S3 bucket 的 versioning：「GC 標記一個 blob 的時候，記下它當時看到的那個 S3 version ID。真正刪除的時候，只刪那個版本。」原文把這個機制講得很直接：「我們把它當成一個 delete fence：它把『刪掉這把 key』變成『刪掉我當時檢查過的那份精確的 bytes』，這讓一次刪除能安全地跟一次寫入賽跑。」這個修法能成立，靠的是 S3 versioning 本身的語意——AWS 官方文件寫得很明確：「如果你覆寫一個物件，結果是 bucket 裡多出一個新的物件版本，你永遠可以還原前一個版本」；而「要永久刪除一個已版本化的物件，你必須使用指定 version ID 的 DELETE」，一般不指定版本的 DELETE 只會插入一個 delete marker，不會真的抹掉任何一個版本。GC 拿到的，正是這個「指定版本才會真的刪」的保證。
同一個 race 現在重新跑一次：GC mark 的時候記下 v1；client 重新推送，S3 那把 key 疊出一個新版本 v2，MySQL commit 新引用；grace period 結束，GC 送出刪除——但它刪的是 v1，不是「這把 key 目前指到的版本」。v2 完好無缺，剛 commit 的 manifest 找得到它的 bytes。窗口本身沒有被關掉，GC 跟 client 還是可以在同一段時間裡各自動作，但刪除的目標從一個會被時間改變的東西（這把 key 現在指向誰），變成一個永遠不會變的東西（mark 那一刻拍下的版本 ID）。
有人可能會問，為什麼不讓 GC 在真正刪除前，再多讀一次 S3 確認版本沒變就好——這其實正是 re-verify 想做的事，只是它 re-verify 的對象一直是 MySQL，不是 S3。delete fence 的關鍵不是「多檢查一次」，而是把檢查的對象換成不會因為新寫入而被覆蓋掉意義的東西：一個具體的 version ID，而不是一把會隨時間變化指向的 key。
這個機制不是沒有代價。AWS 官方文件提醒：「每一個版本都照一般 S3 費率計費——一個物件的每個版本都是完整的物件，不是相對於前一版的差異，所以如果你存了三個版本，就是照三個物件收費。」delete fence 能運作的前提，是舊版本被保留到 GC 真正動手清理為止；如果沒有搭配 lifecycle 規則去清掉真正不再需要的舊版本，版本數會一直往上疊，儲存成本也會跟著疊上去。
拖動或用方向鍵改變「之後又被覆寫幾次」· 5 個版本
模型是多一顆信任的骰子，不是正確性證明
這份 spec 不是工程師逐行手寫出來的——Depot 的 staff engineer Wito Delnat 在文章裡寫得很清楚：「我們現在不再手寫模型了。一個 agent 讀實作——Go 的 transaction、SQL、S3 呼叫——把它翻譯成一份 spec。」人的工作變成審查：invariant 是不是真的講出了工程師想要的意思，一輪一輪修。原文也劃了範圍：「不要把 TLA+ 丟去對付每一件事」——CRUD 端點不值得為它建模，這套工具是留給真正有並行、有跨系統邊界的地方。文章開頭還用了一個更簡單的「玩具範例」暖身，再進入 Depot Registry 這個生產環境的真實案例。審查的重點不是語法對不對，是語意對不對——一個寫得出來、跑得動的 invariant，不代表它真的講出了工程師心裡那句「這件事絕對不能發生」。
這篇文章發表於 2026 年 7 月 20 日，作者是 Depot 的 staff engineer Wito Delnat——把這次修 bug 的過程寫成一篇方法論文章，而不只是一則變更紀錄，本身也是一種選擇：比起單純說「我們修好了」，作者選擇把找到 bug 的推理過程、模型檢查的具體數字，都攤開給讀者看。
作者對模型檢查本身也沒有誇大：「一個 model checker 只是多一顆信任的骰子，不是正確性證明。」他甚至建議不用等看懂 spec 的每一行才動手：「不要等到你看懂一份生成出來的 spec 的每一行才動作。跑跑看，看看會掉出什麼。最壞的情況是浪費一個下午；最好的情況是你抓到了一條值得追下去的線索。」被 TLC 抓出來的 violated invariant，原文的說法是「當成線索，不是判決：模型可能跟現實不符，所以一個被違反的 invariant 是一個起點，一條值得順著拉下去的線」——這句話本身就帶著保留語氣，不是斷言模型永遠正確。
這起事故是這整套說法的示範：測試沒抓到、code review 沒抓到，model checker 抓到了；而 model checker 抓到的東西，最後還是得靠工程師去判斷它是不是真的、該怎麼修——查清楚根因是 MySQL 跟 S3 之間沒有 transaction，再挑出 S3 versioning 這個現成機制當 delete fence，這兩步都是人做的判斷，TLC 只負責把那個沒人想過的交錯順序找出來，攤在桌上。原文收尾的說法也呼應這一點：「測試檢查你想得到的交錯；TLA+ 探索你想不到的交錯。」這也是為什麼原文特別強調「測試和 code review 都漏掉」這句話——不是說 Depot 的工程團隊不夠仔細，而是這種橫跨兩個系統、只在特定順序下才會出現的窗口，本來就不是靠讀程式碼、靠寫幾個測試案例就能可靠抓到的東西。
下次遇到跨系統邊界時：只要一個判斷靠讀系統 A、一個動作靠寫系統 B，中間沒有辦法用一個 transaction 把兩邊鎖在一起，這道縫隙就值得用 model checker 窮舉一次交錯順序——不是因為程式碼寫錯了，而是因為「兩邊都對」本來就可能在時間上對不起來。