Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3

James Bornholt; Rajeev Joshi; Vytautas Astrauskas; Brendan Cully; Bernhard Kragl; Seth Markle; Kyle Sauri; Drew Schleit; Grant Slatton; Serdar Tasiran; Jacob Van Geffen; Andrew Warfield

doi:10.1145/3477132.3483540

SOSP2021顶会

Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3

James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, Andrew Warfield

DOI 出版方

2021年份

63被引次数

43顶会引用

摘要

This paper reports our experience applying lightweight formal methods to validate the correctness of ShardStore, a new key-value storage node implementation for the Amazon S3 cloud object storage service. By "lightweight formal methodsž we mean a pragmatic approach to verifying the correctness of a production storage node that is under ongoing feature development by a full-time engineering team. We do not aim to achieve full formal verification, but instead emphasize automation, usability, and the ability to continually ensure correctness as both software and its specification evolve over time. Our approach decomposes correctness into independent properties, each checked by the most appropriate tool, and develops executable reference models as specifications to be checked against the implementation. Our work has prevented 16 issues from reaching production, including subtle crash consistency and concurrency problems, and has been extended by non-formal-methods experts to check new features and properties as ShardStore has evolved.

• Software and its engineering → Software verification and validation.