ShardStore paper

We have a new paper at SOSP 2021 about applying lightweight formal methods to validate ShardStore, Amazon S3’s new storage node software. As part of this work, we open-sourced a new stateless model checker for Rust called Shuttle, which is great at finding subtle concurrency bugs.