Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems

Authors: 

Travis Hance and 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

Abstract: 

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.

OSDI '23 Open Access Sponsored by
King Abdullah University of Science and Technology (KAUST)

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {288564,
author = {Travis Hance and Yi Zhou and Andrea Lattuada and Reto Achermann and Alex Conway and Ryan Stutsman and Gerd Zellweger and Chris Hawblitzel and Jon Howell and Bryan Parno},
title = {Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems},
booktitle = {17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23)},
year = {2023},
isbn = {978-1-939133-34-2},
address = {Boston, MA},
pages = {911--929},
url = {https://www.usenix.org/conference/osdi23/presentation/hance},
publisher = {USENIX Association},
month = jul
}

Presentation Video