分散式資料正確性
從合約開始
寫下不變量、其範圍，以及必須承受的失敗類型。「訂單最多被收費一次」是有用的描述；「強一致性」則不足夠。識別權威記錄、衍生視圖、參與者，以及每個提交/確認的邊界。詢問客戶端是否需要「讀取自己的寫入」(read-your-writes)、因果順序、可線性化操作、可序列化交易，或僅僅是最終收斂。
審查程序
- 繪製寫入路徑，包括資料庫提交、代理確認和外部副作用。記錄每個成功回應在程序崩潰、機器故障或副本容錯移轉後保證了什麼。超時意味著結果未知，並非一定執行失敗。
- 在每個持久化步驟前後列舉崩潰窗口。針對每個窗口，重播操作並檢查不變量。同時測試並發嘗試和順序重試。請參閱失敗記錄表。
- 當業務效果和其重複資料刪除標記共用同一個資料庫時，將它們放在一個交易中。對於對外事件，考慮使用交易式發件箱。對於遠端效果，需要持久的提供者冪等性合約或一個協調狀態機。代理傳遞保證終止於其文件記載的交易邊界。
- 確定排序範圍：鍵、分區、串流或全域。選擇能保護不變量的最窄範圍。分區日誌會排序其內部各分區；它不會自動排序不同分區中的相關事件。
- 對於複寫和容錯移轉，檢查領導者選舉、隔離、確認策略和復原。
R + W > N在固定成員下提供集合交集；它本身並不能建立可線性化。請參閱一致性。 - 對於分片，驗證交易局部性、熱鍵、再平衡和唯一性強制。測量最繁忙的分片，而不僅僅是聚合吞吐量。
- 針對可疑的保證，產出最小的反例以及一個可以執行它的測試。區分必要的保證和可接受的過時。
審查輸出
回傳：不變量 → 假設 → 失敗時間線 → 違反的保證 → 最小修復方案 → 成本 → 驗證。包含一個針對已不一致資料的復原路徑。指出任何依賴於特定資料庫、代理或提供者版本的行為。
在推薦前檢查
- 重試的請求能否重複使用其穩定的操作 ID，但使用變更後的參數？
- 租約持有者是否需要由資源強制執行一個單調遞增的隔離令牌？僅租約到期無法阻止暫停的進程。
- 在成功寫入後，副本是否可能立即提供過時的值？
- 墓碑記錄或重複資料刪除記錄是否會在重播範圍之前過期？
- 多記錄不變量是否需要交易或明確的協調？
範圍與參考文獻
部分涵蓋範圍對齊《設計資料密集型應用》第二版（Kleppmann 與 Riccomini 著）。這些原始程序使用了公開的作者課程筆記及其他主要文件；完整書籍並未使用。請參閱來源以獲得確切歸屬。此技能不提供共識實作，也不假設拜占庭容錯。