OSDI '23

Currently Playing: OSDI '23 - Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent System

OSDI '23 - Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems Travis Hance, Carnegie Mellon University, Yi Zhou, Carnegie Mellon University, Andrea Lattuada, VMware Research, Reto Achermann, University of British Columbia, Alex Conway, VMware Research, Ryan Stutsman, VMware Research and University of Utah, Gerd Zellweger, VMware Research, Chris Hawblitzel, Microsoft Research, Jon Howell, VMware Research, Bryan Parno, Carnegie Mellon University We present IronSync, an automated verification framework for concurrent code with shared memory. IronSync scales to complex systems by splitting system-wide proofs into isolated concerns such that each can be substantially automated. As a starting point, IronSync's ownership type system allows a developer to straightforwardly prove both data safety and the logical correctness of thread-local operations. IronSync then introduces the concept of a Localized Transition System, which connects the correctness of local actions to the correctness of the entire system. We demonstrate IronSync by verifying two state-of-the-art concurrent systems comprising thousands of lines: a library for black-box replication on NUMA architectures, and a highly concurrent page cache. View the full OSDI '23 program at https://www.usenix.org/conference/osdi23/technical-sessions