Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems - Hance, Travis; Zhou, Yi; Lattuada, Andrea; Achermann, Reto; Conway, Alex; Stutsman, Ryan; Zellweger, Gerd; Hawblitzel, Chris; Howell, Jon; Parno, Bryan (Operating Systems Design and Implementation (OSDI), 2023)
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.