Researchers affiliated with the Allen School took home all three Best Paper Awards at the Association for Computing Machinery’s 28th Symposium on Operating Systems Principles (SOSP). Current Ph.D. student Jacob Van Geffen, recent alumnus James Bornholt (Ph.D.,’19), former postdoc and incoming professor Simon Peter and affiliate professor Daniel Berger contributed to the winning papers that presented new advances in debugging, distributed computing and caching.
In the paper, “Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3,” Van Geffen and Bornholt, now a professor at the University of Texas, Austin, present ShardStore, a new storage backend for Amazon Simple Storage Service (S3). Built on 40,000 lines of Rust code, ShardStore optimizes disk IO efficiency and currently stores hundreds of petabytes of customer data. The paper describes how ShardStore is resilient, resilient and crash-safe, and how AWS uses formal methods to catch and fix bugs early. Additional authors of the paper include Vytautus Astrauskas, a Ph.D. student at ETH Zurich and a team of researchers from Amazon Web Services that included Rajeev Joshi, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran and Andrew Warfield.
Focused on building automated mechanisms to help engineers ensure the correctness of every change they make, ShardStore was developed to employ techniques like property-based testing and model checking with far lower overhead than traditional provable correctness. According to the team, this lightweight formal method prevented a number of issues like crash consistency and concurrency problems, before reaching production. The team plans to continue improving their techniques for cloud-based data storage.
Peter, who is currently a professor at the University of Texas, Austin and will join the Allen School faculty in January, co-authored “LineFS: Efficient SmartNIC Offload of a Distributed File System with Pipeline Parallelism,” about fitting the high demands of a distributed file system (DFS) onto smart network interface cards (SmartNICs). In the paper, the team presents LineFS, a SmartNIC-offloaded, high-performance DFS with support for client-local persistent memory. LineFS moves CPU-intensive tasks to a SmartNIC, improving latency in LevelDB — a fast, key-value store — up to 80%. Korea Advanced Institute of Science and Technology researchers Jongyul Kim, Insu Jang, Jaeseong Im and Youngjin Kwon, along with Waleed Reda and Dejan Kostic from the KTH Royal Institute of Technology and Emmett Witchel also at UT Austin, contributed to the paper.
In “Kangaroo: Caching Billions of Tiny Objects on Flash,” Berger, a researcher at Microsoft and UW, and his co-authors present a new flash cache that enables more efficient caching of tiny objects — often in social media and IoT services — called Kangaroo. Kangaroo overcomes challenges in existing flash cache designs such as minimizing main memory usage, which is expensive and energy hungry, and reduces load on back-end storage systems. Additionally, Kangaroo reduces flash memory wear out, extending flash cache lifetimes by multiple years. This also helps cost and sustainability. The paper was written with Carnegie Mellon University researchers Sara McAllister, Benjamin Berg, Julian Tutuncu-Macias, Juncheng Yang, Nathan Beckman and Gregory Ganger and Facebook researchers Sathya Gunasekar and Jimmy Lu.
Congratulations to all!