無法對分散式protocol做單元測試，但可以做模型檢驗
分散式缺陷在部署後修復成本高昂。模型檢驗能讓你在寫下第一行實作程式碼之前就發現它們。以下是如何使用 TLA+ 做到這一點。
你無法對分散式protocol做單元測試。單元測試在一台機器上以單一順序執行一個程序。而你的protocol在五台機器上以十個程序、以你無法控制的順序執行。這兩種現實之間的鴻溝，正是缺陷藏身之處。…
2 posts
分散式缺陷在部署後修復成本高昂。模型檢驗能讓你在寫下第一行實作程式碼之前就發現它們。以下是如何使用 TLA+ 做到這一點。
你無法對分散式protocol做單元測試。單元測試在一台機器上以單一順序執行一個程序。而你的protocol在五台機器上以十個程序、以你無法控制的順序執行。這兩種現實之間的鴻溝，正是缺陷藏身之處。…
Crash-only software 把每一次失敗都當成 crash，把每一次啟動都當成 recovery。對 Web Service 來說，這意味著刪掉你的 shutdown 邏輯，並設計出能撐過 kill -9 的狀態。
你的 Web Service 有一個 shutdown handler。它會 flush buffer、關閉連線、寫入 checkpoint。你也許測試過一次。在生產環境，它大概一年只在計畫性部署時執行一次。其他時候，你的服務死於 OOM kill、node eviction、斷電，或是部署超時後被 SIGKILL。…