SOSP21 で best paper 賞を受賞した S3 の論文 "Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3" を読んでみる。 Abstract 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 approac