SOSP 2021 Lightweight Formal Methods Validate a Key-Value Storage in Amazon S3

Introduce

​ SOSP 2021的Best paper之一，介紹Amazon採用一種“草量級” formal methods驗證S3的key-value儲存系統。之前沒有研究過formal methdos，最多的認知就停留在lamport的TLA+，透過形式化的語言描述系統的狀態和狀態轉移，並驗證系統的狀態和屬性是否滿足期望，類似Paxos、Raft等共識演算法，可以透過這種方法驗證算法理論上的正確性。但是軟體系統是很多模組和程式碼完美配合出來的，complex and frequntly changing，演算法正確，系統的實現未必正確。為了更好地驗證系統的正確性，Amazon拋棄了傳統formal methods完整的形式驗證，提出了一個 “草量級” formal methods，使得其可以更容易自動化的使用在日常的測試開發中，保證kv儲存系統的正確性。

​ 為什麼 “lightweight” 是 ”草量級“，因為最近關注UFC

草量級

世界冠軍二番戰

Lightweight Formal Methods

（1）Executable reference models as specifications

例如：實際的k-v儲存系統可能是一個很複雜的LSM tree結構，但是對標的reference model，可以簡單使用記憶體的hashmap實現即可，保證k-v storage完全具有相同語義的API-level介面，那麼驗證系統的specifications（或者說properties），就變成了比較reference models和實際k-v storage的狀態是否一致就可以了。其實這個思想其實非常樸素，我想大家實際測試驗證過程中可能都用過。

（2）Automated tools to check implementations against models

透過Property-Based Testing自動化的生成測試inputs，並且驗證系統實現和model是否一致

（3）Coverage tools to track effectiveness over time

系統和真實場景往往是複雜的，而且軟體系統在不停的變更，如何保證測試儘可能覆蓋絕大數的場景，除了採用一些Argument bias的方式儘可能完善我們的測試case之外，

還會引入code coverage metrics來發現一些盲點

。（很關鍵的一個點）

​ 透過放棄formal method完整的形式化驗證，使得相關工作變得更加容易在日常開發中開展。

為了更好的驗證k-v儲存系統的永續性和一致性，具體實踐的時候分3種情況分別進行驗證：

（1）Sequential correctness： refinement of the reference model

第一種，沒有併發的順序操作，不考慮故障，直接驗證和reference model是否一致

（2）For sequential crashing executions：refinement against a weaker reference model

第二種，沒有併發的順序操作，考慮故障，正確性驗證還是和reference model對比，增加的fault injection主要考慮了三類：

Fail-stop crashes （e。g。， power outages， kernel panics）

Transient or permanent disk IO failures （e。g。， HDD failures， timeouts）

Resource exhaustion（e。g。，out of memory or diskspace）

隨著混沌工程的普及，fault injection現在已經深入人心，畢竟確實是分散式系統測試驗證的利器

（3）For concurrent crash-free executions， we write separate reference models and check linearizability

第三種，併發操作，不考慮故障，採用一種stateless mode checking的方法來驗證併發情況下的linearizability，沒研究過stateless model checking，這裡先記個TODO。

對於併發場景的驗證是一個強需求，但也確實是一個難點，因為一旦併發，驗證就是一個難題了。類似的，Raft線性一致性驗證工具Jepsen就是個例子，Client發起併發讀寫，並且記錄下所有op history，底層分散式注入各種crash，最後驗證history是否可線性化來驗證系統是否滿足線性一致性，這個方法優勢很明顯，端到端，自動化，支援併發，支援故障注入，但是有一個致命的缺陷，op history驗證是否可線性化是一個NP難的問題，線性時間無解，所以測試的時間不能太長，太長op history就會很大，正確性驗證所需要的時間就不能收斂了。

Summary

​ 因為要兼得高效能、高可用和高可靠三者，分散式儲存系統自然也就成為了最難搞的系統，良好的頂層設計和工程實踐是基礎，完善科學的測試驗證體系也同樣“一個都不能少”，否則亦是浮沙築高臺。最後用論文Lessons Learned三個關鍵字總結對於測試驗證在分散式系統中實施的最佳實踐吧：

Early

、

Continuous

、

Future

。

（其實對formal methods、stateless model checking不懂，所以可能對很多描述理解上有偏差和錯誤，大家湊合著看，放這裡只是簡單整理記錄下）

Notes

限於作者水平，難免有理解和描述上有疏漏或者錯誤的地方，歡迎共同交流；部分參考已經在正文和參考文獻中列表註明，但仍有可能有疏漏的地方，有任何侵權或者不明確的地方，歡迎指出，必定及時更正或者刪除；文章供於學習交流，轉載註明出處

References

［1］。 Bornholt J， Joshi R， Astrauskas V， et al。 Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3［C］//Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles CD-ROM。 2021： 836-850。